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

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

tests
0

failures
0

ignored
14m22.66s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.012s passed
powPositiveConcrete data()[101] 4.032s passed
powGeq1Concrete data()[102] 3.962s passed
pow2InIntLower data()[103] 4.037s passed
pow2InIntUpper data()[104] 4.137s passed
logSelfConcrete data()[105] 4.382s passed
log1Concrete data()[106] 4.244s passed
logProduct data()[107] 4.362s passed
logTimesBaseConcrete data()[108] 4.284s passed
logProdIdentity data()[109] 4.193s passed
moduloByteIsInByte data()[10] 4.457s passed
logProdIdentityConcrete data()[110] 4.329s passed
logPowIdentity data()[111] 4.359s passed
logPowIdentityConcrete data()[112] 4.211s passed
logPositive data()[113] 4.109s passed
logPositiveConcrete data()[114] 4.384s passed
logMono data()[115] 4.399s passed
logMonoConcrete data()[116] 4.352s passed
powLogLess data()[117] 4.333s passed
powLogMore2 data()[118] 4.363s passed
logLessThanPow data()[119] 4.200s passed
moduloCharIsInChar data()[11] 4.412s passed
logLessThanPowConcrete data()[120] 4.198s passed
logSqueeze data()[121] 4.173s passed
ifthenelse_equals data()[122] 4.196s passed
ifthenelse_equals_1 data()[123] 4.189s passed
ifthenelse_equals_2 data()[124] 4.083s passed
disjointWithSingleton1 data()[125] 4.157s passed
disjointWithSingleton2 data()[126] 4.145s passed
disjointArrayRanges data()[127] 4.267s passed
disjointArrayRangeAllFields1 data()[128] 4.177s passed
disjointArrayRangeAllFields2 data()[129] 4.264s passed
div_unique1 data()[12] 4.365s passed
seqSelfDefinition data()[130] 4.181s passed
seqOutsideValue data()[131] 4.028s passed
castedGetAny data()[132] 4.225s passed
seqGetAlphaCast data()[133] 4.127s passed
getOfSeqSingleton data()[134] 4.244s passed
getOfSeqSingletonConcrete data()[135] 4.311s passed
getOfSeqConcat data()[136] 4.224s passed
getOfSeqSub data()[137] 4.148s passed
getOfSeqReverse data()[138] 4.131s passed
lenOfSeqEmpty data()[139] 4.055s passed
div_unique2 data()[13] 4.435s passed
lenOfSeqSingleton data()[140] 4.128s passed
lenOfSeqConcat data()[141] 4.141s passed
lenOfSeqSub data()[142] 4.095s passed
lenOfSeqReverse data()[143] 4.181s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.158s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.203s passed
getOfSeqSingletonEQ data()[146] 4.127s passed
getOfSeqConcatEQ data()[147] 4.229s passed
getOfSeqSubEQ data()[148] 4.079s passed
getOfSeqReverseEQ data()[149] 4.049s passed
div_exists data()[14] 4.580s passed
lenOfSeqEmptyEQ data()[150] 4.084s passed
lenOfSeqSingletonEQ data()[151] 4.112s passed
lenOfSeqConcatEQ data()[152] 4.114s passed
lenOfSeqSubEQ data()[153] 4.320s passed
lenOfSeqReverseEQ data()[154] 4.285s passed
getOfSeqDefEQ data()[155] 4.079s passed
lenOfSeqDefEQ data()[156] 4.087s passed
seqConcatWithSeqEmpty1 data()[157] 4.045s passed
seqConcatWithSeqEmpty2 data()[158] 4.046s passed
seqReverseOfSeqEmpty data()[159] 4.180s passed
div_one data()[15] 4.330s passed
subSeqComplete data()[160] 4.008s passed
subSeqTailR data()[161] 4.266s passed
subSeqTailL data()[162] 4.120s passed
subSeqTailEQR data()[163] 4.092s passed
subSeqTailEQL data()[164] 4.213s passed
seqDef_split data()[165] 4.278s passed
seqDef_induction_upper data()[166] 4.143s passed
seqDef_induction_upper_concrete data()[167] 4.102s passed
seqDef_induction_lower data()[168] 4.147s passed
seqDef_induction_lower_concrete data()[169] 4.143s passed
jdiv_one data()[16] 4.354s passed
seqDef_split_in_three data()[170] 4.161s passed
seqDef_empty data()[171] 4.259s passed
seqDef_one_summand data()[172] 4.194s passed
seqDef_lower_equals_upper data()[173] 4.142s passed
seqDefOfSeq data()[174] 4.115s passed
seqSelfDefinitionEQ2 data()[175] 4.182s passed
indexOfSeqSingleton data()[176] 4.222s passed
indexOfSeqConcatFirst data()[177] 4.303s passed
indexOfSeqConcatSecond data()[178] 4.256s passed
indexOfSeqSub data()[179] 4.182s passed
div_zero data()[17] 4.389s passed
lenOfArray2seq data()[180] 4.143s passed
getAnyOfArray2seq data()[181] 4.079s passed
getOfArray2seq data()[182] 4.079s passed
getAnyOfNPermInv data()[183] 4.291s passed
seqNPermRange data()[184] 4.293s passed
seqPermTrans data()[185] 4.207s passed
seqPermRefl data()[186] 4.200s passed
seqPermSplit data()[187] 4.029s passed
seqNPermRight data()[188] 4.274s passed
seqPermFromSwap data()[189] 4.273s passed
divResZero1 data()[18] 4.493s passed
seqPermTransAlt0 data()[190] 4.147s passed
seqPermTransAlt1 data()[191] 3.994s passed
seqPermTransAlt2 data()[192] 4.199s passed
seqPermTransAlt3 data()[193] 4.289s passed
seqPermForall data()[194] 4.379s passed
seqPermExists data()[195] 4.407s passed
schiffl_lemma_2 data()[196] 28.137s passed
schiffl_thm_1 data()[197] 5.283s passed
eqSameSeq data()[198] 4.363s passed
divResZero2 data()[19] 4.310s passed
eqTermCut data()[1] 5.112s passed
divResOne1 data()[20] 4.355s passed
divResOne2 data()[21] 4.228s passed
div_cancel1 data()[22] 4.423s passed
div_cancel2 data()[23] 4.308s passed
divAddMultDenom data()[24] 4.471s passed
divMinus data()[25] 4.453s passed
divMinusDenom data()[26] 4.368s passed
divLeastDPos data()[27] 4.325s passed
divLeastDNeg data()[28] 4.286s passed
divGreatestDPos data()[29] 4.183s passed
equivAllRight data()[2] 4.629s passed
divGreatestDNeg data()[30] 4.294s passed
divIncreasingPos data()[31] 4.262s passed
divIncreasingNeg data()[32] 4.349s passed
jdiv_zero data()[33] 4.238s passed
jdivPulloutMinusNum data()[34] 4.300s passed
jdivPulloutMinusDenom data()[35] 4.300s passed
jdiv_uniquePosPos data()[36] 4.301s passed
jdiv_uniquePosNeg data()[37] 4.267s passed
jdiv_uniqueNegPos data()[38] 4.195s passed
jdiv_uniqueNegNeg data()[39] 4.377s passed
irrflConcrete1 data()[3] 4.539s passed
jdivMultDenom1 data()[40] 4.350s passed
jdivMultDenom2 data()[41] 4.233s passed
mod_geZero data()[42] 4.111s passed
mod_lessDenom data()[43] 4.329s passed
jmod_NumPos data()[44] 4.310s passed
jmod_NumNeg data()[45] 4.299s passed
jmod_geZero data()[46] 4.205s passed
jmodNumZero data()[47] 4.149s passed
jmod_pulloutminusNum data()[48] 4.340s passed
jmod_pulloutminusDenom data()[49] 4.369s passed
irrflConcrete2 data()[4] 4.470s passed
jmodUnique1 data()[50] 4.301s passed
jmodUnique2 data()[51] 4.348s passed
intDivRem data()[52] 4.106s passed
jmodjmod data()[53] 4.174s passed
jmodDivisible data()[54] 4.158s passed
jmodDivisibleRep data()[55] 4.098s passed
jdivAddMultDenom data()[56] 4.298s passed
jmodAltZero data()[57] 4.294s passed
jmodAddMultDenomZero data()[58] 4.182s passed
polyDiv_zero data()[59] 4.121s passed
cancel_gtPos data()[5] 4.658s passed
polyMod_ltdivDenom data()[60] 4.311s passed
bsum_empty data()[61] 4.149s passed
bsum_induction_upper data()[62] 4.031s passed
bsum_induction_lower data()[63] 4.214s passed
bsum_num_of_bounds data()[64] 4.095s passed
bsum_num_of_bounds2 data()[65] 4.152s passed
bsum_induction_upper2 data()[66] 4.197s passed
bsum_induction_upper_concrete data()[67] 4.190s passed
bsum_induction_upper_concrete_2 data()[68] 4.280s passed
bsum_induction_upper2_concrete data()[69] 4.171s passed
cancel_gtNeg data()[6] 4.537s passed
bsum_induction_lower_concrete data()[70] 4.069s passed
bsum_induction_lower2 data()[71] 4.149s passed
bsum_induction_lower2_concrete data()[72] 4.215s passed
bsum_positive data()[73] 4.229s passed
bsum_upper_bound data()[74] 4.264s passed
bsum_lower_bound data()[75] 4.299s passed
bsum_positive_lower_bound_element data()[76] 4.057s passed
bsum_sub_same_index data()[77] 4.142s passed
bsum_less_same_index data()[78] 4.102s passed
bsum_equal_except_one_index data()[79] 4.247s passed
moduloIntIsInInt data()[7] 4.363s passed
bsum_num_of_is_max data()[80] 4.179s passed
bsum_num_of_is_max2 data()[81] 4.308s passed
bsum_num_of_is_max3 data()[82] 4.190s passed
bsum_num_of_is_max4 data()[83] 4.170s passed
bsum_num_of_lt_max data()[84] 4.219s passed
bsum_num_of_lt_max2 data()[85] 4.123s passed
bsum_num_of_lt_max3 data()[86] 4.164s passed
bsum_num_of_lt_max4 data()[87] 4.343s passed
bsum_num_of_gt0 data()[88] 4.334s passed
bsum_num_of_gt0_alt data()[89] 4.262s passed
moduloLongIsInLong data()[8] 4.330s passed
bsum_add_concrete data()[90] 4.133s passed
bprod_all_positive data()[91] 4.106s passed
bprod_split data()[92] 4.094s passed
powConcrete0 data()[93] 4.153s passed
powConcrete1 data()[94] 4.099s passed
powSplitFactor data()[95] 4.021s passed
powAdd data()[96] 4.019s passed
powMono data()[97] 4.135s passed
powMonoConcrete data()[98] 4.262s passed
powMonoConcreteRight data()[99] 4.182s passed
moduloShortIsInShort data()[9] 4.237s passed

Standard output

801        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
837        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.94ms 
1165       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1189       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)

2601       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2604       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2607       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2608       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
5082       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
12224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 11.06s 
12344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
12457      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.5ns 
12494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
12494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.9ns 
12499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
16242      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
17552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
17583      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.27ms 
17597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
17598      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.3ns 
17602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21107      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
21107      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
22206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
22223      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms 
22227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
22228      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.2ns 
22230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
25662      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26755      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
26767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.5ns 
26769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
30128      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
31221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
31233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
31239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
31240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 949.81ns 
31242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
34722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35842      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35894      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.15ms 
35897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35898      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.9ns 
35902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
39346      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
40404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
40431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.55ms 
40436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
40436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 503.31ns 
40437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43755      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
43756      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44795      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
44798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.1ns 
44800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48070      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
48071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
49122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
49126      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.11ns 
49132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
49132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 704.81ns 
49134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52293      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
52294      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
53362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
53365      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.21ns 
53371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
53371      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.1ns 
53374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
56771      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
57820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
57826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
57829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
57829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.6ns 
57831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
61128      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
62234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
62238      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984.01ns 
62242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
62243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 847.71ns 
62245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65511      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
65512      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
66533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
66603      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.66ms 
66608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
66608      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
66613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
69935      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
70994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
71040      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.78ms 
71043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
71043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.1ns 
71045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
74399      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
75473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
75620      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.35ms 
75623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
75623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.5ns 
75624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
78847      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
79943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
79950      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
79953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
79954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.7ns 
79957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
83228      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
84301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
84305      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
84309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
84309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.21ns 
84311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87585      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
87586      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
88617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
88695      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.11ms 
88700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
88700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.1ns 
88701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
92058      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
93171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
93190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
93192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
93192      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
93194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96421      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
96422      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
97485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
97500      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.45ms 
97502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
97502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.4ns 
97503      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
100769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
101837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
101854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
101858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
101859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 508.01ns 
101860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
105007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
106068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
106084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.04ms 
106086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
106086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.1ns 
106087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
109413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
110472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
110506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.52ms 
110510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
110511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454ns 
110512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
113773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
114811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
114815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
114817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
114817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns 
114818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
118130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
119218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
119285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.7ms 
119290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
119291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.02ms 
119293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
122584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
123637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
123732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.46ms 
123742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
123743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.3ns 
123744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
126968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
128055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
128108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.65ms 
128110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
128110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
128114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
131412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
132423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
132434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
132435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
132436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
132437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
135662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
136700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
136719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ms 
136721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
136721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.5ns 
136722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
139866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
140887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
140902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
140904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
140904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
140905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
144135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
145186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
145196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
145198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
145198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.2ns 
145199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
148395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
149444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
149457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
149461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
149461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
149463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
152781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
153800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
153808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
153810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
153810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.2ns 
153811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
156979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
158041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
158046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
158047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
158048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns 
158049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
161283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
162332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
162346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.04ms 
162348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
162348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 
162349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
165550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
166591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
166645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.9ms 
166649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
166649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.3ns 
166651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
169899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
170927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
170948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.46ms 
170950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
170951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.31ns 
170952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
174141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
175192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
175215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
175218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
175218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352ns 
175219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
178331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
179385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
179410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.89ms 
179412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
179412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.1ns 
179413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
182718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
183767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
183787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
183788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
183788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
183790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
187048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
188086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
188137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.71ms 
188139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
188139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.9ns 
188140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
191352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
192367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
192371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
192372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
192372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
192373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
195465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
196476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
196481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
196483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
196483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
196485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
199784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
200800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
200810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
200812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
200812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
200813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
204060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
205109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
205120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
205122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
205122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
205123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
208357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
209396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
209419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.77ms 
209421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
209421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
209422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
212603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
213612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
213624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
213625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
213625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
213626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
216740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
217769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
217773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
217776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
217776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.4ns 
217778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
221048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
222101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
222106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
222122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
222122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.1ns 
222123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
225387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
226484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
226489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.71ms 
226491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
226491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
226492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
229668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
230695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
230789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.82ms 
230792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
230792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 
230793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
233976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
235024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
235138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.82ms 
235140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
235141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 
235142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
238295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
239240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
239244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
239246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
239246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
239248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
242357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
243369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
243418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.61ms 
243420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
243420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.1ns 
243421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
246537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
247543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
247576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.4ms 
247578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
247578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
247579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
250671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
251671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
251674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
251675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
251675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
251677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
254780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
255777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
255971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 180.15ms 
255974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
255974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
255976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
259190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
260252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
260265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.77ms 
260268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
260269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.1ns 
260270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
263448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
264441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
264448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
264450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
264450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
264451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
267552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
268540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
268569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.2ms 
268571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
268572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.7ns 
268573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
271850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
272862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
272878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
272882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
272883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.3ns 
272884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
276056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
277026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
277030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
277032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
277032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
277033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
280071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
281057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
281062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
281063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
281063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.9ns 
281064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
284223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
285248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
285273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.19ms 
285282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
285282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.2ns 
285285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
288353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
289351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
289373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
289375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
289376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 785.71ns 
289377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
292480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
293498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
293525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.95ms 
293527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
293527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.4ns 
293528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
296729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
297718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
297722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
297725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
297725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.3ns 
297726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
300876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
301908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
301912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
301914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
301914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
301915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
305155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
306185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
306192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
306194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
306194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
306195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
309335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
310360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
310364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
310365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
310365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
310366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
313439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
314429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
314432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.51ns 
314433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
314434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
314434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
317536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
318576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
318581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
318582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
318582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
318583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
321785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
322793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
322796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
322798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
322798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
322799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
325931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
326950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
327025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.31ms 
327032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
327032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
327033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
330241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
331256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
331293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.86ms 
331295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
331295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
331296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
334511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
335555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
335591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.06ms 
335596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
335596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 494ns 
335598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
338636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
339605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
339650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.15ms 
339651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
339651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
339652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
342791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
343762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
343792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.17ms 
343794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
343795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.6ns 
343796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
346818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
347837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
347894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.53ms 
347895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
347896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.9ns 
347896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
351094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
352110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
352141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.13ms 
352143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
352143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
352144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
355296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
356291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
356320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.22ms 
356322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
356322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
356323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
359549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
360603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
360628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21ms 
360630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
360631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 
360632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
363782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
364796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
364818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.03ms 
364820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
364820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 
364822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
367971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
368960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
368988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.55ms 
368990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
368990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.1ns 
368991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
372148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
373181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
373207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
373208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
373208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
373209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
376284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
377300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
377330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.01ms 
377333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
377333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
377334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
380465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
381469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
381494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.05ms 
381496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
381496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 
381497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
384779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
385813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
385837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.68ms 
385839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
385839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
385840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
389096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
390146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
390171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.07ms 
390173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
390173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
390174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
393353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
394395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
394433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.46ms 
394435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
394436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.8ns 
394437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
397570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
398551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
398566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
398567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
398568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
398569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
401652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
402654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
402672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
402673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
402673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
402674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
405774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
406761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
406766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
406769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
406770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.2ns 
406771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
409897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
410916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
410919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.41ns 
410921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
410921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
410921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
414013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
415013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
415018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
415020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
415020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
415021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
418048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
419023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
419038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
419041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
419041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.7ns 
419043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
422059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
423050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
423058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
423060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
423060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.7ns 
423061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
426215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
427179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
427193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.66ms 
427195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
427195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
427196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
430417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
431450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
431455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
431456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
431456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
431457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
434612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
435635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
435637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.9ns 
435639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
435639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
435640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
438668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
439637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
439649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
439651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
439651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.8ns 
439652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
442694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
443679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
443682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 819.41ns 
443683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
443683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
443684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
446680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
447641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
447644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 754.71ns 
447645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
447645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
447646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
450685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
451677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
451680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.01ns 
451682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
451682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
451683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
454806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
455812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
455818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
455819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
455819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
455820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
459153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
460189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
460199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.05ms 
460200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
460200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
460201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
463439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
464439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
464443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
464445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
464445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
464446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
467751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
468797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
468805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
468807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
468807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
468807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
472040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
473080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
473089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
473091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
473092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.6ns 
473093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
476261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
477262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
477282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.73ms 
477285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
477285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281ns 
477286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
480514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
481607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
481612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
481613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
481613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
481614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
484920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
485962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
485966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
485971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
485972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
485972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
489174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
490176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
490181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
490183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
490183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
490184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
493286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
494269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
494290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.62ms 
494292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
494292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
494293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
497591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
498666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
498673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.61ns 
498676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
498676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.2ns 
498677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
501972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
503031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
503073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.95ms 
503075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
503075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
503076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
506352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
507421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
507425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
507427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
507427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
507428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
510678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
511732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
511758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.11ms 
511759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
511759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
511760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
515054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
516097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
516121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.71ms 
516123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
516124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.5ns 
516125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
519245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
520295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
520321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms 
520323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
520323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
520324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
523506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
524515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
524518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.51ns 
524521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
524521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
524522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
527681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
528685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
528692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
528694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
528694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
528695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
531849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
532883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
532888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
532890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
532890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
532891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
536081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
537074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
537078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
537079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
537079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
537081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
540170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
541157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
541160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
541162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
541162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
541163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
544303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
545312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
545317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
545318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
545318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
545319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
548427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
549458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
549462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
549464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
549464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.4ns 
549465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
552687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
553718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
553729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
553731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
553731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
553732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
556853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
557895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
557906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.82ms 
557907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
557907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
557908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
561141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
562161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
562170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.64ms 
562172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
562172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
562173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
565301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
566341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
566351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
566353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
566353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
566353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
569388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
570373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
570379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
570381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
570381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
570381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
573541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
574599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
574605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
574606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
574606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
574607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
577712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
578728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
578731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.61ns 
578733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
578733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
578733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
581899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
582971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
582975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
582977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
582978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 
582979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
586251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
587283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
587286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
587287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
587287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
587288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
590460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
591498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
591510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
591511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
591512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
591512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
594663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
595655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
595658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
595659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
595659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113ns 
595660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
598735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
599782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
599789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
599790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
599790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
599791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
602823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
603842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
603845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
603846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
603846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
603847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
606925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
607969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
607972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.71ns 
607974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
607974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
607975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
611083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
612109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
612112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
612115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
612115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
612116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
615193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
616206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
616209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
616210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
616210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
616211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
619332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
620385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
620389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
620390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
620390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
620391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
623527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
624541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
624547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
624551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
624552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.1ns 
624555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
627726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
628745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
628750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
628751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
628751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
628752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
631791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
632874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
632877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
632879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
632879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
632880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
636084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
637095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
637106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
637107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
637107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
637108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
640150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
641182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
641185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781.71ns 
641186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
641186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
641187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
644224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
645228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
645234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
645236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
645236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
645237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
648304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
649316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
649319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
649320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
649320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
649321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
652400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
653426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
653431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
653432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
653432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
653433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
656470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
657539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
657544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
657546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
657546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
657546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
660794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
661859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
661863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
661865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
661865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
661866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
665112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
666145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
666149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
666151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
666151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
666151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
669225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
670226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
670229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
670232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
670232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
670233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
673299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
674312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
674318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
674319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
674319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
674320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
677332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
678351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
678362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
678364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
678364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
678365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
681354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
682398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
682408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
682410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
682410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
682411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
685571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
686579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
686588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.87ms 
686590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
686590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
686590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
689595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
690588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
690596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
690598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
690598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
690599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
693790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
694848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
694862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.69ms 
694864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
694864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
694865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
697958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
698969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
698983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms 
698984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
698984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
698985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
702040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
703062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
703075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
703076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
703076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
703077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
706236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
707277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
707287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.27ms 
707289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
707289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
707290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
710484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
711537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
711565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.01ms 
711566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
711566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
711567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
714648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
715677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
715708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.1ms 
715710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
715710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
715711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
718782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
719784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
719810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.82ms 
719812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
719812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
719813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
722901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
723932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
723957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
723959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
723959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
723960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
727040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
728074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
728100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
728101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
728101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
728102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
731167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
732190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
732260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.78ms 
732264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
732264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
732265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
735446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
736510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
736520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
736522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
736522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
736523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
739668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
740708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
740714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
740715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
740715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
740716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
743840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
744852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
744856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
744858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
744858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
744859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
747944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
748953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
748971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.39ms 
748973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
748973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 
748974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
752065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
753142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
753153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
753155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
753155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
753156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
756354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
757372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
757376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
757377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
757377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
757378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
760619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
761664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
761678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms 
761680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
761680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
761681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
764872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
765920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
765935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
765936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
765936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
765937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
769076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
770098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
770116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.09ms 
770118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
770118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
770119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
773199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
774255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
774259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
774261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
774261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.6ns 
774262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
777298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
778334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
778338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
778340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
778340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
778340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
781409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
782410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
782418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
782419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
782419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
782420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
785631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
786702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
786708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
786710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
786710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
786712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
789880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
790942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
791001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.14ms 
791003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
791003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
791004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
794146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
795182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
795208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.26ms 
795210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
795210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.2ns 
795211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
798384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
799394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
799409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 
799410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
799410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
799411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
802442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
803435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
803437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 204.1ns 
803439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
803439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
803440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
806556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
807584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
807711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.52ms 
807713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
807713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.4ns 
807714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
810899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
811932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
811984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.64ms 
811989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
811989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
811990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
815125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
815125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
816132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
816135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 469.5ns 
816137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
816138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns 
816139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
819119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
820126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
820128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 350.9ns 
820129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
820130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
820130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
823267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
824324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
824327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 281.6ns 
824329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
824329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.5ns 
824330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
827549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
828614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
828616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 423.61ns 
828617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
828617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
828618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
831797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
831797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
832875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
832979     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
832994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116ms 
832997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
832997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.6ns 
832999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
836211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
837312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
837401     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
837402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75ms 
837404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
837404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
837407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
840572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
841631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
841633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
841672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
841738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
841766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
841775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
841797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
841798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
841801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
841802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
841807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
841809     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' 
841812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
841814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
842032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
842033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
842034     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' 
842035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
842037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
842192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
842194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
842195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
842196     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' 
842198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
842200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
842410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
842412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
842413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
842415     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' 
842416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
842418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
842581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
842582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
842584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
842585     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' 
842585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
842587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
842595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
842596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
842598     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' 
842600     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' 
842600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
842601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
842614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
842614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
842616     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' 
842617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
842617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
842618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
842789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
842790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
842792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
842942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
842944     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)'' 
842945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
842947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
842948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
842949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
842950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
842957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
842961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
842962     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' 
842964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
842965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
842967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
843115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
843120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
843122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
843123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
843125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
843125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
843126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
843286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
843287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
843289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
843290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
843291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
843292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
843294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
843295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
843428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
843429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
843545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
843551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
843556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
843557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
843559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
843560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
843561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
843562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
843563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
843564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
843574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
843580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
843706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
843707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
843708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
843710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
843711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
843711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
843712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
843713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
843782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
843789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
843912     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]'' 
843914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
843915     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'' 
843917     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'' 
843918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
843920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
844111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
844117     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'' 
844118     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)'' 
844119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
844121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
844123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
844124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
844124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
844139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
844140     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'' 
844142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
844153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
844306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
844308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
844309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
844310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
844311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
844312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
844458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
844461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
844463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
844464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
844465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
844466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
844467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
844468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
844587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
844593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
844707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
844708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
844709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
844716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
844721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
844727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
844884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
844886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
844887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
844888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
844901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
845044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
849640     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'' 
849641     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)'' 
849645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
849647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
849648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
849649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
849649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
849659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
849660     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'' 
849662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
849663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
849664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
849782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
849787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
849788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
849789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
849790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
849790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
849791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
849911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
849913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
849914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
849915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
849916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
849917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
849918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
849918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
850024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
850027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
850125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
850131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
850137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
850138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
850139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
850140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
850153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
850313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
850314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
850315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
850317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
850408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
850422     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'' 
850423     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)'' 
850424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
850426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
850427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
850427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
850428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
850442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
850443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
850444     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'' 
850446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
850447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
850554     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))'' 
850555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
850557     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'' 
850558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
850559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
850676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
850688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
850689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
850691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
850692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
850693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
850694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
850821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
850822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
850823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
850825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
850826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
850827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
850827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
850828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
850829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
850830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
850832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
850833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
850833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
850834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
850834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
850940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
850941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
850949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
851046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
851148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
851150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
851151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
851152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
851153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
851154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
851155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
851155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
851156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
851259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
851267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
851373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
851374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
851375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
851376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
851376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
851377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
851377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
851378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
851384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
851387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
851486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
851493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
851502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
851619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
851620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
851621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
851622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
851623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
851623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
851624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
851624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
851689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
851691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
851691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
851692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
851693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
851700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
851706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
851850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
851959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
851960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
851961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
851962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
852174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
852348     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'' 
852348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
856003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
856009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
856011     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'' 
856012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
856013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
856161     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))'' 
856162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
856164     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'' 
856165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
856166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
856296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
859899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
863919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
863923     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'' 
863925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
863926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
863927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
864072     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))'' 
864073     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'' 
864074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
864075     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)' ...' 
864076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
865542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
865542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127ns 
865544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
868802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
868803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
869982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
869983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
869984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
869992     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)'' 
870003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
870006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
870008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
870010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
870016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
870016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
870021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
870021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
870024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
870036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
870036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
870038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
870103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
870104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
870104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
870105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
870106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
870194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
870195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
870195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
870196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
870197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
870201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
870202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
870202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
870203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
870203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
870204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
870313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
870313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
870314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
870315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
870316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
870317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
870417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
870418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
870418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
870419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
870419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
870420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
870421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
870421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
870422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
870422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
870422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
870423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
870423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
870424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
870424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
870425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
870425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
870426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
870427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
870430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
870473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
870474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
870542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
870543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
870543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
870545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
870546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
870546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
870608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
870611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
870612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
870613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
870614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
870616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
870616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
870672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
870675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
870683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
870755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
870824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
870824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
870825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
874030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
874030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
875162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
875185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.53ms