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

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

tests
0

failures
0

ignored
11m10.64s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.338s passed
powPositiveConcrete data()[101] 3.350s passed
powGeq1Concrete data()[102] 3.314s passed
pow2InIntLower data()[103] 3.293s passed
pow2InIntUpper data()[104] 3.307s passed
logSelfConcrete data()[105] 3.297s passed
log1Concrete data()[106] 3.272s passed
logProduct data()[107] 3.309s passed
logTimesBaseConcrete data()[108] 3.279s passed
logProdIdentity data()[109] 3.303s passed
moduloByteIsInByte data()[10] 3.342s passed
logProdIdentityConcrete data()[110] 3.291s passed
logPowIdentity data()[111] 3.275s passed
logPowIdentityConcrete data()[112] 3.295s passed
logPositive data()[113] 3.278s passed
logPositiveConcrete data()[114] 3.255s passed
logMono data()[115] 3.254s passed
logMonoConcrete data()[116] 3.262s passed
powLogLess data()[117] 3.295s passed
powLogMore2 data()[118] 3.288s passed
logLessThanPow data()[119] 3.296s passed
moduloCharIsInChar data()[11] 3.306s passed
logLessThanPowConcrete data()[120] 3.272s passed
logSqueeze data()[121] 3.277s passed
ifthenelse_equals data()[122] 3.286s passed
ifthenelse_equals_1 data()[123] 3.291s passed
ifthenelse_equals_2 data()[124] 3.271s passed
disjointWithSingleton1 data()[125] 3.246s passed
disjointWithSingleton2 data()[126] 3.286s passed
disjointArrayRanges data()[127] 3.306s passed
disjointArrayRangeAllFields1 data()[128] 3.295s passed
disjointArrayRangeAllFields2 data()[129] 3.277s passed
div_unique1 data()[12] 3.375s passed
seqSelfDefinition data()[130] 3.262s passed
seqOutsideValue data()[131] 3.245s passed
castedGetAny data()[132] 3.248s passed
seqGetAlphaCast data()[133] 3.241s passed
getOfSeqSingleton data()[134] 3.240s passed
getOfSeqSingletonConcrete data()[135] 3.244s passed
getOfSeqConcat data()[136] 3.235s passed
getOfSeqSub data()[137] 3.241s passed
getOfSeqReverse data()[138] 3.240s passed
lenOfSeqEmpty data()[139] 3.245s passed
div_unique2 data()[13] 3.371s passed
lenOfSeqSingleton data()[140] 3.234s passed
lenOfSeqConcat data()[141] 3.246s passed
lenOfSeqSub data()[142] 3.233s passed
lenOfSeqReverse data()[143] 3.248s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.239s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.240s passed
getOfSeqSingletonEQ data()[146] 3.232s passed
getOfSeqConcatEQ data()[147] 3.237s passed
getOfSeqSubEQ data()[148] 3.237s passed
getOfSeqReverseEQ data()[149] 3.239s passed
div_exists data()[14] 3.435s passed
lenOfSeqEmptyEQ data()[150] 3.236s passed
lenOfSeqSingletonEQ data()[151] 3.231s passed
lenOfSeqConcatEQ data()[152] 3.236s passed
lenOfSeqSubEQ data()[153] 3.267s passed
lenOfSeqReverseEQ data()[154] 3.236s passed
getOfSeqDefEQ data()[155] 3.238s passed
lenOfSeqDefEQ data()[156] 3.231s passed
seqConcatWithSeqEmpty1 data()[157] 3.238s passed
seqConcatWithSeqEmpty2 data()[158] 3.243s passed
seqReverseOfSeqEmpty data()[159] 3.235s passed
div_one data()[15] 3.293s passed
subSeqComplete data()[160] 3.237s passed
subSeqTailR data()[161] 3.236s passed
subSeqTailL data()[162] 3.257s passed
subSeqTailEQR data()[163] 3.241s passed
subSeqTailEQL data()[164] 3.243s passed
seqDef_split data()[165] 3.251s passed
seqDef_induction_upper data()[166] 3.258s passed
seqDef_induction_upper_concrete data()[167] 3.249s passed
seqDef_induction_lower data()[168] 3.265s passed
seqDef_induction_lower_concrete data()[169] 3.270s passed
jdiv_one data()[16] 3.302s passed
seqDef_split_in_three data()[170] 3.276s passed
seqDef_empty data()[171] 3.241s passed
seqDef_one_summand data()[172] 3.269s passed
seqDef_lower_equals_upper data()[173] 3.241s passed
seqDefOfSeq data()[174] 3.240s passed
seqSelfDefinitionEQ2 data()[175] 3.237s passed
indexOfSeqSingleton data()[176] 3.257s passed
indexOfSeqConcatFirst data()[177] 3.241s passed
indexOfSeqConcatSecond data()[178] 3.250s passed
indexOfSeqSub data()[179] 3.264s passed
div_zero data()[17] 3.366s passed
lenOfArray2seq data()[180] 3.231s passed
getAnyOfArray2seq data()[181] 3.231s passed
getOfArray2seq data()[182] 3.258s passed
getAnyOfNPermInv data()[183] 3.249s passed
seqNPermRange data()[184] 3.271s passed
seqPermTrans data()[185] 3.283s passed
seqPermRefl data()[186] 3.241s passed
seqPermSplit data()[187] 3.247s passed
seqNPermRight data()[188] 3.383s passed
seqPermFromSwap data()[189] 3.273s passed
divResZero1 data()[18] 3.297s passed
seqPermTransAlt0 data()[190] 3.253s passed
seqPermTransAlt1 data()[191] 3.241s passed
seqPermTransAlt2 data()[192] 3.248s passed
seqPermTransAlt3 data()[193] 3.234s passed
seqPermForall data()[194] 3.314s passed
seqPermExists data()[195] 3.314s passed
schiffl_lemma_2 data()[196] 21.317s passed
schiffl_thm_1 data()[197] 4.006s passed
eqSameSeq data()[198] 3.297s passed
divResZero2 data()[19] 3.324s passed
eqTermCut data()[1] 4.058s passed
divResOne1 data()[20] 3.297s passed
divResOne2 data()[21] 3.355s passed
div_cancel1 data()[22] 3.282s passed
div_cancel2 data()[23] 3.265s passed
divAddMultDenom data()[24] 3.317s passed
divMinus data()[25] 3.317s passed
divMinusDenom data()[26] 3.310s passed
divLeastDPos data()[27] 3.307s passed
divLeastDNeg data()[28] 3.288s passed
divGreatestDPos data()[29] 3.233s passed
equivAllRight data()[2] 3.822s passed
divGreatestDNeg data()[30] 3.276s passed
divIncreasingPos data()[31] 3.285s passed
divIncreasingNeg data()[32] 3.294s passed
jdiv_zero data()[33] 3.278s passed
jdivPulloutMinusNum data()[34] 3.270s passed
jdivPulloutMinusDenom data()[35] 3.292s passed
jdiv_uniquePosPos data()[36] 3.337s passed
jdiv_uniquePosNeg data()[37] 3.299s passed
jdiv_uniqueNegPos data()[38] 3.275s passed
jdiv_uniqueNegNeg data()[39] 3.250s passed
irrflConcrete1 data()[3] 3.568s passed
jdivMultDenom1 data()[40] 3.316s passed
jdivMultDenom2 data()[41] 3.241s passed
mod_geZero data()[42] 3.281s passed
mod_lessDenom data()[43] 3.276s passed
jmod_NumPos data()[44] 3.261s passed
jmod_NumNeg data()[45] 3.282s passed
jmod_geZero data()[46] 3.266s passed
jmodNumZero data()[47] 3.261s passed
jmod_pulloutminusNum data()[48] 3.272s passed
jmod_pulloutminusDenom data()[49] 3.251s passed
irrflConcrete2 data()[4] 3.420s passed
jmodUnique1 data()[50] 3.287s passed
jmodUnique2 data()[51] 3.316s passed
intDivRem data()[52] 3.249s passed
jmodjmod data()[53] 3.279s passed
jmodDivisible data()[54] 3.275s passed
jmodDivisibleRep data()[55] 3.271s passed
jdivAddMultDenom data()[56] 3.359s passed
jmodAltZero data()[57] 3.240s passed
jmodAddMultDenomZero data()[58] 3.247s passed
polyDiv_zero data()[59] 3.266s passed
cancel_gtPos data()[5] 3.418s passed
polyMod_ltdivDenom data()[60] 3.293s passed
bsum_empty data()[61] 3.319s passed
bsum_induction_upper data()[62] 3.284s passed
bsum_induction_lower data()[63] 3.250s passed
bsum_num_of_bounds data()[64] 3.307s passed
bsum_num_of_bounds2 data()[65] 3.305s passed
bsum_induction_upper2 data()[66] 3.263s passed
bsum_induction_upper_concrete data()[67] 3.309s passed
bsum_induction_upper_concrete_2 data()[68] 3.243s passed
bsum_induction_upper2_concrete data()[69] 3.283s passed
cancel_gtNeg data()[6] 3.389s passed
bsum_induction_lower_concrete data()[70] 3.270s passed
bsum_induction_lower2 data()[71] 3.241s passed
bsum_induction_lower2_concrete data()[72] 3.314s passed
bsum_positive data()[73] 3.324s passed
bsum_upper_bound data()[74] 3.318s passed
bsum_lower_bound data()[75] 3.341s passed
bsum_positive_lower_bound_element data()[76] 3.327s passed
bsum_sub_same_index data()[77] 3.333s passed
bsum_less_same_index data()[78] 3.319s passed
bsum_equal_except_one_index data()[79] 3.276s passed
moduloIntIsInInt data()[7] 3.317s passed
bsum_num_of_is_max data()[80] 3.330s passed
bsum_num_of_is_max2 data()[81] 3.304s passed
bsum_num_of_is_max3 data()[82] 3.327s passed
bsum_num_of_is_max4 data()[83] 3.286s passed
bsum_num_of_lt_max data()[84] 3.402s passed
bsum_num_of_lt_max2 data()[85] 3.351s passed
bsum_num_of_lt_max3 data()[86] 3.280s passed
bsum_num_of_lt_max4 data()[87] 3.399s passed
bsum_num_of_gt0 data()[88] 3.315s passed
bsum_num_of_gt0_alt data()[89] 3.391s passed
moduloLongIsInLong data()[8] 3.326s passed
bsum_add_concrete data()[90] 3.337s passed
bprod_all_positive data()[91] 3.365s passed
bprod_split data()[92] 3.319s passed
powConcrete0 data()[93] 3.273s passed
powConcrete1 data()[94] 3.312s passed
powSplitFactor data()[95] 3.343s passed
powAdd data()[96] 3.308s passed
powMono data()[97] 3.309s passed
powMonoConcrete data()[98] 3.295s passed
powMonoConcreteRight data()[99] 3.257s passed
moduloShortIsInShort data()[9] 3.381s passed

Standard output

335        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
358        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.06ms 
556        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568        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)

1431       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1434       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1438       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1438       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2784       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8039       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.48s 
8097       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8130       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.5ns 
8141       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8141       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235ns 
8161       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
11184      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.76ms 
12202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12202      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.8ns 
12206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15110      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
15111      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16022      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
16024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.4ns 
16026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
18686      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19590      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
19593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19593      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.51ns 
19594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
22159      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23010      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
23012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
23014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25560      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
25560      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26423      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.49ms 
26433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.3ns 
26435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
28969      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29819      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.56ms 
29823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.61ns 
29824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
32330      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33137      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.62ns 
33140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.41ns 
33141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35661      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
35661      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36463      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.41ns 
36466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36466      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.2ns 
36467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
39011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39844      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.21ns 
39846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.7ns 
39848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42338      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
42338      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43186      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
43189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns 
43191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
45678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46493      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.41ns 
46494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46495      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
46495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
48983      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49862      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.38ms 
49874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49876      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.09ms 
49878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52379      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
52379      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53233      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.66ms 
53243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.76ms 
53256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
55745      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56676      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.9ms 
56678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56678      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
56679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59153      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
59153      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59965      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
59971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
59972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
62447      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63271      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
63273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.1ns 
63275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
65768      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.44ms 
66640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.11ns 
66641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69119      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
69121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69934      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
69937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69937      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 
69938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
72430      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73258      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
73262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 865.71ns 
73267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
75759      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76555      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.18ms 
76558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.91ns 
76560      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
79073      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79899      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79911      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
79914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.81ns 
79915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
82370      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
83193      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
83195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
83195      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.2ns 
83196      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85647      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
85648      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86458      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
86459      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
86460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
88926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89744      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.99ms 
89778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.11ns 
89780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
92239      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
93091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.38ms 
93095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
93096      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.11ns 
93097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
95563      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
96373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
96403      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.68ms 
96405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
96405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
96406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98875      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
98876      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99709      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
99713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.41ns 
99714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
102174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.73ms 
103000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
103000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.1ns 
103001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
105442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
106221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
106231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
106233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
106233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
106233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
108711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
109495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
109507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
109509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
109510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.91ns 
109511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
111997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
112793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 
112794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
115271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
116086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
116088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
116088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.7ns 
116089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
118552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
119359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
119364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
119369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
119370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.11ns 
119371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
121823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
122627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
122637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.59ms 
122638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
122639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
122639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
125091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.59ms 
125932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.5ns 
125942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
128445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
129250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
129266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
129268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
129268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.11ns 
129269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
131748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
132550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
132565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ms 
132567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
132567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
132568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
135018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
135825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
135841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
135842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
135842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
135843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
138296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
139090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
139091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
139092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
139092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
141593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
142373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
142406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.19ms 
142408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
142408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
142409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
144865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
145644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
145647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
145649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
145649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
145649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
148121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
148923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
148928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
148931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
148931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.1ns 
148933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
151386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
152204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
152205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
152205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
152206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
154654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
155458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
155465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
155467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
155467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
155467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
157927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
158731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
158747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
158749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
158749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
158750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
161198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
162006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
162013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
162015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
162015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
162016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
164457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
165268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
165274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
165277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
165277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.61ns 
165278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
167739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
168542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
168546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
168548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
168548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
168548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
170992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
171794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
171798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
171799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
171799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
171800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
174246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
175025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
175083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.66ms 
175085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
175085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
175086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
177554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
178331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
178400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.88ms 
178401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
178401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
178402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
180867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
181646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
181649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
181651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
181651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
181652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
184099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
184899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
184928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.36ms 
184930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
184930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.9ns 
184931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
187379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
188181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
188203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.03ms 
188204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
188205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
188205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
190663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
191471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
191474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.41ns 
191478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
191478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.71ns 
191479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
193927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
194728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
194834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 96.47ms 
194836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
194837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
194837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
197268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
198066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
198075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
198077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
198077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
198078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
200510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
201316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
201322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.36ms 
201327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
201327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
201328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
203760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
204564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
204590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.52ms 
204595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
204596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.4ns 
204596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
207060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
207873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
207885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.49ms 
207888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
207888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
207889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
210407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
211201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
211205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
211207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
211207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
211208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
213704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
214485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
214489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
214491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
214491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
214491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
216948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
217725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
217740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
217741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
217741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
217742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
220210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
221032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
221046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
221048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
221048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
221049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
223534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
224339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
224352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
224353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
224353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
224354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
226804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
227611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
227614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
227616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
227616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
227617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
230120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
230920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
230923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
230925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
230925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
230925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
233363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
234162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
234166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
234168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
234168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
234169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
236640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
237446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
237449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
237452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
237452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 
237453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
239907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
240717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
240719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.31ns 
240720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
240720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
240721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
243179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
243957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
243961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
243962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
243962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
243963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
246476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
247271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
247274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.71ns 
247275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
247275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
247276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
249782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
250563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
250598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.92ms 
250601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
250601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.3ns 
250602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
253100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
253886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
253916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.67ms 
253918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
253919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.1ns 
253920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
256429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
257236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
257258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.59ms 
257259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
257259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
257260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
259726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
260551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
260584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.49ms 
260587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
260587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.7ns 
260588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
263084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
263899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
263918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.06ms 
263920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
263921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.9ns 
263922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
266381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
267190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
267237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.5ms 
267239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
267239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
267240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
269694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
270494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
270513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ms 
270515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
270516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.8ns 
270517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
273003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
273828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
273843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ms 
273845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
273845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.3ns 
273846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
276326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
277131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
277147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.92ms 
277148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
277149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
277149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
279664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
280458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
280474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.67ms 
280476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
280476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
280477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
282955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
283741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
283760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.96ms 
283762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
283762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
283763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
286339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
287144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
287162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 
287163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
287163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
287164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
289708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
290495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
290513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.06ms 
290514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
290514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
290516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
292966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
293777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
293793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 
293795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
293796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 716.51ns 
293797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
296352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
297175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
297192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
297194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
297195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.5ns 
297196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
299653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
300473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
300507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.76ms 
300509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
300510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
303068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
303882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
303898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
303900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
303901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
306406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
307229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
307235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
307237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
307237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
307238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
309770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
310585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
310600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms 
310603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
310604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.5ns 
310605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
313109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
313917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
313921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
313923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
313923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
313923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
316391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
317192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
317195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.71ns 
317196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
317196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
317197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
319725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
320504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
320507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.11ns 
320508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
320508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
320509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
323036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
323841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
323849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.91ms 
323850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
323850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.4ns 
323851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
326344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
327151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
327157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
327159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
327159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.91ns 
327160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
329655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
330455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
330466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.84ms 
330467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
330467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
330468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
332952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
333758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
333762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
333763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
333763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
333764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
336209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
337016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
337018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 486.41ns 
337020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
337020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
337020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
339528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
340351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
340356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
340358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
340358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
340359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
342882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
343704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
343706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651ns 
343708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
343708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
343709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
346210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
347018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
347021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.51ns 
347022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
347022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
347023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
349489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
350311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
350313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.11ns 
350315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
350315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
350316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
352829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
353616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
353620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
353621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
353622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
353622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
356116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
356901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
356917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 
356919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
356920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.4ns 
356920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
359396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
360186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
360190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
360191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
360191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
360193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
362678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
363492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
363498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
363500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
363500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
363500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
365971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
366773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
366778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
366779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
366779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
366780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
369255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
370066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
370080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
370081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
370082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
370082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
372557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
373367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
373371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
373373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
373373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.2ns 
373374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
375833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
376643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
376646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
376647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
376648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
376648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
379126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
379937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
379942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
379943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
379943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
379944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
382404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
383206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
383219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.81ms 
383221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
383221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
383222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
385685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
386469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
386474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 451.31ns 
386476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
386476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
386477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
388925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
389703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
389729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.66ms 
389730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
389730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
389731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
392202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
392986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
392990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
392992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
392992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
392992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
395458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
396269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
396285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.71ms 
396291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
396291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.2ns 
396292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
398749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
399559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
399574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
399575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
399575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
399576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
402043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
402851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
402870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
402871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
402871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
402872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
405327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
406138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
406141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.61ns 
406142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
406142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
406143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
408603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
409413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
409418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
409421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
409421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
409422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
411890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
412702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
412706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
412707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
412707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
412708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
415182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
415993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
415996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.91ns 
415998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
415998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.2ns 
415999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
418456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
419265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
419267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.01ns 
419269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
419269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
419269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
421721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
422510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
422513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
422515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
422515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
422515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
425003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
425797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
425800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
425801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
425801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
425802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
428301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
429095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
429105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
429107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
429107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
429108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
431584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
432393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
432400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
432402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
432402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
432403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
434855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
435670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
435677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
435678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
435678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
435679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
438118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
438932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
438939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
438941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
438941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
438941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
441363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
442180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
442184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
442186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
442186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
442186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
444610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
445429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
445433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
445435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
445436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.7ns 
445436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
447862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
448672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
448674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 741.01ns 
448676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
448676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
448676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
451100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
451912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
451915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.11ns 
451916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
451916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
451917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
454342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
455156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
455158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.71ns 
455159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
455159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
455160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
457591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
458385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
458393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.37ms 
458395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
458395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
458395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
460843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
461631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
461634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
461635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
461636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
461636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
464081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
464869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
464874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
464875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
464876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.1ns 
464876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
467330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
468117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
468119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.51ns 
468121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
468121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
468121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
470564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
471351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
471354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.01ns 
471355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
471355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
471356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
473806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
474596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
474599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
474601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
474601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
474601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
477043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
477830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
477832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 710.21ns 
477833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
477833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
477834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
480286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
481078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
481080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 982.62ns 
481082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
481082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
481082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
483529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
484317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
484320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 923.51ns 
484321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
484321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
484322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
486766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
487555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
487559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
487561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
487561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
487561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
490000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
490789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
490792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.91ns 
490793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
490793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
490794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
493232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
494020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
494029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
494030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
494030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
494031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
496477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
497263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
497265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 579.41ns 
497267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
497267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
497267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
499711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
500499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
500505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
500506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
500506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
500507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
502950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
503738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
503740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 821.71ns 
503742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
503742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
503743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
506181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
506969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
506972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.61ns 
506973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
506973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
506974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
509411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
510204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
510208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
510209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
510209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
510210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
512659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
513470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
513473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
513476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
513476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.7ns 
513477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
515895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
516708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
516711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
516712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
516712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
516713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
519133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
519945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
519948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
519949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
519949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
519950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
522366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
523176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
523180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
523181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
523181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
523182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
525598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
526410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
526417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
526419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
526419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
526420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
528836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
529652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
529660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.18ms 
529661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
529662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
529662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
532075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
532889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
532895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
532897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
532897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
532897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
535339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
536126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
536132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
536134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
536134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
536134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
538570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
539358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
539368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
539369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
539369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
539370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
541806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
542616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
542626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
542627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
542627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
542628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
545044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
545857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
545867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.14ms 
545868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
545868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
545869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
548284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
549097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
549109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
549111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
549111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.4ns 
549112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
551528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
552340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
552360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.25ms 
552362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
552362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
552363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
554809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
555598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
555619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.54ms 
555620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
555620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
555621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
558060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
558848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
558867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
558868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
558868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
558869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
561301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
562114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
562132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
562133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
562133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
562134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
564571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
565384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
565402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.19ms 
565404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
565404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
565405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
567818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
568632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
568677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.6ms 
568679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
568679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
568680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
571122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
571911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
571918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
571921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
571921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238ns 
571922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
574368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
575183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
575188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
575190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
575190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225ns 
575191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
577609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
578425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
578429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
578430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
578430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
578431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
580843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
581656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
581669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
581670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
581670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
581671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
584109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
584899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
584906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
584907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
584907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
584908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
587347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
588161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
588164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
588165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
588165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
588166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
590582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
591394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
591405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
591406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
591406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
591407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
593821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
594643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
594654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
594655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
594655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
594656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
597093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
597905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
597918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
597920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
597920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
597920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
600334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
601146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
601149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
601151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
601151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
601151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
603563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
604377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
604381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
604382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
604382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
604383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
606818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
607632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
607638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
607639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
607640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
607640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
610063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
610882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
610887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
610888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
610889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
610889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
613303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
614118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
614158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.3ms 
614160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
614160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
614161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
616609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
617424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
617441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.98ms 
617443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
617443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
617443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
619858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
620672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
620683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
620684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
620684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
620685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
623138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
623928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
623930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 266.6ns 
623931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
623931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
623932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
626411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
627234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
627312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.9ms 
627314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
627314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
627315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
629735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
630549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
630585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.39ms 
630587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
630588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.4ns 
630588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
633025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
633836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
633838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 284.5ns 
633840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
633841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.3ns 
633842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
636265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
637079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
637080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 218.9ns 
637082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
637082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
637082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
639515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
640326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
640328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 226.5ns 
640330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
640330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
640330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
642747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
643560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
643562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337ns 
643563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
643563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
643564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
645991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
646781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
646866     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
646876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.28ms 
646879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
646879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.5ns 
646880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
649328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
650141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
650189     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
650190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.13ms 
650191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
650191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
650192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
652642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
653433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
653435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
653464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
653516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
653534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
653540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
653557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
653559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
653560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
653562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
653568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
653572     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' 
653574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
653577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
653807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
653808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
653811     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' 
653811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
653813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
653952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
653953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
653957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
653958     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' 
653959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
653961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
654155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
654158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
654159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
654160     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' 
654161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
654163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
654273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
654276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
654277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
654278     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' 
654278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
654280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
654287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
654288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
654290     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' 
654291     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' 
654293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
654294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
654302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
654302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
654304     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' 
654304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
654305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
654306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
654420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
654422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
654423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
654546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
654547     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)'' 
654548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
654550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
654551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
654552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
654552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
654553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
654556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
654557     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' 
654558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
654559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
654560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
654681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
654684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
654685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
654686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
654687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
654688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
654689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
654815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
654816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
654817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
654819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
654820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
654820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
654821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
654822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
654914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
654916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
655002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
655007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
655011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
655012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
655014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
655015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
655016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
655016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
655017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
655018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
655026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
655030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
655122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
655123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
655124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
655125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
655126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
655127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
655127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
655128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
655174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
655180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
655270     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]'' 
655271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
655272     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'' 
655273     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'' 
655274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
655275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
655401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
655405     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'' 
655406     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)'' 
655408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
655409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
655410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
655411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
655411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
655420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
655421     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'' 
655422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
655423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
655520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
655521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
655522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
655523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
655523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
655524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
655636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
655639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
655640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
655641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
655642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
655642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
655643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
655644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
655729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
655730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
655813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
655814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
655815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
655819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
655823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
655827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
655952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
655954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
655955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
655956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
655966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
656062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
659528     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'' 
659529     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)'' 
659533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
659534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
659535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
659535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
659536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
659543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
659545     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'' 
659546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
659547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
659548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
659636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
659640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
659641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
659642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
659642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
659643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
659644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
659734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
659735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
659736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
659737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
659738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
659738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
659739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
659740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
659812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
659814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
659883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
659888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
659892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
659893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
659894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
659895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
659905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
659981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
659982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
659983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
659984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
660053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
660063     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'' 
660064     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)'' 
660065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
660066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
660067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
660067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
660068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
660078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
660079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
660080     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'' 
660081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
660081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
660165     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))'' 
660166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
660167     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'' 
660168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
660169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
660255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
660260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
660261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
660261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
660262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
660263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
660263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
660358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
660359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
660360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
660361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
660365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
660365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
660366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
660367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
660367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
660368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
660369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
660370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
660370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
660371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
660372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
660454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
660456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
660462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
660535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
660612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
660613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
660614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
660615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
660616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
660616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
660617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
660617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
660618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
660699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
660706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
660791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
660792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
660793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
660794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
660794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
660795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
660795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
660796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
660801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
660802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
660878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
660883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
660889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
660984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
660985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
660986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
660987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
660987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
660988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
660988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
660989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
661041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
661042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
661042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
661043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
661043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
661049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
661054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
661166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
661251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
661259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
661260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
661261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
661465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
661550     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'' 
661550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
664369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
664373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
664374     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'' 
664374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
664375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
664483     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))'' 
664483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
664484     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'' 
664485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
664486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
664585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
667357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
670325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
670329     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'' 
670330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
670331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
670331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
670438     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))'' 
670439     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'' 
670440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
670441     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)' ...' 
670441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
671509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
671509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
671510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
674036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
674828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
674830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
674830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
674839     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)'' 
674848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
674850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
674852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
674854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
674858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
674859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
674863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
674864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
674866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
674945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
674946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
674947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
674995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
674996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
674996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
674997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
674997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
675062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
675063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
675063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
675064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
675065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
675069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
675069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
675070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
675070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
675071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
675072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
675145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
675145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
675146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
675146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
675147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
675148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
675224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
675225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
675226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
675226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
675227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
675228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
675228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
675229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
675229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
675230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
675230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
675231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
675231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
675232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
675232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
675233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
675233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
675234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
675234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
675237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
675270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
675271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
675322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
675324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
675324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
675326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
675327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
675327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
675367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
675370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
675371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
675371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
675373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
675374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
675374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
675412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
675415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
675418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
675465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
675515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
675515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
675516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
677962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
678791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
678810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms