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

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

tests
0

failures
0

ignored
10m49.81s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.139s passed
powPositiveConcrete data()[101] 3.136s passed
powGeq1Concrete data()[102] 3.132s passed
pow2InIntLower data()[103] 3.154s passed
pow2InIntUpper data()[104] 3.135s passed
logSelfConcrete data()[105] 3.163s passed
log1Concrete data()[106] 3.206s passed
logProduct data()[107] 3.155s passed
logTimesBaseConcrete data()[108] 3.137s passed
logProdIdentity data()[109] 3.201s passed
moduloByteIsInByte data()[10] 3.302s passed
logProdIdentityConcrete data()[110] 3.206s passed
logPowIdentity data()[111] 3.136s passed
logPowIdentityConcrete data()[112] 3.157s passed
logPositive data()[113] 3.152s passed
logPositiveConcrete data()[114] 3.148s passed
logMono data()[115] 3.189s passed
logMonoConcrete data()[116] 3.237s passed
powLogLess data()[117] 3.167s passed
powLogMore2 data()[118] 3.157s passed
logLessThanPow data()[119] 3.158s passed
moduloCharIsInChar data()[11] 3.233s passed
logLessThanPowConcrete data()[120] 3.144s passed
logSqueeze data()[121] 3.171s passed
ifthenelse_equals data()[122] 3.167s passed
ifthenelse_equals_1 data()[123] 3.174s passed
ifthenelse_equals_2 data()[124] 3.158s passed
disjointWithSingleton1 data()[125] 3.157s passed
disjointWithSingleton2 data()[126] 3.156s passed
disjointArrayRanges data()[127] 3.163s passed
disjointArrayRangeAllFields1 data()[128] 3.155s passed
disjointArrayRangeAllFields2 data()[129] 3.171s passed
div_unique1 data()[12] 3.326s passed
seqSelfDefinition data()[130] 3.170s passed
seqOutsideValue data()[131] 3.198s passed
castedGetAny data()[132] 3.166s passed
seqGetAlphaCast data()[133] 3.136s passed
getOfSeqSingleton data()[134] 3.200s passed
getOfSeqSingletonConcrete data()[135] 3.144s passed
getOfSeqConcat data()[136] 3.179s passed
getOfSeqSub data()[137] 3.180s passed
getOfSeqReverse data()[138] 3.160s passed
lenOfSeqEmpty data()[139] 3.157s passed
div_unique2 data()[13] 3.378s passed
lenOfSeqSingleton data()[140] 3.173s passed
lenOfSeqConcat data()[141] 3.195s passed
lenOfSeqSub data()[142] 3.163s passed
lenOfSeqReverse data()[143] 3.150s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.172s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.145s passed
getOfSeqSingletonEQ data()[146] 3.157s passed
getOfSeqConcatEQ data()[147] 3.140s passed
getOfSeqSubEQ data()[148] 3.145s passed
getOfSeqReverseEQ data()[149] 3.158s passed
div_exists data()[14] 3.328s passed
lenOfSeqEmptyEQ data()[150] 3.191s passed
lenOfSeqSingletonEQ data()[151] 3.187s passed
lenOfSeqConcatEQ data()[152] 3.165s passed
lenOfSeqSubEQ data()[153] 3.219s passed
lenOfSeqReverseEQ data()[154] 3.137s passed
getOfSeqDefEQ data()[155] 3.140s passed
lenOfSeqDefEQ data()[156] 3.160s passed
seqConcatWithSeqEmpty1 data()[157] 3.190s passed
seqConcatWithSeqEmpty2 data()[158] 3.232s passed
seqReverseOfSeqEmpty data()[159] 3.216s passed
div_one data()[15] 3.203s passed
subSeqComplete data()[160] 3.185s passed
subSeqTailR data()[161] 3.162s passed
subSeqTailL data()[162] 3.177s passed
subSeqTailEQR data()[163] 3.155s passed
subSeqTailEQL data()[164] 3.166s passed
seqDef_split data()[165] 3.165s passed
seqDef_induction_upper data()[166] 3.194s passed
seqDef_induction_upper_concrete data()[167] 3.192s passed
seqDef_induction_lower data()[168] 3.209s passed
seqDef_induction_lower_concrete data()[169] 3.190s passed
jdiv_one data()[16] 3.213s passed
seqDef_split_in_three data()[170] 3.272s passed
seqDef_empty data()[171] 3.150s passed
seqDef_one_summand data()[172] 3.158s passed
seqDef_lower_equals_upper data()[173] 3.129s passed
seqDefOfSeq data()[174] 3.161s passed
seqSelfDefinitionEQ2 data()[175] 3.145s passed
indexOfSeqSingleton data()[176] 3.150s passed
indexOfSeqConcatFirst data()[177] 3.151s passed
indexOfSeqConcatSecond data()[178] 3.163s passed
indexOfSeqSub data()[179] 3.187s passed
div_zero data()[17] 3.317s passed
lenOfArray2seq data()[180] 3.168s passed
getAnyOfArray2seq data()[181] 3.173s passed
getOfArray2seq data()[182] 3.144s passed
getAnyOfNPermInv data()[183] 3.151s passed
seqNPermRange data()[184] 3.248s passed
seqPermTrans data()[185] 3.204s passed
seqPermRefl data()[186] 3.198s passed
seqPermSplit data()[187] 3.198s passed
seqNPermRight data()[188] 3.365s passed
seqPermFromSwap data()[189] 3.189s passed
divResZero1 data()[18] 3.185s passed
seqPermTransAlt0 data()[190] 3.148s passed
seqPermTransAlt1 data()[191] 3.150s passed
seqPermTransAlt2 data()[192] 3.145s passed
seqPermTransAlt3 data()[193] 3.129s passed
seqPermForall data()[194] 3.261s passed
seqPermExists data()[195] 3.234s passed
schiffl_lemma_2 data()[196] 20.811s passed
schiffl_thm_1 data()[197] 3.792s passed
eqSameSeq data()[198] 3.214s passed
divResZero2 data()[19] 3.223s passed
eqTermCut data()[1] 4.046s passed
divResOne1 data()[20] 3.209s passed
divResOne2 data()[21] 3.249s passed
div_cancel1 data()[22] 3.232s passed
div_cancel2 data()[23] 3.175s passed
divAddMultDenom data()[24] 3.216s passed
divMinus data()[25] 3.222s passed
divMinusDenom data()[26] 3.198s passed
divLeastDPos data()[27] 3.169s passed
divLeastDNeg data()[28] 3.158s passed
divGreatestDPos data()[29] 3.160s passed
equivAllRight data()[2] 3.607s passed
divGreatestDNeg data()[30] 3.168s passed
divIncreasingPos data()[31] 3.195s passed
divIncreasingNeg data()[32] 3.168s passed
jdiv_zero data()[33] 3.155s passed
jdivPulloutMinusNum data()[34] 3.199s passed
jdivPulloutMinusDenom data()[35] 3.210s passed
jdiv_uniquePosPos data()[36] 3.207s passed
jdiv_uniquePosNeg data()[37] 3.246s passed
jdiv_uniqueNegPos data()[38] 3.253s passed
jdiv_uniqueNegNeg data()[39] 3.269s passed
irrflConcrete1 data()[3] 3.410s passed
jdivMultDenom1 data()[40] 3.275s passed
jdivMultDenom2 data()[41] 3.220s passed
mod_geZero data()[42] 3.158s passed
mod_lessDenom data()[43] 3.194s passed
jmod_NumPos data()[44] 3.157s passed
jmod_NumNeg data()[45] 3.198s passed
jmod_geZero data()[46] 3.174s passed
jmodNumZero data()[47] 3.156s passed
jmod_pulloutminusNum data()[48] 3.148s passed
jmod_pulloutminusDenom data()[49] 3.149s passed
irrflConcrete2 data()[4] 3.316s passed
jmodUnique1 data()[50] 3.205s passed
jmodUnique2 data()[51] 3.233s passed
intDivRem data()[52] 3.159s passed
jmodjmod data()[53] 3.171s passed
jmodDivisible data()[54] 3.165s passed
jmodDivisibleRep data()[55] 3.129s passed
jdivAddMultDenom data()[56] 3.265s passed
jmodAltZero data()[57] 3.145s passed
jmodAddMultDenomZero data()[58] 3.183s passed
polyDiv_zero data()[59] 3.174s passed
cancel_gtPos data()[5] 3.320s passed
polyMod_ltdivDenom data()[60] 3.141s passed
bsum_empty data()[61] 3.130s passed
bsum_induction_upper data()[62] 3.131s passed
bsum_induction_lower data()[63] 3.154s passed
bsum_num_of_bounds data()[64] 3.150s passed
bsum_num_of_bounds2 data()[65] 3.169s passed
bsum_induction_upper2 data()[66] 3.131s passed
bsum_induction_upper_concrete data()[67] 3.133s passed
bsum_induction_upper_concrete_2 data()[68] 3.135s passed
bsum_induction_upper2_concrete data()[69] 3.127s passed
cancel_gtNeg data()[6] 3.332s passed
bsum_induction_lower_concrete data()[70] 3.128s passed
bsum_induction_lower2 data()[71] 3.127s passed
bsum_induction_lower2_concrete data()[72] 3.125s passed
bsum_positive data()[73] 3.209s passed
bsum_upper_bound data()[74] 3.181s passed
bsum_lower_bound data()[75] 3.204s passed
bsum_positive_lower_bound_element data()[76] 3.204s passed
bsum_sub_same_index data()[77] 3.166s passed
bsum_less_same_index data()[78] 3.211s passed
bsum_equal_except_one_index data()[79] 3.171s passed
moduloIntIsInInt data()[7] 3.259s passed
bsum_num_of_is_max data()[80] 3.150s passed
bsum_num_of_is_max2 data()[81] 3.150s passed
bsum_num_of_is_max3 data()[82] 3.154s passed
bsum_num_of_is_max4 data()[83] 3.165s passed
bsum_num_of_lt_max data()[84] 3.156s passed
bsum_num_of_lt_max2 data()[85] 3.151s passed
bsum_num_of_lt_max3 data()[86] 3.158s passed
bsum_num_of_lt_max4 data()[87] 3.157s passed
bsum_num_of_gt0 data()[88] 3.177s passed
bsum_num_of_gt0_alt data()[89] 3.236s passed
moduloLongIsInLong data()[8] 3.240s passed
bsum_add_concrete data()[90] 3.172s passed
bprod_all_positive data()[91] 3.152s passed
bprod_split data()[92] 3.182s passed
powConcrete0 data()[93] 3.138s passed
powConcrete1 data()[94] 3.130s passed
powSplitFactor data()[95] 3.141s passed
powAdd data()[96] 3.138s passed
powMono data()[97] 3.142s passed
powMonoConcrete data()[98] 3.135s passed
powMonoConcreteRight data()[99] 3.127s passed
moduloShortIsInShort data()[9] 3.230s passed

Standard output

292        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
312        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.03ms 
505        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519        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)

1327       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1361       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1362       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1362       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2547       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7561       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.06s 
7627       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7657       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.6ns 
7669       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7670       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.6ns 
7673       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10644      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
10646      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11704      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.49ms 
11720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.2ns 
11722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
14439      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15323      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 
15326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15326      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.2ns 
15330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
17925      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18735      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
18736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
18739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
21249      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22051      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
22054      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.6ns 
22055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24509      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
24510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25371      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.05ms 
25373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25374      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.5ns 
25375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
27849      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28682      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28703      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.13ms 
28706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.8ns 
28707      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
31135      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31963      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.9ns 
31966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.2ns 
31969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34392      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
34393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35204      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588ns 
35206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.9ns 
35208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
37612      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
38436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.5ns 
38439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40919      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
40920      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41737      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.6ns 
41738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41738      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.6ns 
41739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
44172      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44969      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.1ns 
44970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
44971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
47363      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48293      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.08ms 
48299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
48301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
50800      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51669      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.42ms 
51679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51680      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 531.8ns 
51681      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54090      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
54090      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55005      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.2ms 
55006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
55007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57415      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
57415      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58208      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
58209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.1ns 
58211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
60620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61421      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
61423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61424      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.7ns 
61425      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
63882      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64739      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.13ms 
64741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320ns 
64742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67125      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
67126      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67924      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.12ms 
67926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
67927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70369      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
70370      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71147      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.06ms 
71149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.8ns 
71151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
73578      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74357      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.48ms 
74358      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74358      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.4ns 
74359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76824      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
76824      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77605      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
77607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
77608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
80045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80837      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22ms 
80839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80839      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
80840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83244      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
83244      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84012      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
84015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84015      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.9ns 
84016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86407      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
86407      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87228      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.47ms 
87230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
87231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
89611      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90450      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.31ms 
90452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.9ns 
90453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
92825      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93649      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.9ms 
93650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
93651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
96029      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96816      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
96820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 680.1ns 
96821      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99187      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
99187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99963      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99976      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
99978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
99978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
102349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.42ms 
103138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
103139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
105518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
106306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 
106307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
108691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
109501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.6ns 
109502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
111877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
112669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
112669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
115035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
115829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.2ns 
115830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
118228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.42ms 
119027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.6ns 
119028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
121405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.24ms 
122237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.6ns 
122238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
124647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.01ms 
125444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
125445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
127901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
128671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
128688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.05ms 
128690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
128690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
128691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
131139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
131919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
131941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.19ms 
131943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
131943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.6ns 
131943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
134422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
135194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
135210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.78ms 
135212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
135212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
135213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
137664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.02ms 
138492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.4ns 
138493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
140921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
141711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
141712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
144086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
144863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
144867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
144868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
144868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
144869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
147264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
148062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
148063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
150433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
151210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
151218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
151219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
151219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
151220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
153600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
154377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
154410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.88ms 
154418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
154418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.4ns 
154419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
156798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
157582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
157591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 
157592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
157592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
157593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
159960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
160749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.1ns 
160750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
163114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
163890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
163894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
163896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
163897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 
163897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
166252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
167038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
167043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
167045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
167045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.4ns 
167046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
169409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
170186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
170248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.06ms 
170250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
170250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
170251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
172620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
173407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
173481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.48ms 
173483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
173483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.5ns 
173484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
175856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
176636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
176640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
176642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
176642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.9ns 
176643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
179006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.28ms 
179814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.8ns 
179815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
182194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
182948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
182976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.33ms 
182977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
182977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
182978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
185349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
186103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
186106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
186107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
186107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
186108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
188486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
189239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
189370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 119.24ms 
189372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
189372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.3ns 
189373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
191750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
192517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
192517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
194916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
195700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
195700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
198072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
198858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
198873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.19ms 
198874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
198874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
198875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
201231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
202002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
202013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
202015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
202015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
202015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
204370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
205141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
205144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
205145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
205145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
205146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
207496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
208270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
208274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
208276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
208276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
208276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
210634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
211408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.34ms 
211430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
211431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
213788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
214580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
214581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
216935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
217733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
217748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
217749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
217749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
217750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
220102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
220875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
220878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
220879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
220879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
220880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
223234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
224007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
224011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
224013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
224013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
224013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
226364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
227141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
227146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
227147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
227148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
227148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
229498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
230271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
230274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
230275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
230275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
230276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
232626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
233399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
233401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.1ns 
233403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
233403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
233403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
235771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
236525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
236528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
236529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
236529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
236530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
238898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
239651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
239653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 927.7ns 
239654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
239654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
239655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
242058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
242811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
242861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.59ms 
242864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
242864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
242865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
245259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
246012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
246043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.9ms 
246045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
246045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
246045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
248466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
249219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
249247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.12ms 
249248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
249248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
249249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
251630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
252384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
252451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.6ms 
252453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
252453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.9ns 
252454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
254805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
255588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
255617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.51ms 
255619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
255619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
255619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
258005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
258781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
258828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.74ms 
258830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
258830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
258831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
261197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
261973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
261999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.37ms 
262000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
262000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
262001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
264358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
265131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
265149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.81ms 
265151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
265151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
265151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
267500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
268275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
268299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.85ms 
268301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
268301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
268301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
270656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
271431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
271454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.29ms 
271455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
271456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
271457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
273814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
274591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
274618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
274619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
274619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
274620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
276975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
277751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
277774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.84ms 
277776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
277776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
277776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
280129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
280902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
280926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.43ms 
280927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
280927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
280928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
283278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
284060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
284084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.01ms 
284085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
284085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
284086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
286459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
287218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
287240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.06ms 
287241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
287242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
287242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
289622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
290389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
290417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms 
290419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
290419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
290420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
292868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
293629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
293653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.54ms 
293654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
293655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
293655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
296055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
296817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
296825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
296826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
296826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
296827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
299206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
299961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
299977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ms 
299979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
299979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
299979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
302372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
303156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
303159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
303161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
303161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
303161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
305521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
306296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
306298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.6ns 
306299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
306299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
306300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
308652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
309426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
309428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 660.2ns 
309429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
309429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
309430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
311783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
312561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
312568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
312570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
312570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
312570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
314924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
315700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
315706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
315708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
315708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.5ns 
315709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
318062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
318837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
318849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.41ms 
318850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
318850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
318850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
321206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
321980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
321983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
321984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
321984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
321985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
324335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
325109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
325111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 542.1ns 
325112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
325112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
325113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
327465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
328241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
328249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
328251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
328251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.5ns 
328252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
330607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
331384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
331386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.1ns 
331387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
331387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
331388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
333742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
334515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
334517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.1ns 
334519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
334519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
334519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
336891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
337669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
337671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.8ns 
337672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
337673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
337673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
340026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
340803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
340806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
340807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
340807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
340808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
343172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
343960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
343969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.19ms 
343971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
343971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
343972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
346411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
347172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
347176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
347177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
347177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
347177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
349567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
350323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
350330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
350331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
350331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
350332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
352708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
353464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
353468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
353469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
353469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
353470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
355865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
356651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
356669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.06ms 
356670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
356670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
356671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
359112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
359872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
359875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
359876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
359876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
359877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
362251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
363007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
363010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
363011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
363011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
363012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
365384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
366164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
366167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
366168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
366168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
366169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
368527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
369303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
369319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
369320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
369321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
369321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
371682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
372463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
372467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 454.5ns 
372469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
372469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.9ns 
372470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
374824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
375615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
375656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36ms 
375657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
375657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
375658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
378095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
378890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
378893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
378894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
378894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
378895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
381264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
382039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
382060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms 
382062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
382062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.2ns 
382063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
384416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
385197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
385218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.56ms 
385219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
385219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
385219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
387576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
388352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
388375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.42ms 
388377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
388377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
388377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
390730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
391517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
391519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.9ns 
391521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
391521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
391521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
393906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
394684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
394690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
394691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
394691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
394692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
397062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
397854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
397857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
397859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
397859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.3ns 
397860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
400245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
401029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
401032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.5ns 
401033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
401033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
401033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
403404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
404187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
404189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.7ns 
404191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
404191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
404191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
406579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
407344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
407347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
407348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
407348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
407349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
409733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
410500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
410502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
410503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
410503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
410504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
412891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
413656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
413665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ms 
413667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
413667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
413667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
416047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
416808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
416820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
416821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
416821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
416822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
419196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
419979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
419991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
419993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
419993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
419994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
422365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
423150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
423161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.59ms 
423162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
423162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
423163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
425560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
426355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
426360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.79ms 
426361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
426361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
426362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
428733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
429519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
429525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
429526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
429526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
429527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
431872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
432659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
432661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.8ns 
432663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
432663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
432663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
435073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
435859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
435861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
435863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
435863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
435863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
438239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
439004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
439006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 737.5ns 
439007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
439007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
439007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
441381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
442173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
442184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
442185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
442185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
442186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
444567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
445360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
445364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
445365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
445365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
445366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
447735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
448518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
448524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
448525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
448526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
448526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
450895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
451680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
451682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.9ns 
451683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
451683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
451683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
454072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
454851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
454854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.9ns 
454855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
454855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
454856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
457276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
458046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
458050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
458051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
458051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
458051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
460426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
461209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
461212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
461213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
461213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
461214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
463575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
464360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
464362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
464363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
464364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.2ns 
464364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
466713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
467531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
467534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
467535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
467535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
467536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
469912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
470674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
470679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
470681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
470681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
470681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
473050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
473834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
473836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
473838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
473838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
473838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
476184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
476966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
476976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.54ms 
476977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
476978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
476978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
479338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
480120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
480121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.4ns 
480122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
480122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 42.3ns 
480123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
482509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
483273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
483280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.01ms 
483281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
483281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
483282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
485672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
486469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
486471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 855.8ns 
486472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
486472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
486473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
488870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
489656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
489658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.9ns 
489659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
489659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
489660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
492026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
492809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
492822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.84ms 
492823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
492823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
492824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
495256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
496039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
496042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
496043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
496043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
496043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
498392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
499175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
499178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
499179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
499180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
499180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
501530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
502315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
502319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
502320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
502320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns 
502320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
504690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
505474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
505478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
505479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
505479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
505480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
507858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
508653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
508668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.87ms 
508669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
508669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
508670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
511096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
511883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
511900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.57ms 
511905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
511906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.6ns 
511907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
514318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
515106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
515116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.69ms 
515117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
515117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
515118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
517495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
518290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
518301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
518303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
518303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
518303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
520674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
521438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
521464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.92ms 
521465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
521465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
521466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
523833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
524615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
524640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.06ms 
524642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
524642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
524642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
527009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
527771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
527795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ms 
527796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
527796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
527797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
530166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
530947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
530962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.37ms 
530963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
530963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
530964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
533309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
534097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
534127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.31ms 
534128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
534128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
534129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
536492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
537273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
537320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.38ms 
537321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
537321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
537322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
539684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
540471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
540512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.48ms 
540513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
540513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
540514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
542895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
543679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
543721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.18ms 
543722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
543723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.8ns 
543723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
546082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
546867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
546911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.02ms 
546912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
546912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
546913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
549282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
550063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
550183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.43ms 
550185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
550185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
550185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
552536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
553322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
553332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
553335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
553335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.7ns 
553336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
555702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
556484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
556492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
556493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
556493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
556493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
558835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
559615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
559620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
559621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
559621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
559622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
561983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
562764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
562781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
562783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
562783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
562783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
565153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
565916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
565927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
565928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
565928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
565929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
568294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
569074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
569077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
569078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
569078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
569078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
571448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
572210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
572227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 
572228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
572228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
572229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
574593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
575375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
575391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
575392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
575392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
575392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
577763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
578557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
578577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.96ms 
578578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
578578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
578579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
580958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
581743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
581745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
581746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
581746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
581747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
584132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
584915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
584919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
584920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
584920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
584920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
587293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
588057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
588063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
588064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
588064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
588064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
590426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
591208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
591213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
591214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
591214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
591215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
593588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
594388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
594461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.31ms 
594462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
594462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
594463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
596865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
597635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
597665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.91ms 
597666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
597666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
597667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
600056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
600841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
600863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.35ms 
600865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
600865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
600865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
603266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
604060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
604062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 247.7ns 
604063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
604063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.6ns 
604064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
606431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
607222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
607426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.27ms 
607428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
607428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
607428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
609781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
610565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
610615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.33ms 
610616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
610616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
610617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
612980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
613762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
613764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 292ns 
613766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
613766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.5ns 
613767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
616130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
616912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
616914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 307.2ns 
616915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
616915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
616915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
619274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
620057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
620059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 309ns 
620060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
620060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 41.8ns 
620060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
622405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
623185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
623187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 435.1ns 
623188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
623188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
623189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
625554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
626335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
626431     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
626448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 111.64ms 
626451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
626451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
626452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
628832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
629615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
629681     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
629682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.36ms 
629683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
629683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
629685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
632073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
632856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
632857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
632880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
632912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
632927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
632930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
632935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
632938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
632938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
632940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
632943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
632944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
632946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
632947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
633098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
633099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
633100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
633102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
633103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
633207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
633208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
633209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
633211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
633212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
633213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
633382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
633384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
633386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
633387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
633389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
633392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
633514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
633516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
633517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
633518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
633519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
633521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
633528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
633529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
633529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
633532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
633534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
633535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
633543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
633544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
633545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
633546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
633549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
633550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
633668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
633669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
633671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
633780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
633781     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)'' 
633784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
633785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
633786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
633788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
633789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
633791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
633794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
633796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
633798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
633799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
633799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
633898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
633901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
633903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
633903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
633904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
633905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
633906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
634023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
634024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
634025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
634027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
634028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
634029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
634030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
634033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
634122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
634124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
634204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
634207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
634213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
634214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
634217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
634219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
634220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
634220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
634221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
634222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
634238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
634242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
634344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
634345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
634346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
634347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
634348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
634348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
634348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
634349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
634399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
634403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
634485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
634487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
634489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
634490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
634491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
634491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
634597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
634601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
634602     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)'' 
634603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
634604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
634605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
634605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
634606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
634612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
634614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
634615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
634615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
634695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
634696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
634697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
634697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
634698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
634699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
634789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
634790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
634791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
634792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
634793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
634793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
634794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
634795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
634869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
634870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
634938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
634938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
634939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
634942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
634946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
634949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
635060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
635061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
635062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
635063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
635072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
635196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
638518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
638519     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)'' 
638525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
638526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
638526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
638527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
638528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
638535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
638536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
638537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
638538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
638539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
638626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
638630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
638631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
638631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
638632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
638633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
638633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
638722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
638723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
638724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
638725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
638726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
638726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
638727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
638728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
638801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
638802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
638878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
638882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
638886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
638887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
638887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
638888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
638898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
638975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
638977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
638978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
638981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
639062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
639071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
639072     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)'' 
639074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
639074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
639075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
639075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
639076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
639086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
639087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
639089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
639089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
639090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
639175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
639177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
639178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
639179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
639180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
639269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
639274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
639275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
639276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
639276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
639277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
639277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
639414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
639416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
639416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
639418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
639418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
639419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
639420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
639422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
639423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
639423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
639424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
639425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
639425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
639426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
639427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
639507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
639508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
639513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
639585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
639659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
639660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
639661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
639662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
639663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
639663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
639664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
639664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
639665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
639744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
639750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
639832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
639833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
639834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
639835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
639836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
639836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
639837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
639837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
639842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
639843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
639917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
639921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
639926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
640017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
640018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
640019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
640020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
640021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
640021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
640021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
640022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
640072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
640073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
640074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
640074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
640075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
640080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
640084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
640192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
640274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
640275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
640276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
640277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
640434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
640515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
640516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
643351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
643357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
643358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
643359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
643359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
643467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
643468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
643469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
643470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
643471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
643568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
646313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
649279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
649284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
649285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
649286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
649286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
649394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
649396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
649397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
649398     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)' ...' 
649399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
650495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
650495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
650496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
652924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
653731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
653732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
653732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
653738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
653749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
653751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
653753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
653754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
653757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
653759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
653761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
653764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
653765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
653772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
653774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
653774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
653816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
653816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
653817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
653817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
653818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
653879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
653879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
653881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
653881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
653882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
653885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
653886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
653886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
653887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
653888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
653888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
653957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
653958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
653958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
653959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
653960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
653960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
654022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
654022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
654023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
654023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
654024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
654025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
654025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
654026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
654026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
654027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
654027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
654027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
654028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
654028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
654029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
654029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
654030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
654030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
654031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
654033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
654060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
654061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
654101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
654102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
654103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
654104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
654105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
654105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
654144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
654146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
654146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
654148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
654149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
654150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
654151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
654188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
654190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
654193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
654239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
654286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
654286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
654287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
656663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
657467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
657499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.81ms