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

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

tests
0

failures
0

ignored
10m42.72s

duration
100%

successful

Tests

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

Standard output

546        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
571        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.63ms 
767        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779        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)

1714       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1716       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1720       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1720       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3038       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8388       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.62s 
8452       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8486       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.5ns 
8499       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8500       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 477.3ns 
8504       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
11247      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12154      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
12162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141ns 
12163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
14772      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15595      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
15597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 
15599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
18137      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18968      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
18970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.3ns 
18971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21468      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
21468      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22294      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
22296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.3ns 
22297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24716      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
24717      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.63ms 
25558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.3ns 
25559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
27984      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28792      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.88ms 
28797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28797      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.5ns 
28798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31195      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
31196      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32002      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32006      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.1ns 
32008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.4ns 
32010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34383      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35172      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.4ns 
35174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
35175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37543      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
37543      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38331      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.2ns 
38333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
38334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
40707      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41492      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.9ns 
41494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.3ns 
41495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
43880      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44661      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619.5ns 
44664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44665      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.8ns 
44666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
47035      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47859      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.03ms 
47861      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47861      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
47862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
50280      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51127      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.62ms 
51133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 823.4ns 
51136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
53506      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54490      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.99ms 
54496      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54496      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 619.4ns 
54497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
56858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57649      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
57652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.9ns 
57653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60027      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
60028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
60845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.1ns 
60847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
63211      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.46ms 
64031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64031      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.5ns 
64032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
66415      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67208      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.65ms 
67211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.5ns 
67213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
69577      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70358      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70370      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.98ms 
70373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70373      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.6ns 
70374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72831      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
72831      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
73658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
73659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
76131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76961      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
76963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
76964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79433      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
79434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80277      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
80279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.3ns 
80280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
82749      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
83571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
83574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
83576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
83576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
83577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86049      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
86049      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
86860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
86893      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.69ms 
86895      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
86895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
86896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89364      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
89364      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90196      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.19ms 
90197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
90198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
92554      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.2ms 
93362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 
93363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
95725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96506      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.97ms 
96507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96508      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
96508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
98860      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99650      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
99652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.3ns 
99653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
102009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.54ms 
102791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
102792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
105137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
105909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
105915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
105916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
105916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
105917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
108268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
109046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
109047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
111396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
112182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
112182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
114546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
115321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.2ns 
115322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
117670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
118452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.9ns 
118453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
120796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
121566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
121596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.5ms 
121599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
121599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.7ns 
121600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
123941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
124725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
124726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
127073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
127844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
127857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
127858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
127859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.2ns 
127859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
130210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
130979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
130993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
130994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
130994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
130995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
133335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
134109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
134122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
134123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
134123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
134124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
136503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
137260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
137289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.2ms 
137292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
137292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.3ns 
137293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
139655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
140406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
140409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
140410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
140410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 
140411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
142767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
143522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.2ns 
143523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
145881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
146628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
146635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
146637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
146637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.5ns 
146638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
149001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
149750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
149758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
149760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
149760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.6ns 
149761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
152130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
152877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
152892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.41ms 
152894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
152894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 
152895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
155244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
155991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
155997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
155998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
155998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
155999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
158347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
159095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
159097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.5ns 
159099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
159099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.6ns 
159100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
161471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
162220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
162223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
162225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
162225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
162225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
164582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
165333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
165336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
165337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
165337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
165338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
167700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
168450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
168500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.64ms 
168501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
168501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
168502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
170869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
171624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
171679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.71ms 
171681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
171681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.2ns 
171682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
174048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
174799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
174802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
174804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
174804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.8ns 
174805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
177156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
177902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
177927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
177930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
177930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389ns 
177931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
180286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
181032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
181049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.52ms 
181051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
181051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
181051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
183411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
184178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
184180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.5ns 
184181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
184181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
184182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
186532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
187287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
187379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.71ms 
187382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
187382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.2ns 
187383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
189743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
190489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
190497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
190499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
190499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.8ns 
190500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
192868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
193614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
193619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
193620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
193620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
193621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
195982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
196731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
196758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.9ms 
196768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
196769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.1ns 
196770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
199197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
199941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
199951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
199953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
199953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.4ns 
199954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
202305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
203052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
203055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
203056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
203056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
203057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
205402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
206148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
206151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
206152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
206152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
206153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
208496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
209242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
209255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
209256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
209256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
209257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
211604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
212353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
212364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
212365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
212365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
212366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
214707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
215451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
215461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
215463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
215463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
215463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
217824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
218569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
218572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.1ns 
218573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
218573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
218574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
220922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
221674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
221677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
221679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
221679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
221680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
224042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
224787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
224791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
224792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
224792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
224793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
227135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
227880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
227882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 716.5ns 
227883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
227883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
227884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
230233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
230977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
230979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 390.5ns 
230980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
230980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
230981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
233324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
234070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
234073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
234074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
234074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
234075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
236417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
237161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
237163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 543.9ns 
237164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
237164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
237165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
239515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
240261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
240295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.62ms 
240297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
240297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.9ns 
240298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
242653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
243399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
243443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.76ms 
243446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
243446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.5ns 
243447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
245813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
246560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
246584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
246585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
246585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
246586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
248938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
249684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
249715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27ms 
249717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
249717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
249717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
252102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
252850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
252871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.75ms 
252873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
252873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.7ns 
252874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
255221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
255969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
256005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.16ms 
256007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
256007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.5ns 
256008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
258404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
259149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
259168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
259169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
259169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
259170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
261518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
262263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
262276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
262277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
262277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
262277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
264633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
265381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
265395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
265396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
265396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
265397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
267755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
268503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
268514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
268515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
268515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
268516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
270859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
271604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
271619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.88ms 
271620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
271621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
271621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
273974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
274719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
274733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 
274734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
274734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
274735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
277085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
277829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
277844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
277845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
277845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
277846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
280206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
280951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
280964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms 
280966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
280966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
280966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
283349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
284095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
284108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.51ms 
284109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
284109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
284110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
286456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
287200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
287219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
287220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
287220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
287220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
289572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
290325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
290340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
290342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
290342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.6ns 
290343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
292698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
293442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
293448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
293449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
293449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
293450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
295790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
296535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
296545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.49ms 
296546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
296546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
296547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
298894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
299640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
299643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
299644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
299644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
299645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
301989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
302735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
302737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 449.3ns 
302738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
302738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
302739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
305094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
305843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
305848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.3ns 
305849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
305849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
305850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
308203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
308949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
308955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
308956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
308956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
308956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
311303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
312090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
312095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
312097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
312097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.8ns 
312098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
314570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
315354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
315363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ms 
315364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
315364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
315364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
317831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
318614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
318617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
318618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
318618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
318619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
321094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
321877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
321879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 359.8ns 
321880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
321880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
321880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
324357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
325140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
325145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
325146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
325146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
325146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
327606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
328376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
328378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 405.4ns 
328379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
328379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
328380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
330713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
331487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
331489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 405.5ns 
331490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
331490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
331491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
333826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
334595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
334596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 414.8ns 
334597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
334597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
334598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
336935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
337706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
337710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
337711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
337711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
337711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
340042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
340809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
340817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
340818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
340818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
340819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
343156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
343924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
343927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
343928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
343928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
343929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
346269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
347035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
347040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
347041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
347041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
347042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
349380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
350145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
350149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
350150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
350150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
350150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
352486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
353252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
353263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.11ms 
353264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
353264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
353265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
355593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
356362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
356364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
356365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
356365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
356366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
358700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
359466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
359469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 814ns 
359470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
359470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
359470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
361805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
362571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
362574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
362575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
362575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
362576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
364930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
365736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
365748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.04ms 
365749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
365749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
365750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
368180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
368947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
368951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 257.2ns 
368952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
368952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
368953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
371282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
372045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
372068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 
372069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
372070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
372070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
374405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
375173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
375175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
375178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
375178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
375179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
377514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
378280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
378294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.88ms 
378295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
378295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
378296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
380634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
381402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
381423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.36ms 
381425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
381425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.9ns 
381426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
383766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
384535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
384552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.78ms 
384553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
384553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
384554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
386891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
387660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
387662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 468.8ns 
387663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
387663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
387664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
389996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
390762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
390767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
390768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
390768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
390768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
393100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
393869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
393873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
393875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
393875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
393875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
396225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
396996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
396998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.8ns 
396999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
396999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
397000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
399334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
400107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
400109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 621.3ns 
400110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
400110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
400111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
402447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
403219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
403222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 937.4ns 
403223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
403223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
403223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
405557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
406328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
406330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 880.6ns 
406332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
406332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
406332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
408691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
409503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
409510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
409511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
409511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
409511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
411840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
412612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
412618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
412619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
412619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
412620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
414960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
415731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
415737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
415738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
415738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
415739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
418067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
418843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
418850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
418851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
418851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
418852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
421180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
421959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
421963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
421965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
421965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.5ns 
421965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
424297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
425078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
425082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
425083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
425083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
425084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
427412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
428190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
428192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.6ns 
428193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
428193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
428194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
430527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
431305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
431307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 831.1ns 
431309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
431309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.8ns 
431310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
433674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
434433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
434435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.8ns 
434436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
434436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
434437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
436786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
437543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
437551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
437552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
437552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
437552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
439904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
440681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
440684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 957.2ns 
440685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
440685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
440685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
443019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
443800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
443805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
443806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
443806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
443807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
446143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
446921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
446923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.6ns 
446924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
446924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
446925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
449253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
450030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
450031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525ns 
450033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
450033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
450033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
452363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
453139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
453142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
453143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
453143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
453143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
455497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
456253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
456256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.2ns 
456257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
456257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
456257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
458606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
459365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
459367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910ns 
459368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
459368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
459369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
461819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
462599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
462601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.6ns 
462602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
462602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
462603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
464938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
465718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
465725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
465726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
465726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
465727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
468058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
468837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
468839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.9ns 
468840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
468840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
468841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
471169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
471946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
471953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
471954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
471955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
471955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
474306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
475063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
475065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 407.2ns 
475066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
475066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
475067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
477412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
478190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
478194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
478196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
478196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
478196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
480528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
481305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
481308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
481309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
481309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
481310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
483644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
484423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
484425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612ns 
484426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
484426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
484426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
486788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
487545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
487548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
487549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
487549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
487549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
489904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
490680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
490682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757ns 
490683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
490683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
490684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
493013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
493790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
493792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
493793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
493794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
493794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
496118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
496897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
496899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.1ns 
496900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
496900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.7ns 
496901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
499255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
500013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
500017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
500018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
500018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
500018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
502365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
503142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
503148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
503149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
503149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
503150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
505475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
506258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
506265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
506266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
506266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
506267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
508612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
509370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
509376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
509377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
509377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
509377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
511721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
512499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
512505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
512506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
512506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
512507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
514835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
515614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
515623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ms 
515624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
515624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
515625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
517972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
518730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
518739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ms 
518740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
518740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
518741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
521090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
521869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
521877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
521878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
521878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
521879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
524205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
524984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
524991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
524992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
524992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
524992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
527345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
528128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
528146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
528147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
528147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
528147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
530479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
531260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
531279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.93ms 
531281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
531281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
531281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
533627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
534387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
534404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
534405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
534405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
534406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
536754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
537534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
537551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
537552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
537552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
537552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
539881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
540659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
540677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ms 
540678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
540678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
540679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
543023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
543800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
543842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.49ms 
543844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
543844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
543844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
546179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
546961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
546965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
546966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
546966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
546967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
549315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
550093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
550098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
550100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
550100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.1ns 
550101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
552430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
553210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
553216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
553217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
553217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
553218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
555567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
556344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
556355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
556356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
556356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
556357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
558691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
559469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
559474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
559475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
559476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
559476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
561823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
562603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
562605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
562606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
562606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
562607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
564940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
565718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
565727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
565728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
565728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
565728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
568095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
568876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
568885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
568886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
568886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
568887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
571225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
572011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
572024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.35ms 
572026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
572026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
572027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
574492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
575311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
575314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.8ns 
575315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
575315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.5ns 
575315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
577759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
578577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
578580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
578581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
578581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
578581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
581045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
581851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
581856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
581857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
581857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.7ns 
581858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
584188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
584966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
584970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
584971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
584971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
584971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
587320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
588100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
588138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.08ms 
588139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
588139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
588140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
590553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
591363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
591380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
591381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
591381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174ns 
591382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
593717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
594498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
594507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
594508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
594508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
594509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
596857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
597638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
597640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 156.3ns 
597641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
597641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
597642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
599993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
600754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
600826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.18ms 
600827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
600828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
600828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
603182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
603964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
603995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.21ms 
603996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
603996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
603996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
606352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
607134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
607136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244.6ns 
607137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
607137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
607138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
609492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
610279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
610281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 183.9ns 
610282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
610282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.3ns 
610283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
612628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
613412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
613413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 183.9ns 
613415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
613415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
613415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
615766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
616549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
616551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 376.7ns 
616552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
616552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
616553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
618892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
619668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
619751     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
619758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.02ms 
619760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
619760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.8ns 
619761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
622121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
622881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
622918     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
622920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.32ms 
622921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
622921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
622922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
625272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
626071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
626072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
626101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
626137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
626157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
626163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
626179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
626180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
626183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
626185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
626192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
626193     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' 
626196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
626199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
626428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
626429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
626432     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' 
626433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
626434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
626570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
626571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
626574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
626575     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' 
626577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
626579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
626762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
626763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
626764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
626765     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' 
626765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
626766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
626896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
626897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
626898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
626899     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' 
626900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
626901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
626908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
626908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
626910     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' 
626911     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' 
626911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
626912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
626919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
626920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
626921     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' 
626922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
626922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
626923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
627062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
627062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
627063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
627193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
627194     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)'' 
627195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
627197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
627198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
627199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
627199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
627200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
627204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
627205     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' 
627206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
627207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
627208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
627348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
627351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
627352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
627353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
627354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
627354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
627355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
627476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
627477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
627478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
627479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
627480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
627481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
627481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
627482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
627580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
627582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
627672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
627676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
627681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
627681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
627682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
627683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
627684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
627684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
627685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
627685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
627693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
627697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
627799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
627800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
627801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
627802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
627803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
627803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
627804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
627804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
627858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
627864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
627969     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]'' 
627969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
627970     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'' 
627972     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'' 
627973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
627973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
628107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
628111     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'' 
628112     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)'' 
628112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
628114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
628114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
628115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
628115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
628125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
628125     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'' 
628126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
628127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
628236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
628236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
628237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
628238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
628239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
628239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
628369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
628370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
628371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
628372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
628372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
628373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
628374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
628374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
628455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
628456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
628528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
628528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
628529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
628533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
628537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
628541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
628656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
628657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
628658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
628659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
628669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
628751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
632330     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'' 
632331     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)'' 
632335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
632337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
632337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
632338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
632338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
632345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
632346     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'' 
632347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
632348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
632349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
632433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
632437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
632438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
632439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
632439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
632440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
632441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
632528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
632528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
632529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
632530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
632530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
632531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
632531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
632532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
632602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
632603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
632679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
632683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
632686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
632687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
632688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
632688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
632697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
632775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
632776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
632777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
632777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
632847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
632856     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'' 
632857     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)'' 
632857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
632859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
632860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
632860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
632861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
632871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
632872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
632872     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'' 
632873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
632874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
632958     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))'' 
632959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
632960     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'' 
632961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
632964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
633053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
633057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
633058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
633059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
633059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
633059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
633060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
633151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
633151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
633152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
633153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
633154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
633154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
633154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
633155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
633155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
633156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
633157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
633157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
633158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
633158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
633158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
633238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
633239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
633245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
633316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
633391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
633391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
633392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
633393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
633393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
633394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
633394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
633395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
633395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
633474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
633480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
633562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
633563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
633564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
633564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
633565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
633565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
633565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
633566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
633570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
633571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
633644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
633648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
633653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
633745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
633746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
633747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
633748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
633748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
633749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
633749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
633750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
633800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
633801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
633802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
633802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
633803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
633808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
633813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
633961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
634041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
634042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
634042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
634043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
634195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
634276     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'' 
634276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
637020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
637024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
637025     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'' 
637026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
637026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
637131     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))'' 
637132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
637132     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'' 
637133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
637134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
637230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
639975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
642935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
642939     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'' 
642940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
642940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
642941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
643045     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))'' 
643045     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'' 
643046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
643047     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)' ...' 
643048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
644053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
644053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
644054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
646498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
647308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
647310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
647310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
647316     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)'' 
647325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
647327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
647329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
647330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
647334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
647335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
647338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
647338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
647340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
647349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
647349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
647350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
647393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
647393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
647394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
647394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
647395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
647455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
647456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
647456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
647457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
647457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
647461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
647461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
647461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
647462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
647463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
647463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
647544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
647544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
647544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
647545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
647546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
647546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
647674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
647675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
647676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
647676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
647677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
647677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
647678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
647678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
647679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
647679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
647680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
647680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
647681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
647681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
647681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
647682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
647682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
647683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
647683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
647686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
647713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
647714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
647754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
647755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
647756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
647757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
647758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
647758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
647795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
647797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
647797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
647798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
647799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
647800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
647801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
647838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
647840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
647843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
647888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
647936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
647936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
647936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
650371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
651209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
651224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.64ms