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

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

tests
0

failures
0

ignored
14m9.39s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.115s passed
powPositiveConcrete data()[101] 4.217s passed
powGeq1Concrete data()[102] 4.248s passed
pow2InIntLower data()[103] 4.180s passed
pow2InIntUpper data()[104] 4.109s passed
logSelfConcrete data()[105] 4.154s passed
log1Concrete data()[106] 4.215s passed
logProduct data()[107] 4.091s passed
logTimesBaseConcrete data()[108] 4.184s passed
logProdIdentity data()[109] 4.127s passed
moduloByteIsInByte data()[10] 4.192s passed
logProdIdentityConcrete data()[110] 4.114s passed
logPowIdentity data()[111] 4.142s passed
logPowIdentityConcrete data()[112] 4.094s passed
logPositive data()[113] 4.184s passed
logPositiveConcrete data()[114] 4.095s passed
logMono data()[115] 4.142s passed
logMonoConcrete data()[116] 4.080s passed
powLogLess data()[117] 4.161s passed
powLogMore2 data()[118] 4.051s passed
logLessThanPow data()[119] 4.079s passed
moduloCharIsInChar data()[11] 4.288s passed
logLessThanPowConcrete data()[120] 3.999s passed
logSqueeze data()[121] 3.985s passed
ifthenelse_equals data()[122] 3.965s passed
ifthenelse_equals_1 data()[123] 3.994s passed
ifthenelse_equals_2 data()[124] 4.011s passed
disjointWithSingleton1 data()[125] 4.009s passed
disjointWithSingleton2 data()[126] 4.178s passed
disjointArrayRanges data()[127] 4.213s passed
disjointArrayRangeAllFields1 data()[128] 4.247s passed
disjointArrayRangeAllFields2 data()[129] 4.240s passed
div_unique1 data()[12] 4.249s passed
seqSelfDefinition data()[130] 4.336s passed
seqOutsideValue data()[131] 4.094s passed
castedGetAny data()[132] 4.344s passed
seqGetAlphaCast data()[133] 4.126s passed
getOfSeqSingleton data()[134] 4.206s passed
getOfSeqSingletonConcrete data()[135] 4.202s passed
getOfSeqConcat data()[136] 4.085s passed
getOfSeqSub data()[137] 4.107s passed
getOfSeqReverse data()[138] 3.993s passed
lenOfSeqEmpty data()[139] 4.025s passed
div_unique2 data()[13] 4.145s passed
lenOfSeqSingleton data()[140] 3.956s passed
lenOfSeqConcat data()[141] 3.955s passed
lenOfSeqSub data()[142] 4.018s passed
lenOfSeqReverse data()[143] 4.033s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.002s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.078s passed
getOfSeqSingletonEQ data()[146] 4.181s passed
getOfSeqConcatEQ data()[147] 4.080s passed
getOfSeqSubEQ data()[148] 4.089s passed
getOfSeqReverseEQ data()[149] 4.185s passed
div_exists data()[14] 4.386s passed
lenOfSeqEmptyEQ data()[150] 4.184s passed
lenOfSeqSingletonEQ data()[151] 4.165s passed
lenOfSeqConcatEQ data()[152] 4.202s passed
lenOfSeqSubEQ data()[153] 4.185s passed
lenOfSeqReverseEQ data()[154] 4.148s passed
getOfSeqDefEQ data()[155] 4.005s passed
lenOfSeqDefEQ data()[156] 3.987s passed
seqConcatWithSeqEmpty1 data()[157] 4.096s passed
seqConcatWithSeqEmpty2 data()[158] 4.002s passed
seqReverseOfSeqEmpty data()[159] 4.037s passed
div_one data()[15] 4.172s passed
subSeqComplete data()[160] 4.196s passed
subSeqTailR data()[161] 4.304s passed
subSeqTailL data()[162] 4.168s passed
subSeqTailEQR data()[163] 4.169s passed
subSeqTailEQL data()[164] 4.264s passed
seqDef_split data()[165] 4.152s passed
seqDef_induction_upper data()[166] 4.322s passed
seqDef_induction_upper_concrete data()[167] 4.269s passed
seqDef_induction_lower data()[168] 4.300s passed
seqDef_induction_lower_concrete data()[169] 4.221s passed
jdiv_one data()[16] 4.129s passed
seqDef_split_in_three data()[170] 4.116s passed
seqDef_empty data()[171] 4.038s passed
seqDef_one_summand data()[172] 4.025s passed
seqDef_lower_equals_upper data()[173] 4.001s passed
seqDefOfSeq data()[174] 4.038s passed
seqSelfDefinitionEQ2 data()[175] 4.136s passed
indexOfSeqSingleton data()[176] 4.021s passed
indexOfSeqConcatFirst data()[177] 4.054s passed
indexOfSeqConcatSecond data()[178] 4.059s passed
indexOfSeqSub data()[179] 4.085s passed
div_zero data()[17] 4.158s passed
lenOfArray2seq data()[180] 3.997s passed
getAnyOfArray2seq data()[181] 4.119s passed
getOfArray2seq data()[182] 4.026s passed
getAnyOfNPermInv data()[183] 4.019s passed
seqNPermRange data()[184] 4.030s passed
seqPermTrans data()[185] 4.042s passed
seqPermRefl data()[186] 4.135s passed
seqPermSplit data()[187] 4.052s passed
seqNPermRight data()[188] 4.268s passed
seqPermFromSwap data()[189] 4.297s passed
divResZero1 data()[18] 4.099s passed
seqPermTransAlt0 data()[190] 4.162s passed
seqPermTransAlt1 data()[191] 4.065s passed
seqPermTransAlt2 data()[192] 4.061s passed
seqPermTransAlt3 data()[193] 4.032s passed
seqPermForall data()[194] 4.249s passed
seqPermExists data()[195] 4.263s passed
schiffl_lemma_2 data()[196] 28.730s passed
schiffl_thm_1 data()[197] 5.279s passed
eqSameSeq data()[198] 4.444s passed
divResZero2 data()[19] 4.170s passed
eqTermCut data()[1] 4.915s passed
divResOne1 data()[20] 4.117s passed
divResOne2 data()[21] 4.190s passed
div_cancel1 data()[22] 4.183s passed
div_cancel2 data()[23] 4.208s passed
divAddMultDenom data()[24] 4.290s passed
divMinus data()[25] 4.265s passed
divMinusDenom data()[26] 4.179s passed
divLeastDPos data()[27] 4.242s passed
divLeastDNeg data()[28] 4.153s passed
divGreatestDPos data()[29] 4.272s passed
equivAllRight data()[2] 4.837s passed
divGreatestDNeg data()[30] 4.239s passed
divIncreasingPos data()[31] 4.223s passed
divIncreasingNeg data()[32] 4.108s passed
jdiv_zero data()[33] 4.253s passed
jdivPulloutMinusNum data()[34] 4.210s passed
jdivPulloutMinusDenom data()[35] 4.199s passed
jdiv_uniquePosPos data()[36] 4.282s passed
jdiv_uniquePosNeg data()[37] 4.225s passed
jdiv_uniqueNegPos data()[38] 4.179s passed
jdiv_uniqueNegNeg data()[39] 4.158s passed
irrflConcrete1 data()[3] 4.643s passed
jdivMultDenom1 data()[40] 4.250s passed
jdivMultDenom2 data()[41] 4.163s passed
mod_geZero data()[42] 4.235s passed
mod_lessDenom data()[43] 4.269s passed
jmod_NumPos data()[44] 4.284s passed
jmod_NumNeg data()[45] 4.207s passed
jmod_geZero data()[46] 4.208s passed
jmodNumZero data()[47] 4.245s passed
jmod_pulloutminusNum data()[48] 4.183s passed
jmod_pulloutminusDenom data()[49] 4.184s passed
irrflConcrete2 data()[4] 4.463s passed
jmodUnique1 data()[50] 4.290s passed
jmodUnique2 data()[51] 4.162s passed
intDivRem data()[52] 4.037s passed
jmodjmod data()[53] 3.983s passed
jmodDivisible data()[54] 4.001s passed
jmodDivisibleRep data()[55] 4.052s passed
jdivAddMultDenom data()[56] 4.151s passed
jmodAltZero data()[57] 4.060s passed
jmodAddMultDenomZero data()[58] 4.218s passed
polyDiv_zero data()[59] 4.211s passed
cancel_gtPos data()[5] 4.455s passed
polyMod_ltdivDenom data()[60] 4.147s passed
bsum_empty data()[61] 4.117s passed
bsum_induction_upper data()[62] 4.252s passed
bsum_induction_lower data()[63] 4.175s passed
bsum_num_of_bounds data()[64] 4.239s passed
bsum_num_of_bounds2 data()[65] 4.250s passed
bsum_induction_upper2 data()[66] 4.175s passed
bsum_induction_upper_concrete data()[67] 4.178s passed
bsum_induction_upper_concrete_2 data()[68] 4.069s passed
bsum_induction_upper2_concrete data()[69] 3.969s passed
cancel_gtNeg data()[6] 4.409s passed
bsum_induction_lower_concrete data()[70] 4.088s passed
bsum_induction_lower2 data()[71] 4.107s passed
bsum_induction_lower2_concrete data()[72] 4.046s passed
bsum_positive data()[73] 4.161s passed
bsum_upper_bound data()[74] 4.105s passed
bsum_lower_bound data()[75] 4.025s passed
bsum_positive_lower_bound_element data()[76] 4.097s passed
bsum_sub_same_index data()[77] 4.023s passed
bsum_less_same_index data()[78] 4.146s passed
bsum_equal_except_one_index data()[79] 4.049s passed
moduloIntIsInInt data()[7] 4.321s passed
bsum_num_of_is_max data()[80] 4.035s passed
bsum_num_of_is_max2 data()[81] 3.950s passed
bsum_num_of_is_max3 data()[82] 4.026s passed
bsum_num_of_is_max4 data()[83] 4.027s passed
bsum_num_of_lt_max data()[84] 4.112s passed
bsum_num_of_lt_max2 data()[85] 4.134s passed
bsum_num_of_lt_max3 data()[86] 4.120s passed
bsum_num_of_lt_max4 data()[87] 4.172s passed
bsum_num_of_gt0 data()[88] 4.174s passed
bsum_num_of_gt0_alt data()[89] 4.117s passed
moduloLongIsInLong data()[8] 4.361s passed
bsum_add_concrete data()[90] 4.211s passed
bprod_all_positive data()[91] 4.232s passed
bprod_split data()[92] 4.161s passed
powConcrete0 data()[93] 4.219s passed
powConcrete1 data()[94] 4.167s passed
powSplitFactor data()[95] 4.240s passed
powAdd data()[96] 4.164s passed
powMono data()[97] 4.114s passed
powMonoConcrete data()[98] 4.162s passed
powMonoConcreteRight data()[99] 4.141s passed
moduloShortIsInShort data()[9] 4.400s passed

Standard output

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

1793       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1795       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1797       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1797       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3511       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.77s 
10638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10686      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.1ns 
10710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10710      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 536.2ns 
10718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14416      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
14418      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15612      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.1ms 
15629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15629      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.6ns 
15633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
19126      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20462      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.13ms 
20465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249ns 
20467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
23927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25103      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.73ms 
25110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282ns 
25113      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28493      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
28493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29571      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
29574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29574      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 492.2ns 
29576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32932      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
32933      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34027      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.46ms 
34031      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34032      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.1ns 
34034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
37326      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38414      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38437      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.2ms 
38441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366ns 
38442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
41720      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42759      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
42761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42761      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338ns 
42762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46059      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
46059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
47113      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.8ns 
47123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
47125      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.32ms 
47127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
50485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
51517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
51520      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.9ns 
51522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
51522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns 
51523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
54664      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
55712      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.4ns 
55714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
55714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 
55715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58951      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
58951      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
60000      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702ns 
60003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
60003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 675.2ns 
60005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63198      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
63198      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
64249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.72ms 
64251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
64251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 
64253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
67343      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
68356      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
68394      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.13ms 
68397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
68397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
68398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
71506      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
72507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
72775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 258.41ms 
72794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
72795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.17ms 
72799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
75961      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
76955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
76961      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
76964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
76964      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.9ns 
76965      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
80121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
81088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
81091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
81093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
81094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141ns 
81095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
84166      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
85199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
85249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.74ms 
85252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
85252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 558.9ns 
85254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88311      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
88311      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
89331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
89349      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.15ms 
89351      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
89351      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 508.9ns 
89353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
92515      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
93502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
93519      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
93521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
93521      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
93522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
96624      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
97619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
97637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
97639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
97639      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.9ns 
97641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
100772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
101810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
101827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 
101828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
101828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
101830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
104969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
105984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
106009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.39ms 
106010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
106011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
106011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
109188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
110213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
110217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
110219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
110220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.7ns 
110221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
113445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
114455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
114506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.27ms 
114509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
114510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 522.1ns 
114511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
117644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
118675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
118766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.75ms 
118774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
118774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
118776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
121904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
122906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
122951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.69ms 
122953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
122953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.4ns 
122954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
126158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
127183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
127193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
127195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
127195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
127196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
130311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
131329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
131346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.65ms 
131348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
131348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.3ns 
131349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
134547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
135604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
135618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.58ms 
135620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
135620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.2ns 
135621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
138801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
139848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
139857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.21ms 
139859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
139859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
139860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
143013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
144068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
144079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
144086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
144090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.84ms 
144091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
147208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
148182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
148190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.11ms 
148193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
148193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
148194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
151396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
152439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
152444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
152446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
152446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
152447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
155662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
156643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
156655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
156656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
156656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
156657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
159791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
160791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
160850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.43ms 
160856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
160857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.1ns 
160858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
164064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
165089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
165134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.31ms 
165138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
165138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
165139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
168314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
169339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
169361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.68ms 
169362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
169363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
169363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
172499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
173519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
173540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.41ms 
173542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
173542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
173543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
176683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
177679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
177698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
177700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
177701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.5ns 
177703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
180899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
181904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
181948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.34ms 
181950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
181950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.3ns 
181951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
185089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
186108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
186111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
186112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
186113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
186113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
189319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
190340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
190346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
190348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
190348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
190349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
193591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
194606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
194615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.77ms 
194617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
194617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 
194618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
197807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
198889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
198899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
198900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
198900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
198901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
202062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
203085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
203107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.31ms 
203108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
203108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
203109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
206259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
207304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
207314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
207315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
207316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
207317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
210519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
211555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
211559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
211561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
211562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.8ns 
211563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
214725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
215738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
215743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
215744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
215744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
215745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
218895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
219922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
219926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
219928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
219928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns 
219929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
223099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
224132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
224215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.66ms 
224222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
224223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.7ns 
224226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
227323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
228279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
228382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.76ms 
228385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
228385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275ns 
228386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
231446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
232415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
232419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
232421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
232421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.6ns 
232423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
235385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
236365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
236402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.44ms 
236404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
236404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns 
236405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
239428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
240375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
240403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.38ms 
240405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
240405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
240406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
243464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
244440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
244444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
244456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
244456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
244460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
247496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
248446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
248605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.45ms 
248608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
248609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.4ns 
248610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
251678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
252655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
252666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
252667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
252667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
252668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
255849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
256876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
256884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
256885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
256885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
256886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
260084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
261076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
261095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.95ms 
261097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
261097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
261098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
264210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
265227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
265241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms 
265243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
265243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
265244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
268331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
269356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
269360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
269361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
269361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
269362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
272605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
273606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
273611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
273613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
273613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
273614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
276776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
277768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
277786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ms 
277787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
277788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
277788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
280946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
282009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
282025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ms 
282027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
282027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
282028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
285254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
286260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
286275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
286277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
286277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
286278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
289434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
290447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
290450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
290452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
290452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
290453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
293610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
294625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
294628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
294630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
294630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
294631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
297684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
298691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
298697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
298699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
298699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
298700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
301704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
302664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
302667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
302668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
302668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
302669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
305746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
306752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
306754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.7ns 
306756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
306756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
306757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
309854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
310857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
310861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
310863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
310863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
310864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
313922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
314905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
314908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.4ns 
314909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
314909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.2ns 
314910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
317990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
319018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
319067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.57ms 
319070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
319070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.2ns 
319072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
322144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
323129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
323173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.46ms 
323174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
323175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
323175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
326195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
327169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
327198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.98ms 
327200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
327200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
327201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
330251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
331251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
331295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.88ms 
331297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
331297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.3ns 
331298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
334333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
335293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
335318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.8ms 
335319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
335319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
335320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
338417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
339418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
339464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.67ms 
339466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
339466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 
339467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
342513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
343488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
343514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.56ms 
343515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
343515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
343516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
346557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
347531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
347548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
347550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
347550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
347551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
350544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
351479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
351498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.15ms 
351500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
351500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
351501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
354543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
355506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
355524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.07ms 
355525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
355525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
355526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
358538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
359528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
359551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.13ms 
359553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
359553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
359553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
362655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
363639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
363662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.79ms 
363666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
363669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.8ns 
363672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
366758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
367776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
367798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.36ms 
367799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
367799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
367800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
370952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
371898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
371918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.49ms 
371920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
371920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
371920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
375066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
376056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
376090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.33ms 
376091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
376091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
376092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
379226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
380241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
380264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.54ms 
380266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
380266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
380267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
383394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
384359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
384382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.23ms 
384383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
384383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
384384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
387557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
388584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
388592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
388594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
388594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
388595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
391789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
392810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
392825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
392826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
392826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.3ns 
392827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
395971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
396977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
396985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
396988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
396988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 
396989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
400175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
401201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
401204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 687.8ns 
401205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
401206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
401206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
404365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
405369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
405371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713.9ns 
405373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
405373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
405373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
408567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
409595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
409610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms 
409614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
409615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362ns 
409616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
412755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
413771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
413777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
413779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
413779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
413780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
416908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
417879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
417891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
417893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
417893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
417894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
421025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
422048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
422053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
422055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
422056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.5ns 
422056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
425186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
426192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
426195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551.21ns 
426196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
426196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
426197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
429309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
430304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
430310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
430311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
430311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
430312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
433493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
434523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
434526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 586.2ns 
434527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
434528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
434528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
437694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
438772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
438775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.9ns 
438777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
438777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
438778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
441936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
442952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
442955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.1ns 
442956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
442956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.8ns 
442957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
446063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
447060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
447064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
447065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
447065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
447066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
450223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
451208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
451218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.58ms 
451219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
451219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
451220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
454406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
455428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
455432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
455433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
455434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
455434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
458525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
459516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
459524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
459525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
459525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
459526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
462677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
463702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
463707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.68ms 
463709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
463709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
463710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
466825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
467819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
467834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
467836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
467836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
467837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
470973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
471944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
471948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
471949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
471949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
471950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
475066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
476087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
476091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
476092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
476092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
476093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
479187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
480180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
480184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
480186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
480186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
480187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
483345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
484351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
484368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.67ms 
484370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
484370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
484370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
487466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
488458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
488463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 333.6ns 
488466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
488466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
488467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
491561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
492570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
492606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.44ms 
492608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
492608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
492609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
495663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
496683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
496687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
496688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
496688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
496689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
499848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
500829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
500848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.45ms 
500850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
500850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.5ns 
500851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
503882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
504876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
504898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 
504901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
504901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.8ns 
504902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
507969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
508955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
508978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.67ms 
508979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
508979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
508980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
512002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
512973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
512976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584ns 
512978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
512978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.9ns 
512979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
516004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
516955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
516961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
516963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
516964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.07ms 
516965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
519959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
520923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
520927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
520929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
520929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.7ns 
520930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
523955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
524917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
524921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
524922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
524922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
524923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
527962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
528929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
528932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.8ns 
528933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
528933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
528934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
531942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
532937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
532940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
532941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
532941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
532942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
536088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
537115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
537118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
537119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
537119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
537121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
540264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
541321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
541331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
541333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
541334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
541334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
544527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
545569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
545577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
545582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
545582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.7ns 
545584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
548782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
549812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
549820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
549821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
549821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
549822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
553054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
554142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
554156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
554157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
554157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
554158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
557179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
558246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
558250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
558252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
558252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
558253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
561561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
562589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
562594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
562595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
562595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
562596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
565729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
566718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
566720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840ns 
566722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
566722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
566722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
569897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
570924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
570926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
570928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
570928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.2ns 
570929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
574110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
575126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
575129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
575130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
575131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.4ns 
575132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
578210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
579202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
579214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
579215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
579215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
579216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
582319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
583316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
583320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
583322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
583322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
583322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
586324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
587307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
587314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
587315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
587315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
587316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
590348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
591335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
591338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 845.3ns 
591339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
591339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
591340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
594313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
595292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
595295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781.5ns 
595296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
595296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
595297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
598282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
599245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
599249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
599251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
599251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
599251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
602293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
603266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
603268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 813.9ns 
603269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
603269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
603270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
606314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
607298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
607301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
607302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
607302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
607302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
610296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
611299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
611303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
611304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
611304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
611304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
614387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
615376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
615381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
615382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
615382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
615383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
618526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
619558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
619561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
619562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
619562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
619563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
622662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
623631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
623642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
623643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
623643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
623644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
626725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
627728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
627730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.7ns 
627731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
627731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
627732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
630822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
631909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
631915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
631917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
631917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
631917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
635053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
636095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
636098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 986.5ns 
636101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
636101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
636102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
639246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
640262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
640265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 909.2ns 
640266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
640266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
640267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
643433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
644462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
644467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
644468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
644468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
644469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
647604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
648648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
648651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
648653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
648653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
648653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
651782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
652796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
652799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
652801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
652801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
652802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
655807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
656800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
656804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
656808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
656808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
656809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
659806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
660788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
660793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
660795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
660795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
660795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
663847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
664878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
664889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.19ms 
664892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
664892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
664892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
667888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
668882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
668891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.27ms 
668892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
668892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
668893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
671928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
672921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
672928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
672929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
672929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
672930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
676067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
677117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
677124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms 
677125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
677125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
677126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
680386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
681416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
681429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
681430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
681430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
681431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
684560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
685583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
685597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.74ms 
685598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
685598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
685599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
688718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
689752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
689765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.85ms 
689767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
689767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
689767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
692970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
694021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
694029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
694030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
694030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
694031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
697165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
698156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
698181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
698183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
698183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
698184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
701376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
702473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
702503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.11ms 
702504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
702504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
702505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
705699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
706746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
706772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.14ms 
706773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
706773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
706774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
709983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
711049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
711072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ms 
711074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
711074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.9ns 
711075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
714260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
715268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
715293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
715295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
715295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
715296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
718337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
719349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
719409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.57ms 
719411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
719411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
719412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
722486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
723441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
723447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
723449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
723449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
723449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
726454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
727466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
727472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
727473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
727473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
727474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
730469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
731469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
731473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
731475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
731475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
731476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
734513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
735494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
735511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.65ms 
735513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
735513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
735513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
738614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
739640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
739648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
739649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
739649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
739650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
742677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
742678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
743665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
743669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
743670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
743670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
743671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
746719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
747710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
747722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
747723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
747723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
747724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
750738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
751769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
751782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.48ms 
751783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
751783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
751784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
754819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
755848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
755866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ms 
755868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
755869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 532.5ns 
755870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
758878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
759860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
759863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
759864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
759864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
759865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
762945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
763978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
763983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
763984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
763984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
763985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
767011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
768002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
768008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
768010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
768010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
768010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
771045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
772021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
772027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
772028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
772028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
772029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
774999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
776001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
776057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.41ms 
776059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
776059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
776060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
779078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
780074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
780099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.39ms 
780101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
780102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.2ns 
780103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
783231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
784220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
784235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ms 
784236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
784236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
784237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
787286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
788284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
788287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 165.8ns 
788289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
788289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.1ns 
788290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
791404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
792445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
792553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.68ms 
792555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
792555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
792556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
795736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
796805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
796851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.51ms 
796853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
796853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
796853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
800006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
801011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
801013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 336.1ns 
801016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
801016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
801017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
804071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
805076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
805078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244ns 
805080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
805080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
805081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
808120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
809137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
809139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 301.8ns 
809140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
809141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
809141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
812182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
813169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
813172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.1ns 
813173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
813173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
813174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
816253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
817278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
817406     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
817420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 138.35ms 
817423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
817423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.2ns 
817425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
820597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
821634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
821683     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
821684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.56ms 
821686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
821686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
821687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
824893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
824896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
826099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
826102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
826169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
826242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
826274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
826279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
826314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
826316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
826318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
826320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
826333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
826336     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' 
826341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
826354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
826720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
826728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
826730     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' 
826730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
826732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
826874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
826875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
826876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
826878     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' 
826879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
826881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
827086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
827088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
827089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
827090     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' 
827091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
827093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
827242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
827244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
827245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
827246     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' 
827246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
827248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
827257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
827257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
827259     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' 
827260     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' 
827261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
827262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
827271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
827272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
827273     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' 
827274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
827275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
827276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
827441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
827442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
827444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
827608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
827610     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)'' 
827611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
827614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
827615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
827616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
827616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
827617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
827622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
827623     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' 
827624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
827625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
827627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
827804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
827809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
827811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
827812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
827814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
827814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
827819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
828027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
828029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
828030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
828033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
828034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
828035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
828036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
828038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
828218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
828221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
828379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
828386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
828395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
828396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
828399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
828401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
828403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
828404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
828405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
828406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
828419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
828427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
828578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
828579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
828582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
828584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
828585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
828585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
828586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
828587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
828659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
828667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
828793     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]'' 
828794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
828795     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'' 
828797     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'' 
828799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
828800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
828967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
828972     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'' 
828975     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)'' 
828976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
828978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
828979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
828980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
828981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
828993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
828999     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'' 
829001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
829002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
829120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
829121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
829122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
829124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
829124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
829126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
829262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
829264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
829266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
829268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
829269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
829270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
829271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
829272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
829420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
829422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
829570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
829572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
829573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
829577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
829582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
829588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
829741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
829742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
829743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
829745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
829758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
829864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
834248     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'' 
834250     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)'' 
834255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
834257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
834258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
834258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
834259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
834269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
834270     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'' 
834271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
834273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
834274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
834400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
834405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
834406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
834407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
834408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
834409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
834410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
834568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
834569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
834571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
834572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
834573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
834574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
834575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
834575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
834675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
834676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
834772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
834777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
834783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
834784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
834785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
834786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
834800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
834905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
834906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
834907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
834909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
835003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
835015     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'' 
835016     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)'' 
835017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
835019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
835020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
835021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
835022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
835036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
835037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
835039     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'' 
835040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
835041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
835158     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))'' 
835159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
835160     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'' 
835161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
835162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
835285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
835291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
835293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
835294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
835295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
835295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
835296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
835429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
835430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
835432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
835433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
835434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
835435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
835435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
835436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
835437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
835438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
835439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
835440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
835441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
835442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
835443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
835559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
835561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
835569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
835669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
835772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
835773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
835774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
835775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
835776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
835776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
835777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
835777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
835778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
835887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
835896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
836010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
836011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
836012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
836013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
836014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
836015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
836015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
836016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
836022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
836023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
836122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
836130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
836137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
836267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
836267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
836268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
836269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
836270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
836270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
836271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
836271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
836346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
836347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
836348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
836348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
836349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
836357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
836364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
836515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
836663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
836664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
836664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
836665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
836873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
836987     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'' 
836987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
840716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
840721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
840722     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'' 
840723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
840724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
840935     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))'' 
840936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
840937     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'' 
840938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
840939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
841074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
844776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
848781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
848786     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'' 
848787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
848788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
848788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
848930     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))'' 
848931     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'' 
848932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
848934     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)' ...' 
848935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
850417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
850417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.2ns 
850418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
853804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
853804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
854907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
854909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
854910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
854917     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)'' 
854927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
854930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
854933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
854935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
854941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
854942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
854947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
854947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
854950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
854961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
854963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
854964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
855024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
855025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
855026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
855026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
855027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
855120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
855121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
855122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
855123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
855124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
855129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
855130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
855131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
855131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
855132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
855133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
855239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
855240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
855241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
855242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
855243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
855244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
855335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
855335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
855336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
855337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
855338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
855339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
855340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
855340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
855342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
855343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
855343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
855344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
855344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
855345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
855346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
855347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
855347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
855348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
855349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
855352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
855387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
855388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
855444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
855446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
855446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
855448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
855449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
855450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
855501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
855503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
855504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
855506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
855507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
855508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
855509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
855562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
855565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
855568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
855631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
855696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
855697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.3ns 
855698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
859008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
859008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
860118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
860139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.86ms