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

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

tests
0

failures
0

ignored
10m39.58s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.101s passed
powPositiveConcrete data()[101] 3.092s passed
powGeq1Concrete data()[102] 3.208s passed
pow2InIntLower data()[103] 3.201s passed
pow2InIntUpper data()[104] 3.090s passed
logSelfConcrete data()[105] 3.119s passed
log1Concrete data()[106] 3.095s passed
logProduct data()[107] 3.105s passed
logTimesBaseConcrete data()[108] 3.104s passed
logProdIdentity data()[109] 3.096s passed
moduloByteIsInByte data()[10] 3.150s passed
logProdIdentityConcrete data()[110] 3.109s passed
logPowIdentity data()[111] 3.093s passed
logPowIdentityConcrete data()[112] 3.102s passed
logPositive data()[113] 3.108s passed
logPositiveConcrete data()[114] 3.102s passed
logMono data()[115] 3.123s passed
logMonoConcrete data()[116] 3.092s passed
powLogLess data()[117] 3.128s passed
powLogMore2 data()[118] 3.115s passed
logLessThanPow data()[119] 3.143s passed
moduloCharIsInChar data()[11] 3.137s passed
logLessThanPowConcrete data()[120] 3.079s passed
logSqueeze data()[121] 3.105s passed
ifthenelse_equals data()[122] 3.104s passed
ifthenelse_equals_1 data()[123] 3.094s passed
ifthenelse_equals_2 data()[124] 3.105s passed
disjointWithSingleton1 data()[125] 3.106s passed
disjointWithSingleton2 data()[126] 3.112s passed
disjointArrayRanges data()[127] 3.114s passed
disjointArrayRangeAllFields1 data()[128] 3.113s passed
disjointArrayRangeAllFields2 data()[129] 3.117s passed
div_unique1 data()[12] 3.182s passed
seqSelfDefinition data()[130] 3.130s passed
seqOutsideValue data()[131] 3.104s passed
castedGetAny data()[132] 3.103s passed
seqGetAlphaCast data()[133] 3.114s passed
getOfSeqSingleton data()[134] 3.091s passed
getOfSeqSingletonConcrete data()[135] 3.103s passed
getOfSeqConcat data()[136] 3.112s passed
getOfSeqSub data()[137] 3.089s passed
getOfSeqReverse data()[138] 3.104s passed
lenOfSeqEmpty data()[139] 3.110s passed
div_unique2 data()[13] 3.282s passed
lenOfSeqSingleton data()[140] 3.128s passed
lenOfSeqConcat data()[141] 3.113s passed
lenOfSeqSub data()[142] 3.092s passed
lenOfSeqReverse data()[143] 3.112s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.098s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.106s passed
getOfSeqSingletonEQ data()[146] 3.115s passed
getOfSeqConcatEQ data()[147] 3.114s passed
getOfSeqSubEQ data()[148] 3.087s passed
getOfSeqReverseEQ data()[149] 3.118s passed
div_exists data()[14] 3.298s passed
lenOfSeqEmptyEQ data()[150] 3.127s passed
lenOfSeqSingletonEQ data()[151] 3.109s passed
lenOfSeqConcatEQ data()[152] 3.111s passed
lenOfSeqSubEQ data()[153] 3.097s passed
lenOfSeqReverseEQ data()[154] 3.101s passed
getOfSeqDefEQ data()[155] 3.102s passed
lenOfSeqDefEQ data()[156] 3.103s passed
seqConcatWithSeqEmpty1 data()[157] 3.110s passed
seqConcatWithSeqEmpty2 data()[158] 3.113s passed
seqReverseOfSeqEmpty data()[159] 3.110s passed
div_one data()[15] 3.142s passed
subSeqComplete data()[160] 3.107s passed
subSeqTailR data()[161] 3.116s passed
subSeqTailL data()[162] 3.110s passed
subSeqTailEQR data()[163] 3.108s passed
subSeqTailEQL data()[164] 3.105s passed
seqDef_split data()[165] 3.140s passed
seqDef_induction_upper data()[166] 3.124s passed
seqDef_induction_upper_concrete data()[167] 3.123s passed
seqDef_induction_lower data()[168] 3.120s passed
seqDef_induction_lower_concrete data()[169] 3.115s passed
jdiv_one data()[16] 3.134s passed
seqDef_split_in_three data()[170] 3.162s passed
seqDef_empty data()[171] 3.107s passed
seqDef_one_summand data()[172] 3.107s passed
seqDef_lower_equals_upper data()[173] 3.105s passed
seqDefOfSeq data()[174] 3.125s passed
seqSelfDefinitionEQ2 data()[175] 3.119s passed
indexOfSeqSingleton data()[176] 3.106s passed
indexOfSeqConcatFirst data()[177] 3.108s passed
indexOfSeqConcatSecond data()[178] 3.125s passed
indexOfSeqSub data()[179] 3.124s passed
div_zero data()[17] 3.171s passed
lenOfArray2seq data()[180] 3.105s passed
getAnyOfArray2seq data()[181] 3.113s passed
getOfArray2seq data()[182] 3.104s passed
getAnyOfNPermInv data()[183] 3.123s passed
seqNPermRange data()[184] 3.142s passed
seqPermTrans data()[185] 3.141s passed
seqPermRefl data()[186] 3.110s passed
seqPermSplit data()[187] 3.114s passed
seqNPermRight data()[188] 3.184s passed
seqPermFromSwap data()[189] 3.149s passed
divResZero1 data()[18] 3.161s passed
seqPermTransAlt0 data()[190] 3.113s passed
seqPermTransAlt1 data()[191] 3.124s passed
seqPermTransAlt2 data()[192] 3.108s passed
seqPermTransAlt3 data()[193] 3.116s passed
seqPermForall data()[194] 3.230s passed
seqPermExists data()[195] 3.167s passed
schiffl_lemma_2 data()[196] 21.385s passed
schiffl_thm_1 data()[197] 3.886s passed
eqSameSeq data()[198] 3.267s passed
divResZero2 data()[19] 3.166s passed
eqTermCut data()[1] 3.750s passed
divResOne1 data()[20] 3.124s passed
divResOne2 data()[21] 3.177s passed
div_cancel1 data()[22] 3.159s passed
div_cancel2 data()[23] 3.126s passed
divAddMultDenom data()[24] 3.189s passed
divMinus data()[25] 3.206s passed
divMinusDenom data()[26] 3.137s passed
divLeastDPos data()[27] 3.138s passed
divLeastDNeg data()[28] 3.118s passed
divGreatestDPos data()[29] 3.150s passed
equivAllRight data()[2] 3.532s passed
divGreatestDNeg data()[30] 3.133s passed
divIncreasingPos data()[31] 3.114s passed
divIncreasingNeg data()[32] 3.129s passed
jdiv_zero data()[33] 3.110s passed
jdivPulloutMinusNum data()[34] 3.114s passed
jdivPulloutMinusDenom data()[35] 3.153s passed
jdiv_uniquePosPos data()[36] 3.109s passed
jdiv_uniquePosNeg data()[37] 3.138s passed
jdiv_uniqueNegPos data()[38] 3.121s passed
jdiv_uniqueNegNeg data()[39] 3.107s passed
irrflConcrete1 data()[3] 3.391s passed
jdivMultDenom1 data()[40] 3.152s passed
jdivMultDenom2 data()[41] 3.103s passed
mod_geZero data()[42] 3.094s passed
mod_lessDenom data()[43] 3.127s passed
jmod_NumPos data()[44] 3.095s passed
jmod_NumNeg data()[45] 3.099s passed
jmod_geZero data()[46] 3.120s passed
jmodNumZero data()[47] 3.098s passed
jmod_pulloutminusNum data()[48] 3.117s passed
jmod_pulloutminusDenom data()[49] 3.099s passed
irrflConcrete2 data()[4] 3.383s passed
jmodUnique1 data()[50] 3.135s passed
jmodUnique2 data()[51] 3.202s passed
intDivRem data()[52] 3.092s passed
jmodjmod data()[53] 3.111s passed
jmodDivisible data()[54] 3.129s passed
jmodDivisibleRep data()[55] 3.100s passed
jdivAddMultDenom data()[56] 3.210s passed
jmodAltZero data()[57] 3.116s passed
jmodAddMultDenomZero data()[58] 3.093s passed
polyDiv_zero data()[59] 3.115s passed
cancel_gtPos data()[5] 3.365s passed
polyMod_ltdivDenom data()[60] 3.088s passed
bsum_empty data()[61] 3.074s passed
bsum_induction_upper data()[62] 3.089s passed
bsum_induction_lower data()[63] 3.097s passed
bsum_num_of_bounds data()[64] 3.096s passed
bsum_num_of_bounds2 data()[65] 3.165s passed
bsum_induction_upper2 data()[66] 3.079s passed
bsum_induction_upper_concrete data()[67] 3.117s passed
bsum_induction_upper_concrete_2 data()[68] 3.088s passed
bsum_induction_upper2_concrete data()[69] 3.079s passed
cancel_gtNeg data()[6] 3.324s passed
bsum_induction_lower_concrete data()[70] 3.101s passed
bsum_induction_lower2 data()[71] 3.089s passed
bsum_induction_lower2_concrete data()[72] 3.092s passed
bsum_positive data()[73] 3.153s passed
bsum_upper_bound data()[74] 3.135s passed
bsum_lower_bound data()[75] 3.159s passed
bsum_positive_lower_bound_element data()[76] 3.129s passed
bsum_sub_same_index data()[77] 3.122s passed
bsum_less_same_index data()[78] 3.139s passed
bsum_equal_except_one_index data()[79] 3.123s passed
moduloIntIsInInt data()[7] 3.362s passed
bsum_num_of_is_max data()[80] 3.114s passed
bsum_num_of_is_max2 data()[81] 3.119s passed
bsum_num_of_is_max3 data()[82] 3.109s passed
bsum_num_of_is_max4 data()[83] 3.108s passed
bsum_num_of_lt_max data()[84] 3.116s passed
bsum_num_of_lt_max2 data()[85] 3.102s passed
bsum_num_of_lt_max3 data()[86] 3.112s passed
bsum_num_of_lt_max4 data()[87] 3.097s passed
bsum_num_of_gt0 data()[88] 3.097s passed
bsum_num_of_gt0_alt data()[89] 3.123s passed
moduloLongIsInLong data()[8] 3.345s passed
bsum_add_concrete data()[90] 3.091s passed
bprod_all_positive data()[91] 3.090s passed
bprod_split data()[92] 3.099s passed
powConcrete0 data()[93] 3.081s passed
powConcrete1 data()[94] 3.105s passed
powSplitFactor data()[95] 3.085s passed
powAdd data()[96] 3.100s passed
powMono data()[97] 3.110s passed
powMonoConcrete data()[98] 3.089s passed
powMonoConcreteRight data()[99] 3.083s passed
moduloShortIsInShort data()[9] 3.262s passed

Standard output

680        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
705        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.34ms 
920        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
932        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)

1798       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1800       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1803       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1804       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3522       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8514       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.59s 
8588       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8622       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.8ns 
8665       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8665       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 575.39ns 
8675       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
11436      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12405      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.44ms 
12415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.8ns 
12418      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
15045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15944      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
15947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.4ns 
15950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18503      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
18504      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19334      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
19341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.8ns 
19345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
21867      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22722      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
22725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22727      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 993.09ns 
22731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25168      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
25169      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.33ms 
26091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.4ns 
26092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28582      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
28583      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29412      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.13ms 
29414      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29414      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
29415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
31961      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.99ns 
32775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.2ns 
32776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
35292      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.39ns 
36120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.6ns 
36121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
38579      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39382      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.79ns 
39383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
39384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41751      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
41751      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42531      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 493.6ns 
42533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.8ns 
42534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
44888      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45668      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.49ns 
45671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.4ns 
45672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
48054      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48850      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.64ms 
48853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.3ns 
48855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51228      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
51228      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52133      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.63ms 
52136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 614.59ns 
52140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
54499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55430      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.61ms 
55434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 482.29ns 
55435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57813      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
57813      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
58576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.8ns 
58577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
60931      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61708      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
61710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.1ns 
61711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
64059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64879      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.51ms 
64881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.2ns 
64882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
67252      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68040      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
68042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
68043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
70404      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71206      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.99ms 
71208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.9ns 
71209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
73545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74331      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
74332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.5ns 
74334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
76720      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77507      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.39ms 
77509      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77509      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.2ns 
77510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
79878      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80666      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
80667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
80668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
83034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
83786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
83792      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
83795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
83795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312ns 
83798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
86156      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
86929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
86980      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.22ms 
86983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
86983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.3ns 
86984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89373      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
89373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90143      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90187      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.64ms 
90189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.2ns 
90191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92541      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
92541      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93324      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25ms 
93326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93326      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
93326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
95685      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96462      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
96463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
96464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98796      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
98796      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99567      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99579      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
99587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.6ns 
99588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
101953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
102738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 585.29ns 
102739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
105091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
105861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
105868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
105869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
105869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
105870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
108226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
108976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
108983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.45ms 
108984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
108984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 
108985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
111334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
112113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.1ns 
112114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
114448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
115222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 
115223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
117578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.61ms 
118337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.6ns 
118338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
120691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
121456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
121488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.68ms 
121490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
121490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.4ns 
121491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
123816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.87ms 
124598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.3ns 
124599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
126946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
127713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
127735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.2ms 
127737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
127738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.3ns 
127739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
130075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
130842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
130857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.36ms 
130858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
130858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
130859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
133182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
133950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
133964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
133965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
133965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
133966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
136317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
137085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
137115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.2ms 
137117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
137117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
137118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
139446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
140216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
140218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
140219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
140219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
140220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
142561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
143314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
143314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
145662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
146433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
146439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
146441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
146441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
146442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
148763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
149527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
149534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
149535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
149535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.6ns 
149536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
151873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
152619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
152634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ms 
152635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
152635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
152636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
154979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
155747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
155754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
155755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
155755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
155756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
158074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
158848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
158851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
158852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
158852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
158853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
161195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
161962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
161968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
161969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
161969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
161970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
164297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
165065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
165068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
165069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
165069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
165070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
167385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
168152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
168202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.58ms 
168204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
168204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
168205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
170576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
171345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
171404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.09ms 
171405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
171406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
171406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
173727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
174493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
174496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
174497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
174498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
174498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
176835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
177581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
177607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.35ms 
177608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
177608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.3ns 
177609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
179953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
180717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
180736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.46ms 
180737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
180737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
180738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
183059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
183834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
183837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.29ns 
183838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
183838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 
183839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
186173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
186937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
187046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.88ms 
187047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
187047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
187051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
189381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
190154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
190163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
190164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
190164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.9ns 
190167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
192506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
193250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
193255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
193256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
193256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
193257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
195593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
196358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
196371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
196372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
196372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
196373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
198686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
199448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
199458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
199460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
199460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
199461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
201786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
202530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
202533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
202534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
202534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
202535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
204855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
205618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
205622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
205623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
205623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
205623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
207931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
208705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
208718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.19ms 
208719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
208720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
208720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
211058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
211803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
211814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.45ms 
211815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
211816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
211816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
214204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
214968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
214979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.35ms 
214980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
214980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
214981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
217292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
218056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
218058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 866.49ns 
218060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
218060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
218060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
220403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
221173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
221176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
221177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
221177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
221177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
223495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
224259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
224264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
224265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
224265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
224265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
226597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
227341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
227343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.39ns 
227344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
227344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
227345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
229677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
230441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
230443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 429.3ns 
230444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
230446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.31ms 
230447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
232767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
233529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
233532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
233534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
233534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
233534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
235873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
236621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
236624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.69ns 
236625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
236625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.5ns 
236626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
238967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
239734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
239777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.68ms 
239779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
239779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.2ns 
239780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
242105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
242875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
242912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.28ms 
242913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
242914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
242914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
245275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
246023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
246071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.62ms 
246072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
246072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
246073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
248400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
249172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
249200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.61ms 
249202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
249202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.1ns 
249203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
251536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
252305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
252323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
252324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
252324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
252325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
254660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
255427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
255461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.93ms 
255463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
255463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.2ns 
255464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
257800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
258565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
258584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.4ms 
258585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
258585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
258586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
260938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
261685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
261698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.97ms 
261699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
261700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
261700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
264037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
264802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
264817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.51ms 
264819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
264819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
264819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
267146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
267914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
267926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.23ms 
267927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
267927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
267928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
270276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
271019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
271034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.74ms 
271036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
271036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
271036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
273370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
274136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
274150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.57ms 
274152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
274152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
274153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
276471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
277237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
277252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
277253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
277253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
277254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
279585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
280350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
280365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.73ms 
280366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
280366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
280367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
282684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
283448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
283462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.08ms 
283463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
283463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
283464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
285800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
286544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
286559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.63ms 
286560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
286560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
286561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
288906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
289667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
289681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.83ms 
289682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
289682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
289683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
291997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
292767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
292772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
292773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
292773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
292774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
295106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
295852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
295862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
295863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
295863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
295864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
298195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
298958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
298962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
298963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
298963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
298964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
301276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
302041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
302043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.29ns 
302044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
302044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
302045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
304383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
305146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
305148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.79ns 
305149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
305149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
305149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
307463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
308228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
308233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
308244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
308244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns 
308246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
310562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
311327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
311332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
311333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
311333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
311334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
313662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
314430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
314443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ms 
314444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
314445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.6ns 
314445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
316760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
317529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
317532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
317533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
317533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
317533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
319868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
320613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
320615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 444.8ns 
320616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
320616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
320617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
322945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
323710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
323715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
323717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
323717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 
323717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
326037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
326806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
326808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 472ns 
326809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
326809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
326809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
329227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
330013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
330015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.7ns 
330016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
330016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
330017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
332447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
333214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
333216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 473.6ns 
333218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
333218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.9ns 
333219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
335536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
336303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
336307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
336308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
336308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
336308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
338651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
339418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
339425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
339426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
339426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
339427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
341750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
342517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
342520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
342521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
342521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
342522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
344869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
345617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
345625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.06ms 
345627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
345627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
345628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
347956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
348726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
348729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
348730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
348730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
348731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
351048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
351814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
351825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.51ms 
351826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
351826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
351827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
354166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
354932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
354935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
354936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
354936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
354937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
357258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
358025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
358027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.29ns 
358028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
358029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
358029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
360356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
361102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
361130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.52ms 
361131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
361131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
361131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
363458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
364225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
364237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms 
364238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
364238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
364239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
366590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
367335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
367339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 285ns 
367341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
367341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
367341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
369674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
370437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
370462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.51ms 
370463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
370464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
370464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
372805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
373552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
373555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
373556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
373556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
373557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
375895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
376667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
376683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.79ms 
376685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
376685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.6ns 
376686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
379033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
379780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
379797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.94ms 
379799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
379800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 
379800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
382158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
382923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
382940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
382941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
382941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
382942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
385273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
386018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
386020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 457.6ns 
386021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
386021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
386022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
388355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
389119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
389124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
389125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
389125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
389126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
391458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
392225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
392228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
392229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
392229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
392230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
394551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
395320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
395322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.99ns 
395324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
395324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
395324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
397656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
398425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
398427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.99ns 
398433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
398433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
398434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
400781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
401534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
401537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
401539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
401539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
401539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
403875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
404645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
404649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
404654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
404654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.9ns 
404655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
406987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
407757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
407765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
407766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
407766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
407767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
410099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
410871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
410877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
410878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
410878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
410879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
413214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
413988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
413994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
413995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
413995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
413996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
416332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
417113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
417124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
417125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
417125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
417137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
419453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
420225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
420228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
420229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
420230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
420230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
422555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
423328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
423331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
423332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
423332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
423333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
425668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
426444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
426446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.89ns 
426447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
426447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
426448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
428760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
429534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
429536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.19ns 
429537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
429537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
429538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
431864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
432637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
432639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.69ns 
432640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
432640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
432641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
434968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
435744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
435752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
435753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
435753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
435754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
438081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
438838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
438841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
438842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
438842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
438843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
441166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
441939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
441944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
441945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
441945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
441946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
444276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
445052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
445054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698ns 
445056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
445056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
445056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
447406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
448180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
448182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.39ns 
448183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
448183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
448184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
450517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
451293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
451295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
451296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
451297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
451297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
453610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
454385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
454387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.29ns 
454388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
454388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
454389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
456722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
457495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
457500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
457501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
457501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
457501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
459824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
460595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
460597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.59ns 
460599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
460599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
460599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
462925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
463700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
463703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
463705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
463705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
463706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
466040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
466817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
466819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.29ns 
466820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
466820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
466821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
469152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
469925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
469933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms 
469934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
469934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
469935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
472262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
473018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
473019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 440.1ns 
473020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
473021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
473021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
475353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
476132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
476137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
476139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
476139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
476139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
478486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
479261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
479264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
479266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
479266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.2ns 
479267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
481597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
482372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
482374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.2ns 
482375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
482375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
482376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
484706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
485481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
485484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
485485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
485485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
485486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
487805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
488579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
488581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.69ns 
488582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
488582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
488583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
490901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
491676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
491682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
491683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
491683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
491684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
494007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
494782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
494785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
494786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
494786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
494786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
497108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
497883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
497887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
497888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
497888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
497889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
500214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
500989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
500998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
500999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
501000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 576.39ns 
501000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
503328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
504103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
504110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
504111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
504111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
504112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
506441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
507215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
507221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
507222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
507222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
507223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
509547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
510322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
510327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
510328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
510329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
510329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
512658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
513434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
513443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
513444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
513444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
513445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
515770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
516544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
516553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 
516554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
516554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
516555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
518878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
519652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
519661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
519662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
519662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
519663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
522004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
522760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
522766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
522767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
522767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
522768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
525109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
525885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
525906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.27ms 
525908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
525908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.6ns 
525909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
528233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
529009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
529030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms 
529031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
529032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
529032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
531360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
532135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
532153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.06ms 
532154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
532154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
532155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
534478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
535255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
535273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.37ms 
535274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
535274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
535275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
537595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
538371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
538389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.9ms 
538390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
538390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
538391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
540730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
541506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
541550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.75ms 
541552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
541552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
541552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
543878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
544653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
544657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
544658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
544659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
544659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
546982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
547757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
547764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
547766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
547766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.4ns 
547767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
550091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
550866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
550869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
550870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
550871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
550871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
553207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
553983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
553995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.88ms 
553996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
553996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
553996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
556331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
557107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
557113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
557114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
557114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
557115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
559441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
560216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
560219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
560220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
560220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
560221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
562544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
563318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
563328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
563329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
563329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
563330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
565665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
566442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
566452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.55ms 
566453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
566453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
566454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
568784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
569565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
569577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.68ms 
569578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
569578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
569579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
571903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
572679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
572681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880.19ns 
572682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
572682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
572683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
575015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
575791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
575795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
575796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
575796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
575796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
578119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
578894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
578899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
578900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
578900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
578901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
581242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
582017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
582022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
582024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
582024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.4ns 
582025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
584349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
585124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
585163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.03ms 
585164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
585164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
585165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
587515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
588288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
588304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms 
588306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
588306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
588306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
590630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
591404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
591414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
591415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
591415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
591416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
593752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
594527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
594529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.7ns 
594530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
594530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.4ns 
594531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
596863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
597637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
597712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.06ms 
597713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
597713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
597714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
600050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
600829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
600861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.22ms 
600863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
600863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.2ns 
600864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
603197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
603973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
603975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 171.6ns 
603976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
603976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
603977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
606321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
607097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
607099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.8ns 
607100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
607100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
607101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
609426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
610204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
610206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 197.6ns 
610207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
610207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
610208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
612547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
613321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
613322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 305.7ns 
613324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
613324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
613324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
615643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
616437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
616542     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
616552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.48ms 
616555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
616555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.8ns 
616556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
618904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
619681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
619720     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
619721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.87ms 
619722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
619722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
619723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
622161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
623051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
623053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 
623109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
623156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
623171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
623178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
623194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
623195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
623197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
623199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
623206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
623209     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' 
623212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
623216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
623449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
623450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
623451     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' 
623452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
623453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
623566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
623567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
623568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
623568     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' 
623570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
623571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
623750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
623751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
623752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
623753     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' 
623753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
623754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
623901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
623902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
623903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
623904     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' 
623904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
623905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
623913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
623914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
623915     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' 
623916     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' 
623917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
623918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
623925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
623926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
623927     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' 
623928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
623929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
623929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
624087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
624088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
624089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
624243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
624244     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)'' 
624245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
624247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
624248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
624249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
624250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
624250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
624255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
624256     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' 
624257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
624258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
624259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
624395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
624399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
624400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
624402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
624402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
624403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
624404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
624552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
624554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
624555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
624556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
624557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
624558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
624558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
624559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
624669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
624670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
624758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
624762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
624766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
624767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
624768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
624769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
624770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
624771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
624771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
624772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
624779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
624784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
624878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
624879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
624880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
624881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
624881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
624882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
624882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
624883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
624934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
624940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
625026     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]'' 
625027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
625028     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'' 
625029     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'' 
625030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
625031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
625146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
625150     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'' 
625151     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)'' 
625151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
625153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
625153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
625154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
625155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
625163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
625164     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'' 
625165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
625166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
625284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
625284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
625286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
625287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
625287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
625288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
625383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
625385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
625386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
625387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
625388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
625388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
625389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
625389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
625484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
625485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
625558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
625559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
625559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
625565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
625568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
625572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
625681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
625682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
625682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
625683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
625693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
625773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
629057     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'' 
629058     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)'' 
629062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
629063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
629064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
629064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
629065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
629072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
629073     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'' 
629074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
629075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
629076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
629164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
629168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
629169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
629170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
629170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
629171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
629171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
629262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
629263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
629264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
629265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
629265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
629266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
629266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
629267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
629339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
629340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
629410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
629415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
629419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
629419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
629420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
629421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
629431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
629507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
629508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
629509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
629509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
629578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
629587     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'' 
629588     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)'' 
629588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
629590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
629590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
629591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
629591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
629602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
629602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
629603     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'' 
629604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
629604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
629688     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))'' 
629689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
629690     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'' 
629690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
629691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
629778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
629783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
629783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
629784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
629785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
629785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
629786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
629881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
629881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
629883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
629883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
629884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
629885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
629885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
629886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
629887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
629887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
629888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
629889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
629889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
629890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
629890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
629973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
629974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
629980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
630053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
630130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
630131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
630132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
630133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
630134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
630134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
630135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
630135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
630136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
630217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
630223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
630309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
630310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
630311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
630311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
630312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
630312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
630313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
630313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
630318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
630319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
630395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
630400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
630405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
630501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
630501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
630502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
630503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
630504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
630504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
630505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
630505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
630596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
630597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
630598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
630599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
630600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
630606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
630611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
630722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
630806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
630807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
630807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
630808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
630967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
631051     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'' 
631051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
633903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
633907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
633907     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'' 
633908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
633909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
634016     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))'' 
634016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
634017     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'' 
634018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
634019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
634118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
636842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
639924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
639927     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'' 
639928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
639928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
639929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
640036     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))'' 
640036     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'' 
640037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
640038     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)' ...' 
640039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
641106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
641106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
641107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
643546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
644347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
644349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
644349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
644357     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)'' 
644366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
644368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
644370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
644371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
644376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
644376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
644380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
644381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
644382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
644392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
644392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
644393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
644439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
644440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
644440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
644441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
644441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
644502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
644502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
644503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
644503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
644504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
644507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
644507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
644508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
644508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
644509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
644509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
644587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
644588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
644588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
644589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
644589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
644590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
644676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
644676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
644677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
644677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
644678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
644678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
644679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
644679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
644680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
644681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
644681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
644681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
644682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
644682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
644683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
644683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
644684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
644684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
644685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
644687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
644725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
644725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
644783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
644784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
644785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
644786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
644787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
644787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
644835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
644838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
644839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
644839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
644840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
644841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
644842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
644889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
644892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
644895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
644943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
644994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
644994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.3ns 
644995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
647421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
648243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
648258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms