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

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

tests
0

failures
0

ignored
13m7.87s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.951s passed
powPositiveConcrete data()[101] 3.884s passed
powGeq1Concrete data()[102] 3.895s passed
pow2InIntLower data()[103] 3.862s passed
pow2InIntUpper data()[104] 3.842s passed
logSelfConcrete data()[105] 3.879s passed
log1Concrete data()[106] 3.864s passed
logProduct data()[107] 3.842s passed
logTimesBaseConcrete data()[108] 3.852s passed
logProdIdentity data()[109] 3.819s passed
moduloByteIsInByte data()[10] 4.034s passed
logProdIdentityConcrete data()[110] 3.818s passed
logPowIdentity data()[111] 3.838s passed
logPowIdentityConcrete data()[112] 3.854s passed
logPositive data()[113] 3.882s passed
logPositiveConcrete data()[114] 3.829s passed
logMono data()[115] 3.977s passed
logMonoConcrete data()[116] 3.820s passed
powLogLess data()[117] 3.862s passed
powLogMore2 data()[118] 3.854s passed
logLessThanPow data()[119] 3.941s passed
moduloCharIsInChar data()[11] 4.028s passed
logLessThanPowConcrete data()[120] 3.880s passed
logSqueeze data()[121] 3.878s passed
ifthenelse_equals data()[122] 3.847s passed
ifthenelse_equals_1 data()[123] 3.901s passed
ifthenelse_equals_2 data()[124] 3.870s passed
disjointWithSingleton1 data()[125] 3.867s passed
disjointWithSingleton2 data()[126] 3.870s passed
disjointArrayRanges data()[127] 3.827s passed
disjointArrayRangeAllFields1 data()[128] 3.855s passed
disjointArrayRangeAllFields2 data()[129] 3.882s passed
div_unique1 data()[12] 4.049s passed
seqSelfDefinition data()[130] 3.886s passed
seqOutsideValue data()[131] 3.941s passed
castedGetAny data()[132] 3.920s passed
seqGetAlphaCast data()[133] 3.873s passed
getOfSeqSingleton data()[134] 3.856s passed
getOfSeqSingletonConcrete data()[135] 3.901s passed
getOfSeqConcat data()[136] 3.892s passed
getOfSeqSub data()[137] 3.901s passed
getOfSeqReverse data()[138] 3.918s passed
lenOfSeqEmpty data()[139] 3.890s passed
div_unique2 data()[13] 3.993s passed
lenOfSeqSingleton data()[140] 3.870s passed
lenOfSeqConcat data()[141] 3.855s passed
lenOfSeqSub data()[142] 3.898s passed
lenOfSeqReverse data()[143] 3.954s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.936s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.977s passed
getOfSeqSingletonEQ data()[146] 3.974s passed
getOfSeqConcatEQ data()[147] 3.890s passed
getOfSeqSubEQ data()[148] 3.843s passed
getOfSeqReverseEQ data()[149] 3.893s passed
div_exists data()[14] 4.244s passed
lenOfSeqEmptyEQ data()[150] 3.856s passed
lenOfSeqSingletonEQ data()[151] 3.850s passed
lenOfSeqConcatEQ data()[152] 3.826s passed
lenOfSeqSubEQ data()[153] 3.911s passed
lenOfSeqReverseEQ data()[154] 3.821s passed
getOfSeqDefEQ data()[155] 3.858s passed
lenOfSeqDefEQ data()[156] 3.861s passed
seqConcatWithSeqEmpty1 data()[157] 3.851s passed
seqConcatWithSeqEmpty2 data()[158] 3.954s passed
seqReverseOfSeqEmpty data()[159] 3.885s passed
div_one data()[15] 3.886s passed
subSeqComplete data()[160] 3.912s passed
subSeqTailR data()[161] 3.899s passed
subSeqTailL data()[162] 3.897s passed
subSeqTailEQR data()[163] 3.887s passed
subSeqTailEQL data()[164] 3.882s passed
seqDef_split data()[165] 3.922s passed
seqDef_induction_upper data()[166] 3.937s passed
seqDef_induction_upper_concrete data()[167] 3.898s passed
seqDef_induction_lower data()[168] 3.889s passed
seqDef_induction_lower_concrete data()[169] 3.957s passed
jdiv_one data()[16] 3.817s passed
seqDef_split_in_three data()[170] 4.084s passed
seqDef_empty data()[171] 3.873s passed
seqDef_one_summand data()[172] 3.810s passed
seqDef_lower_equals_upper data()[173] 3.854s passed
seqDefOfSeq data()[174] 3.880s passed
seqSelfDefinitionEQ2 data()[175] 3.889s passed
indexOfSeqSingleton data()[176] 3.874s passed
indexOfSeqConcatFirst data()[177] 3.916s passed
indexOfSeqConcatSecond data()[178] 3.912s passed
indexOfSeqSub data()[179] 3.902s passed
div_zero data()[17] 3.958s passed
lenOfArray2seq data()[180] 3.921s passed
getAnyOfArray2seq data()[181] 3.972s passed
getOfArray2seq data()[182] 3.947s passed
getAnyOfNPermInv data()[183] 3.888s passed
seqNPermRange data()[184] 3.970s passed
seqPermTrans data()[185] 3.982s passed
seqPermRefl data()[186] 3.859s passed
seqPermSplit data()[187] 3.867s passed
seqNPermRight data()[188] 4.319s passed
seqPermFromSwap data()[189] 4.075s passed
divResZero1 data()[18] 3.927s passed
seqPermTransAlt0 data()[190] 3.927s passed
seqPermTransAlt1 data()[191] 3.912s passed
seqPermTransAlt2 data()[192] 3.928s passed
seqPermTransAlt3 data()[193] 3.967s passed
schiffl_lemma_2 data()[194] 24.869s passed
schiffl_thm_1 data()[195] 4.629s passed
eqSameSeq data()[196] 3.931s passed
divResZero2 data()[19] 3.963s passed
eqTermCut data()[1] 4.782s passed
divResOne1 data()[20] 3.851s passed
divResOne2 data()[21] 3.817s passed
div_cancel1 data()[22] 3.863s passed
div_cancel2 data()[23] 3.885s passed
divAddMultDenom data()[24] 3.904s passed
divMinus data()[25] 4.007s passed
divMinusDenom data()[26] 3.953s passed
divLeastDPos data()[27] 3.873s passed
divLeastDNeg data()[28] 3.932s passed
divGreatestDPos data()[29] 3.847s passed
equivAllRight data()[2] 4.328s passed
divGreatestDNeg data()[30] 3.876s passed
divIncreasingPos data()[31] 3.825s passed
divIncreasingNeg data()[32] 3.852s passed
jdiv_zero data()[33] 3.898s passed
jdivPulloutMinusNum data()[34] 3.903s passed
jdivPulloutMinusDenom data()[35] 3.875s passed
jdiv_uniquePosPos data()[36] 3.834s passed
jdiv_uniquePosNeg data()[37] 3.840s passed
jdiv_uniqueNegPos data()[38] 3.905s passed
jdiv_uniqueNegNeg data()[39] 3.900s passed
irrflConcrete1 data()[3] 4.171s passed
jdivMultDenom1 data()[40] 3.931s passed
jdivMultDenom2 data()[41] 3.751s passed
mod_geZero data()[42] 3.856s passed
mod_lessDenom data()[43] 3.910s passed
jmod_NumPos data()[44] 3.878s passed
jmod_NumNeg data()[45] 3.828s passed
jmod_geZero data()[46] 3.901s passed
jmodNumZero data()[47] 3.844s passed
jmod_pulloutminusNum data()[48] 3.846s passed
jmod_pulloutminusDenom data()[49] 3.819s passed
irrflConcrete2 data()[4] 4.042s passed
jmodUnique1 data()[50] 3.934s passed
jmodUnique2 data()[51] 4.015s passed
intDivRem data()[52] 3.868s passed
jmodjmod data()[53] 3.961s passed
jmodDivisible data()[54] 3.904s passed
jmodDivisibleRep data()[55] 3.853s passed
jdivAddMultDenom data()[56] 4.143s passed
jmodAltZero data()[57] 3.906s passed
jmodAddMultDenomZero data()[58] 3.905s passed
polyDiv_zero data()[59] 3.989s passed
cancel_gtPos data()[5] 4.018s passed
polyMod_ltdivDenom data()[60] 3.894s passed
bsum_empty data()[61] 3.885s passed
bsum_induction_upper data()[62] 3.950s passed
bsum_induction_lower data()[63] 3.922s passed
bsum_num_of_bounds data()[64] 3.920s passed
bsum_num_of_bounds2 data()[65] 3.844s passed
bsum_induction_upper2 data()[66] 3.867s passed
bsum_induction_upper_concrete data()[67] 3.901s passed
bsum_induction_upper_concrete_2 data()[68] 3.849s passed
bsum_induction_upper2_concrete data()[69] 3.861s passed
cancel_gtNeg data()[6] 4.029s passed
bsum_induction_lower_concrete data()[70] 3.843s passed
bsum_induction_lower2 data()[71] 3.825s passed
bsum_induction_lower2_concrete data()[72] 3.866s passed
bsum_positive data()[73] 3.955s passed
bsum_upper_bound data()[74] 3.876s passed
bsum_lower_bound data()[75] 3.868s passed
bsum_positive_lower_bound_element data()[76] 3.812s passed
bsum_sub_same_index data()[77] 3.861s passed
bsum_less_same_index data()[78] 3.906s passed
bsum_equal_except_one_index data()[79] 3.897s passed
moduloIntIsInInt data()[7] 3.949s passed
bsum_num_of_is_max data()[80] 3.890s passed
bsum_num_of_is_max2 data()[81] 3.848s passed
bsum_num_of_is_max3 data()[82] 3.887s passed
bsum_num_of_is_max4 data()[83] 3.881s passed
bsum_num_of_lt_max data()[84] 3.924s passed
bsum_num_of_lt_max2 data()[85] 3.867s passed
bsum_num_of_lt_max3 data()[86] 3.941s passed
bsum_num_of_lt_max4 data()[87] 3.932s passed
bsum_num_of_gt0 data()[88] 3.889s passed
bsum_num_of_gt0_alt data()[89] 3.907s passed
moduloLongIsInLong data()[8] 3.905s passed
bsum_add_concrete data()[90] 3.902s passed
bprod_all_positive data()[91] 3.840s passed
bprod_split data()[92] 3.891s passed
powConcrete0 data()[93] 3.828s passed
powConcrete1 data()[94] 3.865s passed
powSplitFactor data()[95] 3.868s passed
powAdd data()[96] 3.861s passed
powMono data()[97] 3.917s passed
powMonoConcrete data()[98] 3.884s passed
powMonoConcreteRight data()[99] 3.873s passed
moduloShortIsInShort data()[9] 3.947s passed

Standard output

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

14079      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
18544      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
22806      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26872      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30852      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34908      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38906      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42849      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46771      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50753      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58800      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
62823      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
66854      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
74860      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
78742      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
82724      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
86709      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
90569      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
94382      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
98233      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
102150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
105989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
109920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
113947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
117899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
121803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
125634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
129524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
133351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
137218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
141108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
144949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
148845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
152701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
156533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
160428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
164326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
168243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
172087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
175901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
179815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
183676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
187530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
191427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
195251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
199150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
202937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
206732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
210723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
214731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
218664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
222587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
226467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
230360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
234499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
238435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
242388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
246287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
250196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
254124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
258052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
261947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
265829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
269724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
273595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
277447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
281311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
285157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
289001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
292846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
296688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
300665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
304509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
308332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
312196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
316058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
319984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
323884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
327745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
331621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
335474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
339432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
343281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
347185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
351154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
355044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
358981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
362863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
366723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
370569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
374446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
378330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
382181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
386039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
389938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
393843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
397717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
401629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
405548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
409446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
413309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
417150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
421031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
424897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
428734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
432598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
436397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
440252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
444056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
447908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
451779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
455630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
459527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
463436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
467267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
471117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
475006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
478982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
482837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
486705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
490587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
494460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
498323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
502194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
506036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
509866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
513735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
517624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
521566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
525487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
529375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
533232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
537128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
541020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
544905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
548833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
552730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
556618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
560460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
564355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
568305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
572205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
576174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
580196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
584067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
587921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
591795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
595679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
599530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
603357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
607291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
611094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
614941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
618797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
622641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
626579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
630486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
634400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
638278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
642181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
646064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
649956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
653818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
657772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
661686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
665565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
669526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
673387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
677531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
681348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
685195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
689045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
692933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
696831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
700717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
704626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
708525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
712483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
716421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
720396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
724297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
728147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
732159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
736096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
739975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
743865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
748233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
752286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
756200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
760108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
764026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
768180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
769201     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
769300     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
769333     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
769342     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
769355     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
769359     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
769361     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
769365     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
769372     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
769375     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
769380     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
769382     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
769632     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
769634     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
769636     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
769637     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
769639     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
769791     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
769793     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
769797     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
769799     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
769801     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
769802     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
769993     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
769996     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
769997     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
769998     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
770000     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
770003     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
770163     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
770165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
770168     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
770169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
770170     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
770171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
770180     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
770181     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
770182     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
770185     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
770187     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
770188     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
770199     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
770200     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
770201     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
770205     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
770206     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
770207     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
770409     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
770410     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
770412     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
770596     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
770598     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
770602     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
770609     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
770610     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
770612     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
770613     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
770616     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
770621     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
770626     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
770631     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
770635     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
770637     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
770764     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
770769     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
770771     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
770773     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
770775     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
770778     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
770780     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
770914     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
770917     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
770918     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
770921     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
770922     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
770923     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
770924     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
770927     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
771028     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
771030     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
771128     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
771133     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
771139     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
771141     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
771143     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
771145     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
771146     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
771147     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
771148     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
771149     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
771159     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
771164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
771261     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
771263     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
771265     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
771266     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
771267     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
771268     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
771268     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
771270     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
771322     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
771328     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
771417     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
771419     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
771421     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
771423     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
771424     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
771425     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
771591     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
771596     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
771597     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
771601     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
771603     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
771605     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
771607     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
771607     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
771617     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
771619     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
771620     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
771621     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
771727     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
771728     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
771729     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
771730     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
771731     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
771736     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
771837     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
771840     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
771841     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
771843     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
771843     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
771844     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
771844     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
771845     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
771953     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
771955     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
772035     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
772035     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
772036     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
772040     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
772044     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
772049     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
772176     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
772177     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
772178     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
772179     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
772189     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
772273     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
776058     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
776059     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
776066     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
776067     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
776068     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
776069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
776069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
776079     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
776081     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
776083     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
776084     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
776085     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
776181     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
776185     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
776187     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
776188     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
776188     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
776189     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
776190     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
776288     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
776290     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
776291     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
776292     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
776293     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
776294     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
776295     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
776296     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
776375     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
776377     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
776454     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
776459     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
776464     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
776465     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
776466     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
776467     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
776478     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
776559     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
776561     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
776562     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
776565     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
776641     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
776651     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
776652     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
776654     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
776655     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
776656     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
776657     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
776658     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
776669     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
776671     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
776672     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
776673     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
776674     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
776767     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
776769     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
776770     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
776771     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
776772     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
776867     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
776872     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
776874     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
776875     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
776875     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
776876     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
776877     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
776980     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
776982     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
776986     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
776987     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
776989     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
776992     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
776994     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
776996     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
776998     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
776998     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
777000     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
777001     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
777002     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
777002     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
777003     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
777099     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
777100     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
777107     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
777197     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
777283     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
777284     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
777286     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
777286     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
777287     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
777288     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
777288     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
777289     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
777289     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
777382     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
777389     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
777484     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
777485     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
777486     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
777487     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
777488     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
777488     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
777489     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
777489     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
777495     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
777496     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
777580     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
777586     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
777592     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
777698     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
777699     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
777700     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
777701     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
777701     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
777702     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
777702     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
777703     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
777808     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
777810     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
777811     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
777812     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
777813     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
777818     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
777823     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
777945     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
778036     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
778037     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
778038     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
778039     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
778214     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
778306     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
778307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
781667     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
781673     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
781675     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
781676     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
781677     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
781798     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
781800     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
781802     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
781803     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
781804     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
781916     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
785140     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
788565     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
788571     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
788572     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
788573     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
788574     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
788695     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
788696     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
788697     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
788698     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
788700     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
792836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
793810     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
793818     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
793833     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
793836     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
793838     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
793839     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
793843     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
793845     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
793849     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
793852     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
793853     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
793862     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
793865     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
793866     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
793915     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
793919     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
793919     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
793920     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
793921     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
793989     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
793990     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
793991     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
793992     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
793993     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
793997     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
793998     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
793999     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
794000     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
794001     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
794002     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
794105     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
794106     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
794106     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
794108     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
794109     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
794110     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
794193     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
794194     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
794194     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
794195     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
794196     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
794197     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
794198     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
794198     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
794199     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
794200     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
794200     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
794201     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
794202     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
794202     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
794203     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
794203     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
794204     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
794205     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
794206     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
794209     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
794247     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
794249     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
794311     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
794312     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
794314     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
794316     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
794317     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
794317     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
794370     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
794373     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
794374     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
794376     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
794377     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
794378     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
794379     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
794434     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
794436     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
794439     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
794508     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
797450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq