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

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

tests
0

failures
0

ignored
11m18.21s

duration
100%

successful

Tests

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

Standard output

362        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
385        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.53ms 
609        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623        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)

1517       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1519       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1522       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1522       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3053       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8662       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.05s 
8726       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8758       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32ns 
8769       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8769       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.5ns 
8774       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
11596      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12722      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.64ms 
12752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
12754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
15498      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16426      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.74ms 
16429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.8ns 
16431      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
19064      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19946      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
19948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19948      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.2ns 
19949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
22564      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23415      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23420      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
23423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 515.71ns 
23424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
25972      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26856      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.77ms 
26859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.4ns 
26861      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
29384      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30213      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30232      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.21ms 
30236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30236      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.7ns 
30237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
32782      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33588      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 701.21ns 
33590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.7ns 
33592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
36116      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.41ns 
36928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.4ns 
36929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
39457      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.21ns 
40262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.31ns 
40263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
42780      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43580      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.61ns 
43583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.4ns 
43584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46108      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
46109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46959      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
46962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
46963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
49472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.17ms 
50335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns 
50336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
52907      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53764      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.25ms 
53766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53766      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
53767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56276      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
56277      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57296      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 183.81ms 
57299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 492.31ns 
57301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59796      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
59797      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60622      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
60624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.5ns 
60625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63108      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
63109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63930      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
63933      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310ns 
63935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
66439      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
67322      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.73ms 
67325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
67325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns 
67327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
69840      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70680      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
70683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.61ns 
70685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73187      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
73187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73998      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
74012      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.18ms 
74014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
74014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.4ns 
74015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
76543      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
77353      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
77354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
77354      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.8ns 
77355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
79927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
80739      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.02ms 
80748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
80748      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.01ns 
80749      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
83268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
84064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
84090      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms 
84092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
84092      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.2ns 
84093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
86618      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
87439      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
87440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
87440      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
87441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89929      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
89929      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
90782      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.08ms 
90783      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
90783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
90784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
93267      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
94121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
94179      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.24ms 
94182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
94182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.11ns 
94183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96681      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
96682      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
97572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.43ms 
97575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
97576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.31ns 
97577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
100068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
100882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
100890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
100891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
100891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
100892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
103381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
104193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
104206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
104208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
104209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
104209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
106700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
107512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
107524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
107526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
107526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.4ns 
107527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
110008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
110823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
110831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.29ms 
110832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
110832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
110833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
113345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
114134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
114141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
114142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
114143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.4ns 
114143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
116640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
117435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
117445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
117446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
117446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
117447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
119958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
120754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
120757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
120759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
120759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
120760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
123270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
124058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
124070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.68ms 
124072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
124072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
124073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
126593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
127407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
127458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.64ms 
127459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
127460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
127460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
129953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
130765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
130783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
130786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
130786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318ns 
130787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
133286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
134099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
134117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.75ms 
134119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
134120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.2ns 
134121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
136598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
137414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
137432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms 
137434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
137434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.2ns 
137435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
139907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
140743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
140760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.24ms 
140761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
140761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
140762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
143242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
144057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
144095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.63ms 
144097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
144097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
144097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
146570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
147381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
147387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
147389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
147389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
147390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
149883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
150694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
150699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
150700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
150700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
150701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
153180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
153992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
154000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
154002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
154002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.7ns 
154003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
156508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
157298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
157306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
157308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
157308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.4ns 
157309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
159806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
160592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
160611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.1ms 
160613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
160613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
160613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
163107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
163894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
163902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
163904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
163904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
163904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
166391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
167190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
167194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
167197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
167197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.7ns 
167198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
169737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
170550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
170553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
170555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
170555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns 
170556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
173019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
173823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
173827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
173829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
173829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.1ns 
173831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
176301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
177117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
177200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.27ms 
177203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
177203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.8ns 
177205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
179707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
180513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
180590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.83ms 
180591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
180592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
180592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
183062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
183876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
183880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
183881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
183881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
183882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
186372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
187181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
187215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.66ms 
187216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
187216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.4ns 
187217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
189702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
190518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
190547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.2ms 
190549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
190549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
190549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
193036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
193852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
193855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
193856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
193856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
193857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
196379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
197198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
197375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 167.41ms 
197378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
197379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 551.41ns 
197380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
199916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
200706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
200718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms 
200724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
200724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289ns 
200725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
203264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
204068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
204076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.58ms 
204078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
204078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
204079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
206605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
207417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
207433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
207435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
207435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
207436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
209911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
210726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
210738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.34ms 
210741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
210741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
210741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
213215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
214015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
214019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
214020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
214020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
214021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
216494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
217306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
217312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
217315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
217315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 618.11ns 
217316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
219788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
220598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
220620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.78ms 
220622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
220622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
220623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
223095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
223905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
223921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
223923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
223923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
223924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
226385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
227196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
227212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
227215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
227215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.3ns 
227216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
229699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
230509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
230512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
230513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
230514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
230514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
232991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
233802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
233806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
233807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
233807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
233808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
236309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
237096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
237101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
237102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
237102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
237103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
239585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
240375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
240378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
240380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.7ns 
240381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
242865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
243651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
243653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.61ns 
243655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
243655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
243655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
246142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
246929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
246933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
246934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
246934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
246935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
249442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
250248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
250251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
250252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
250252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
250253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
252711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
253519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
253578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.66ms 
253581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
253581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.4ns 
253582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
256059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
256867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
256902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.72ms 
256904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
256904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
256905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
259385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
260191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
260223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.68ms 
260224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
260225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
260225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
262699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
263507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
263552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.7ms 
263553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
263553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
263554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
266024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
266831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
266861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.6ms 
266863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
266863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
266864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
269328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
270138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
270191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.95ms 
270194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
270194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.2ns 
270195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
272657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
273473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
273501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.24ms 
273502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
273503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
275994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
276780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
276800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.82ms 
276802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
276803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.1ns 
276804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
279286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
280076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
280101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22ms 
280102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
280102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
280103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
282602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
283390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
283410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
283412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
283412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
283413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
285903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
286712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
286739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.92ms 
286741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
286741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
286742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
289223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
290036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
290062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.46ms 
290063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
290063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
290064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
292538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
293348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
293375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.39ms 
293377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
293377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
293380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
295879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
296697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
296721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.93ms 
296724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
296724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238ns 
296725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
299177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
299984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
300005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ms 
300006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
300006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
300007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
302482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
303289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
303315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.81ms 
303316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
303316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
303317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
305772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
306580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
306609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.26ms 
306611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
306611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.6ns 
306612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
309081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
309890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
309898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
309899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
309899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
309900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
312397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
313183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
313201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.6ms 
313202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
313202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
313203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
315689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
316475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
316480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
316481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
316482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.8ns 
316482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
318966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
319750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
319752     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.71ns 
319753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
319753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
319754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
322234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
323020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
323022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.11ns 
323023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
323023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
323024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
325509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
326320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
326327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
326328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
326328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
326329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
328803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
329612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
329619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
329621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
329621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.5ns 
329622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
332091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
332899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
332912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.15ms 
332913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
332913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
332914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
335369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
336177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
336180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
336181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
336181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
336182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
338646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
339456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
339458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.21ns 
339460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
339460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
339460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
341915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
342722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
342728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
342729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
342729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
342729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
345188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
345996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
345999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 731.51ns 
346000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
346000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
346001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
348488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
349296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
349298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.91ns 
349299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
349299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
349300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
351759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
352589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
352591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.91ns 
352593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
352593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200ns 
352594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
355079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
355871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
355874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
355876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
355876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
355876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
358360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
359147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
359157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
359158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
359158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
359159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
361659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
362444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
362448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
362449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
362450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
362450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
364934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
365721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
365729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
365730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
365730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
365731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
368219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
369026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
369030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
369032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
369032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
369032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
371490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
372298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
372314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.33ms 
372316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
372316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
372316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
374781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
375590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
375593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
375594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
375595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
375595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
378081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
378912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
378921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
378925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
378925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
378926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
381396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
382205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
382209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
382210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
382210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
382211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
384660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
385466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
385483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.78ms 
385484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
385484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
385485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
387954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
388762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
388766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.21ns 
388767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
388767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
388768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
391234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
392036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
392076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.88ms 
392077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
392078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
392078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
394532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
395344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
395348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
395349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
395349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
395350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
397847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
398635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
398656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.35ms 
398658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
398658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
398659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
401151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
401937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
401958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.33ms 
401959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
401959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
401960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
404451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
405240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
405264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
405266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
405266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
405267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
407755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
408572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
408574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 694.21ns 
408575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
408575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
408576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
411040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
411849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
411855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
411856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
411856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
411857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
414330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
415143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
415146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
415147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
415147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
415148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
417635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
418451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
418453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 836.61ns 
418455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
418455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
418455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
420913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
421725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
421728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
421730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
421730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
421731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
424185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
425000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
425003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
425004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
425004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
425005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
427473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
428290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
428293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
428294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
428294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
428295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
430750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
431566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
431575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.67ms 
431576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
431576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
431577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
434057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
434849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
434860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.68ms 
434862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
434862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
434862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
437338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
438130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
438169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.31ms 
438170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
438170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
438171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
440626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
441448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
441459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
441460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
441460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
441461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
443932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
444756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
444760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
444761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
444761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
444762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
447230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
448052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
448057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
448059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
448059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
448059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
450540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
451370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
451372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.61ns 
451373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
451373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
451374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
453911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
454735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
454738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
454739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
454739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
454740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
457226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
458046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
458049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.81ns 
458050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
458050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
458050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
460517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
461340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
461351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
461352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
461352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
461353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
463816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
464638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
464642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
464643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
464643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
464644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
467122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
467944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
467950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
467952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
467952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
467952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
470452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
471250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
471252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.31ns 
471253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
471253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
471254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
473751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
474575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
474579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.81ns 
474580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
474580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
474581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
477044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
477879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
477883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
477884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
477884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
477885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
480356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
481178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
481181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
481182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
481183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
481183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
483685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
484484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
484487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
484488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
484488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
484489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
486983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
487806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
487809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
487810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
487810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
487811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
490277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
491111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
491116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
491117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
491117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
491118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
493600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
494400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
494403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
494404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
494405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
494405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
496890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
497713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
497724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
497725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
497725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
497726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
500189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
501011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
501014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.31ns 
501015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
501015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
501016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
503471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
504294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
504301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
504302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
504302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
504303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
506787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
507609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
507611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 916.11ns 
507612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
507612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
507613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
510081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
510903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
510905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.61ns 
510907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
510907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
510907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
513393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
514191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
514196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
514197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
514197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
514198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
516690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
517512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
517516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
517518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
517518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.8ns 
517519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
519990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
520814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
520817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
520818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
520818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
520819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
523351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
524152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
524155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
524157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
524157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
524157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
526666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
527496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
527501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
527503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
527503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
527503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
529999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
530826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
530843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms 
530845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
530845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
530846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
533367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
534191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
534207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.65ms 
534208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
534208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
534209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
536687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
537511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
537521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
537523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
537523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
537524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
540009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
540836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
540847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ms 
540849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
540849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
540849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
543325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
544167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
544193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.81ms 
544194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
544194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
544195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
546684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
547483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
547509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.09ms 
547510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
547510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
547511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
550004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
550827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
550851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.88ms 
550852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
550852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
550853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
553353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
554156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
554170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
554171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
554171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
554172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
556670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
557491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
557523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29ms 
557525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
557525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
557525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
560043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
560840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
560887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.78ms 
560889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
560889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
560889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
563377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
564201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
564246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.7ms 
564249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
564249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.2ns 
564250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
566732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
567558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
567600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.21ms 
567602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
567602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
567602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
570062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
570882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
570927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.52ms 
570928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
570928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
570929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
573414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
574237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
574354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.45ms 
574356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
574356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
574356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
576810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
577632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
577640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
577641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
577641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
577642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
580127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
580946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
580958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
580960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
580960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.5ns 
580961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
583431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
584227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
584232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
584233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
584233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
584234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
586696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
587513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
587531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.57ms 
587532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
587532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
587533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
590006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
590826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
590837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 
590838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
590838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
590838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
593283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
594101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
594105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
594106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
594106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
594106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
596583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
597401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
597418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.32ms 
597419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
597419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
597419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
599889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
600686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
600701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.62ms 
600703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
600703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
600703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
603164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
603982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
604000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.94ms 
604001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
604001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
604002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
606466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
607283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
607286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
607287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
607287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
607288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
609744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
610540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
610544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
610545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
610545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
610546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
613007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
613825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
613831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
613832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
613832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
613833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
616292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
617108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
617114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
617115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
617115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
617116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
619575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
620397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
620463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.97ms 
620464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
620464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
620465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
622915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
623733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
623760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
623761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
623761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
623762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
626220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
627039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
627060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ms 
627062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
627062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
627062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
629524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
630344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
630346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.8ns 
630347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
630347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
630348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
632810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
633628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
633825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.1ms 
633828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
633828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns 
633829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
636302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
637100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
637149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.33ms 
637150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
637151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
637151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
639610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
640430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
640432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314ns 
640434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
640435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229ns 
640435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
642897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
643716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
643718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 345.81ns 
643719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
643719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
643720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
646179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
647000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
647002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.4ns 
647003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
647003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
647004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
649493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
650315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
650317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.21ns 
650318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
650318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
650319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
652788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
653588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
653677     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
653693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.1ms 
653695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
653695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.7ns 
653696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
656195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
657019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
657069     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
657070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.36ms 
657071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
657071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
657072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
659569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
660398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
660399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
660424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
660457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
660472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
660476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
660481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
660483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
660484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
660486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
660488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
660490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
660492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
660493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
660701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
660702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
660704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
660705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
660706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
660840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
660841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
660844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
660846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
660847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
660851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
661012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
661014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
661015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
661016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
661018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
661020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
661164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
661166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
661167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
661168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
661169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
661170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
661178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
661178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
661179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
661182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
661185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
661185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
661197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
661198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
661199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
661200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
661200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
661202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
661343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
661344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
661345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
661469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
661470     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)'' 
661472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
661473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
661474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
661475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
661476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
661477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
661480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
661481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
661482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
661483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
661484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
661605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
661608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
661610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
661611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
661612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
661613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
661613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
661764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
661766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
661767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
661769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
661770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
661771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
661772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
661773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
661875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
661878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
661972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
661980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
661988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
661989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
661992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
661993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
661995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
661996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
661996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
661997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
662011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
662018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
662158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
662160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
662161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
662163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
662163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
662164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
662164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
662165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
662220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
662227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
662323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
662325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
662327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
662328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
662329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
662330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
662471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
662476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
662478     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)'' 
662480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
662482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
662485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
662486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
662487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
662496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
662502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
662503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
662504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
662600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
662602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
662603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
662604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
662604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
662606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
662706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
662710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
662711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
662713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
662713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
662714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
662714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
662716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
662808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
662810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
662884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
662885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
662886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
662891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
662895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
662899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
663019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
663020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
663021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
663022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
663033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
663116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
666619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
666620     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)'' 
666626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
666627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
666628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
666628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
666629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
666637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
666638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
666639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
666640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
666641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
666735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
666739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
666740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
666741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
666742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
666743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
666743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
666838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
666840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
666840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
666842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
666842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
666843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
666844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
666845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
666922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
666924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
666998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
667002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
667007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
667008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
667009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
667010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
667020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
667101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
667102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
667103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
667104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
667176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
667186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
667187     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)'' 
667189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
667190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
667190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
667191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
667192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
667203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
667204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
667205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
667206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
667207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
667296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
667297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
667299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
667300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
667300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
667392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
667397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
667398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
667399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
667400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
667400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
667401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
667508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
667510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
667511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
667513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
667514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
667517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
667518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
667519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
667520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
667520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
667521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
667522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
667522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
667522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
667523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
667613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
667614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
667621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
667699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
667782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
667783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
667784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
667785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
667786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
667786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
667786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
667787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
667788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
667875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
667881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
667973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
667974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
667975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
667976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
667976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
667977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
667977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
667978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
667983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
667984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
668066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
668072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
668078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
668180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
668181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
668182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
668183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
668184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
668184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
668184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
668185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
668242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
668243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
668243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
668244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
668245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
668251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
668256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
668423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
668512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
668513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
668514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
668515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
668685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
668773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
668774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
671809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
671814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
671815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
671816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
671816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
671930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
671931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
671932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
671933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
671934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
672039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
675121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
678350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
678355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
678357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
678358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
678358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
678472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
678474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
678475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
678476     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)' ...' 
678478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
679627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
679627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
679628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
682176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
683023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
683025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
683025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
683034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
683044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
683047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
683048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
683049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
683054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
683055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
683058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
683061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
683062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
683071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
683073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
683073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
683160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
683161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
683162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
683162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
683163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
683221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
683221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
683222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
683223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
683223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
683226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
683227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
683227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
683228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
683229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
683229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
683291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
683292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
683292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
683293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
683294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
683295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
683356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
683357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
683357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
683358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
683358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
683359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
683360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
683360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
683361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
683361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
683361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
683362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
683362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
683362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
683363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
683363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
683364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
683364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
683365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
683367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
683395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
683396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
683440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
683441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
683442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
683443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
683444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
683444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
683483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
683485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
683487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
683488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
683489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
683490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
683490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
683531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
683533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
683536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
683585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
683637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
683637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
683637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
686137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
686988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
687018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.55ms