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

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

tests
0

failures
0

ignored
10m45.47s

duration
100%

successful

Tests

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

Standard output

324        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
352        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.1ms 
602        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)

1639       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1640       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1643       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1643       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3083       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8784       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.18s 
8846       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8880       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ns 
8893       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8894       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 625.21ns 
8898       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11823      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
11826      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12789      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.33ms 
12799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12799      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.8ns 
12801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
15477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16350      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16363      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
16366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 429.1ns 
16368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
18946      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.36ms 
19830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19831      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.2ns 
19833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
22336      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23185      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
23188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.4ns 
23189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
25654      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26472      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.23ms 
26500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.7ns 
26501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
28950      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.42ms 
29767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388ns 
29769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
32224      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33005      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.4ns 
33008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.5ns 
33010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
35455      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.6ns 
36237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36238      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.2ns 
36239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38691      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
38691      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.3ns 
39482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39482      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.6ns 
39484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
41968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42742      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.3ns 
42745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.2ns 
42746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45162      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
45163      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45956      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.11ns 
45961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.7ns 
45962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
48395      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49206      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49240      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.07ms 
49255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.4ns 
49256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
51721      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.16ms 
52549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
52550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54974      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
54975      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55922      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.43ms 
55927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 488.1ns 
55928      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58317      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
58318      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59123      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
59132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.6ns 
59133      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61520      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
61521      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62333      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
62335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62335      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
62336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
64717      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65547      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.22ms 
65549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.2ns 
65551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
67926      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68723      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms 
68724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.1ns 
68725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71096      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
71096      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71886      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71897      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
71899      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71899      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns 
71900      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74281      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
74281      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75083      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
75086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75087      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.6ns 
75088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
77480      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78292      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
78294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
78295      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80670      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
80670      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81469      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
81470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81471      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
81471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
83855      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84637      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84641      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
84643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.7ns 
84645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87021      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
87021      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87837      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.45ms 
87838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87839      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.6ns 
87840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90212      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
90212      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91087      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.37ms 
91093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
91094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
93467      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94284      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.18ms 
94286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.4ns 
94287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
96655      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97418      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
97419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
97420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
99808      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.22ms 
100578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.8ns 
100578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
102963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
103731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
103731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
106118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
106881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
106882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
109262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
110018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
110024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
110025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
110025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
110026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
112433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
113201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
113202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
115579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
116363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
116364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
118731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
119523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
119524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
121882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.45ms 
122704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.3ns 
122705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
125075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
125870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.2ns 
125871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
128242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
129045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
129046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
131400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.42ms 
132193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
132194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
134553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
135331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
135345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.52ms 
135358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
135358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.8ns 
135359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
137747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.82ms 
138578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
138579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
140931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
141720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168ns 
141723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
144082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
144883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
144886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
144888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
144888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
144888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
147240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
148027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
148028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
150386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
151174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
151181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
151182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
151182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
151183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
153546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
154325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
154340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
154341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
154341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
154342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
156692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
157466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
157473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
157474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
157474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
157475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
159822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
160578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
160578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
162961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
163713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
163716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
163718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
163718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
163718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
166098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
166854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
166857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
166859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
166859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
166860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
169242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
169995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
170058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.38ms 
170064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
170064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326ns 
170066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
172442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
173196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
173263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.25ms 
173265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
173265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
173266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
175639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
176393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
176396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
176398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
176398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
176399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
178774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.25ms 
179557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.9ns 
179558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
181906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
182680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
182699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms 
182700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
182701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
182701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
185055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
185836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
185840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
185844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
185845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.2ns 
185846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
188194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
188976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
189070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.26ms 
189072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
189072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258ns 
189073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
191422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
192215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
192223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.22ms 
192224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
192225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.5ns 
192225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
194575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
195353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
195359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
195360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
195360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
195361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
197712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
198493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
198508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
198509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
198510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
198510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
200854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
201630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
201643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
201646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
201647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.8ns 
201647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
203982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
204752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
204755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
204757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
204757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.1ns 
204757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
207093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
207865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
207868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
207869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
207869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
207870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
210223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
210996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
211013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.95ms 
211016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
211016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.4ns 
211017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
213377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
214154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
214166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
214167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
214167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
214168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
216518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
217301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
217313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
217315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
217315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.4ns 
217316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
219661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
220434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
220436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.61ns 
220438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
220438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
220438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
222783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
223558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
223561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
223562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
223562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
223562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
225912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
226686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
226691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
226692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
226692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
226693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
229068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
229824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
229827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.51ns 
229828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
229828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
229829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
232194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
232945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
232947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540.9ns 
232948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
232948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
232949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
235318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
236069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
236073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
236074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
236074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
236075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
238448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
239199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
239202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.41ns 
239203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
239203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
239204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
241571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
242331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
242382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.26ms 
242384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
242385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
242386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
244767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
245519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
245544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.23ms 
245547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
245547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.5ns 
245548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
247892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
248669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
248690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.35ms 
248691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
248691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
248692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
251047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
251819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
251852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.82ms 
251854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
251854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
251855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
254196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
254981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
255001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ms 
255003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
255003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
255004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
257353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
258127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
258164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.48ms 
258165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
258165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
258166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
260523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
261296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
261315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.79ms 
261316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
261316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
261317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
263667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
264443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
264457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.79ms 
264458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
264458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
264459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
266809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
267586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
267601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.06ms 
267602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
267602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
267603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
269948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
270725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
270737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.01ms 
270739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
270739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
270740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
273092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
273867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
273884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.06ms 
273886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
273886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.8ns 
273887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
276241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
277021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
277036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ms 
277038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
277038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.3ns 
277039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
279392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
280168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
280185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
280186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
280186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
280187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
282536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
283318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
283333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
283334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
283334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
283335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
285691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
286466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
286480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
286481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
286481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
286482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
288836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
289610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
289627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
289628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
289628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
289629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
291984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
292760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
292776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
292777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
292778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
292778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
295137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
295915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
295928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
295930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
295930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.8ns 
295931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
298285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
299039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
299050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
299052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
299052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
299052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
301431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
302186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
302190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
302191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
302191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
302192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
304572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
305326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
305329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 740.21ns 
305330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
305330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
305331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
307691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
308445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
308447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.11ns 
308448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
308449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
308449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
310822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
311580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
311586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
311588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
311588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.6ns 
311589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
313953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
314707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
314712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
314714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
314714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.4ns 
314715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
317068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
317841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
317851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.36ms 
317852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
317852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
317853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
320194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
320975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
320978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
320979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
320979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
320980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
323322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
324103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
324105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 429.3ns 
324106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
324106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
324107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
326452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
327229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
327234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
327235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
327235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
327236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
329578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
330355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
330357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 575.2ns 
330358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
330358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
330359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
332705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
333484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
333486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 566.3ns 
333487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
333487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
333488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
335832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
336609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
336611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 481.8ns 
336612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
336612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
336613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
338961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
339738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
339742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
339744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
339744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 
339745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
342100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
342884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
342891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
342892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
342892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
342893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
345240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
346018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
346022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
346023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
346023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
346024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
348390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
349169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
349174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
349175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
349175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
349176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
351521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
352298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
352302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
352303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
352303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
352304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
354657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
355433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
355445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.65ms 
355446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
355446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
355447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
357792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
358568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
358571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
358573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
358573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
358573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
360934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
361687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
361689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
361691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
361691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
361691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
364077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
364832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
364836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
364837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
364837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
364838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
367214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
367967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
367980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
367981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
367981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
367982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
370353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
371106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
371110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.1ns 
371112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
371112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
371113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
373474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
374228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
374253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.38ms 
374255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
374255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.6ns 
374256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
376614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
377367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
377370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
377371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
377371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
377372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
379716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
380494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
380508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.65ms 
380510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
380511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.6ns 
380511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
382854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
383630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
383644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 
383645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
383645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
383646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
385995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
386770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
386787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
386788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
386788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
386789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
389138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
389912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
389914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 476.6ns 
389916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
389916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
389916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
392259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
393034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
393038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
393040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
393040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
393040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
395391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
396171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
396174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
396176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
396176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
396176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
398517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
399297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
399299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 774.71ns 
399300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
399300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
399301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
401642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
402421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
402423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.71ns 
402425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
402425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
402425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
404769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
405552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
405555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
405556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
405556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
405557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
407914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
408697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
408700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
408701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
408701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
408702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
411046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
411827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
411835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
411836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
411836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
411837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
414196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
414978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
414985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
414986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
414986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
414987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
417331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
418117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
418123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
418126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
418126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
418127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
420474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
421263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
421270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
421271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
421271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
421272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
423611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
424401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
424405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
424406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
424406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
424407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
426751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
427542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
427546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
427548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
427548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
427548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
429895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
430687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
430689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.91ns 
430691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
430691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49ns 
430691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
433036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
433827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
433830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 929.91ns 
433831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
433831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
433832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
436186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
436975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
436977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.81ns 
436979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
436979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
436979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
439331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
440121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
440130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ms 
440131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
440131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
440132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
442478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
443274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
443278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
443279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
443279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
443280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
445632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
446424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
446431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.06ms 
446433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
446433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
446433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
448780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
449570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
449572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.81ns 
449574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
449574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
449574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
451914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
452703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
452705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.8ns 
452706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
452706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
452707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
455052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
455839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
455842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
455844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
455844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
455844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
458183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
458972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
458974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.6ns 
458976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
458976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
458976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
461307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
462095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
462098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
462099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
462099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
462100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
464446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
465236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
465238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
465239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
465240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
465240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
467588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
468378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
468382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
468383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
468383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
468384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
470721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
471511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
471513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816.01ns 
471514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
471514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
471515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
473880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
474647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
474655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
474656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
474656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
474657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
477027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
477793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
477795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553.2ns 
477796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
477796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
477797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
480156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
480922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
480927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
480928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
480928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
480929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
483285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
484073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
484075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 805.71ns 
484077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
484077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
484077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
486419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
487207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
487209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 700.21ns 
487210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
487210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
487211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
489551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
490338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
490341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
490342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
490342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
490343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
492678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
493467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
493470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.21ns 
493471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
493471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
493472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
495838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
496630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
496635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
496637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
496637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.6ns 
496638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
499008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
499775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
499777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
499778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
499779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
499779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
502138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
502927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
502931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
502932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
502932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
502933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
505277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
506067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
506074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
506076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
506076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
506076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
508417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
509208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
509219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
509221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
509221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.3ns 
509222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
511564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
512351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
512356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
512358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
512358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.9ns 
512359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
514713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
515480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
515486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
515487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
515487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
515488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
517853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
518643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
518653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
518654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
518654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
518655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
520995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
521782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
521791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
521793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
521793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
521793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
524135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
524927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
524936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
524937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
524937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
524937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
527302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
528069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
528079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.91ms 
528080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
528080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
528081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
530443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
531232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
531251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.51ms 
531252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
531252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
531253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
533593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
534385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
534405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.94ms 
534407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
534407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
534407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
536743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
537534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
537552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.89ms 
537555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
537555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.7ns 
537556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
539922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
540689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
540737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.9ms 
540739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
540739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
540740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
543072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
543864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
543882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.18ms 
543884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
543884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
543884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
546229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
547022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
547066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.52ms 
547068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
547068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
547068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
549439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
550206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
550215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ms 
550216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
550216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
550217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
552565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
553354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
553359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
553360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
553360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
553361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
555695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
556487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
556490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
556491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
556491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
556492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
558850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
559649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
559661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
559662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
559662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
559663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
561997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
562787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
562793     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
562794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
562794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
562795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
565148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
565940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
565943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
565944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
565944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
565945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
568300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
569089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
569099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
569100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
569100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
569100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
571441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
572228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
572238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.51ms 
572239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
572239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
572239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
574599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
575366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
575378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.69ms 
575379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
575379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
575380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
577742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
578532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
578534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 957.91ns 
578535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
578535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
578536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
580868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
581658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
581661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
581662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
581662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
581663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
584016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
584804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
584809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
584810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
584811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
584811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
587148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
587940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
587945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
587946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
587946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
587947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
590301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
591088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
591128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.36ms 
591129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
591129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
591130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
593509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
594306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
594325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.93ms 
594327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
594327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
594327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
596686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
597472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
597483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
597484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
597484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
597485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
599825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
600613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
600615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 169ns 
600617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
600617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 
600619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
602980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
603772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
603852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.94ms 
603854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
603854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
603855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
606194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
606983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
607015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.48ms 
607016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
607016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
607017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
609370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
610162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
610164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.8ns 
610165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
610165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
610166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
612499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
613287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
613289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 198.59ns 
613290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
613290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
613291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
615642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
616432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
616433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 211.8ns 
616435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
616435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
616435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
618774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
619562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
619564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.4ns 
619565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
619565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
619565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
621914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
622703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
622797     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
622804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.42ms 
622806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
622806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
622806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
625194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
625968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
626017     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
626019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.98ms 
626020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
626020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
626021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
628407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
629225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
629226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
629255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
629308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
629324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
629331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
629347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
629348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
629350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
629352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
629358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
629361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
629364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
629368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
629596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
629597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
629600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
629601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
629603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
629745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
629746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
629750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
629751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
629753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
629755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
629934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
629936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
629937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
629938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
629939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
629942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
630071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
630073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
630074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
630075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
630076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
630077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
630086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
630087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
630089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
630090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
630092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
630093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
630102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
630103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
630105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
630105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
630107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
630107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
630236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
630238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
630239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
630362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
630363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
630364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
630366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
630368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
630369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
630371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
630376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
630384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
630386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
630387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
630388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
630389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
630498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
630502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
630503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
630504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
630506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
630507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
630511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
630649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
630651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
630652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
630653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
630654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
630655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
630656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
630658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
630770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
630772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
630874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
630879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
630886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
630887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
630890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
630891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
630892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
630893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
630893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
630894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
630904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
630910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
631021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
631022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
631024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
631026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
631026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
631027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
631027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
631028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
631080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
631087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
631174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
631175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
631176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
631177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
631179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
631180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
631354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
631358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
631358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
631359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
631360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
631361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
631362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
631362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
631371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
631372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
631373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
631374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
631465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
631466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
631467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
631468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
631469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
631470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
631568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
631569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
631570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
631571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
631572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
631572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
631573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
631574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
631651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
631652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
631722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
631723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
631724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
631728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
631731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
631736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
631855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
631856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
631857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
631858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
631868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
631948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
635127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
635128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
635133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
635134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
635135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
635136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
635136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
635144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
635145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
635146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
635147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
635148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
635237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
635241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
635241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
635242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
635243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
635244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
635244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
635336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
635337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
635338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
635339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
635340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
635340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
635342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
635343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
635415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
635417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
635486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
635490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
635494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
635495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
635496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
635496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
635506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
635581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
635582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
635583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
635583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
635697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
635706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
635706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
635707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
635708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
635709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
635709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
635709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
635720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
635720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
635721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
635722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
635723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
635806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
635806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
635807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
635808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
635809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
635894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
635898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
635899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
635900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
635900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
635901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
635901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
635995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
635995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
635996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
635997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
635998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
635998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
635999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
635999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
636000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
636001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
636001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
636002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
636002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
636003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
636003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
636086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
636087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
636092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
636165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
636241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
636242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
636243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
636243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
636244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
636245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
636245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
636245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
636246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
636328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
636334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
636419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
636420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
636421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
636424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
636424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
636425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
636425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
636426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
636432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
636432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
636509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
636514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
636525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
636621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
636621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
636622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
636623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
636623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
636624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
636624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
636624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
636677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
636678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
636678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
636679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
636680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
636685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
636690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
636799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
636884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
636885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
636885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
636886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
637045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
637130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
637130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
640031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
640035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
640037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
640037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
640038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
640150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
640151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
640152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
640152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
640153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
640256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
643000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
646011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
646015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
646016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
646017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
646018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
646127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
646128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
646129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
646130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
646131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
647221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
647221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
647222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
649668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
650441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
650442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
650443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
650451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
650461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
650463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
650465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
650466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
650471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
650472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
650476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
650477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
650479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
650489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
650489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
650555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
650607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
650608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
650609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
650609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
650610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
650680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
650680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
650680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
650681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
650682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
650685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
650685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
650686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
650686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
650687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
650688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
650765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
650765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
650766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
650766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
650767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
650768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
650852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
650853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
650853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
650854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
650854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
650855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
650856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
650856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
650857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
650857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
650858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
650858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
650859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
650859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
650860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
650860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
650861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
650861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
650862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
650865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
650903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
650904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
650963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
650964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
650965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
650966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
650967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
650968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
651018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
651020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
651021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
651022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
651023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
651024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
651025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
651074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
651077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
651080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
651132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
651185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
651185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.1ns 
651186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
653546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
654356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
654398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.54ms