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

198

tests

0

failures

0

ignored

10m57.23s

duration

100%

successful

Tests

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

Standard output

646        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)

11324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15146      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18670      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22080      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25457      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28798      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
32087      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
35385      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38686      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41956      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
45181      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
48429      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51761      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
55102      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58453      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
61681      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68219      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
71464      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
74686      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77942      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
81205      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
84456      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90904      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
94186      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97448      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
100664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
107113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
110351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
113606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
119994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
123227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
126501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
129687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
132908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
136129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
142578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
145763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
148978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
155374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
158554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
161756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
164960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
168157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
171350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
174619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
181135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
184337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
187569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
190768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
194108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
197307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
200475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
203683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
206895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
210083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
213248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
216454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
219669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
222891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
226088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
229256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
232458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
235659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
238845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
242021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
245223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
248500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
251735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
254934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
261394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
264648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
267866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
271049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
274251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
277456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
280699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
283927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
287144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
290357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
293574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
296801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
299981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
303171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
306376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
309567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
312724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
315925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
319124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
322320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
325487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
328666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
331856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
335061     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
338247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
341403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
344598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
347790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
350985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
354142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
357327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
360521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
363725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
366887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
370069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
373263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
376471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
379627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
382836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
386020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
389246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
392504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
395698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
398904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
402104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
405302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
408467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
411685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
414890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
418091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
421269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
424470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
427682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
430896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
434100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
437272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
440464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
443652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
446851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
450025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
453219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
456420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
459631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
462796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
466008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
469204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
472410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
475601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
478777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
481983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
485213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
488428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
491641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
494820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
498025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
501246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
504452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
507647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
510839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
514013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
517223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
520430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
523630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
526841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
530071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
533290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
536509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
539725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
542948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
546187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
549418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
552654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
555886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
559203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
562411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
565612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
568811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
572027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
575235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
578427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
581641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
584853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
588067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
591276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
594485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
597685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
600894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
604166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
607394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
610626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
613840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
617266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
620515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
623713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
626904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
630095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
633285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
636614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
639850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
661013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
664884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq