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

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

tests
0

failures
0

ignored
11m17.70s

duration
100%

successful

Tests

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

Standard output

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

1690       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1691       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1697       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1697       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2996       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8488       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.71s 
8548       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8584       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.4ns 
8599       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8601       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.6ms 
8605       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
11401      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12414      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12443      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
12455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.5ns 
12457      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
15265      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16223      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ms 
16228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16228      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.71ns 
16232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18906      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
18907      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19795      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
19799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.51ns 
19801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22368      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
22369      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
23247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23247      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.21ns 
23249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
25779      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26653      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.56ms 
26657      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26658      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.91ns 
26660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
29181      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30074      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30104      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.37ms 
30115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.6ns 
30117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
32642      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33471      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.02ns 
33473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33474      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.01ns 
33475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36003      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
36004      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36835      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.82ns 
36838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.71ns 
36839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
39362      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40185      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.01ns 
40191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40191      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.31ns 
40193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42707      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
42707      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43502      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.82ns 
43505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.01ns 
43506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46004      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
46005      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46798      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.31ns 
46800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.11ns 
46802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49293      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
49294      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50130      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.33ms 
50134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50135      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.68ms 
50137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
52663      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53456      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53492      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.11ms 
53495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53495      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.71ns 
53497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56012      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
56012      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57010      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 200.09ms 
57013      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.91ns 
57015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
59488      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60312      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
60313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60314      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
60315      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
62784      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63596      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
63599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.61ns 
63601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
66065      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66915      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.55ms 
66918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66919      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.01ns 
66920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
69400      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70227      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.81ms 
70229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70229      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.61ns 
70230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72702      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
72703      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73533      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
73536      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73536      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.91ns 
73537      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76017      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
76017      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.12ms 
76844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76844      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.5ns 
76845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
79340      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
80191      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.94ms 
80197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
80199      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.83ms 
80201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82673      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
82674      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
83506      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.44ms 
83507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
83507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.1ns 
83508      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
85987      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86804      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
86806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
86807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
89257      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
90098      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.28ms 
90099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
90100      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
90101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92564      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
92565      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
93423      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.44ms 
93426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
93426      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.41ns 
93427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95903      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
95903      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
96684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
96724      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.04ms 
96726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
96726      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns 
96727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99199      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
99200      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
99988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
99989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
102463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
103261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.57ms 
103263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
103263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
103264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
105735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
106519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
106530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
106539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
106539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns 
106540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
109017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
109823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
109831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.49ms 
109832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
109832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
109833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
112291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
113112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
113120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.61ms 
113122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
113122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns 
113122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
115605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
116415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
116416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
116417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
116417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
118869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
119683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
119687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
119691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
119691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.21ns 
119692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
122160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
122963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
122976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
122977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
122977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
122978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
125441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
126241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
126293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.55ms 
126296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
126297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.41ns 
126298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
128754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
129561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
129578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 
129580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
129580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
129581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
132022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
132834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
132852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
132854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
132855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.81ns 
132856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
135300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
136109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
136127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms 
136129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
136129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
136130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
138583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
139410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
139411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
139411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 
139412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
141872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
142676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
142714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.14ms 
142721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
142722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.61ns 
142723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
145186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
145987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
145990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 989.23ns 
145991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
145992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.6ns 
145992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
148474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
149255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
149259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
149260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
149261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
149261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
151726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
152510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
152511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
152511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
152512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
154975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
155754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
155762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.85ms 
155763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
155763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
155764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
158229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
159014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
159033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ms 
159035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
159036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.11ns 
159037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
161570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
162352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
162360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
162361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
162361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.8ns 
162362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
164862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
165791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
165794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
165797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
165797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.21ns 
165798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
168310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
169129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
169133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
169134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
169135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
169135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
171631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
172449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
172453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
172454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
172454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
172455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
174939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
175754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
175824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.96ms 
175832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
175832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.71ns 
175834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
178328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
179147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
179225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.24ms 
179227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
179227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
179228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
181667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
182471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
182474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
182476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
182477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.91ns 
182478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
184909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
185711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
185757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.4ms 
185763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
185771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.87ms 
185775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
188223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
189023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
189052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.12ms 
189054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
189054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
189055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
191495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
192299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
192302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
192303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
192303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
192304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
194739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
195541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
195686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 133.72ms 
195688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
195688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
195689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
198158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
198934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
198945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ms 
198948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
198949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.71ns 
198949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
201412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
202189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
202197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.44ms 
202199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
202199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
202199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
204677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
205457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
205474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
205476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
205476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
205477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
207962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
208744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
208757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
208761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
208761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.01ns 
208762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
211225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
212008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
212012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
212014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
212014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.8ns 
212015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
214474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
215273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
215278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
215279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
215280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
215280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
217756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
218556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
218578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ms 
218580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
218580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
218581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
221029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
221838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
221858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.69ms 
221861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
221861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
221862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
224334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
225130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
225145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
225147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
225147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns 
225148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
227588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
228388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
228391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
228392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
228393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
228393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
230835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
231635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
231639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
231641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
231641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
231642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
234087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
234887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
234893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
234894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
234895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
234895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
237328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
238128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
238132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
238134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
238134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.61ns 
238135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
240570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
241372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
241375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.72ns 
241376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
241376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.5ns 
241377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
243811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
244606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
244610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
244611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
244611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 624.01ns 
244612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
247043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
247841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
247844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
247845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
247845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
247846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
250293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
251089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
251157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.29ms 
251159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
251159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.31ns 
251160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
253631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
254406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
254448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.65ms 
254450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
254450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.41ns 
254451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
256919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
257697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
257729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.21ms 
257731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
257731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.61ns 
257732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
260217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
260997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
261041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.87ms 
261042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
261042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
261043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
263507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
264285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
264317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.44ms 
264319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
264319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
264319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
266778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
267573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
267627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.86ms 
267628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
267628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
267629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
270061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
270860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
270906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.27ms 
270907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
270907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
270908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
273353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
274151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
274172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms 
274174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
274174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
274174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
276668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
277483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
277513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.88ms 
277516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
277516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.1ns 
277517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
279962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
280766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
280787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
280789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
280789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.8ns 
280790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
283236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
284041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
284071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.22ms 
284072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
284072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
284073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
286525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
287326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
287353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.67ms 
287355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
287358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.41ns 
287363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
289801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
290604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
290631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.74ms 
290632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
290633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
290633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
293080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
293886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
293912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.88ms 
293913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
293913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
293914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
296360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
297158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
297180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.82ms 
297181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
297181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
297182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
299650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
300431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
300457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.64ms 
300459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
300459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
302927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
303702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
303727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.63ms 
303728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
303729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
306215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
306993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
307001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
307002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
307002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
307003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
309445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
310218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
310236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
310238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
310238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
310238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
312715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
313490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
313494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
313495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
313495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
313495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
315999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
316806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
316809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.72ns 
316810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
316810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
316811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
319295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
320099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
320102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.02ns 
320103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
320103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
320104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
322589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
323396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
323404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
323405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
323405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
323406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
325896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
326713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
326720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
326722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
326722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
326723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
329215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
330030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
330044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.54ms 
330046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
330046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
330046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
332541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
333350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
333353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
333355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
333355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
333355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
335890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
336751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
336754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.51ns 
336756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
336756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.91ns 
336757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
339245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
340050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
340056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
340057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
340057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
340058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
342511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
343326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
343328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.22ns 
343329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
343329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
343330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
345811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
346639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
346641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619.72ns 
346643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
346643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
346643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
349130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
349940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
349942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.12ns 
349944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
349944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
349944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
352427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
353266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
353271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
353273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
353273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.51ns 
353274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
355786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
356579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
356588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
356589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
356589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
356590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
359142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
359929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
359933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
359935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
359935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
359935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
362488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
363280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
363287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 
363288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
363288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
363289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
365763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
366554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
366559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
366560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
366560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
366561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
369080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
369877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
369894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.66ms 
369895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
369895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
369896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
372405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
373226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
373229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
373230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
373231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
373231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
375739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
376558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
376561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
376562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
376562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
376563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
379058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
379874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
379878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
379880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
379880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
379881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
382381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
383199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
383217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.81ms 
383219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
383219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.31ns 
383220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
385746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
386563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
386568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.31ns 
386570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
386570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
386571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
389060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
389866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
389905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ms 
389907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
389907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.5ns 
389908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
392374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
393190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
393194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
393195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
393196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.5ns 
393196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
395691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
396517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
396541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.21ms 
396544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
396544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.71ns 
396545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
399001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
399810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
399830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.54ms 
399831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
399832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
399832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
402314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
403133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
403159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
403161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
403161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
403161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
405647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
406465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
406467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 731.42ns 
406468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
406468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
406469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
408952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
409770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
409776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
409777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
409777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
409778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
412288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
413084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
413087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
413089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
413089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
413090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
415592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
416381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
416384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.02ns 
416385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
416385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
416386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
418900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
419697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
419699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.52ns 
419701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
419701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
419702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
422253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
423056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
423059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
423061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
423061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
423062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
425597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
426408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
426411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
426413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
426413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
426413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
428888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
429712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
429722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
429723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
429724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
429727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
432239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
433055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
433068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.23ms 
433070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
433070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
433070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
435565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
436375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
436387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
436389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
436389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.71ns 
436390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
438875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
439700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
439715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms 
439717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
439717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
439718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
442205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
443029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
443034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
443036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
443036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.41ns 
443037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
445556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
446344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
446362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.54ms 
446363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
446363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
446364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
448843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
449639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
449641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 812.12ns 
449643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
449643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
449643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
452140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
452961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
452964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
452965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
452965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
452966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
455449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
456271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
456273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.02ns 
456274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
456275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
456275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
458749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
459561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
459572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
459573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
459573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
459574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
462041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
462863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
462867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
462868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
462868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
462869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
465366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
466168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
466175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
466176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
466176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
466177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
468655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
469466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
469468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.82ns 
469469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
469469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
469470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
471954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
472777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
472779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.62ns 
472780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
472780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
472781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
475259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
476081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
476085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
476087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
476087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
476087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
478571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
479384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
479387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
479388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
479388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
479389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
481898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
482702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
482705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
482706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
482706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
482707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
485214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
486038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
486041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
486042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
486042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
486043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
488509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
489320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
489326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
489327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
489327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
489328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
491811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
492634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
492638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
492639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
492639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
492640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
495151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
495976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
495987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
495988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
495988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
495989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
498452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
499265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
499267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.82ns 
499268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
499268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
499269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
501716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
502532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
502539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.08ms 
502540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
502540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
502541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
505039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
505840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
505842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 977.12ns 
505843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
505843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
505844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
508458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
509280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
509282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 821.82ns 
509283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
509283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
509284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
511729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
512550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
512554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
512556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
512556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
512557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
515145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
515943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
515946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
515947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
515948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
515948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
518439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
519258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
519261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
519263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
519263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
519263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
521697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
522517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
522521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
522522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
522522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
522523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
525025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
525824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
525829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
525831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
525831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
525831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
528336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
529156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
529171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
529172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
529172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
529173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
531618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
532442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
532457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
532459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
532459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
532460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
534979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
535801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
535811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.48ms 
535813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
535813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
535814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
538291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
539124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
539135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
539136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
539136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.92ns 
539137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
541616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
542443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
542469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.25ms 
542471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
542472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.31ns 
542472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
544951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
545774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
545799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.74ms 
545801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
545801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
545801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
548293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
549092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
549116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.12ms 
549117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
549117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
549118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
551580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
552402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
552416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
552418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
552418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
552418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
554907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
555707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
555737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.92ms 
555738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
555738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
555739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
558256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
559080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
559130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.68ms 
559132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
559132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
559133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
561586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
562375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
562411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.98ms 
562413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
562413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
562414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
564912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
565732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
565773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.48ms 
565774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
565774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
565775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
568297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
569108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
569152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.34ms 
569154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
569154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
569155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
571664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
572484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
572597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.89ms 
572599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
572599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
572599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
575107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
575931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
575939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
575940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
575940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
575941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
578431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
579251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
579259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
579260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
579260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
579261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
581736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
582552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
582557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
582558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
582558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
582559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
585043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
585867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
585885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.92ms 
585887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
585887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
585887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
588391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
589216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
589227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
589230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
589230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
589230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
591713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
592503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
592506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
592508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
592508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 
592509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
595005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
595826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
595842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms 
595844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
595844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
595845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
598334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
599164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
599185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.74ms 
599186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
599186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
599187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
601667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
602484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
602503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.12ms 
602505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
602505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.61ns 
602506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
605012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
605838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
605841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
605843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
605843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
605843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
608343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
609167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
609170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
609172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
609172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
609172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
611638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
612451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
612458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
612459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
612459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
612460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
614956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
615781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
615787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
615789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
615789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
615790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
618319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
619147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
619218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.47ms 
619220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
619220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
619220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
621699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
622516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
622542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.96ms 
622543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
622543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
622544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
625037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
625864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
625886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.74ms 
625887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
625887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
625888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
628428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
629251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
629254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 370.71ns 
629255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
629255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
629256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
631743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
632537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
632765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 216.78ms 
632767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
632767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.6ns 
632768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
635212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
636050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
636099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.2ms 
636100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
636101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
636101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
638599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
639426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
639428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 391.31ns 
639429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
639429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
639430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
641935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
642761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
642763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 367.01ns 
642764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
642764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
642765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
645271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
646085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
646087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.91ns 
646088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
646088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
646089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
648589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
649395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
649397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.41ns 
649398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
649398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
649399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
651913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
652739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
652856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.29ms 
652859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
652859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.11ns 
652860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
655383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
656201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
656253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50ms 
656255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
656255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
656256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
658774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
659601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
659602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
659629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
659679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
659715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
659719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
659729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
659732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
659735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
659737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
659741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
659743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
659748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
659750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
660009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
660017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
660018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
660020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
660021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
660131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
660132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
660133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
660135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
660136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
660137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
660297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
660299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
660300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
660301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
660302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
660303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
660424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
660426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
660428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
660428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
660430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
660431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
660438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
660439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
660440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
660443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
660444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
660445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
660451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
660452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
660453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
660454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
660455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
660456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
660594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
660596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
660597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
660723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
660726     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)'' 
660728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
660730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
660731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
660732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
660733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
660734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
660738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
660740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
660742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
660743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
660744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
660858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
660862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
660864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
660865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
660866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
660867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
660868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
660997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
660999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
661000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
661002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
661003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
661004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
661004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
661006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
661101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
661103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
661219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
661224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
661229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
661231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
661232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
661233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
661234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
661235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
661235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
661237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
661245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
661250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
661351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
661352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
661353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
661355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
661355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
661356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
661356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
661357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
661409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
661414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
661508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
661510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
661512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
661514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
661515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
661516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
661665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
661670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
661671     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)'' 
661673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
661675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
661676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
661676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
661677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
661687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
661690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
661691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
661692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
661853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
661855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
661856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
661856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
661857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
661858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
661976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
661977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
661978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
661980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
661981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
661981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
661982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
661983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
662082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
662084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
662172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
662173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
662174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
662178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
662182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
662188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
662306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
662308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
662309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
662310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
662320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
662403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
665966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
665967     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)'' 
665973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
665974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
665975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
665975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
665976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
665984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
665985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
665986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
665987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
665988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
666077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
666080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
666081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
666082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
666083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
666083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
666084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
666174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
666176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
666176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
666179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
666180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
666180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
666181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
666182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
666255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
666256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
666368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
666372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
666376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
666377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
666378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
666381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
666392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
666476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
666477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
666478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
666481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
666554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
666563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
666564     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)'' 
666566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
666567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
666568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
666569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
666569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
666580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
666581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
666582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
666583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
666584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
666667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
666669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
666670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
666670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
666671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
666758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
666762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
666763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
666763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
666764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
666764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
666765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
666859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
666860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
666860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
666862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
666862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
666863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
666863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
666864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
666865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
666865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
666866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
666867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
666867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
666867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
666868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
666952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
666953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
666958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
667033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
667110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
667112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
667113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
667113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
667114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
667114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
667115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
667115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
667116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
667198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
667204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
667292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
667293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
667294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
667295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
667296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
667296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
667296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
667297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
667302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
667303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
667389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
667394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
667400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
667497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
667498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
667499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
667500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
667500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
667501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
667501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
667502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
667556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
667557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
667558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
667558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
667559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
667565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
667570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
667685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
667771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
667772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
667773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
667774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
667938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
668024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
668025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
671106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
671112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
671113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
671113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
671114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
671226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
671227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
671228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
671229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
671230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
671334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
674315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
677391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
677395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
677396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
677397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
677398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
677562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
677563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
677564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
677565     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)' ...' 
677566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
678669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
678669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
678670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
681264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
682119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
682120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
682121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
682130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
682142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
682144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
682146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
682146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
682151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
682153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
682156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
682159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
682159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
682169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
682171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
682171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
682223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
682224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
682224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
682225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
682225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
682299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
682300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
682301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
682302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
682303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
682307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
682307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
682308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
682309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
682310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
682310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
682406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
682407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
682407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
682409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
682410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
682410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
682508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
682509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
682509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
682510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
682511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
682512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
682513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
682513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
682514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
682515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
682515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
682516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
682516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
682517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
682517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
682518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
682519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
682520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
682521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
682523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
682563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
682564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
682628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
682629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
682631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
682632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
682633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
682633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
682690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
682693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
682694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
682696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
682697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
682698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
682698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
682815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
682818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
682821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
682894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
682970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
682970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.31ns 
682971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
685451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
686297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
686328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.59ms