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

198

tests

0

failures

0

ignored

11m7.38s

duration

100%

successful

Tests

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

Standard output

387        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
411        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.38ms 
642        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659        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)

1576       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1578       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1582       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1583       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2991       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8393       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.75s 
8449       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8477       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.5ns 
8488       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8488       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 
8492       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
11335      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12308      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.74ms 
12325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420ns 
12327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15048      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
15048      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15895      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.41ms 
15897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.1ns 
15898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
18549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19446      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
19452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.1ns 
19454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21997      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
21998      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
22881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns 
22882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
25398      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26271      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.21ms 
26350      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 
26352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28878      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
28878      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29738      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
29740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29740      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
29741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32241      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
32241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.8ns 
33087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33088      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
33088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35584      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
35585      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36399      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 523ns 
36400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
36401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
38895      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39711      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551ns 
39712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
39713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
42182      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42993      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 513.3ns 
42994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42994      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
42995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
45449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46258      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.11ns 
46260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46260      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
46261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48718      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
48718      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49543      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.21ms 
49545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.5ns 
49546      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
52045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52881      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.64ms 
52883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52883      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns 
52884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
55339      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56311      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 150.57ms 
56316      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56316      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.7ns 
56317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58760      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
58761      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
59569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59569      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298ns 
59570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
62034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62863      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
62865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62865      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
62866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65321      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
65323      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.4ms 
66183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66183      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.4ns 
66184      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
68664      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.74ms 
69481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69482      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.8ns 
69483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71923      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
71923      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72749      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
72751      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 774.6ns 
72756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
75233      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76057      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.74ms 
76058      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 
76059      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
78511      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79327      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
79329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
79330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
81795      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82605      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.52ms 
82606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
82607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85051      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
85052      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85854      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
85856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.6ns 
85858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
88310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89148      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.73ms 
89150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns 
89151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
91595      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92443      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.54ms 
92445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92445      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns 
92446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
94890      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95729      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.59ms 
95732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95732      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.2ns 
95733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
98197      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98985      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
98987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.3ns 
98988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
101452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.35ms 
102264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.5ns 
102265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
104703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.57ms 
105513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.9ns 
105514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
107954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
108757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.6ns 
108758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
111202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 
112005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 
112007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
114451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
115237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 
115238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
117724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
118524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.8ns 
118525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
120959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.71ms 
121768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
121769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
124198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.82ms 
125053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.8ns 
125055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
127567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
128379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.4ns 
128380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
130809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.15ms 
131624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
131625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
134056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
134908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
134909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
137398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.48ms 
138212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
138213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
140639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.4ms 
141476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 
141477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
143911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
144707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
144708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
144709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
147133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
147931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
147932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
150361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
151155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
151162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
151163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
151163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
151164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
153608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
154380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
154388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms 
154390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
154390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
154390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
156827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
157645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.02ms 
157650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
157650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 
157651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
160104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
160907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
160908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
160909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
163345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
164154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
164157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
164160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
164160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns 
164162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
166601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
167392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
167396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
167397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
167397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
167398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
169825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
170599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
170603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
170604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
170604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
170605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
173046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
173839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
173907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.9ms 
173908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
173908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
173909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
176356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
177234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.95ms 
177236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
177236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.5ns 
177237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
179655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
180447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
180450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
180451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
180451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
180452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
182885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
183676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
183712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.17ms 
183715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
183721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.78ms 
183721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
186158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
186933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
186960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.89ms 
186961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
186961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
186962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
189389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
190181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
190183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984.61ns 
190184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
190184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
190185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
192601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
193389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
193522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 122.05ms 
193525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
193525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.2ns 
193526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
195955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
196760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
196770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.17ms 
196772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
196772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.4ns 
196773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
199217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
200010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
200018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms 
200019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
200019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
200020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
202548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
203392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
203424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.59ms 
203427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
203427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.7ns 
203428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
205972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
206774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
206795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.82ms 
206797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
206798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.2ns 
206799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
209225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
210010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
210014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
210015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
210015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
210016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
212421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
213209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
213214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
213215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
213215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
213216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
215632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
216425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
216446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.13ms 
216450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
216450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.1ns 
216451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
218896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
219670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
219685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.88ms 
219687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
219687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
219687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
222118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
222941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
222956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
222957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
222957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
222958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
225412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
226201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
226204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
226206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
226206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
226206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
228615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
229402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
229406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
229407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
229407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198ns 
229408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
231839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
232628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
232633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
232634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
232634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
232634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
235061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
235838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
235841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
235842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
235842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
235842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
238259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
239046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
239048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.5ns 
239049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
239049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
239049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
241469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
242259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
242262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
242263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
242263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
242264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
244683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
245473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
245476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
245477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
245477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
245477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
247905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
248694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
248742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.74ms 
248744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
248744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.9ns 
248745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
251194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
251965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
251996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.26ms 
252009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
252009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.5ns 
252010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
254441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
255235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
255263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.19ms 
255264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
255264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
255265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
257727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
258557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.22ms 
258558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
258558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
258559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
260975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
261764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
261792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.73ms 
261793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
261793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
261794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
264233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
265022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
265069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.96ms 
265070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
265070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
265071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
267501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
268272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
268296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.48ms 
268297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
268297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
268298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
270723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
271515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
271534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms 
271535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
271535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
271536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
273961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
274749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
274773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
274774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
274774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
274775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
277186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
277979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
277998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
277999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
277999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
278000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
280441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
281233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
281262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.08ms 
281264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
281264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
281264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
283702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
284475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
284500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
284501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
284501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
284502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
286936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
287727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
287752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
287753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
287753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
287754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
290181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
290974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
290998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.16ms 
290999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
290999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
291000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
293423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
294215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
294234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.04ms 
294235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
294236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
294236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
296670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
297461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
297485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms 
297486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
297486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
297487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
299914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
300684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
300709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.48ms 
300710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
300710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
300711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
303144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
303937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
303946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
303948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
303948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.2ns 
303949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
306385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
307175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
307192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.19ms 
307193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
307193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
307194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
309609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
310400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
310404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
310405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
310405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
310405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
312823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
313611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
313613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.4ns 
313614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
313614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
313615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
316050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
316833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
316835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.1ns 
316836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
316836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
316837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
319264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
320055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
320063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
320065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
320065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
320066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
322488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
323279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
323284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
323285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
323286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
323286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
325697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
326485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
326496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.08ms 
326497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
326497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
326498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
328930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
329727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
329730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
329731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
329731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
329732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
332161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
332931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
332933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.2ns 
332934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
332934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
332935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
335348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
336135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
336140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
336141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
336141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
336142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
338562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
339353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
339355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.1ns 
339356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
339356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
339357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
341845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
342618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
342620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.9ns 
342621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
342621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
342622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
345048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
345839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
345840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.3ns 
345841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
345841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
345842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
348265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
349053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
349056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
349057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
349057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
349058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
351477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
352269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
352277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
352279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
352279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
352279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
354697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
355486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
355489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
355490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
355491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
355491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
357908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
358696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
358703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
358704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
358704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
358704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
361120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
361909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
361913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
361914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
361914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
361914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
364354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
365145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
365161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
365162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
365162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
365163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
367579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
368369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
368372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
368373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
368373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
368374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
370790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
371582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
371585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
371587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
371587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.1ns 
371587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
374006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
374796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
374800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
374801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
374801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
374802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
377230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
378022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
378037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms 
378039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
378039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
378040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
380525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
381361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
381365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.2ns 
381367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
381367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.9ns 
381368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
383787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
384559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
384594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.08ms 
384596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
384597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns 
384597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
387018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
387808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
387811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
387813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
387813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
387814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
390240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
391031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
391052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ms 
391054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
391054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.8ns 
391055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
393480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
394300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
394321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.88ms 
394323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
394323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
394324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
396773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
397568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
397590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.09ms 
397591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
397591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
397592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
400017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
400810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
400812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.2ns 
400813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
400813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
400814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
403243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
404034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
404040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
404041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
404041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
404041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
406460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
407252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
407255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
407257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
407257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.5ns 
407258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
409683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
410478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
410481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.6ns 
410482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
410482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns 
410482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
412905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
413699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
413701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.6ns 
413702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
413702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
413703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
416128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
416922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
416924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
416925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
416925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
416926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
419342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
420135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
420137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
420138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
420138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
420139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
422556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
423350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
423359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
423361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
423361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
423361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
425794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
426591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
426602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
426604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
426604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
426604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
429028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
429821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
429831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
429832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
429832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
429832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
432249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
433046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
433057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
433058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
433058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
433059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
435480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
436284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
436288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
436289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
436289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
436290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
438716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
439521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
439528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
439530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
439530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
439531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
441950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
442756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
442758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.2ns 
442759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
442759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
442760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
445174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
445973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
445975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
445976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
445976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
445977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
448401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
449200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
449202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 849.21ns 
449203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
449203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
449204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
451629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
452427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
452437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
452438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
452438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
452439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
454877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
455681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
455686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
455687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
455688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.5ns 
455688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
458108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
458906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
458912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
458913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
458913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
458914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
461332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
462131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
462133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.5ns 
462134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
462134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
462135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
464550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
465345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
465347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.1ns 
465348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
465348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.1ns 
465349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
467765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
468563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
468566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
468568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
468568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.2ns 
468569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
471009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
471807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
471809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
471810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
471810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
471811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
474240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
475041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
475044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
475045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
475045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
475045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
477456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
478254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
478257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
478258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
478258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
478258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
480704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
481509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
481514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
481515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
481515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
481516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
483991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
484804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
484807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
484808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
484808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
484809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
487279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
488089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
488099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
488100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
488100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
488101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
490551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
491358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
491361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.8ns 
491362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
491362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
491362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
493839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
494648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
494655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
494657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
494657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
494658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
497125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
497936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
497938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.5ns 
497939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
497939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
497940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
500407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
501211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
501213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 745.3ns 
501214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
501215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
501215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
503690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
504497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
504501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
504502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
504502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
504503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
506961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
507772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
507775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
507777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
507777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns 
507778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
510258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
511064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
511067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
511068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
511068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
511069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
513532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
514337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
514340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
514341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
514342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
514342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
516782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
517607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
517611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
517613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
517613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
517613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
520066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
520872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
520886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms 
520887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
520887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
520888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
523337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
524160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
524175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms 
524177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
524177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
524177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
526614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
527415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
527425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
527426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
527426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
527426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
529880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
530681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
530691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
530693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
530693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
530693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
533141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
533944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
533969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms 
533970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
533970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
533971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
536440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
537247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
537272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms 
537273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
537273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
537273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
539711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
540513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
540536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.77ms 
540537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
540537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
540538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
542992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
543798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
543812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.93ms 
543813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
543813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
543814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
546275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
547081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
547110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.22ms 
547111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
547111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
547112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
549567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
550369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
550415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.55ms 
550417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
550417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
550418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
552889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
553697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
553734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.98ms 
553736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
553736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171ns 
553736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
556213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
557022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
557063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.77ms 
557065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
557065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
557065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
559533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
560363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
560405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.19ms 
560406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
560406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
560407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
562856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
563659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
563775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.45ms 
563777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
563777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
563777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
566231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
567033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
567040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
567041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
567041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
567042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
569506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
570311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
570319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
570320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
570321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265ns 
570321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
572785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
573584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
573589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
573591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
573591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
573591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
576030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
576853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
576869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
576870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
576870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
576871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
579301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
580101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
580112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
580113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
580113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
580114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
582578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
583380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
583383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
583384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
583384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
583385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
585842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
586650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
586666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
586668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
586668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
586668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
589118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
589918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
589934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
589935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
589935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
589935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
592375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
593180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
593200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.52ms 
593201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
593201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
593201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
595658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
596462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
596465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 970ns 
596466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
596466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
596467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
598928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
599731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
599734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
599736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
599736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
599736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
602184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
602984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
602990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
602991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
602991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
602992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
605514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
606315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
606323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
606324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
606324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
606325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
608754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
609563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
609637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.51ms 
609639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
609639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 
609640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
612105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
612908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
612937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.59ms 
612938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
612938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
612939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
615370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
616195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
616216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.45ms 
616217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
616218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
616218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
618676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
619481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
619483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 267.7ns 
619484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
619484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
619485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
621971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
622775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
622972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185.12ms 
622974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
622974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.1ns 
622975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
625452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
626258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
626307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.36ms 
626309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
626309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
626310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
628751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
629580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
629582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.7ns 
629583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
629583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
629584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
632042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
632848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
632849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 323.5ns 
632851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
632851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
632851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
635312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
636119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
636121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.8ns 
636122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
636122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
636123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
638580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
639384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
639386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 439.8ns 
639387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
639387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
639388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
641830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
642654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
642732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.22ms 
642736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
642736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.7ns 
642737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
645206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
646015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
646063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.38ms 
646065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
646065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
646066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
648541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
649351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
649353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
649382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
649419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
649436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
649440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
649445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
649448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
649449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
649451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
649454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
649456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
649458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
649459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
649687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
649689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
649690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
649691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
649692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
649831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
649832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
649833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
649834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
649836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
649837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
649985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
649986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
649987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
649988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
649989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
649990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
650103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
650105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
650106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
650106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
650107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
650108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
650115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
650115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
650116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
650118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
650119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
650120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
650127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
650128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
650129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
650130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
650131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
650131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
650264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
650265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
650266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
650425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
650426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
650429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
650430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
650431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
650432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
650432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
650433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
650436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
650438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
650439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
650440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
650441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
650549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
650553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
650554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
650555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
650556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
650556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
650557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
650682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
650684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
650685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
650686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
650687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
650687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
650688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
650689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
650781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
650782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
650902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
650906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
650912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
650913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
650914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
650915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
650915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
650916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
650916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
650917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
650926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
650940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
651035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
651037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
651037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
651038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
651039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
651039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
651040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
651041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
651101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
651106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
651213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
651215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
651217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
651218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
651219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
651219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
651337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
651341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
651342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
651343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
651344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
651346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
651346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
651347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
651356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
651357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
651358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
651359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
651472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
651473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
651474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
651475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
651475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
651476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
651578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
651579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
651580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
651581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
651582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
651582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
651583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
651584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
651664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
651665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
651735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
651735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
651736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
651740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
651744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
651748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
651859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
651860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
651861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
651862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
651872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
651957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
655359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
655360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
655366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
655367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
655368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
655368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
655369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
655376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
655378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
655379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
655380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
655381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
655470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
655473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
655476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
655476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
655477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
655478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
655478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
655569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
655570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
655571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
655572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
655573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
655573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
655574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
655575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
655648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
655650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
655755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
655759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
655764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
655765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
655765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
655766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
655775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
655851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
655853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
655853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
655854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
655924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
655933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
655934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
655936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
655937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
655937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
655938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
655939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
655949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
655951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
655952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
655952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
655953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
656037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
656039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
656040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
656041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
656042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
656129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
656133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
656134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
656134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
656134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
656135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
656136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
656230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
656231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
656232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
656233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
656233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
656233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
656234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
656235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
656235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
656236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
656237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
656237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
656238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
656238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
656239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
656324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
656325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
656330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
656405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
656482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
656483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
656484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
656485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
656485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
656486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
656486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
656486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
656487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
656570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
656576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
656663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
656664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
656665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
656666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
656666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
656666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
656667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
656667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
656672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
656673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
656766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
656771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
656776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
656873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
656874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
656875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
656876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
656876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
656877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
656877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
656878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
656931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
656932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
656933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
656934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
656935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
656940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
656945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
657058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
657178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
657180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
657181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
657182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
657343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
657428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
657429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
660447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
660452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
660454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
660455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
660455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
660564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
660565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
660567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
660567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
660568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
660670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
663732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
667050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
667056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
667057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
667058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
667059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
667202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
667203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
667212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
667222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
667224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
668465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
668465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
668466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
671137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
671929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
671931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
671931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
671937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
671948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
671950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
671952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
671953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
671956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
671958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
671960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
671963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
671964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
671971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
671973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
671974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
672014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
672015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
672016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
672016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
672017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
672079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
672080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
672081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
672082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
672082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
672086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
672086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
672087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
672088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
672089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
672089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
672169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
672170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
672170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
672171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
672172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
672173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
672261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
672262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
672262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
672263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
672263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
672264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
672265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
672265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
672266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
672266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
672267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
672267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
672268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
672268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
672269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
672269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
672270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
672271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
672271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
672274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
672313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
672314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
672367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
672368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
672369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
672371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
672371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
672372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
672419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
672422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
672423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
672424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
672425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
672426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
672427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
672477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
672479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
672482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
672537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
672589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
672589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.1ns 
672590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
675026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
675850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
675881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.01ms