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

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

tests
0

failures
0

ignored
14m17.32s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.104s passed
powPositiveConcrete data()[101] 4.104s passed
powGeq1Concrete data()[102] 4.112s passed
pow2InIntLower data()[103] 4.163s passed
pow2InIntUpper data()[104] 4.177s passed
logSelfConcrete data()[105] 4.146s passed
log1Concrete data()[106] 4.119s passed
logProduct data()[107] 4.127s passed
logTimesBaseConcrete data()[108] 4.117s passed
logProdIdentity data()[109] 4.135s passed
moduloByteIsInByte data()[10] 4.313s passed
logProdIdentityConcrete data()[110] 4.152s passed
logPowIdentity data()[111] 4.126s passed
logPowIdentityConcrete data()[112] 4.128s passed
logPositive data()[113] 4.138s passed
logPositiveConcrete data()[114] 4.137s passed
logMono data()[115] 4.170s passed
logMonoConcrete data()[116] 4.162s passed
powLogLess data()[117] 4.252s passed
powLogMore2 data()[118] 4.153s passed
logLessThanPow data()[119] 4.175s passed
moduloCharIsInChar data()[11] 4.187s passed
logLessThanPowConcrete data()[120] 4.146s passed
logSqueeze data()[121] 4.177s passed
ifthenelse_equals data()[122] 4.117s passed
ifthenelse_equals_1 data()[123] 4.164s passed
ifthenelse_equals_2 data()[124] 4.124s passed
disjointWithSingleton1 data()[125] 4.170s passed
disjointWithSingleton2 data()[126] 4.138s passed
disjointArrayRanges data()[127] 4.171s passed
disjointArrayRangeAllFields1 data()[128] 4.146s passed
disjointArrayRangeAllFields2 data()[129] 4.159s passed
div_unique1 data()[12] 4.574s passed
seqSelfDefinition data()[130] 4.197s passed
seqOutsideValue data()[131] 4.132s passed
castedGetAny data()[132] 4.141s passed
seqGetAlphaCast data()[133] 4.082s passed
getOfSeqSingleton data()[134] 4.146s passed
getOfSeqSingletonConcrete data()[135] 4.113s passed
getOfSeqConcat data()[136] 4.169s passed
getOfSeqSub data()[137] 4.126s passed
getOfSeqReverse data()[138] 4.108s passed
lenOfSeqEmpty data()[139] 4.151s passed
div_unique2 data()[13] 4.328s passed
lenOfSeqSingleton data()[140] 4.124s passed
lenOfSeqConcat data()[141] 4.157s passed
lenOfSeqSub data()[142] 4.121s passed
lenOfSeqReverse data()[143] 4.191s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.223s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.156s passed
getOfSeqSingletonEQ data()[146] 4.130s passed
getOfSeqConcatEQ data()[147] 4.137s passed
getOfSeqSubEQ data()[148] 4.121s passed
getOfSeqReverseEQ data()[149] 4.109s passed
div_exists data()[14] 4.520s passed
lenOfSeqEmptyEQ data()[150] 4.154s passed
lenOfSeqSingletonEQ data()[151] 4.133s passed
lenOfSeqConcatEQ data()[152] 4.138s passed
lenOfSeqSubEQ data()[153] 4.077s passed
lenOfSeqReverseEQ data()[154] 4.096s passed
getOfSeqDefEQ data()[155] 4.093s passed
lenOfSeqDefEQ data()[156] 4.104s passed
seqConcatWithSeqEmpty1 data()[157] 4.101s passed
seqConcatWithSeqEmpty2 data()[158] 4.139s passed
seqReverseOfSeqEmpty data()[159] 4.156s passed
div_one data()[15] 4.193s passed
subSeqComplete data()[160] 4.147s passed
subSeqTailR data()[161] 4.171s passed
subSeqTailL data()[162] 4.150s passed
subSeqTailEQR data()[163] 4.154s passed
subSeqTailEQL data()[164] 4.183s passed
seqDef_split data()[165] 4.236s passed
seqDef_induction_upper data()[166] 4.163s passed
seqDef_induction_upper_concrete data()[167] 4.149s passed
seqDef_induction_lower data()[168] 4.243s passed
seqDef_induction_lower_concrete data()[169] 4.219s passed
jdiv_one data()[16] 4.186s passed
seqDef_split_in_three data()[170] 4.355s passed
seqDef_empty data()[171] 4.162s passed
seqDef_one_summand data()[172] 4.194s passed
seqDef_lower_equals_upper data()[173] 4.205s passed
seqDefOfSeq data()[174] 4.124s passed
seqSelfDefinitionEQ2 data()[175] 4.207s passed
indexOfSeqSingleton data()[176] 4.075s passed
indexOfSeqConcatFirst data()[177] 4.093s passed
indexOfSeqConcatSecond data()[178] 4.134s passed
indexOfSeqSub data()[179] 4.108s passed
div_zero data()[17] 4.216s passed
lenOfArray2seq data()[180] 4.058s passed
getAnyOfArray2seq data()[181] 4.027s passed
getOfArray2seq data()[182] 4.127s passed
getAnyOfNPermInv data()[183] 4.106s passed
seqNPermRange data()[184] 4.140s passed
seqPermTrans data()[185] 4.167s passed
seqPermRefl data()[186] 4.340s passed
seqPermSplit data()[187] 4.272s passed
seqNPermRight data()[188] 4.433s passed
seqPermFromSwap data()[189] 4.335s passed
divResZero1 data()[18] 4.227s passed
seqPermTransAlt0 data()[190] 4.191s passed
seqPermTransAlt1 data()[191] 4.116s passed
seqPermTransAlt2 data()[192] 4.234s passed
seqPermTransAlt3 data()[193] 4.095s passed
seqPermForall data()[194] 4.302s passed
seqPermExists data()[195] 4.232s passed
schiffl_lemma_2 data()[196] 30.841s passed
schiffl_thm_1 data()[197] 5.325s passed
eqSameSeq data()[198] 4.460s passed
divResZero2 data()[19] 4.260s passed
eqTermCut data()[1] 5.304s passed
divResOne1 data()[20] 4.179s passed
divResOne2 data()[21] 4.205s passed
div_cancel1 data()[22] 4.230s passed
div_cancel2 data()[23] 4.131s passed
divAddMultDenom data()[24] 4.293s passed
divMinus data()[25] 4.258s passed
divMinusDenom data()[26] 4.217s passed
divLeastDPos data()[27] 4.219s passed
divLeastDNeg data()[28] 4.189s passed
divGreatestDPos data()[29] 4.158s passed
equivAllRight data()[2] 4.758s passed
divGreatestDNeg data()[30] 4.234s passed
divIncreasingPos data()[31] 4.157s passed
divIncreasingNeg data()[32] 4.126s passed
jdiv_zero data()[33] 4.140s passed
jdivPulloutMinusNum data()[34] 4.236s passed
jdivPulloutMinusDenom data()[35] 4.191s passed
jdiv_uniquePosPos data()[36] 4.197s passed
jdiv_uniquePosNeg data()[37] 4.284s passed
jdiv_uniqueNegPos data()[38] 4.347s passed
jdiv_uniqueNegNeg data()[39] 4.261s passed
irrflConcrete1 data()[3] 4.479s passed
jdivMultDenom1 data()[40] 4.302s passed
jdivMultDenom2 data()[41] 4.117s passed
mod_geZero data()[42] 4.161s passed
mod_lessDenom data()[43] 4.140s passed
jmod_NumPos data()[44] 4.148s passed
jmod_NumNeg data()[45] 4.155s passed
jmod_geZero data()[46] 4.136s passed
jmodNumZero data()[47] 4.095s passed
jmod_pulloutminusNum data()[48] 4.182s passed
jmod_pulloutminusDenom data()[49] 4.117s passed
irrflConcrete2 data()[4] 4.407s passed
jmodUnique1 data()[50] 4.232s passed
jmodUnique2 data()[51] 4.322s passed
intDivRem data()[52] 4.158s passed
jmodjmod data()[53] 4.181s passed
jmodDivisible data()[54] 4.198s passed
jmodDivisibleRep data()[55] 4.106s passed
jdivAddMultDenom data()[56] 4.367s passed
jmodAltZero data()[57] 4.152s passed
jmodAddMultDenomZero data()[58] 4.182s passed
polyDiv_zero data()[59] 4.177s passed
cancel_gtPos data()[5] 4.447s passed
polyMod_ltdivDenom data()[60] 4.139s passed
bsum_empty data()[61] 4.128s passed
bsum_induction_upper data()[62] 4.080s passed
bsum_induction_lower data()[63] 4.229s passed
bsum_num_of_bounds data()[64] 4.165s passed
bsum_num_of_bounds2 data()[65] 4.163s passed
bsum_induction_upper2 data()[66] 4.171s passed
bsum_induction_upper_concrete data()[67] 4.145s passed
bsum_induction_upper_concrete_2 data()[68] 4.108s passed
bsum_induction_upper2_concrete data()[69] 4.143s passed
cancel_gtNeg data()[6] 4.337s passed
bsum_induction_lower_concrete data()[70] 4.125s passed
bsum_induction_lower2 data()[71] 4.100s passed
bsum_induction_lower2_concrete data()[72] 4.105s passed
bsum_positive data()[73] 4.223s passed
bsum_upper_bound data()[74] 4.268s passed
bsum_lower_bound data()[75] 4.198s passed
bsum_positive_lower_bound_element data()[76] 4.186s passed
bsum_sub_same_index data()[77] 4.216s passed
bsum_less_same_index data()[78] 4.256s passed
bsum_equal_except_one_index data()[79] 4.145s passed
moduloIntIsInInt data()[7] 4.273s passed
bsum_num_of_is_max data()[80] 4.182s passed
bsum_num_of_is_max2 data()[81] 4.211s passed
bsum_num_of_is_max3 data()[82] 4.166s passed
bsum_num_of_is_max4 data()[83] 4.173s passed
bsum_num_of_lt_max data()[84] 4.175s passed
bsum_num_of_lt_max2 data()[85] 4.149s passed
bsum_num_of_lt_max3 data()[86] 4.152s passed
bsum_num_of_lt_max4 data()[87] 4.126s passed
bsum_num_of_gt0 data()[88] 4.143s passed
bsum_num_of_gt0_alt data()[89] 4.180s passed
moduloLongIsInLong data()[8] 4.204s passed
bsum_add_concrete data()[90] 4.124s passed
bprod_all_positive data()[91] 4.129s passed
bprod_split data()[92] 4.172s passed
powConcrete0 data()[93] 4.092s passed
powConcrete1 data()[94] 4.108s passed
powSplitFactor data()[95] 4.232s passed
powAdd data()[96] 4.165s passed
powMono data()[97] 4.096s passed
powMonoConcrete data()[98] 4.136s passed
powMonoConcreteRight data()[99] 4.134s passed
moduloShortIsInShort data()[9] 4.180s passed

Standard output

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

2268       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2271       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2281       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2281       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4037       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.82s 
10996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11052      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.2ns 
11072      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.71ns 
11080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15077      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 
15085      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16323      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16361      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.8ms 
16380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16380      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.82ns 
16383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19957      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
19958      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21099      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21133      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.22ms 
21139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.61ns 
21142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
24566      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25616      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.08ms 
25620      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.62ns 
25622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
28931      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30020      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
30036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30037      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 902.64ns 
30039      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
33310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34470      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.19ms 
34475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34475      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.01ns 
34476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37746      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
37747      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.75ms 
38814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 518.12ns 
38816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
42034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
43085      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 969.55ns 
43089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
43089      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.72ns 
43090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
46241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47285      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
47289      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.34ns 
47292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
47293      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.42ns 
47294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
50481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
51467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
51470      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.74ns 
51473      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
51474      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.12ns 
51475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54768      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
54768      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
55783      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.53ns 
55786      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
55786      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.22ns 
55788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58924      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
58924      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
59970      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
59976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
59977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.62ns 
59978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
63489      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
64487      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
64547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.49ms 
64553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
64554      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 541.72ns 
64558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67729      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
67730      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
68765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
68877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.11ms 
68882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
68882      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.61ns 
68884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72082      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
72082      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
73096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
73396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 290.13ms 
73404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
73405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.92ns 
73407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
76588      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
77585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
77593      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
77597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
77597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.01ns 
77598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80760      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
80763      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
81775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
81781      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 
81785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
81785      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.12ns 
81787      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84906      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
84907      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
85926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
85998      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.19ms 
86001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
86002      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.01ns 
86003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89209      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
89209      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
90194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
90225      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.1ms 
90230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
90232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.41ms 
90233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
93437      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
94463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
94485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.02ms 
94488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
94488      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.91ns 
94490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97616      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
97617      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
98637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
98664      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.04ms 
98667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
98668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415.72ns 
98678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
101861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
102848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
102870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.39ms 
102872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
102873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 701.83ns 
102874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
106021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
107059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
107100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.9ms 
107102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
107102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.91ns 
107103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
110195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
111227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
111231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
111233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
111233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.41ns 
111234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
114425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
115417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
115524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 101ms 
115527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
115528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.02ns 
115529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
118650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
119663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
119777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.81ms 
119787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
119788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 435.12ns 
119789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
122905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
123930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
124000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.01ms 
124003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
124003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.31ns 
124004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
127176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
128198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
128219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.17ms 
128222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
128222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.41ns 
128224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
131377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
132389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
132409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.62ms 
132411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
132411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
132412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
135530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
136549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
136567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
136569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
136569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.01ns 
136570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
139763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
140789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
140800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.25ms 
140803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
140803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.71ns 
140804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
143919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
144940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
144957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
144961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
144962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.21ns 
144963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
148055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
149074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
149085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
149087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
149087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.91ns 
149088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
152207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
153218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
153225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
153228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
153229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.61ns 
153230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
156399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
157448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
157464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.63ms 
157465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
157465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.11ns 
157467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
160570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
161569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
161653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.39ms 
161656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
161656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.02ns 
161658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
164777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
165823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
165850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
165853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
165854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.61ns 
165855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
169049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
170109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
170135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.47ms 
170136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
170137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 559.12ns 
170140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
173406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
174456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
174482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.03ms 
174484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
174484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.3ns 
174485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
177707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
178717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
178743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.23ms 
178745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
178745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns 
178747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
181954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
182979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
183045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.07ms 
183047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
183047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.81ns 
183048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
186153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
187140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
187161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
187165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
187166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
187168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
190295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
191316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
191324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.28ms 
191326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
191326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
191327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
194436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
195450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
195464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.47ms 
195466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
195466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.41ns 
195467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
198610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
199597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
199612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.77ms 
199614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
199614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.2ns 
199615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
202738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
203738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
203767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.83ms 
203769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
203770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.51ns 
203771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
206864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
207887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
207903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
207907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
207907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.41ns 
207908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
211030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
211994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
211999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
212000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
212002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.37ms 
212003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
215140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
216175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
216181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
216182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
216183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
216183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
219285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
220290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
220298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
220300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
220300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
220301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
223425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
224400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
224529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 118.13ms 
224532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
224532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.81ns 
224534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
227690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
228708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
228852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 132.94ms 
228855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
228855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.61ns 
228856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
231964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
233001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
233009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
233013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
233013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.31ns 
233014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
236166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
237131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
237191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.15ms 
237194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
237195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 468.82ns 
237196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
240313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
241333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
241391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.14ms 
241393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
241394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.92ns 
241395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
244479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
245490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
245496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
245505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
245506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.61ns 
245507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
248637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
249615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
249870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 242.77ms 
249872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
249873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.41ns 
249874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
252981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
254000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
254022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.8ms 
254024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
254024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
254029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
257158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
258175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
258204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.45ms 
258208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
258208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.71ns 
258209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
261343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
262349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
262384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.16ms 
262385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
262385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
262386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
265495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
266496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
266520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.83ms 
266525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
266525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.91ns 
266526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
269651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
270646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
270651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
270652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
270652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
270653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
273750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
274725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
274731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
274733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
274733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
274734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
277906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
278919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
278960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.47ms 
278962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
278962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
278962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
282100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
283094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
283125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.28ms 
283126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
283126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
283127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
286288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
287262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
287288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
287290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
287290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
287291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
290428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
291453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
291459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
291462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
291463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.31ns 
291466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
294607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
295597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
295604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
295605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
295605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
295606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
298729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
299704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
299712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
299714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
299714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
299715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
302848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
303851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
303856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
303858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
303858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.91ns 
303859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
306976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
307977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
307980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
307982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
307982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
307983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
311098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
312074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
312080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
312081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
312082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 552.02ns 
312083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
315165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
316181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
316185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
316186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
316187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.01ns 
316187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
319297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
320321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
320408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.19ms 
320411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
320412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.81ns 
320413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
323574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
324553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
324675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 118.02ms 
324678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
324679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.91ns 
324680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
327779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
328811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
328874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.29ms 
328877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
328879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.44ms 
328880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
331982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
332981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
333059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.04ms 
333062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
333062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.81ns 
333063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
336189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
337225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
337276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.29ms 
337278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
337278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
337279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
340429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
341439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
341532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.19ms 
341534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
341535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.61ns 
341536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
344627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
345630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
345677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.66ms 
345679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
345679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
345680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
348806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
349825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
349859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.94ms 
349861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
349861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
349862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
352972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
354026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
354070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.86ms 
354072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
354072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.21ns 
354074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
357222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
358196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
358231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.92ms 
358239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
358239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.71ns 
358240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
361361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
362362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
362410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.89ms 
362411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
362411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
362413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
365540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
366541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
366585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.67ms 
366586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
366586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
366587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
369722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
370690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
370733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.27ms 
370735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
370735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
370736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
373846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
374845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
374885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.09ms 
374887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
374887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
374888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
377950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
378946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
379011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.99ms 
379013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
379013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
379014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
382133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
383102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
383154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.31ms 
383157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
383157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.01ns 
383158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
386285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
387283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
387334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.53ms 
387335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
387336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.31ns 
387336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
390430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
391446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
391458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.98ms 
391459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
391460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.8ns 
391460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
394568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
395555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
395587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.66ms 
395589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
395589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
395589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
398714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
399753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
399759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
399761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
399761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.62ns 
399762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
402849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
403848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
403851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
403853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
403853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
403854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
406977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
407956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
407959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
407961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
407961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
407962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
411137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
412180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
412191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
412194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
412194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.21ns 
412195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
415337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
416344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
416356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
416358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
416358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.31ns 
416359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
419462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
420432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
420452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.39ms 
420453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
420453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.61ns 
420454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
423588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
424583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
424588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
424589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
424590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.91ns 
424590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
427718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
428719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
428722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.56ns 
428724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
428724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.01ns 
428725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
431823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
432817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
432826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 
432828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
432828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.31ns 
432829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
435938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
436927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
436930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
436931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
436931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.81ns 
436932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
440032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
441039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
441042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
441044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
441044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.91ns 
441045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
444233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
445202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
445205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 912.26ns 
445207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
445207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.31ns 
445208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
448341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
449377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
449382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
449384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
449384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
449385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
452510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
453514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
453528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
453530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
453530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
453531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
456670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
457642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
457648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
457649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
457649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.31ns 
457650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
460749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
461763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
461774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
461776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
461776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
461776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
464881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
465878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
465888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
465893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
465894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.12ns 
465897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
469017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
470000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
470026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.15ms 
470027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
470027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.81ns 
470028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
473165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
474173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
474178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
474179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
474180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.71ns 
474180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
477304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
478299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
478304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
478305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
478306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.91ns 
478306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
481434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
482426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
482432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
482433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
482433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.31ns 
482434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
485525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
486541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
486570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.65ms 
486572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
486572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
486573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
489716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
490700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
490707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
490711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
490711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.11ns 
490712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
493816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
494815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
494876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.31ms 
494878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
494878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
494879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
498050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
499034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
499038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
499041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
499041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.61ns 
499042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
502195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
503258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
503291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.35ms 
503292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
503293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
503293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
506409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
507414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
507444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27ms 
507446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
507446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.41ns 
507447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
510558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
511575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
511619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.1ms 
511621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
511621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.71ns 
511622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
514743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
515762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
515765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723.44ns 
515768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
515768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.31ns 
515769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
518907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
519934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
519942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.99ms 
519944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
519944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
519945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
523035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
524055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
524060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
524061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
524061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.11ns 
524062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
527199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
528220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
528223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
528225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
528225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.81ns 
528226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
531342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
532344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
532347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
532349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
532349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
532350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
535497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
536512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
536517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
536518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
536518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
536519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
539636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
540651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
540655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
540657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
540657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
540658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
543798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
544810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
544826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.85ms 
544827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
544828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.71ns 
544828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
547937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
548951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
548968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
548975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
548976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 744.24ns 
548977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
552117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
553117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
553132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.41ms 
553134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
553134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
553135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
556285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
557302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
557329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.92ms 
557331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
557332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.32ns 
557333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
560429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
561455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
561461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.91ms 
561462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
561462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
561463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
564574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
565593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
565602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
565603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
565603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
565605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
568703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
569681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
569684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.64ns 
569685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
569686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
569686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
572809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
573826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
573830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
573832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
573832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
573832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
576898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
577940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
577943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
577945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
577945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.71ns 
577946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
581095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
582097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
582112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
582114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
582114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
582115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
585206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
586233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
586238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
586240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
586240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
586241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
589320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
590337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
590346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
590348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
590348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
590349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
593498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
594494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
594497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 966.35ns 
594500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
594501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.21ns 
594502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
597587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
598619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
598622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838.74ns 
598623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
598623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
598624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
601757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
602774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
602779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
602781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
602781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns 
602781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
605877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
606896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
606900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
606902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
606902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
606902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
610039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
611086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
611090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
611092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
611092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
611093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
614267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
615311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
615315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
615316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
615316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
615317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
618413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
619461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
619471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
619472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
619472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.51ns 
619473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
622558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
623597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
623600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
623602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
623602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
623603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
626718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
627720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
627737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.58ms 
627739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
627739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
627740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
630831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
631855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
631858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
631859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
631860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.01ns 
631860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
634922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
635956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
635967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
635969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
635969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.81ns 
635970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
639085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
640118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
640121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
640123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
640123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
640123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
643222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
644251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
644254     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
644256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
644256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
644256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
647371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
648384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
648391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
648394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
648394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.71ns 
648395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
651470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
652464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
652469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
652470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
652470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
652471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
655549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
656561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
656565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
656567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
656567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
656568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
659634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
660653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
660658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
660660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
660660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
660660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
663742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
664754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
664761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
664763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
664763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
664764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
667829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
668843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
668863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.42ms 
668865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
668865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.69ns 
668866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
671947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
672981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
673002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms 
673004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
673004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
673005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
676125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
677143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
677158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
677160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
677160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
677160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
680265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
681289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
681305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
681306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
681306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
681307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
684404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
685441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
685476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.16ms 
685478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
685478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
685479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
688566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
689593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
689627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.51ms 
689628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
689628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
689629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
692729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
693744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
693780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.29ms 
693782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
693782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
693783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
696903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
696904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
697943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
697963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.48ms 
697965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
697965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
697966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
701118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
702152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
702199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.13ms 
702201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
702201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
702202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
705282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
706296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
706362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.28ms 
706364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
706364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
706364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
709447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
710457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
710511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.41ms 
710512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
710512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
710513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
713654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
714696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
714754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.76ms 
714756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
714756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.81ns 
714757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
717867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
718908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
718973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.73ms 
718975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
718975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
718976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
722113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
723145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
723328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 174.73ms 
723330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
723330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.81ns 
723331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
726438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
727474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
727488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.77ms 
727492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
727492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.11ns 
727493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
730635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
731674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
731684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
731685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
731685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
731686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
734857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
735882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
735889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
735890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
735891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
735891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
738986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
739988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
740013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 
740014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
740014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
740016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
743182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
744203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
744220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
744221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
744221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
744222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
747271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
748291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
748296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
748297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
748297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
748298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
751371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
752364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
752388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.18ms 
752390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
752390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
752391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
755471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
756499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
756522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.36ms 
756523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
756524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
756524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
759594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
760603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
760630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.24ms 
760632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
760632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
760632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
763660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
764685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
764688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
764690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
764690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
764690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
767707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
768710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
768715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
768716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
768717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
768717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
771794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
772833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
772842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
772844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
772844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
772845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
775938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
776940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
776948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.08ms 
776949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
776949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
776951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
779981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
780987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
781088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.95ms 
781090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
781090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
781091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
784161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
785206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
785255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.05ms 
785258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
785258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.21ns 
785259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
788502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
789565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
789596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.08ms 
789598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
789598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
789598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
792824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
793866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
793868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 459.02ns 
793870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
793870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
793871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
796961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
797986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
798301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 301.69ms 
798303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
798304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.41ns 
798305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
801477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
802561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
802636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.37ms 
802638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
802638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
802639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
805774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
805774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
806824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
806827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 449.12ns 
806828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
806828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
806829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
809935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
810941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
810943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 779.24ns 
810945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
810945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
810946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
814158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
815175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
815177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 495.12ns 
815179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
815179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
815180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
818244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
819270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
819273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 771.23ns 
819274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
819274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
819275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
822393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
822393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
823427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
823537     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
823574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 143.82ms 
823576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
823577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.91ns 
823578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
826697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
827717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
827806     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
827807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.86ms 
827808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
827808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
827819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
830931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
831936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
831939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 
831973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
832023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
832045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
832051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
832058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
832062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
832063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
832066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
832070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
832073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
832076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
832077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
832341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
832342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
832343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
832345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
832346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
832507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
832509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
832510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
832512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
832514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
832515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
832744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
832745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
832746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
832747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
832748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
832749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
832952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
832954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
832955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
832956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
832957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
832958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
832967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
832968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
832969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
832971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
832973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
832974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
832982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
832983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
832984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
832986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
832986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
832988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
833183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
833185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
833186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
833343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
833345     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)'' 
833347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
833349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
833350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
833351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
833352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
833353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
833358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
833360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
833362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
833363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
833364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
833510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
833515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
833517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
833518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
833518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
833519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
833520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
833691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
833694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
833695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
833697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
833698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
833698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
833699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
833701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
833830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
833832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
833990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
833996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
834002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
834004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
834004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
834006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
834007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
834007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
834008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
834010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
834036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
834046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
834213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
834215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
834216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
834218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
834220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
834222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
834223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
834225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
834311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
834319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
834461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
834463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
834465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
834467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
834468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
834469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
834662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
834669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
834670     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)'' 
834673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
834676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
834677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
834679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
834680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
834693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
834700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
834702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
834703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
834856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
834858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
834859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
834859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
834861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
834862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
835040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
835042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
835043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
835045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
835046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
835047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
835048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
835049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
835168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
835170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
835327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
835327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
835328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
835333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
835338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
835343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
835515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
835517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
835517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
835519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
835532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
835650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
840574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
840579     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)'' 
840585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
840586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
840587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
840588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
840589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
840603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
840605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
840607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
840607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
840608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
840750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
840755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
840756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
840757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
840757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
840758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
840759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
840886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
840888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
840889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
840890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
840891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
840892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
840892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
840894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
841000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
841001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
841106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
841111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
841117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
841118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
841119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
841120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
841133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
841243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
841246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
841247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
841248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
841344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
841358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
841358     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)'' 
841360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
841361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
841362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
841363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
841363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
841379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
841380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
841381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
841382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
841383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
841507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
841509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
841510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
841511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
841512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
841635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
841641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
841642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
841643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
841643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
841644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
841644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
841786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
841787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
841788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
841790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
841790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
841791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
841791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
841793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
841794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
841795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
841796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
841796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
841797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
841797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
841798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
841924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
841925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
841935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
842044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
842156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
842158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
842159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
842159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
842161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
842161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
842162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
842162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
842163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
842279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
842287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
842408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
842409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
842410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
842411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
842411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
842412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
842412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
842413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
842420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
842421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
842530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
842538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
842546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
842727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
842728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
842729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
842730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
842730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
842731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
842731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
842732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
842805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
842806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
842808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
842808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
842809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
842820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
842827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
842981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
843097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
843099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
843100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
843101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
843321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
843438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
843439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
848005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
848011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
848013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
848013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
848014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
848164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
848166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
848167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
848168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
848169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
848309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
852514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
856880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
856885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
856886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
856887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
856888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
857037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
857039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
857040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
857041     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)' ...' 
857043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
858649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
858650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.81ns 
858650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
861896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
861896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
862975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
862977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
862977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
862984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
862998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
863001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
863003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
863004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
863009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
863010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
863014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
863016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
863018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
863030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
863032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
863032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
863098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
863100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
863100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
863101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
863102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
863198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
863199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
863201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
863202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
863202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
863207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
863208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
863208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
863210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
863211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
863212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
863327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
863328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
863329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
863331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
863332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
863332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
863462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
863463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
863464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
863465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
863465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
863467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
863467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
863468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
863469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
863470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
863471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
863471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
863472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
863473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
863473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
863474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
863475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
863476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
863477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
863481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
863542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
863545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
863649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
863660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
863664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
863665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
863666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
863667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
863741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
863744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
863746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
863748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
863749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
863750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
863751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
863820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
863823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
863827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
863897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
863975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
863975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.71ns 
863976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
867238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
868383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
868434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.78ms