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

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

tests
0

failures
0

ignored
12m10.54s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.739s passed
powPositiveConcrete data()[101] 3.456s passed
powGeq1Concrete data()[102] 3.465s passed
pow2InIntLower data()[103] 3.436s passed
pow2InIntUpper data()[104] 3.500s passed
logSelfConcrete data()[105] 3.376s passed
log1Concrete data()[106] 3.504s passed
logProduct data()[107] 3.322s passed
logTimesBaseConcrete data()[108] 3.509s passed
logProdIdentity data()[109] 3.351s passed
moduloByteIsInByte data()[10] 3.667s passed
logProdIdentityConcrete data()[110] 3.535s passed
logPowIdentity data()[111] 3.364s passed
logPowIdentityConcrete data()[112] 3.519s passed
logPositive data()[113] 3.590s passed
logPositiveConcrete data()[114] 3.614s passed
logMono data()[115] 3.592s passed
logMonoConcrete data()[116] 3.679s passed
powLogLess data()[117] 3.868s passed
powLogMore2 data()[118] 3.549s passed
logLessThanPow data()[119] 3.485s passed
moduloCharIsInChar data()[11] 3.586s passed
logLessThanPowConcrete data()[120] 3.426s passed
logSqueeze data()[121] 3.531s passed
ifthenelse_equals data()[122] 3.317s passed
ifthenelse_equals_1 data()[123] 3.550s passed
ifthenelse_equals_2 data()[124] 3.479s passed
disjointWithSingleton1 data()[125] 3.523s passed
disjointWithSingleton2 data()[126] 3.373s passed
disjointArrayRanges data()[127] 3.469s passed
disjointArrayRangeAllFields1 data()[128] 3.441s passed
disjointArrayRangeAllFields2 data()[129] 3.448s passed
div_unique1 data()[12] 3.779s passed
seqSelfDefinition data()[130] 3.465s passed
seqOutsideValue data()[131] 3.419s passed
castedGetAny data()[132] 3.482s passed
seqGetAlphaCast data()[133] 3.682s passed
getOfSeqSingleton data()[134] 3.735s passed
getOfSeqSingletonConcrete data()[135] 3.530s passed
getOfSeqConcat data()[136] 3.496s passed
getOfSeqSub data()[137] 3.597s passed
getOfSeqReverse data()[138] 3.823s passed
lenOfSeqEmpty data()[139] 3.450s passed
div_unique2 data()[13] 3.776s passed
lenOfSeqSingleton data()[140] 3.568s passed
lenOfSeqConcat data()[141] 3.375s passed
lenOfSeqSub data()[142] 3.496s passed
lenOfSeqReverse data()[143] 3.464s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.460s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.516s passed
getOfSeqSingletonEQ data()[146] 3.501s passed
getOfSeqConcatEQ data()[147] 3.577s passed
getOfSeqSubEQ data()[148] 3.569s passed
getOfSeqReverseEQ data()[149] 3.795s passed
div_exists data()[14] 3.921s passed
lenOfSeqEmptyEQ data()[150] 3.684s passed
lenOfSeqSingletonEQ data()[151] 3.766s passed
lenOfSeqConcatEQ data()[152] 3.507s passed
lenOfSeqSubEQ data()[153] 3.478s passed
lenOfSeqReverseEQ data()[154] 3.535s passed
getOfSeqDefEQ data()[155] 3.524s passed
lenOfSeqDefEQ data()[156] 3.424s passed
seqConcatWithSeqEmpty1 data()[157] 3.451s passed
seqConcatWithSeqEmpty2 data()[158] 3.660s passed
seqReverseOfSeqEmpty data()[159] 3.467s passed
div_one data()[15] 3.762s passed
subSeqComplete data()[160] 3.499s passed
subSeqTailR data()[161] 3.420s passed
subSeqTailL data()[162] 3.567s passed
subSeqTailEQR data()[163] 3.391s passed
subSeqTailEQL data()[164] 3.579s passed
seqDef_split data()[165] 3.474s passed
seqDef_induction_upper data()[166] 3.639s passed
seqDef_induction_upper_concrete data()[167] 3.703s passed
seqDef_induction_lower data()[168] 3.865s passed
seqDef_induction_lower_concrete data()[169] 3.606s passed
jdiv_one data()[16] 3.714s passed
seqDef_split_in_three data()[170] 3.703s passed
seqDef_empty data()[171] 3.580s passed
seqDef_one_summand data()[172] 3.615s passed
seqDef_lower_equals_upper data()[173] 3.436s passed
seqDefOfSeq data()[174] 3.596s passed
seqSelfDefinitionEQ2 data()[175] 3.646s passed
indexOfSeqSingleton data()[176] 3.389s passed
indexOfSeqConcatFirst data()[177] 3.522s passed
indexOfSeqConcatSecond data()[178] 3.397s passed
indexOfSeqSub data()[179] 3.530s passed
div_zero data()[17] 3.529s passed
lenOfArray2seq data()[180] 3.353s passed
getAnyOfArray2seq data()[181] 3.520s passed
getOfArray2seq data()[182] 3.441s passed
getAnyOfNPermInv data()[183] 3.633s passed
seqNPermRange data()[184] 3.836s passed
seqPermTrans data()[185] 3.703s passed
seqPermRefl data()[186] 3.615s passed
seqPermSplit data()[187] 3.416s passed
seqNPermRight data()[188] 3.819s passed
seqPermFromSwap data()[189] 3.509s passed
divResZero1 data()[18] 3.628s passed
seqPermTransAlt0 data()[190] 3.594s passed
seqPermTransAlt1 data()[191] 3.385s passed
seqPermTransAlt2 data()[192] 3.518s passed
seqPermTransAlt3 data()[193] 3.741s passed
seqPermForall data()[194] 3.677s passed
seqPermExists data()[195] 3.729s passed
schiffl_lemma_2 data()[196] 27.473s passed
schiffl_thm_1 data()[197] 4.232s passed
eqSameSeq data()[198] 3.651s passed
divResZero2 data()[19] 3.425s passed
eqTermCut data()[1] 4.249s passed
divResOne1 data()[20] 3.591s passed
divResOne2 data()[21] 3.642s passed
div_cancel1 data()[22] 3.717s passed
div_cancel2 data()[23] 3.572s passed
divAddMultDenom data()[24] 3.612s passed
divMinus data()[25] 3.765s passed
divMinusDenom data()[26] 3.642s passed
divLeastDPos data()[27] 3.515s passed
divLeastDNeg data()[28] 3.415s passed
divGreatestDPos data()[29] 3.594s passed
equivAllRight data()[2] 3.992s passed
divGreatestDNeg data()[30] 3.493s passed
divIncreasingPos data()[31] 3.824s passed
divIncreasingNeg data()[32] 3.636s passed
jdiv_zero data()[33] 3.602s passed
jdivPulloutMinusNum data()[34] 3.383s passed
jdivPulloutMinusDenom data()[35] 3.771s passed
jdiv_uniquePosPos data()[36] 3.535s passed
jdiv_uniquePosNeg data()[37] 3.472s passed
jdiv_uniqueNegPos data()[38] 3.437s passed
jdiv_uniqueNegNeg data()[39] 3.590s passed
irrflConcrete1 data()[3] 3.923s passed
jdivMultDenom1 data()[40] 3.538s passed
jdivMultDenom2 data()[41] 3.458s passed
mod_geZero data()[42] 3.541s passed
mod_lessDenom data()[43] 3.397s passed
jmod_NumPos data()[44] 3.530s passed
jmod_NumNeg data()[45] 3.530s passed
jmod_geZero data()[46] 3.678s passed
jmodNumZero data()[47] 3.546s passed
jmod_pulloutminusNum data()[48] 3.767s passed
jmod_pulloutminusDenom data()[49] 3.648s passed
irrflConcrete2 data()[4] 4.000s passed
jmodUnique1 data()[50] 3.677s passed
jmodUnique2 data()[51] 3.551s passed
intDivRem data()[52] 3.549s passed
jmodjmod data()[53] 3.607s passed
jmodDivisible data()[54] 3.390s passed
jmodDivisibleRep data()[55] 3.628s passed
jdivAddMultDenom data()[56] 3.774s passed
jmodAltZero data()[57] 3.579s passed
jmodAddMultDenomZero data()[58] 3.445s passed
polyDiv_zero data()[59] 3.477s passed
cancel_gtPos data()[5] 3.594s passed
polyMod_ltdivDenom data()[60] 3.435s passed
bsum_empty data()[61] 3.521s passed
bsum_induction_upper data()[62] 3.359s passed
bsum_induction_lower data()[63] 3.596s passed
bsum_num_of_bounds data()[64] 3.614s passed
bsum_num_of_bounds2 data()[65] 3.788s passed
bsum_induction_upper2 data()[66] 3.731s passed
bsum_induction_upper_concrete data()[67] 3.358s passed
bsum_induction_upper_concrete_2 data()[68] 3.573s passed
bsum_induction_upper2_concrete data()[69] 3.388s passed
cancel_gtNeg data()[6] 3.700s passed
bsum_induction_lower_concrete data()[70] 3.517s passed
bsum_induction_lower2 data()[71] 3.392s passed
bsum_induction_lower2_concrete data()[72] 3.521s passed
bsum_positive data()[73] 3.434s passed
bsum_upper_bound data()[74] 3.623s passed
bsum_lower_bound data()[75] 3.489s passed
bsum_positive_lower_bound_element data()[76] 3.515s passed
bsum_sub_same_index data()[77] 3.508s passed
bsum_less_same_index data()[78] 3.629s passed
bsum_equal_except_one_index data()[79] 3.437s passed
moduloIntIsInInt data()[7] 3.626s passed
bsum_num_of_is_max data()[80] 3.497s passed
bsum_num_of_is_max2 data()[81] 3.552s passed
bsum_num_of_is_max3 data()[82] 3.671s passed
bsum_num_of_is_max4 data()[83] 3.875s passed
bsum_num_of_lt_max data()[84] 3.519s passed
bsum_num_of_lt_max2 data()[85] 3.547s passed
bsum_num_of_lt_max3 data()[86] 3.459s passed
bsum_num_of_lt_max4 data()[87] 3.645s passed
bsum_num_of_gt0 data()[88] 3.350s passed
bsum_num_of_gt0_alt data()[89] 3.533s passed
moduloLongIsInLong data()[8] 3.530s passed
bsum_add_concrete data()[90] 3.403s passed
bprod_all_positive data()[91] 3.552s passed
bprod_split data()[92] 3.447s passed
powConcrete0 data()[93] 3.456s passed
powConcrete1 data()[94] 3.397s passed
powSplitFactor data()[95] 3.444s passed
powAdd data()[96] 3.451s passed
powMono data()[97] 3.516s passed
powMonoConcrete data()[98] 3.553s passed
powMonoConcreteRight data()[99] 3.635s passed
moduloShortIsInShort data()[9] 3.578s passed

Standard output

409        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
430        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.28ms 
696        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722        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)

1783       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1785       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1787       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1787       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3541       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9835       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.14s 
9908       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9952       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ns 
9968       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9970       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.6ns 
9976       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13097      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
13100      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14207      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
14218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.1ns 
14220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
17312      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18208      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
18210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
18212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
21130      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
22131      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
22137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.3ns 
22140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
25139      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
26129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
26134      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
26137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.6ns 
26139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
28782      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
29681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
29729      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.97ms 
29733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
29734      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 971ns 
29736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32514      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
32515      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
33380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
33429      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.73ms 
33436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
33436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 475.5ns 
33438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36148      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
36148      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
37056      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
37059      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.7ns 
37061      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
37061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
37062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
39745      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
40586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
40589      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927ns 
40592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
40592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.5ns 
40593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
43281      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
44164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
44166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 579.6ns 
44169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
44170      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 733.8ns 
44171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
46987      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
47832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
47834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.9ns 
47837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
47837      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.9ns 
47839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50573      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
50574      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
51416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
51419      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725ns 
51422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
51423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.1ns 
51424      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
54254      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
55152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
55199      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.17ms 
55204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
55205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.3ns 
55206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58058      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
58058      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
58889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
58977      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.68ms 
58980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
58981      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.3ns 
58984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61749      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
61750      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
62694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
62898      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.5ms 
62902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
62903      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.8ns 
62904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65773      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
65774      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
66655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
66661      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
66663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
66664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 
66665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
69454      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
70372      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
70376      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
70378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
70378      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.3ns 
70379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
72973      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
73852      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
73903      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.9ms 
73907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
73907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.2ns 
73908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76614      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
76614      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
77505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
77532      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.43ms 
77535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
77535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.9ns 
77536      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
80100      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
80940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
80957      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.51ms 
80960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
80960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.9ns 
80961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83680      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
83681      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
84526      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
84548      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ms 
84551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
84551      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.4ns 
84552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
87249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
88165      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
88190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.99ms 
88193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
88193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328ns 
88194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
91062      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
91872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
91907      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.88ms 
91910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
91910      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.6ns 
91911      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
94632      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
95470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
95479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
95481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
95481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
95482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
98174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
99023      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
99091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.99ms 
99093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
99094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.6ns 
99095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
101811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
102767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
102855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.65ms 
102859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
102859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.4ns 
102861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
105571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
106442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
106499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.5ms 
106501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
106501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
106502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
109102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
110005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
110014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
110016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
110016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
110017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
112591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
113414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
113430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 
113431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
113431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
113432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
116080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
117007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
117023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.32ms 
117027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
117027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 603.6ns 
117028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
119585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
120504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
120516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
120519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
120519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.5ns 
120520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
123355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
124330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
124341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 
124342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
124343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.1ns 
124344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
127116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
127968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
127977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ms 
127979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
127979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
127980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
130781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
131574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
131579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
131581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
131581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309ns 
131582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
134121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
134929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
134962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.79ms 
134965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
134965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.1ns 
134967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
137792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
138661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
138733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.13ms 
138736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
138736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.3ns 
138737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
141366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
142246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
142269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.13ms 
142271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
142271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
142275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
144881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
145719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
145741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
145743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
145743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163ns 
145744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
148280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
149152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
149178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.86ms 
149179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
149179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
149180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
151844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
152747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
152768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.91ms 
152770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
152770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
152771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
155356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
156248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
156306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.64ms 
156308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
156308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
156309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
158875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
159762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
159764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
159766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
159766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.6ns 
159767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
162425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
163301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
163306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
163307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
163307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
163308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
165904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
166693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
166702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.42ms 
166704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
166704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
166705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
169370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
170223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
170233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
170234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
170234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
170235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
172940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
173738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
173762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
173764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
173764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
173764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
176594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
177429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
177440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
177443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
177443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.7ns 
177444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
180061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
180982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
180986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
180989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
180989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.4ns 
180990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
183845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
184747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
184755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
184756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
184757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
184757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
187487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
188395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
188402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
188404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
188404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
188405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
191099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
191943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
192079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.3ms 
192085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
192085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.6ns 
192086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
194620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
195508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
195632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.13ms 
195636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
195636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.2ns 
195637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
198356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
199178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
199183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
199185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
199185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306ns 
199186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
201817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
202737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
202789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.29ms 
202791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
202791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.2ns 
202792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
205335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
206143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
206179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.27ms 
206181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
206181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.2ns 
206182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
208915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
209804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
209807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
209809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
209809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
209810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
212479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
213351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
213581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 219.18ms 
213583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
213584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.3ns 
213585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
216310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
217146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
217160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.37ms 
217161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
217162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
217162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
219705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
220596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
220606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
220607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
220607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
220608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
223262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
224061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
224082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.72ms 
224083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
224083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
224084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
226694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
227499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
227517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
227520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
227520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.7ns 
227521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
230197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
231033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
231038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
231040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
231040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
231041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
233569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
234392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
234398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
234399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
234399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
234400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
237130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
237962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
237993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.67ms 
237994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
237994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
237995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
240641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
241584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
241607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.36ms 
241609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
241609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
241610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
244476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
245368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
245394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.76ms 
245397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
245398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.2ns 
245398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
248173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
249123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
249127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
249128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
249128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
249129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
251702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
252479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
252484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
252486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
252486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
252486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
255149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
256052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
256057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
256059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
256059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
256060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
258618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
259442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
259446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
259447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
259447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
259452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
262095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
262960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
262962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.4ns 
262963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
262963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
262964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
265501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
266350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
266354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
266356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
266356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
266357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
269017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
269871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
269873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
269876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
269876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
269877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
272417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
273257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
273309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.6ms 
273311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
273312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.5ns 
273313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
276047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
276889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
276933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.27ms 
276934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
276934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.3ns 
276935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
279552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
280379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
280421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.3ms 
280423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
280423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.9ns 
280424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
283096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
283879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
283936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.58ms 
283938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
283938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
283938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
286580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
287397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
287444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.62ms 
287446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
287446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
287447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
290132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
290967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
291073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.66ms 
291074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
291074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
291075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
293622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
294464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
294510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.76ms 
294512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
294513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.1ns 
294514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
297153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
297981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
298007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.64ms 
298009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
298009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
298009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
300585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
301524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
301559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.78ms 
301561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
301561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
301562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
304312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
305206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
305230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.6ms 
305232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
305232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
305233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
308131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
309068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
309105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.07ms 
309107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
309107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
309108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
311771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
312594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
312625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.83ms 
312626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
312626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
312627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
315281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
316139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
316172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.9ms 
316173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
316173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
316174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
318800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
319598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
319630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.02ms 
319632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
319632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
319633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
322421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
323249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
323275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.76ms 
323277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
323277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.9ns 
323279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
325798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
326593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
326625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.07ms 
326627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
326627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.7ns 
326628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
329316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
330127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
330158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.58ms 
330159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
330160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
330160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
332717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
333551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
333561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
333563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
333563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
333564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
336281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
337091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
337114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.96ms 
337115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
337115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
337116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
339698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
340556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
340560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
340562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
340562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
340562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
343210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
344014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
344017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.5ns 
344018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
344018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
344019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
346531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
347409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
347413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.3ns 
347415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
347415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.8ns 
347416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
350028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
350841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
350856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.59ms 
350860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
350860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
350861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
353407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
354300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
354310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms 
354311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
354311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
354312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
357006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
357811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
357826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.95ms 
357827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
357827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
357828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
360407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
361374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
361378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
361380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
361380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
361380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
364148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
365011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
365014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.8ns 
365015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
365015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
365016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
367802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
368746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
368753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
368754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
368754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
368755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
371376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
372206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
372209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 835ns 
372215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
372215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
372216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
374844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
375675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
375677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.8ns 
375678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
375678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
375679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
378250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
379111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
379113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.11ns 
379115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
379115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
379115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
381793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
382610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
382614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
382615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
382615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
382616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
385159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
385979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
385990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
385991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
385991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
385992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
388643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
389488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
389493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
389495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
389495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
389496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
392011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
392807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
392815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
392816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
392816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
392817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
395483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
396320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
396325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
396326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
396326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
396327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
398818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
399653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
399676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.93ms 
399677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
399677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
399678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
402385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
403207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
403211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
403212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
403212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
403213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
405720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
406570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
406575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
406577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
406577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
406578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
409266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
410090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
410095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
410096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
410096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
410097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
412701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
413660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
413684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.62ms 
413685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
413686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
413686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
416462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
417293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
417298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.9ns 
417300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
417300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.7ns 
417301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
419859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
420831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
420890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.98ms 
420893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
420893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.2ns 
420894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
423645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
424565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
424570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
424571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
424571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
424572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
427451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
428393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
428437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.59ms 
428439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
428439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.7ns 
428440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
431144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
431959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
431986     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.25ms 
431987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
431988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
431988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
434627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
435438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
435472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.43ms 
435473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
435473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
435474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
438059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
438895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
438897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
438898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
438898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
438899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
441611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
442422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
442429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
442430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
442430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
442431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
444947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
445742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
445746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
445747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
445747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
445748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
448470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
449292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
449295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
449296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
449297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
449297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
451857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
452772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
452774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 997.41ns 
452776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
452776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
452776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
455462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
456294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
456297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
456299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
456299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
456299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
458814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
459666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
459670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
459672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
459672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
459673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
462290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
463115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
463137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.13ms 
463145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
463146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 596.7ns 
463147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
465681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
466558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
466578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.91ms 
466585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
466585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
466586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
469172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
470017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
470032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
470033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
470033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
470034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
472592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
473476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
473496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.75ms 
473498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
473498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.3ns 
473499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
476097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
476910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
476915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
476916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
476916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
476917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
479483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
480389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
480397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
480399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
480399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
480399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
483169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
484076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
484079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 980.41ns 
484081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
484081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
484082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
486893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
487810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
487814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
487815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
487815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
487816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
490510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
491342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
491344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
491345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
491346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
491346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
493999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
494826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
494841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
494842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
494842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
494843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
497559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
498432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
498437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
498439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
498439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
498440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
501361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
502253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
502260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
502262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
502262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
502262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
504833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
505708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
505710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.41ns 
505712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
505712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
505714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
508416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
509275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
509277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 848.81ns 
509279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
509279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
509280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
511807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
512649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
512653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
512655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
512655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.1ns 
512656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
515281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
516146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
516149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
516151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
516151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.4ns 
516152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
518684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
519610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
519614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
519615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
519615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
519616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
522241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
523070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
523073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
523074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
523074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
523075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
525639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
526580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
526589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.08ms 
526590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
526590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
526591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
529195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
530085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
530090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
530091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
530091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
530092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
532757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
533654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
533667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
533668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
533669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
533669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
536367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
537233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
537236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.41ns 
537237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
537237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
537238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
540072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
541022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
541031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.45ms 
541032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
541033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
541033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
543803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
544712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
544715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
544716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
544716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
544717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
547598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
548478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
548481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
548482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
548482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
548483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
551143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
551983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
551989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
551990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
551990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
551991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
554608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
555463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
555467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
555468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
555468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
555469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
558115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
558995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
559002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
559003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
559003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
559004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
561679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
562522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
562526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
562527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
562527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
562527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
565046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
565941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
565950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms 
565951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
565951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
565952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
568557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
569382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
569400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.48ms 
569402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
569402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
569402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
572110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
573036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
573060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ms 
573062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
573062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
573062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
575643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
576515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
576528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ms 
576529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
576529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
576530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
579122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
580011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
580026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
580027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
580027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
580028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
582569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
583416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
583446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.85ms 
583448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
583448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
583448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
586092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
586980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
587013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.93ms 
587014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
587014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
587015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
589551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
590375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
590404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.03ms 
590406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
590406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
590406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
593119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
593965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
593984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.21ms 
593985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
593985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
593986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
596575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
597416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
597457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.95ms 
597458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
597458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
597459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
600138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
601033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
601096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.89ms 
601097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
601097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
601098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
603814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
604744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
604799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.09ms 
604800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
604801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
604801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
607714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
608610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
608664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.91ms 
608665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
608665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
608666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
611262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
612209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
612271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.98ms 
612272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
612272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
612273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
614936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
615789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
615973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 175.49ms 
615975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
615975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
615975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
618631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
619537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
619551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
619555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
619556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.5ns 
619556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
622256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
623159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
623169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.47ms 
623170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
623170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
623170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
625726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
626598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
626604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
626606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
626606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
626606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
629330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
630177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
630200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.49ms 
630202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
630202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
630202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
632915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
633831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
633846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
633848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
633848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
633849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
636411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
637232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
637236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
637237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
637237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
637238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
639892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
640736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
640758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.46ms 
640759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
640759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
640759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
643297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
644135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
644154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.68ms 
644156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
644156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
644156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
646828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
647659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
647685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.63ms 
647687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
647687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
647687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
650209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
651036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
651039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
651040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
651040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
651041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
653702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
654554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
654558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
654559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
654560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
654560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
657129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
657991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
657999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
658000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
658001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
658001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
660667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
661608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
661632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.86ms 
661635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
661638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.86ms 
661639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
664393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
665375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
665468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.06ms 
665470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
665470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
665470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
668241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
669132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
669171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.37ms 
669173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
669173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
669174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
671892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
672759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
672786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.86ms 
672788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
672788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
672788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
675328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
676199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
676203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 441.5ns 
676205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
676205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.7ns 
676207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
678871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
679747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
680022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.89ms 
680024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
680024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.6ns 
680025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
682610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
683468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
683531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.84ms 
683534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
683534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.3ns 
683535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
686278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
687124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
687126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.2ns 
687127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
687127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
687128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
689650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
690508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
690511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 476.6ns 
690512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
690512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
690513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
693219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
694025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
694028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 621ns 
694029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
694029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
694030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
696833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
697766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
697769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.11ns 
697770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
697770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
697771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
700457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
700457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
701341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
701428     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
701446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.66ms 
701448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
701449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.5ns 
701450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
704140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
705120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
705174     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
705175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.34ms 
705177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
705177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
705178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
708086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
709038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
709040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
709079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
709121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
709140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
709146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
709153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
709156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
709157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
709159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
709162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
709165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
709167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
709169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
709425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
709428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
709429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
709431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
709432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
709585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
709587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
709591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
709593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
709595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
709597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
709827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
709830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
709831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
709832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
709834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
709837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
710021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
710023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
710025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
710026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
710027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
710029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
710038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
710040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
710041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
710044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
710047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
710048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
710059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
710060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
710061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
710062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
710064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
710065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
710227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
710228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
710230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
710402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
710404     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)'' 
710408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
710409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
710410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
710411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
710413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
710416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
710420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
710422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
710423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
710424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
710425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
710568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
710578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
710580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
710581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
710583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
710584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
710587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
710727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
710729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
710730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
710732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
710733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
710734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
710735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
710737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
710881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
710884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
711061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
711069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
711076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
711078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
711079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
711081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
711082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
711082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
711084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
711086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
711101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
711112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
711263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
711268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
711281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
711282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
711283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
711284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
711284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
711286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
711366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
711376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
711497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
711499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
711501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
711503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
711504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
711505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
711686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
711691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
711695     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)'' 
711697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
711700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
711701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
711702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
711703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
711715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
711726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
711728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
711729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
711852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
711854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
711855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
711856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
711856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
711858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
711975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
711978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
711979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
711981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
711982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
711983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
711984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
711986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
712096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
712098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
712201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
712202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
712203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
712209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
712214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
712220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
712434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
712435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
712436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
712438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
712450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
712554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
716748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
716763     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)'' 
716771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
716775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
716775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
716776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
716777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
716787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
716789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
716790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
716792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
716793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
716916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
716921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
716922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
716923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
716924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
716925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
716926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
717055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
717057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
717057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
717059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
717060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
717061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
717062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
717063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
717162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
717164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
717256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
717262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
717266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
717267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
717268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
717269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
717281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
717401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
717403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
717404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
717407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
717508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
717521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
717522     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)'' 
717524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
717525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
717526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
717527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
717527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
717542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
717545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
717546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
717547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
717547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
717670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
717672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
717673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
717674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
717675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
717850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
717855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
717857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
717858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
717859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
717860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
717861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
717988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
717990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
717991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
717993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
717994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
717994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
717995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
717996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
717997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
717998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
718000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
718000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
718001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
718001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
718002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
718128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
718130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
718138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
718242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
718400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
718404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
718406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
718407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
718409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
718411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
718412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
718413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
718415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
718559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
718567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
718677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
718679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
718680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
718681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
718682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
718682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
718683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
718684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
718691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
718692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
718794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
718800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
718807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
718932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
718934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
718934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
718936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
718937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
718937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
718938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
718938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
719006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
719007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
719008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
719009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
719010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
719016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
719023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
719167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
719272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
719273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
719274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
719276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
719473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
719585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
719586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
723281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
723287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
723289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
723289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
723290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
723429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
723431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
723432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
723433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
723434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
723560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
727400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
731099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
731104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
731105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
731106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
731107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
731237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
731238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
731239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
731240     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)' ...' 
731242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
732650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
732650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
732651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
735332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
736256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
736257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
736258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
736265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
736275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
736278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
736280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
736281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
736285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
736287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
736289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
736292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
736292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
736301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
736303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
736303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
736353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
736354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
736354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
736355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
736356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
736419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
736420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
736421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
736421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
736422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
736426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
736426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
736427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
736428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
736428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
736429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
736499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
736500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
736501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
736502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
736503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
736504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
736571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
736571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
736572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
736572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
736573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
736574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
736574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
736575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
736576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
736576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
736577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
736578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
736578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
736579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
736579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
736580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
736581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
736582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
736583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
736586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
736617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
736619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
736667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
736668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
736670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
736671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
736671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
736672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
736714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
736716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
736717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
736718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
736719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
736720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
736720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
736762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
736764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
736767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
736823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
736881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
736881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
736882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
739584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
740490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
740532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.95ms