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

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

tests
0

failures
0

ignored
13m42.66s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.395s passed
powPositiveConcrete data()[101] 4.087s passed
powGeq1Concrete data()[102] 4.456s passed
pow2InIntLower data()[103] 4.379s passed
pow2InIntUpper data()[104] 4.275s passed
logSelfConcrete data()[105] 4.279s passed
log1Concrete data()[106] 3.996s passed
logProduct data()[107] 3.845s passed
logTimesBaseConcrete data()[108] 3.661s passed
logProdIdentity data()[109] 3.645s passed
moduloByteIsInByte data()[10] 3.794s passed
logProdIdentityConcrete data()[110] 3.704s passed
logPowIdentity data()[111] 3.746s passed
logPowIdentityConcrete data()[112] 3.648s passed
logPositive data()[113] 3.702s passed
logPositiveConcrete data()[114] 3.692s passed
logMono data()[115] 3.814s passed
logMonoConcrete data()[116] 3.691s passed
powLogLess data()[117] 3.759s passed
powLogMore2 data()[118] 3.883s passed
logLessThanPow data()[119] 3.732s passed
moduloCharIsInChar data()[11] 3.950s passed
logLessThanPowConcrete data()[120] 3.721s passed
logSqueeze data()[121] 3.879s passed
ifthenelse_equals data()[122] 3.802s passed
ifthenelse_equals_1 data()[123] 3.825s passed
ifthenelse_equals_2 data()[124] 4.073s passed
disjointWithSingleton1 data()[125] 3.771s passed
disjointWithSingleton2 data()[126] 3.744s passed
disjointArrayRanges data()[127] 3.771s passed
disjointArrayRangeAllFields1 data()[128] 3.715s passed
disjointArrayRangeAllFields2 data()[129] 3.688s passed
div_unique1 data()[12] 4.225s passed
seqSelfDefinition data()[130] 3.653s passed
seqOutsideValue data()[131] 3.662s passed
castedGetAny data()[132] 3.683s passed
seqGetAlphaCast data()[133] 3.597s passed
getOfSeqSingleton data()[134] 3.908s passed
getOfSeqSingletonConcrete data()[135] 3.855s passed
getOfSeqConcat data()[136] 3.920s passed
getOfSeqSub data()[137] 4.074s passed
getOfSeqReverse data()[138] 3.724s passed
lenOfSeqEmpty data()[139] 3.678s passed
div_unique2 data()[13] 4.067s passed
lenOfSeqSingleton data()[140] 3.646s passed
lenOfSeqConcat data()[141] 3.695s passed
lenOfSeqSub data()[142] 3.941s passed
lenOfSeqReverse data()[143] 4.003s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.947s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.960s passed
getOfSeqSingletonEQ data()[146] 3.954s passed
getOfSeqConcatEQ data()[147] 4.047s passed
getOfSeqSubEQ data()[148] 4.357s passed
getOfSeqReverseEQ data()[149] 4.358s passed
div_exists data()[14] 4.507s passed
lenOfSeqEmptyEQ data()[150] 4.156s passed
lenOfSeqSingletonEQ data()[151] 4.243s passed
lenOfSeqConcatEQ data()[152] 4.240s passed
lenOfSeqSubEQ data()[153] 3.990s passed
lenOfSeqReverseEQ data()[154] 4.206s passed
getOfSeqDefEQ data()[155] 4.056s passed
lenOfSeqDefEQ data()[156] 4.135s passed
seqConcatWithSeqEmpty1 data()[157] 4.034s passed
seqConcatWithSeqEmpty2 data()[158] 3.901s passed
seqReverseOfSeqEmpty data()[159] 3.780s passed
div_one data()[15] 3.927s passed
subSeqComplete data()[160] 3.756s passed
subSeqTailR data()[161] 4.161s passed
subSeqTailL data()[162] 4.315s passed
subSeqTailEQR data()[163] 4.139s passed
subSeqTailEQL data()[164] 4.284s passed
seqDef_split data()[165] 4.269s passed
seqDef_induction_upper data()[166] 4.109s passed
seqDef_induction_upper_concrete data()[167] 4.257s passed
seqDef_induction_lower data()[168] 4.285s passed
seqDef_induction_lower_concrete data()[169] 4.178s passed
jdiv_one data()[16] 4.103s passed
seqDef_split_in_three data()[170] 4.567s passed
seqDef_empty data()[171] 3.977s passed
seqDef_one_summand data()[172] 3.951s passed
seqDef_lower_equals_upper data()[173] 3.916s passed
seqDefOfSeq data()[174] 4.006s passed
seqSelfDefinitionEQ2 data()[175] 3.944s passed
indexOfSeqSingleton data()[176] 3.973s passed
indexOfSeqConcatFirst data()[177] 3.878s passed
indexOfSeqConcatSecond data()[178] 4.087s passed
indexOfSeqSub data()[179] 4.079s passed
div_zero data()[17] 3.988s passed
lenOfArray2seq data()[180] 3.954s passed
getAnyOfArray2seq data()[181] 4.067s passed
getOfArray2seq data()[182] 4.050s passed
getAnyOfNPermInv data()[183] 4.104s passed
seqNPermRange data()[184] 4.134s passed
seqPermTrans data()[185] 4.269s passed
seqPermRefl data()[186] 4.061s passed
seqPermSplit data()[187] 4.130s passed
seqNPermRight data()[188] 4.566s passed
seqPermFromSwap data()[189] 4.124s passed
divResZero1 data()[18] 3.833s passed
seqPermTransAlt0 data()[190] 4.033s passed
seqPermTransAlt1 data()[191] 3.952s passed
seqPermTransAlt2 data()[192] 3.943s passed
seqPermTransAlt3 data()[193] 4.066s passed
schiffl_lemma_2 data()[194] 27.317s passed
schiffl_thm_1 data()[195] 5.072s passed
eqSameSeq data()[196] 4.372s passed
divResZero2 data()[19] 3.931s passed
eqTermCut data()[1] 5.239s passed
divResOne1 data()[20] 4.055s passed
divResOne2 data()[21] 4.142s passed
div_cancel1 data()[22] 4.155s passed
div_cancel2 data()[23] 3.985s passed
divAddMultDenom data()[24] 4.188s passed
divMinus data()[25] 4.219s passed
divMinusDenom data()[26] 4.140s passed
divLeastDPos data()[27] 4.032s passed
divLeastDNeg data()[28] 4.150s passed
divGreatestDPos data()[29] 4.414s passed
equivAllRight data()[2] 4.500s passed
divGreatestDNeg data()[30] 4.639s passed
divIncreasingPos data()[31] 4.664s passed
divIncreasingNeg data()[32] 4.629s passed
jdiv_zero data()[33] 4.547s passed
jdivPulloutMinusNum data()[34] 4.413s passed
jdivPulloutMinusDenom data()[35] 4.250s passed
jdiv_uniquePosPos data()[36] 4.288s passed
jdiv_uniquePosNeg data()[37] 4.314s passed
jdiv_uniqueNegPos data()[38] 4.263s passed
jdiv_uniqueNegNeg data()[39] 4.351s passed
irrflConcrete1 data()[3] 4.167s passed
jdivMultDenom1 data()[40] 4.214s passed
jdivMultDenom2 data()[41] 4.221s passed
mod_geZero data()[42] 4.400s passed
mod_lessDenom data()[43] 4.344s passed
jmod_NumPos data()[44] 4.502s passed
jmod_NumNeg data()[45] 4.428s passed
jmod_geZero data()[46] 4.430s passed
jmodNumZero data()[47] 4.501s passed
jmod_pulloutminusNum data()[48] 4.027s passed
jmod_pulloutminusDenom data()[49] 4.202s passed
irrflConcrete2 data()[4] 3.907s passed
jmodUnique1 data()[50] 4.406s passed
jmodUnique2 data()[51] 4.393s passed
intDivRem data()[52] 4.085s passed
jmodjmod data()[53] 4.134s passed
jmodDivisible data()[54] 4.102s passed
jmodDivisibleRep data()[55] 3.963s passed
jdivAddMultDenom data()[56] 4.261s passed
jmodAltZero data()[57] 4.020s passed
jmodAddMultDenomZero data()[58] 4.104s passed
polyDiv_zero data()[59] 4.125s passed
cancel_gtPos data()[5] 4.000s passed
polyMod_ltdivDenom data()[60] 4.039s passed
bsum_empty data()[61] 4.103s passed
bsum_induction_upper data()[62] 4.045s passed
bsum_induction_lower data()[63] 4.159s passed
bsum_num_of_bounds data()[64] 3.994s passed
bsum_num_of_bounds2 data()[65] 3.981s passed
bsum_induction_upper2 data()[66] 4.137s passed
bsum_induction_upper_concrete data()[67] 4.171s passed
bsum_induction_upper_concrete_2 data()[68] 4.147s passed
bsum_induction_upper2_concrete data()[69] 4.131s passed
cancel_gtNeg data()[6] 3.974s passed
bsum_induction_lower_concrete data()[70] 4.185s passed
bsum_induction_lower2 data()[71] 3.971s passed
bsum_induction_lower2_concrete data()[72] 4.096s passed
bsum_positive data()[73] 4.217s passed
bsum_upper_bound data()[74] 4.088s passed
bsum_lower_bound data()[75] 3.999s passed
bsum_positive_lower_bound_element data()[76] 4.010s passed
bsum_sub_same_index data()[77] 3.909s passed
bsum_less_same_index data()[78] 3.985s passed
bsum_equal_except_one_index data()[79] 3.706s passed
moduloIntIsInInt data()[7] 3.853s passed
bsum_num_of_is_max data()[80] 3.769s passed
bsum_num_of_is_max2 data()[81] 3.769s passed
bsum_num_of_is_max3 data()[82] 3.957s passed
bsum_num_of_is_max4 data()[83] 3.975s passed
bsum_num_of_lt_max data()[84] 3.886s passed
bsum_num_of_lt_max2 data()[85] 3.758s passed
bsum_num_of_lt_max3 data()[86] 3.896s passed
bsum_num_of_lt_max4 data()[87] 4.234s passed
bsum_num_of_gt0 data()[88] 4.270s passed
bsum_num_of_gt0_alt data()[89] 4.129s passed
moduloLongIsInLong data()[8] 3.890s passed
bsum_add_concrete data()[90] 3.987s passed
bprod_all_positive data()[91] 4.157s passed
bprod_split data()[92] 4.175s passed
powConcrete0 data()[93] 4.094s passed
powConcrete1 data()[94] 4.102s passed
powSplitFactor data()[95] 4.072s passed
powAdd data()[96] 4.368s passed
powMono data()[97] 4.700s passed
powMonoConcrete data()[98] 4.290s passed
powMonoConcreteRight data()[99] 4.441s passed
moduloShortIsInShort data()[9] 3.873s passed

Standard output

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

15129      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
19874      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
24116      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
28079      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
32042      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35988      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43793      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
47687      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
51477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
55389      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59467      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63541      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67804      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
72149      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
76241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
80170      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
84054      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
87981      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
91973      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
96072      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
100309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
104314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
108393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
112614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
116805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
120884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
125039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
129351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
133914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
138591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
143217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
147847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
152325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
156475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
160801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
165110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
169396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
173751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
177963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
182254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
186562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
190943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
195379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
199805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
204261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
208765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
212915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
217051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
221210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
225614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
229996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
234043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
238190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
242198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
246126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
250483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
254483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
258633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
262716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
266822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
270899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
274967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
278995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
283018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
287118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
291319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
295448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
299577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
303792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
307770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
311841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
316010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
320123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
324162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
328110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
332116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
335991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
339849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
343568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
347321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
351233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
355264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
359121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
362901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
366764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
370944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
375192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
379368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
383368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
387497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
391680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
395750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
399948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
403913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
408341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
412933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
417331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
421700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
426096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
430297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
434564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
439062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
443302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
447648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
451713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
455590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
459267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
462892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
466573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
470364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
474001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
477681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
481397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
485115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
488910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
492618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
496509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
500203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
504015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
507813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
511689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
515399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
519523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
523330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
527059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
530859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
534567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
538215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
541905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
545545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
549274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
552848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
556741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
560553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
564438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
568528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
572300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
576033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
579692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
583319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
587233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
591226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
595181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
599110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
603090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
607101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
611384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
615786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
619934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
624152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
628405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
632463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
636621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
640707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
644834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
648892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
652819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
656643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
660376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
664431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
668672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
672917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
677167     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
681398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
685533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
689678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
694071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
698200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
702492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
706889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
710856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
714763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
718728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
722736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
726690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
730579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
734518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
738671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
742628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
746704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
750787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
754833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
758928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
763025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
767303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
771486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
775533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
779991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
784212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
788204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
792115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
796233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
800226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
801228     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
801271     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
801291     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
801296     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
801303     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
801306     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
801307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
801310     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
801317     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
801320     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
801325     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
801327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
801577     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
801579     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
801580     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
801583     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
801584     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
801717     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
801719     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
801720     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
801721     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
801723     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
801724     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
801927     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
801929     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
801931     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
801933     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
801934     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
801938     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
802128     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
802130     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
802131     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
802132     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
802133     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
802134     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
802143     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
802144     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
802145     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
802147     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
802148     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
802149     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
802160     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
802161     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
802162     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
802163     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
802164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
802164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
802340     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
802342     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
802344     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
802473     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
802475     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)'' 
802478     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
802480     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
802482     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
802483     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
802485     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
802486     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
802490     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
802493     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
802494     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
802495     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
802496     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
802615     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
802619     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
802620     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
802621     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
802623     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
802624     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
802625     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
802759     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
802761     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
802763     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
802764     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
802765     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
802768     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
802769     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
802770     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
802874     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
802876     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
802974     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
802980     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
802985     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
802986     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
802988     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
802989     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
802990     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
802991     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
802992     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
802993     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
803002     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
803007     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
803114     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
803116     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
803117     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
803118     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
803119     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
803120     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
803120     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
803122     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
803183     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
803190     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
803303     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
803305     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
803307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
803308     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
803309     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
803310     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
803458     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
803465     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
803467     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)'' 
803472     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
803474     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
803475     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
803476     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
803477     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
803488     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
803490     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
803491     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
803492     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
803606     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
803609     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
803610     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
803611     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
803612     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
803613     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
803748     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
803750     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
803751     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
803753     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
803754     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
803755     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
803755     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
803757     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
803885     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
803887     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
803979     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
803980     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
803981     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
803986     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
803991     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
803995     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
804139     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
804141     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
804143     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
804144     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
804155     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
804253     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
808214     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
808216     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)'' 
808221     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
808223     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
808224     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
808225     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
808225     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
808234     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
808279     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
808280     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
808281     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
808282     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
808389     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
808394     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
808396     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
808396     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
808397     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
808398     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
808399     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
808511     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
808513     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
808514     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
808515     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
808516     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
808517     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
808518     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
808519     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
808609     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
808610     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
808705     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
808711     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
808718     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
808719     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
808720     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
808721     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
808733     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
808830     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
808832     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
808832     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
808834     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
808921     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
808932     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
808934     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)'' 
808937     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
808937     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
808938     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
808939     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
808939     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
808951     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
808952     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
808953     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
808954     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
808955     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
809051     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
809053     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
809054     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
809055     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
809056     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
809160     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
809167     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
809169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
809169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
809170     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
809171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
809171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
809277     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
809282     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
809283     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
809285     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
809285     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
809286     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
809286     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
809287     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
809288     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
809289     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
809290     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
809291     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
809291     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
809291     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
809292     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
809452     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
809453     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
809461     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
809603     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
809719     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
809720     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
809721     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
809722     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
809723     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
809723     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
809724     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
809724     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
809725     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
809839     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
809846     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
809950     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
809952     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
809953     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
809954     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
809954     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
809955     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
809955     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
809956     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
809963     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
809964     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
810059     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
810066     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
810072     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
810232     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
810234     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
810235     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
810236     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
810236     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
810237     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
810237     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
810238     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
810306     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
810307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
810307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
810308     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
810309     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
810315     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
810321     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
810451     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
810548     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
810550     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
810550     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
810551     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
810738     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
810840     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
810842     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
814339     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
814345     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
814346     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
814347     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
814347     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
814487     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
814489     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
814490     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
814491     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
814492     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
814637     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
818812     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
822683     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
822689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
822690     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
822691     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
822692     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
822829     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
822831     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
822832     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
822833     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)' ...' 
822836     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
827684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
828734     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
828742     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
828755     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
828757     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
828760     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
828760     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
828765     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
828767     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
828770     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
828773     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
828774     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
828783     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
828785     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
828786     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
828840     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
828847     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
828847     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
828848     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
828848     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
828952     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
828953     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
828955     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
828956     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
828957     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
828960     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
828962     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
828963     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
828964     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
828965     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
828965     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
829064     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
829065     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
829066     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
829068     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
829069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
829070     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
829162     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
829163     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
829164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
829165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
829165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
829167     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
829167     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
829168     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
829169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
829170     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
829171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
829171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
829172     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
829173     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
829174     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
829174     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
829175     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
829176     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
829178     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
829180     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
829221     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
829223     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
829290     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
829292     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
829295     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
829296     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
829297     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
829298     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
829355     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
829358     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
829360     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
829361     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
829363     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
829364     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
829365     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
829413     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
829416     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
829420     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
829485     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
832775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq