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

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

tests
0

failures
0

ignored
10m56.16s

duration
100%

successful

Tests

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

Standard output

806        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
833        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.29ms 
1019       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1032       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)

1896       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1898       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1904       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1905       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3089       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8048       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.03s 
8116       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8146       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.8ns 
8158       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8158       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.6ns 
8163       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
10948      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11916      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.48ms 
11926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.4ns 
11929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14655      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
14656      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15589      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.08ms 
15592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.2ns 
15594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
18205      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19096      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
19103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385ns 
19105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21629      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
21629      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
22489      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22490      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 657.2ns 
22491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
25023      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25950      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.15ms 
25952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25952      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 
25953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28493      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
28493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29318      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.81ms 
29320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 
29321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
31776      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32586      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.3ns 
32588      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.9ns 
32589      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
35034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35815      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35818      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.4ns 
35819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
35820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
38286      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39097      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 542.7ns 
39100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39100      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.5ns 
39101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41605      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
41605      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42409      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 529ns 
42410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
42411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44955      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
44955      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45735      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.4ns 
45737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.3ns 
45738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
48174      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49018      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.09ms 
49019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49019      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
49020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
51432      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52253      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.54ms 
52255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
52257      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
54672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.75ms 
55576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.3ns 
55577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
58011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58794      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
58797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58797      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.9ns 
58799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
61240      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
62042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.9ns 
62043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
64458      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65288      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.37ms 
65290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.3ns 
65291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
67732      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68511      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
68513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68513      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
68514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
70942      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71766      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.75ms 
71768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 941.9ns 
71771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
74175      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74997      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.95ms 
75001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.9ns 
75002      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
77406      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78198      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
78208      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
78210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
78210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.9ns 
78211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
80650      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81435      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.99ms 
81437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 
81438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
83874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84665      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
84666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
84667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
87061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87886      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.19ms 
87888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
87889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
90306      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91076      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
91118      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.57ms 
91120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
91120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
91121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93550      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
93550      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
94371      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.17ms 
94372      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
94372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
94373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96775      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
96775      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
97572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
97580      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
97583      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
97583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 503.7ns 
97584      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
99984      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
100784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
100785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
103205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
104011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
104012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
104012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 
104013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
106404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
107196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
107197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
107198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
107198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
109593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
110385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
110392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
110395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
110396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 632.1ns 
110397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
112810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
113575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
113582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
113583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
113583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
113584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
115997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
116781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
116784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
116786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
116786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
116786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
119178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
119964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
119973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.62ms 
119974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
119974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
119975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
122380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
123167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
123201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.24ms 
123202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
123202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
123203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
125648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
126415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
126432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms 
126434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
126435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.5ns 
126436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
128899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
129686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
129701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
129702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
129702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
129703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
132095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
132883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
132905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.5ms 
132908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
132908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.7ns 
132909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
135341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
136107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
136120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.59ms 
136122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
136122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
136123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
138537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
139323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
139355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.09ms 
139357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
139358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.1ns 
139358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
141767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
142557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
142559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 896.3ns 
142561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
142561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
142561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
144954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
145743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
145746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
145748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
145748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
145748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
148155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
148919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
148925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 
148927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
148927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
148927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
151322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
152110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
152120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.53ms 
152124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
152125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
152125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
154513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
155296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
155311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms 
155313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
155313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
155313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
157717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
158480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
158487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
158488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
158488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
158489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
160883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
161675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
161678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
161679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
161679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.7ns 
161680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
164076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
164865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
164868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
164869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
164870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 
164870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
167267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
168053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
168057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
168058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
168058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
168059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
170490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
171255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
171309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.68ms 
171311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
171312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.1ns 
171313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
173743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
174530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
174593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.84ms 
174595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
174595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
174596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
177001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
177789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
177792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
177799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
177799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.6ns 
177800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
180195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
180959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
180988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.99ms 
180989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
180989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
180990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
183423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
184206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
184227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.65ms 
184228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
184228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
184229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
186621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
187405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
187407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.61ns 
187408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
187409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
187410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
189801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
190584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
190693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.45ms 
190695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
190695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
190695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
193109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
193894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
193902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
193903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
193903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
193903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
196288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
197071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
197076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
197077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
197077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
197078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
199464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
200251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
200265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
200266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
200266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
200267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
202678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
203439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
203448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
203450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
203450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
203451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
205863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
206646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
206650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
206652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
206652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
206653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
209034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
209815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
209819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
209820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
209820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
209821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
212198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
212990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
213004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.86ms 
213005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
213005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
213006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
215423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
216209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
216221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.93ms 
216222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
216222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
216223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
218610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
219401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
219414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.39ms 
219415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
219415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
219416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
221800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
222583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
222586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973.9ns 
222587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
222587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
222588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
224982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
225745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
225747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
225749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
225749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
225749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
228145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
228929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
228934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
228935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
228935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
228935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
231315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
232101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
232104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
232106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
232106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
232106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
234497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
235283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
235285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 430.2ns 
235286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
235287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 
235287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
237697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
238458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
238491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.91ms 
238492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
238492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
238493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
240867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
241649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
241651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.4ns 
241653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
241653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.9ns 
241654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
244123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
244949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
244997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.18ms 
245002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
245002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.5ns 
245003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
247411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
248173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
248198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
248200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
248200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
248201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
250605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
251391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
251416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
251419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
251419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
251420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
253808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
254591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
254620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.52ms 
254622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
254622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
254622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
257012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
257793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
257812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.54ms 
257813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
257813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
257814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
260217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
261010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
261043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.7ms 
261044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
261044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
261045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
263478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
264262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
264278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
264280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
264280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
264280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
266676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
267461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
267474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
267475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
267475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
267476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
269887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
270649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
270663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.35ms 
270664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
270665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
270665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
273068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
273850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
273862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
273863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
273863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
273864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
276244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
277027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
277043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
277044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
277044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
277045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
279426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
280207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
280222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.18ms 
280223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
280223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
280224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
282637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
283421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
283436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
283437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
283437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
283438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
285819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
286599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
286613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.28ms 
286614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
286614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
286615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
288982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
289763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
289776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.13ms 
289777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
289777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
289778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
292177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
292937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
292958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.68ms 
292960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
292960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.8ns 
292961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
295371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
296156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
296170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
296171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
296171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
296172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
298554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
299335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
299341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
299342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
299342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
299342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
301737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
302500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
302510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.92ms 
302512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
302512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
302512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
304920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
305704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
305707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
305708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
305708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
305708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
308113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
308896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
308898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.6ns 
308899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
308899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
308900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
311280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
312064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
312066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 589.6ns 
312067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
312067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
312068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
314467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
315230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
315235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
315236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
315237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
315237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
317634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
318420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
318424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
318426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
318426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
318426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
320821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
321605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
321615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.94ms 
321616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
321616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
321616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
323990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
324774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
324777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
324778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
324778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
324778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
327195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
327982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
327984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 385.3ns 
327985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
327985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
327985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
330378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
331168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
331172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
331173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
331173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
331174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
333567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
334351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
334353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.1ns 
334354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
334354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
334355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
336756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
337519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
337521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 439.6ns 
337522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
337522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
337522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
339941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
340727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
340729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 464.6ns 
340730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
340730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
340730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
343124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
343911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
343915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
343916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
343916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
343916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
346293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
347083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
347089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
347090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
347090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
347091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
349486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
350269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
350272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
350274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
350274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
350274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
352654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
353436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
353441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
353442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
353442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
353443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
355820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
356602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
356608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
356609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
356609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
356610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
359016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
359778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
359790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.42ms 
359791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
359791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
359791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
362196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
362979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
362982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
362983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
362983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
362984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
365362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
366145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
366148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.3ns 
366149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
366149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
366150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
368548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
369314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
369317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
369319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
369319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
369320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
371727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
372508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
372520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
372521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
372521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
372522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
374902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
375684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
375688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 326.8ns 
375689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
375690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
375690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
378082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
378845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
378869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.07ms 
378870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
378870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
378871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
381272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
382057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
382062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
382064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
382064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.3ns 
382065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
384448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
385232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
385246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.32ms 
385247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
385247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
385248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
387653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
388435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
388448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.48ms 
388449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
388449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
388450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
390837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
391624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
391641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
391642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
391642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
391643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
394055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
394817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
394819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 461.3ns 
394820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
394820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
394821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
397211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
397994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
397998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
397999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
398000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
398000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
400374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
401162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
401165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
401166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
401166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
401167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
403571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
404355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
404357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.5ns 
404358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
404359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.9ns 
404359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
406737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
407524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
407526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 641.3ns 
407529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
407530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
407531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
409924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
410714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
410717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 961.61ns 
410718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
410718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
410719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
413105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
413891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
413894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 893.6ns 
413895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
413895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
413896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
416297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
417086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
417094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
417095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
417095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
417095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
419483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
420269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
420275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
420276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
420276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
420277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
422699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
423526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
423532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
423533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
423533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
423533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
426041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
426872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
426879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
426880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
426880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
426880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
429342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
430134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
430137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
430138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
430138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
430139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
432525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
433316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
433319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
433320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
433320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
433321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
435740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
436529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
436531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 598.2ns 
436532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
436532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
436533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
438914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
439705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
439707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.5ns 
439708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
439708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
439709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
442120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
442911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
442913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 859.7ns 
442914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
442914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
442915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
445310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
446083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
446091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
446092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
446092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
446093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
448492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
449280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
449283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
449284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
449284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
449284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
451702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
452492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
452497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
452498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
452498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
452499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
454874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
455668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
455670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.9ns 
455671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
455671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
455672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
458066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
458857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
458859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.1ns 
458860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
458860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
458861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
461257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
462046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
462049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
462051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
462051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.9ns 
462051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
464434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
465224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
465226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713.3ns 
465227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
465227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
465227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
467628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
468417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
468420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 962.3ns 
468421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
468421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
468421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
470809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
471598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
471600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 920ns 
471601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
471601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
471602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
473974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
474762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
474765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
474767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
474767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
474767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
477165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
477954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
477956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.6ns 
477957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
477957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
477958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
480343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
481133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
481141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.05ms 
481142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
481142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
481143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
483527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
484298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
484300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 440.1ns 
484301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
484301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
484302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
486697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
487490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
487495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
487496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
487496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
487497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
489896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
490687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
490689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 704.5ns 
490690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
490690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
490691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
493085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
493879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
493881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.2ns 
493882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
493882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
493883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
496291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
497071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
497075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
497076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
497076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
497077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
499474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
500272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
500274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.2ns 
500276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
500276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.1ns 
500277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
502689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
503481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
503483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
503484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
503484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
503485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
505877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
506668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
506670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 932.1ns 
506671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
506672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
506672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
509104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
509893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
509897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
509898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
509898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
509898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
512292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
513065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
513071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
513073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
513073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
513073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
515482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
516273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
516280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
516281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
516281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
516282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
518681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
519471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
519477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
519478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
519478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 
519479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
521874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
522662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
522668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
522669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
522669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
522670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
525067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
525858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
525868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
525869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
525869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
525869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
528257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
529046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
529056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.19ms 
529057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
529057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
529058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
531454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
532251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
532260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
532261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
532261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
532262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
534654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
535463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
535469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
535470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
535471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
535471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
537870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
538661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
538680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.47ms 
538681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
538681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
538682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
541080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
541872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
541893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.18ms 
541894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
541894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
541895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
544303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
545097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
545116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.83ms 
545117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
545117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
545118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
547522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
548317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
548334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
548335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
548335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
548336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
550747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
551543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
551562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.05ms 
551563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
551563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
551564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
553965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
554760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
554805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.63ms 
554807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
554807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
554807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
557208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
558001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
558008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
558011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
558011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.4ns 
558011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
560420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
561213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
561218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
561219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
561219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
561219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
563612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
564407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
564410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
564411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
564411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
564412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
566836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
567642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
567654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
567656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
567656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
567656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
570055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
570851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
570857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
570858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
570858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
570859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
573265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
574061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
574064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
574065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
574065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
574066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
576460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
577254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
577264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.17ms 
577265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
577265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
577266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
579684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
580458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
580492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.29ms 
580494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
580494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.1ns 
580495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
582891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
583680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
583693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.83ms 
583694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
583694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
583695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
586097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
586889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
586892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.1ns 
586893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
586893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
586893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
589297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
590091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
590094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
590095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
590095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
590095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
592483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
593275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
593280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
593281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
593281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
593282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
595686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
596478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
596483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
596484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
596484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
596484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
598893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
599683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
599722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.23ms 
599723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
599723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
599724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
602117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
602916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
602935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.17ms 
602937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
602937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.7ns 
602938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
605336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
606130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
606140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.94ms 
606141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
606141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
606142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
608542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
609335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
609337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 226.7ns 
609338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
609338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.5ns 
609339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
611756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
612546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
612622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.96ms 
612623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
612624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
612624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
615022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
615819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
615851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.87ms 
615852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
615852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
615853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
618268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
619063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
619065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 251.4ns 
619066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
619066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
619067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
621484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
622284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
622285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.2ns 
622286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
622286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
622287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
624700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
625500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
625502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 197.5ns 
625503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
625503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
625504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
627919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
628710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
628712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 329.4ns 
628713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
628713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
628714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
631114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
631905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
631984     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
631995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.12ms 
631997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
631997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
631998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
634422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
635213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
635254     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
635255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.49ms 
635256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
635256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
635257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
637657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
638448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
638450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ns 
638485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
638535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
638549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
638556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
638573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
638574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
638577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
638578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
638583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
638585     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' 
638588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
638590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
638813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
638814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
638817     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' 
638818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
638820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
638969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
638970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
638973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
638974     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' 
638976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
638978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
639155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
639157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
639158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
639159     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' 
639160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
639161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
639281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
639282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
639284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
639285     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' 
639285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
639286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
639293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
639294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
639296     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' 
639297     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' 
639297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
639298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
639305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
639306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
639307     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' 
639308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
639309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
639310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
639441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
639442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
639443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
639570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
639571     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)'' 
639572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
639574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
639575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
639575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
639576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
639577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
639581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
639582     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' 
639583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
639584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
639585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
639696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
639701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
639702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
639703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
639703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
639704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
639705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
639856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
639857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
639858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
639859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
639860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
639861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
639862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
639863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
639961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
639963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
640057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
640062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
640066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
640067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
640068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
640069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
640070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
640070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
640071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
640071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
640079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
640084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
640198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
640198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
640199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
640200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
640201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
640202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
640202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
640203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
640268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
640274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
640396     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]'' 
640396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
640397     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'' 
640399     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'' 
640400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
640401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
640542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
640546     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'' 
640547     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)'' 
640548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
640549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
640550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
640551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
640551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
640562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
640563     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'' 
640564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
640565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
640671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
640672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
640673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
640673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
640674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
640675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
640794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
640795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
640796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
640797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
640798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
640798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
640799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
640800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
640905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
640907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
640994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
640995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
640995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
641000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
641004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
641009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
641161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
641161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
641164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
641165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
641178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
641279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
644685     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'' 
644686     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)'' 
644690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
644692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
644692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
644694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
644696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
644703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
644704     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'' 
644705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
644706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
644707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
644799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
644803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
644804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
644805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
644806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
644807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
644809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
644903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
644904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
644905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
644908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
644909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
644909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
644910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
644910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
644988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
644989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
645085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
645089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
645093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
645094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
645094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
645095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
645105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
645183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
645184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
645184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
645185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
645252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
645261     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'' 
645262     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)'' 
645262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
645264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
645264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
645264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
645265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
645275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
645275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
645276     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'' 
645277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
645278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
645360     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))'' 
645360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
645361     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'' 
645362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
645363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
645447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
645451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
645452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
645492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
645493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
645493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
645494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
645593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
645593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
645594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
645595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
645596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
645597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
645597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
645598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
645598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
645599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
645600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
645600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
645601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
645601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
645602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
645684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
645685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
645690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
645764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
645838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
645839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
645840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
645840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
645841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
645842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
645842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
645842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
645843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
645922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
645928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
646011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
646012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
646013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
646013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
646014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
646014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
646015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
646015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
646020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
646021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
646095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
646100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
646105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
646197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
646198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
646199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
646200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
646200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
646200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
646201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
646201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
646252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
646253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
646253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
646254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
646255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
646260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
646264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
646374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
646456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
646457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
646457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
646458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
646616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
646699     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'' 
646699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
649526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
649530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
649531     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'' 
649532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
649533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
649643     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))'' 
649643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
649644     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'' 
649645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
649646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
649744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
652822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
655881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
655885     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'' 
655886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
655887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
655887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
655996     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))'' 
655996     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'' 
655997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
655998     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)' ...' 
655999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
657071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
657071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
657072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
659529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
660336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
660338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
660338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
660347     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)'' 
660355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
660358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
660360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
660362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
660366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
660367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
660371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
660372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
660374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
660384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
660384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
660386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
660433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
660433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
660434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
660434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
660435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
660500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
660501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
660501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
660502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
660503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
660506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
660507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
660507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
660507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
660508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
660509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
660587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
660588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
660588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
660590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
660591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
660592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
660733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
660734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
660734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
660734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
660735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
660735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
660736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
660736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
660737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
660737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
660738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
660738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
660738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
660739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
660739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
660740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
660740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
660740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
660741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
660743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
660775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
660776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
660825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
660826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
660827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
660828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
660829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
660829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
660875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
660877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
660878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
660878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
660880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
660881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
660881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
660920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
660922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
660925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
660971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
661019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
661019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.7ns 
661020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
663475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
664308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
664323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.88ms