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

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

tests
0

failures
0

ignored
12m34.34s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.648s passed
powPositiveConcrete data()[101] 3.651s passed
powGeq1Concrete data()[102] 3.672s passed
pow2InIntLower data()[103] 3.681s passed
pow2InIntUpper data()[104] 3.638s passed
logSelfConcrete data()[105] 3.621s passed
log1Concrete data()[106] 3.649s passed
logProduct data()[107] 3.671s passed
logTimesBaseConcrete data()[108] 3.642s passed
logProdIdentity data()[109] 3.618s passed
moduloByteIsInByte data()[10] 3.747s passed
logProdIdentityConcrete data()[110] 3.612s passed
logPowIdentity data()[111] 3.633s passed
logPowIdentityConcrete data()[112] 3.600s passed
logPositive data()[113] 3.631s passed
logPositiveConcrete data()[114] 3.633s passed
logMono data()[115] 3.645s passed
logMonoConcrete data()[116] 3.636s passed
powLogLess data()[117] 3.651s passed
powLogMore2 data()[118] 3.661s passed
logLessThanPow data()[119] 3.727s passed
moduloCharIsInChar data()[11] 3.748s passed
logLessThanPowConcrete data()[120] 3.711s passed
logSqueeze data()[121] 3.654s passed
ifthenelse_equals data()[122] 3.641s passed
ifthenelse_equals_1 data()[123] 3.672s passed
ifthenelse_equals_2 data()[124] 3.676s passed
disjointWithSingleton1 data()[125] 3.691s passed
disjointWithSingleton2 data()[126] 3.664s passed
disjointArrayRanges data()[127] 3.688s passed
disjointArrayRangeAllFields1 data()[128] 3.699s passed
disjointArrayRangeAllFields2 data()[129] 3.648s passed
div_unique1 data()[12] 3.751s passed
seqSelfDefinition data()[130] 3.668s passed
seqOutsideValue data()[131] 3.664s passed
castedGetAny data()[132] 3.633s passed
seqGetAlphaCast data()[133] 3.634s passed
getOfSeqSingleton data()[134] 3.668s passed
getOfSeqSingletonConcrete data()[135] 3.653s passed
getOfSeqConcat data()[136] 3.648s passed
getOfSeqSub data()[137] 3.684s passed
getOfSeqReverse data()[138] 3.657s passed
lenOfSeqEmpty data()[139] 3.702s passed
div_unique2 data()[13] 3.791s passed
lenOfSeqSingleton data()[140] 3.659s passed
lenOfSeqConcat data()[141] 3.643s passed
lenOfSeqSub data()[142] 3.628s passed
lenOfSeqReverse data()[143] 3.677s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.652s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.644s passed
getOfSeqSingletonEQ data()[146] 3.623s passed
getOfSeqConcatEQ data()[147] 3.668s passed
getOfSeqSubEQ data()[148] 3.627s passed
getOfSeqReverseEQ data()[149] 3.613s passed
div_exists data()[14] 3.957s passed
lenOfSeqEmptyEQ data()[150] 3.647s passed
lenOfSeqSingletonEQ data()[151] 3.634s passed
lenOfSeqConcatEQ data()[152] 3.617s passed
lenOfSeqSubEQ data()[153] 3.607s passed
lenOfSeqReverseEQ data()[154] 3.608s passed
getOfSeqDefEQ data()[155] 3.607s passed
lenOfSeqDefEQ data()[156] 3.682s passed
seqConcatWithSeqEmpty1 data()[157] 3.654s passed
seqConcatWithSeqEmpty2 data()[158] 3.678s passed
seqReverseOfSeqEmpty data()[159] 3.642s passed
div_one data()[15] 3.705s passed
subSeqComplete data()[160] 3.696s passed
subSeqTailR data()[161] 3.661s passed
subSeqTailL data()[162] 3.641s passed
subSeqTailEQR data()[163] 3.688s passed
subSeqTailEQL data()[164] 3.661s passed
seqDef_split data()[165] 3.678s passed
seqDef_induction_upper data()[166] 3.679s passed
seqDef_induction_upper_concrete data()[167] 3.731s passed
seqDef_induction_lower data()[168] 3.734s passed
seqDef_induction_lower_concrete data()[169] 3.697s passed
jdiv_one data()[16] 3.719s passed
seqDef_split_in_three data()[170] 3.769s passed
seqDef_empty data()[171] 3.643s passed
seqDef_one_summand data()[172] 3.667s passed
seqDef_lower_equals_upper data()[173] 3.641s passed
seqDefOfSeq data()[174] 3.625s passed
seqSelfDefinitionEQ2 data()[175] 3.593s passed
indexOfSeqSingleton data()[176] 3.670s passed
indexOfSeqConcatFirst data()[177] 3.654s passed
indexOfSeqConcatSecond data()[178] 3.650s passed
indexOfSeqSub data()[179] 3.662s passed
div_zero data()[17] 3.721s passed
lenOfArray2seq data()[180] 3.669s passed
getAnyOfArray2seq data()[181] 3.618s passed
getOfArray2seq data()[182] 3.676s passed
getAnyOfNPermInv data()[183] 3.661s passed
seqNPermRange data()[184] 3.703s passed
seqPermTrans data()[185] 3.681s passed
seqPermRefl data()[186] 3.677s passed
seqPermSplit data()[187] 3.667s passed
seqNPermRight data()[188] 3.909s passed
seqPermFromSwap data()[189] 3.760s passed
divResZero1 data()[18] 3.724s passed
seqPermTransAlt0 data()[190] 3.663s passed
seqPermTransAlt1 data()[191] 3.675s passed
seqPermTransAlt2 data()[192] 3.667s passed
seqPermTransAlt3 data()[193] 3.638s passed
seqPermForall data()[194] 3.790s passed
seqPermExists data()[195] 3.738s passed
schiffl_lemma_2 data()[196] 25.185s passed
schiffl_thm_1 data()[197] 4.494s passed
eqSameSeq data()[198] 3.816s passed
divResZero2 data()[19] 3.713s passed
eqTermCut data()[1] 4.457s passed
divResOne1 data()[20] 3.716s passed
divResOne2 data()[21] 3.711s passed
div_cancel1 data()[22] 3.711s passed
div_cancel2 data()[23] 3.672s passed
divAddMultDenom data()[24] 3.780s passed
divMinus data()[25] 3.765s passed
divMinusDenom data()[26] 3.763s passed
divLeastDPos data()[27] 3.737s passed
divLeastDNeg data()[28] 3.721s passed
divGreatestDPos data()[29] 3.699s passed
equivAllRight data()[2] 4.114s passed
divGreatestDNeg data()[30] 3.722s passed
divIncreasingPos data()[31] 3.701s passed
divIncreasingNeg data()[32] 3.708s passed
jdiv_zero data()[33] 3.682s passed
jdivPulloutMinusNum data()[34] 3.699s passed
jdivPulloutMinusDenom data()[35] 3.770s passed
jdiv_uniquePosPos data()[36] 3.700s passed
jdiv_uniquePosNeg data()[37] 3.712s passed
jdiv_uniqueNegPos data()[38] 3.852s passed
jdiv_uniqueNegNeg data()[39] 3.679s passed
irrflConcrete1 data()[3] 4.131s passed
jdivMultDenom1 data()[40] 3.795s passed
jdivMultDenom2 data()[41] 3.704s passed
mod_geZero data()[42] 3.679s passed
mod_lessDenom data()[43] 3.720s passed
jmod_NumPos data()[44] 3.693s passed
jmod_NumNeg data()[45] 3.716s passed
jmod_geZero data()[46] 3.663s passed
jmodNumZero data()[47] 3.695s passed
jmod_pulloutminusNum data()[48] 3.690s passed
jmod_pulloutminusDenom data()[49] 3.657s passed
irrflConcrete2 data()[4] 3.936s passed
jmodUnique1 data()[50] 3.750s passed
jmodUnique2 data()[51] 3.757s passed
intDivRem data()[52] 3.724s passed
jmodjmod data()[53] 3.731s passed
jmodDivisible data()[54] 3.704s passed
jmodDivisibleRep data()[55] 3.652s passed
jdivAddMultDenom data()[56] 3.868s passed
jmodAltZero data()[57] 3.683s passed
jmodAddMultDenomZero data()[58] 3.657s passed
polyDiv_zero data()[59] 3.671s passed
cancel_gtPos data()[5] 3.867s passed
polyMod_ltdivDenom data()[60] 3.654s passed
bsum_empty data()[61] 3.646s passed
bsum_induction_upper data()[62] 3.670s passed
bsum_induction_lower data()[63] 3.687s passed
bsum_num_of_bounds data()[64] 3.685s passed
bsum_num_of_bounds2 data()[65] 3.720s passed
bsum_induction_upper2 data()[66] 3.671s passed
bsum_induction_upper_concrete data()[67] 3.687s passed
bsum_induction_upper_concrete_2 data()[68] 3.669s passed
bsum_induction_upper2_concrete data()[69] 3.671s passed
cancel_gtNeg data()[6] 3.762s passed
bsum_induction_lower_concrete data()[70] 3.730s passed
bsum_induction_lower2 data()[71] 3.675s passed
bsum_induction_lower2_concrete data()[72] 3.690s passed
bsum_positive data()[73] 3.778s passed
bsum_upper_bound data()[74] 3.751s passed
bsum_lower_bound data()[75] 3.702s passed
bsum_positive_lower_bound_element data()[76] 3.744s passed
bsum_sub_same_index data()[77] 3.733s passed
bsum_less_same_index data()[78] 3.727s passed
bsum_equal_except_one_index data()[79] 3.715s passed
moduloIntIsInInt data()[7] 3.726s passed
bsum_num_of_is_max data()[80] 3.688s passed
bsum_num_of_is_max2 data()[81] 3.700s passed
bsum_num_of_is_max3 data()[82] 3.673s passed
bsum_num_of_is_max4 data()[83] 3.671s passed
bsum_num_of_lt_max data()[84] 3.679s passed
bsum_num_of_lt_max2 data()[85] 3.665s passed
bsum_num_of_lt_max3 data()[86] 3.678s passed
bsum_num_of_lt_max4 data()[87] 3.672s passed
bsum_num_of_gt0 data()[88] 3.666s passed
bsum_num_of_gt0_alt data()[89] 3.690s passed
moduloLongIsInLong data()[8] 3.703s passed
bsum_add_concrete data()[90] 3.704s passed
bprod_all_positive data()[91] 3.679s passed
bprod_split data()[92] 3.637s passed
powConcrete0 data()[93] 3.626s passed
powConcrete1 data()[94] 3.678s passed
powSplitFactor data()[95] 3.644s passed
powAdd data()[96] 3.666s passed
powMono data()[97] 3.662s passed
powMonoConcrete data()[98] 3.650s passed
powMonoConcreteRight data()[99] 3.655s passed
moduloShortIsInShort data()[9] 3.760s passed

Standard output

383        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
410        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.8ms 
671        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689        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)

1713       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1716       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1721       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1722       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3388       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9748       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.08s 
9849       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9892       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.9ns 
9908       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9911       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.23ms 
9916       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
13189      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14355      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.61ms 
14370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.94ns 
14372      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
17395      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
18485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.13ns 
18491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
21571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
22612      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.42ms 
22623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 987.98ns 
22626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
25537      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
26539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
26556      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ms 
26561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 894.56ns 
26564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29448      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
29448      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
30378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
30425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.92ms 
30429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
30429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.63ns 
30431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
33212      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
34153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
34188      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.17ms 
34189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
34190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.31ns 
34192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36981      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
36981      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
37911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
37914      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.56ns 
37917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
37917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.02ns 
37918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40673      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
40673      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
41613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
41617      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 701.64ns 
41619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
41620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 869.05ns 
41622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
44418      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
45373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
45376      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.43ns 
45379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
45380      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.72ns 
45381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
48172      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
49121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
49124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.95ns 
49126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
49127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.43ns 
49129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
51961      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
52864      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
52871      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
52876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
52876      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.93ns 
52877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
55684      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
56580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
56624      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.41ms 
56626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
56626      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.11ns 
56627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
59435      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
60334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
60415      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.58ms 
60417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
60417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.21ns 
60424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
63254      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
64139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
64371      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 187.12ms 
64376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
64376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.73ns 
64378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
67140      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
68073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
68078      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
68079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
68079      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.11ns 
68080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
70851      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
71794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
71797      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
71800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
71800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.53ns 
71802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
74546      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
75464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
75516      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.21ms 
75521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
75522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 479.53ns 
75523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
78309      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
79226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
79244      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
79247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
79247      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.73ns 
79248      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
82005      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
82938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
82957      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.08ms 
82959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
82960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.37ms 
82966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85736      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
85736      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
86655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
86673      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.15ms 
86675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
86675      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.51ns 
86676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89448      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
89449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
90367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
90384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
90386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
90386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.82ns 
90387      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
93153      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
94068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
94095      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.12ms 
94097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
94097      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.61ns 
94098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
96874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
97764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
97767      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
97769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
97769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.41ns 
97770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
100607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
101499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
101547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.81ms 
101549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
101549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.31ns 
101550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
104349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
105242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
105312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.14ms 
105314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
105315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.43ns 
105316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
108126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
109022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
109075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.05ms 
109077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
109077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.61ns 
109107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
111878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
112803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
112812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.72ms 
112815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
112815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.91ns 
112816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
115596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
116517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
116533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.46ms 
116534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
116534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.21ns 
116535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
119301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
120220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
120233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.13ms 
120234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
120234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.21ns 
120235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
123025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
123946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
123955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
123956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
123956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.91ns 
123957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
126723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
127647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
127656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
127657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
127657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.41ns 
127658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
130434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
131355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
131363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
131366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
131366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.21ns 
131368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
134130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
135041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
135045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
135047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
135047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.61ns 
135048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
137822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
138733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
138744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
138746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
138746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.01ns 
138747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
141485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
142411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
142514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.43ms 
142516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
142516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.91ns 
142517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
145291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
146188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
146214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.41ms 
146216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
146216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
146217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
149014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
149905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
149926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
149928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
149928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.91ns 
149929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
152794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
153756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
153778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.52ms 
153779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
153779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
153780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
156550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
157437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
157458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.45ms 
157459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
157459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.31ns 
157460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
160286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
161203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
161252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.23ms 
161254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
161254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.22ns 
161255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
164036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
164952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
164956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
164958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
164959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.31ns 
164960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
167716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
168630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
168635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
168637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
168637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.32ns 
168639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
171421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
172346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
172355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.86ms 
172357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
172357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.71ns 
172358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
175118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
176038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
176048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.62ms 
176050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
176050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.42ns 
176051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
178829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
179742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
179765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.33ms 
179766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
179766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.61ns 
179767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
182510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
183417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
183427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.63ms 
183429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
183429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.41ns 
183429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
186204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
187118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
187122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
187124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
187124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.31ns 
187125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
189883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
190807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
190812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
190813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
190813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.21ns 
190814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
193582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
194465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
194469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
194471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
194471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.81ns 
194472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
197240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
198126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
198219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.77ms 
198221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
198221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.82ns 
198223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
200995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
201881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
201976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.2ms 
201978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
201978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.81ns 
201979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
204746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
205696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
205700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
205702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
205703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.32ns 
205704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
208474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
209388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
209431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38ms 
209433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
209434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.72ns 
209435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
212180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
213092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
213135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.18ms 
213138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
213138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.61ns 
213139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
215882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
216784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
216788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
216789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
216789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
216790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
219571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
220486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
220654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 156.39ms 
220657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
220658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.02ns 
220659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
223409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
224326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
224338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.36ms 
224340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
224340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
224341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
227079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
227986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
227995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
227996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
227997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
227997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
230735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
231647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
231666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.06ms 
231667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
231667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.91ns 
231668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
234401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
235304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
235318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.72ms 
235322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
235322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
235323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
238073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
238962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
238966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
238967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
238967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
238968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
241739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
242628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
242635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
242639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
242639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.42ns 
242641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
245410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
246297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
246324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.17ms 
246326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
246326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.31ns 
246327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
249105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
249991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
250009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.83ms 
250011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
250011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
250012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
252795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
253711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
253729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
253731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
253731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
253732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
256484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
257395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
257400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
257403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
257404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.72ns 
257404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
260168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
261082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
261087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
261088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
261088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
261089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
263839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
264750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
264756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
264758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
264758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
264759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
267513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
268424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
268427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
268429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
268429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.61ns 
268430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
271235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
272154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
272157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.44ns 
272158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
272158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
272159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
274916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
275828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
275832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
275834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
275839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.7ms 
275840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
278595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
279519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
279522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
279524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
279525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.01ns 
279526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
282330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
283246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
283300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.11ms 
283302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
283303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.61ns 
283304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
286125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
287011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
287051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.16ms 
287052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
287052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.91ns 
287053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
289829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
290714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
290753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.12ms 
290755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
290755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
290756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
293562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
294449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
294497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.32ms 
294499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
294499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
294500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
297270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
298157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
298230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.17ms 
298232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
298232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
298233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
300982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
301898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
301957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.35ms 
301959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
301959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.31ns 
301960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
304709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
305631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
305671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.16ms 
305674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
305675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.21ns 
305676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
308425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
309337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
309361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.16ms 
309362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
309362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
309363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
312116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
313033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
313061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.18ms 
313063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
313063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
313064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
315803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
316711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
316734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.84ms 
316735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
316735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
316736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
319464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
320373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
320405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.52ms 
320407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
320407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
320408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
323141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
324055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
324084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.46ms 
324086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
324086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
324087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
326810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
327719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
327749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.85ms 
327751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
327751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
327752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
330517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
331398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
331427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.84ms 
331429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
331429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
331430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
334189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
335075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
335099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.3ms 
335100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
335100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
335101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
337856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
338737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
338765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.4ms 
338767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
338767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
338767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
341513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
342425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
342456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.21ms 
342457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
342457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
342458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
345239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
346151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
346160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
346161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
346161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
346162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
348906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
349818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
349838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.25ms 
349840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
349840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
349841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
352562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
353471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
353475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
353476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
353476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
353477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
356192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
357099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
357101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 654.13ns 
357103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
357103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
357103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
359856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
360776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
360779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 856.14ns 
360781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
360781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.81ns 
360782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
363507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
364415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
364423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.47ms 
364426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
364426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.41ns 
364427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
367159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
368082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
368089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
368091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
368092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.31ns 
368092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
370830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
371736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
371751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
371752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
371753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
371753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
374483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
375397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
375401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
375403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
375403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
375403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
378165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
379053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
379056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.73ns 
379058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
379058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.21ns 
379059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
381813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
382698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
382704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
382706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
382706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
382706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
385460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
386352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
386355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.43ns 
386356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
386356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
386357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
389134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
390025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
390027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.13ns 
390029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
390029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
390030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
392791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
393705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
393708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.73ns 
393710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
393710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.81ns 
393711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
396438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
397342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
397346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
397348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
397348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
397348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
400051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
400957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
400968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.92ms 
400969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
400969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
400970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
403702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
404612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
404616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
404618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
404618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
404619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
407361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
408279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
408287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
408288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
408288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
408289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
411026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
411924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
411929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
411930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
411930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
411931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
414628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
415530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
415547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.84ms 
415549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
415549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
415550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
418252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
419156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
419159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
419161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
419161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
419162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
421866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
422789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
422792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
422794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
422794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
422795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
425522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
426388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
426393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
426394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
426394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
426395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
429122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
430003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
430023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.12ms 
430024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
430025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
430025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
432768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
433650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
433655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.73ns 
433657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
433657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
433658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
436383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
437256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
437301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.91ms 
437302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
437302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
437303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
440021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
440933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
440937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
440938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
440938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
440939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
443656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
444563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
444589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.14ms 
444590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
444590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
444591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
447314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
448220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
448249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.87ms 
448252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
448252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.91ns 
448253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
450996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
451944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
451976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.73ms 
451977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
451978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
451978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
454770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
455684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
455687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.33ns 
455688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
455689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
455689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
458419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
459335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
459342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.42ms 
459343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
459343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
459344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
462064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
462979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
462983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
462984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
462984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
462985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
465726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
466651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
466654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 930.44ns 
466655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
466656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
466656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
469402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
470328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
470331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 959.94ns 
470332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
470332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
470333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
473087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
474018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
474021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
474023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
474023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.31ns 
474024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
476790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
477682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
477685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
477687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
477687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
477689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
480468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
481363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
481374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
481375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
481375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
481376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
484138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
485059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
485072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.55ms 
485074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
485074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
485075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
487789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
488707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
488720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.73ms 
488722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
488722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.01ns 
488723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
491450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
492373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
492389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
492390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
492390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
492391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
495122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
496048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
496053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
496054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
496054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
496055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
498764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
499678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
499685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
499687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
499687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
499688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
502418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
503316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
503318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.54ns 
503321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
503321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
503321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
506050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
506984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
506987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
506989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
506989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
506989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
509718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
510638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
510640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
510642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
510642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
510643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
513355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
514270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
514284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.14ms 
514290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
514290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.31ns 
514291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
517034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
517962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
517972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.53ms 
517974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
517975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.11ns 
517976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
520721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
521621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
521629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms 
521631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
521631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.91ns 
521631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
524390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
525329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
525331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.24ns 
525333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
525333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
525333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
528070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
528988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
528991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.93ns 
528992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
528992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
528993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
531707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
532629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
532633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
532635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
532635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
532636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
535363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
536258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
536261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
536263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
536263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
536263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
539007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
539935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
539938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
539939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
539940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
539940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
542663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
543587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
543591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
543592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
543592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
543593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
546300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
547228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
547234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
547235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
547235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
547236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
549961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
550854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
550857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
550859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
550859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
550860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
553598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
554512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
554525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.01ms 
554527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
554527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
554527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
557228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
558150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
558152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 704.73ns 
558153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
558153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
558154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
560877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
561757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
561765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms 
561766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
561766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
561767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
564486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
565409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
565412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.04ns 
565413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
565413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
565414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
568128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
569043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
569046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.04ns 
569047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
569047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
569048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
571764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
572657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
572663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
572664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
572664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
572665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
575362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
576267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
576270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
576272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
576272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
576273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
578966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
579875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
579878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
579880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
579880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
579880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
582594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
583482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
583486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
583487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
583487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
583488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
586234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
587162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
587167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
587168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
587168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
587169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
589883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
590805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
590821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.61ms 
590823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
590823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
590824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
593561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
594481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
594499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.81ms 
594501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
594501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
594501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
597203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
598130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
598142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
598143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
598143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
598144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
600892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
601787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
601837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.11ms 
601838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
601838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
601839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
604540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
605467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
605498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.53ms 
605500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
605500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
605500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
608225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
609109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
609139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.72ms 
609141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
609141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
609141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
611864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
612799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
612827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.99ms 
612828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
612829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
612829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
615594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
616471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
616488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.56ms 
616489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
616489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
616490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
619212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
620129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
620166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.71ms 
620168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
620168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
620169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
622906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
623790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
623845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.39ms 
623847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
623847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
623848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
626596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
627521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
627576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.82ms 
627578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
627578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
627579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
630337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
631260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
631310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.39ms 
631311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
631311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
631312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
634032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
634956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
635007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.15ms 
635009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
635009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
635010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
637735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
638634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
638774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 133.17ms 
638777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
638777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
638778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
641462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
642406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
642419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 
642420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
642420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
642421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
645159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
646078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
646087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
646088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
646088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
646089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
648796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
649721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
649727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
649728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
649729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
649729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
652416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
653328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
653352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.75ms 
653353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
653353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
653354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
656052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
656933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
656945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
656946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
656947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
656947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
659688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
660611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
660615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
660616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
660616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
660617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
663338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
664251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
664269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms 
664271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
664271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
664271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
666981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
667900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
667919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.38ms 
667921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
667921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
667921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
670644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
671559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
671581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.38ms 
671582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
671582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
671583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
674323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
675247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
675250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
675251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
675251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
675252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
677938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
678864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
678868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
678869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
678870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
678870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
681612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
682537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
682545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
682546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
682546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
682547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
685277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
686195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
686205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
686207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
686208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.71ns 
686209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
688909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
689826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
689908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.39ms 
689909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
689909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
689910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
692637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
693558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
693589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.42ms 
693591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
693591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
693592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
696320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
697241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
697266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.99ms 
697268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
697268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
697268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
700007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
700931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
700933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 316.41ns 
700935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
700935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
700936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
703683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
704611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
704842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 220.28ms 
704845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
704845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.31ns 
704846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
707615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
708544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
708603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.71ms 
708605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
708605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
708605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
711351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
712265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
712267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 382.71ns 
712268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
712268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
712269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
715019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
715019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
715939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
715941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 413.92ns 
715942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
715942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
715943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
718675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
719606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
719608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 411.12ns 
719610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
719610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
719611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
722344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
723244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
723246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.12ns 
723248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
723248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
723248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
725986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
726914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
727020     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
727035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.96ms 
727038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
727038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.01ns 
727039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
729792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
730718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
730773     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
730774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.12ms 
730775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
730775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
730777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
733547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
734484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
734486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
734515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
734556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
734574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
734579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
734585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
734588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
734590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
734592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
734595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
734597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
734599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
734601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
734836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
734838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
734840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
734841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
734843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
734986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
734987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
734991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
734994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
734996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
734997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
735191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
735193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
735194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
735195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
735196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
735198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
735340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
735342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
735343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
735344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
735345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
735346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
735355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
735356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
735357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
735359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
735360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
735361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
735369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
735370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
735371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
735372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
735373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
735374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
735540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
735541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
735542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
735716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
735718     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)'' 
735721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
735722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
735723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
735724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
735725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
735726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
735731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
735733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
735735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
735736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
735737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
735880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
735884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
735886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
735887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
735888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
735889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
735890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
736022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
736024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
736025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
736027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
736028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
736029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
736030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
736031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
736135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
736137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
736246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
736250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
736254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
736256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
736257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
736259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
736260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
736260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
736261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
736263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
736272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
736277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
736378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
736379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
736381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
736382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
736383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
736384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
736384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
736386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
736439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
736445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
736540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
736542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
736544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
736546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
736547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
736548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
736731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
736735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
736737     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)'' 
736739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
736740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
736741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
736742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
736742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
736752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
736754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
736755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
736756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
736861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
736862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
736863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
736864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
736865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
736866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
736976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
736978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
736979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
736980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
736981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
736982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
736983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
736984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
737075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
737077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
737159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
737160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
737160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
737165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
737169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
737174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
737305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
737308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
737309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
737311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
737321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
737412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
741296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
741297     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)'' 
741303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
741304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
741304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
741305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
741306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
741314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
741316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
741317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
741318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
741318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
741422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
741426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
741427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
741428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
741429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
741429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
741430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
741591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
741592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
741593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
741594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
741595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
741595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
741596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
741597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
741683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
741685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
741767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
741771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
741776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
741777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
741777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
741778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
741789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
741878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
741879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
741880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
741881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
741963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
741974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
741974     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)'' 
741976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
741977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
741978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
741978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
741979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
741991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
741993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
741994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
741994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
741995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
742093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
742095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
742096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
742097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
742098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
742201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
742205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
742207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
742207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
742208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
742208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
742209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
742322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
742323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
742324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
742325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
742326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
742326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
742327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
742328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
742329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
742330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
742331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
742331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
742332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
742332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
742333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
742434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
742435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
742441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
742531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
742624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
742625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
742626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
742627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
742628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
742629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
742629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
742629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
742630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
742728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
742735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
742838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
742840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
742840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
742842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
742842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
742842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
742843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
742844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
742849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
742850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
742941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
742947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
742953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
743068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
743069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
743070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
743071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
743072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
743072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
743073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
743073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
743136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
743137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
743138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
743139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
743139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
743146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
743152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
743286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
743388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
743389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
743390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
743391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
743586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
743743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
743746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
747256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
747262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
747263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
747264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
747264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
747397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
747399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
747400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
747401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
747402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
747524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
750926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
754546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
754552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
754553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
754554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
754555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
754686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
754688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
754689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
754690     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)' ...' 
754692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
755961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
755961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
755962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
758778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
758778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
759717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
759718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
759719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
759726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
759738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
759741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
759743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
759743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
759747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
759749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
759752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
759755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
759756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
759765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
759767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
759767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
759873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
759875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
759876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
759876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
759877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
759938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
759939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
759941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
759942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
759942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
759946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
759947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
759947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
759948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
759949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
759950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
760026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
760027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
760028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
760029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
760030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
760031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
760111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
760112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
760112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
760113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
760114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
760115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
760116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
760116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
760117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
760118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
760118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
760119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
760120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
760120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
760121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
760122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
760122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
760123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
760124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
760127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
760164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
760166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
760220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
760221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
760223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
760224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
760225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
760226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
760273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
760276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
760277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
760279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
760281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
760281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
760282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
760330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
760332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
760336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
760395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
760456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
760456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.61ns 
760457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
763249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
764233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
764269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.72ms