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

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

tests
0

failures
0

ignored
12m39.92s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.625s passed
powPositiveConcrete data()[101] 3.655s passed
powGeq1Concrete data()[102] 3.758s passed
pow2InIntLower data()[103] 3.631s passed
pow2InIntUpper data()[104] 3.573s passed
logSelfConcrete data()[105] 3.651s passed
log1Concrete data()[106] 3.868s passed
logProduct data()[107] 3.588s passed
logTimesBaseConcrete data()[108] 3.769s passed
logProdIdentity data()[109] 3.712s passed
moduloByteIsInByte data()[10] 3.662s passed
logProdIdentityConcrete data()[110] 3.669s passed
logPowIdentity data()[111] 3.603s passed
logPowIdentityConcrete data()[112] 3.771s passed
logPositive data()[113] 3.959s passed
logPositiveConcrete data()[114] 3.671s passed
logMono data()[115] 3.738s passed
logMonoConcrete data()[116] 3.771s passed
powLogLess data()[117] 3.643s passed
powLogMore2 data()[118] 3.712s passed
logLessThanPow data()[119] 3.712s passed
moduloCharIsInChar data()[11] 3.640s passed
logLessThanPowConcrete data()[120] 3.619s passed
logSqueeze data()[121] 3.752s passed
ifthenelse_equals data()[122] 3.594s passed
ifthenelse_equals_1 data()[123] 3.533s passed
ifthenelse_equals_2 data()[124] 3.578s passed
disjointWithSingleton1 data()[125] 3.616s passed
disjointWithSingleton2 data()[126] 3.676s passed
disjointArrayRanges data()[127] 3.560s passed
disjointArrayRangeAllFields1 data()[128] 3.668s passed
disjointArrayRangeAllFields2 data()[129] 3.832s passed
div_unique1 data()[12] 3.730s passed
seqSelfDefinition data()[130] 3.913s passed
seqOutsideValue data()[131] 3.718s passed
castedGetAny data()[132] 3.725s passed
seqGetAlphaCast data()[133] 3.644s passed
getOfSeqSingleton data()[134] 3.679s passed
getOfSeqSingletonConcrete data()[135] 3.678s passed
getOfSeqConcat data()[136] 3.617s passed
getOfSeqSub data()[137] 3.715s passed
getOfSeqReverse data()[138] 3.666s passed
lenOfSeqEmpty data()[139] 3.723s passed
div_unique2 data()[13] 3.706s passed
lenOfSeqSingleton data()[140] 3.890s passed
lenOfSeqConcat data()[141] 3.965s passed
lenOfSeqSub data()[142] 3.782s passed
lenOfSeqReverse data()[143] 3.648s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.985s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.670s passed
getOfSeqSingletonEQ data()[146] 3.909s passed
getOfSeqConcatEQ data()[147] 3.674s passed
getOfSeqSubEQ data()[148] 3.717s passed
getOfSeqReverseEQ data()[149] 3.737s passed
div_exists data()[14] 4.154s passed
lenOfSeqEmptyEQ data()[150] 3.754s passed
lenOfSeqSingletonEQ data()[151] 3.673s passed
lenOfSeqConcatEQ data()[152] 3.708s passed
lenOfSeqSubEQ data()[153] 3.815s passed
lenOfSeqReverseEQ data()[154] 3.661s passed
getOfSeqDefEQ data()[155] 3.669s passed
lenOfSeqDefEQ data()[156] 3.669s passed
seqConcatWithSeqEmpty1 data()[157] 3.849s passed
seqConcatWithSeqEmpty2 data()[158] 3.887s passed
seqReverseOfSeqEmpty data()[159] 3.818s passed
div_one data()[15] 3.762s passed
subSeqComplete data()[160] 3.976s passed
subSeqTailR data()[161] 3.740s passed
subSeqTailL data()[162] 3.735s passed
subSeqTailEQR data()[163] 3.693s passed
subSeqTailEQL data()[164] 3.676s passed
seqDef_split data()[165] 3.885s passed
seqDef_induction_upper data()[166] 3.933s passed
seqDef_induction_upper_concrete data()[167] 3.856s passed
seqDef_induction_lower data()[168] 3.704s passed
seqDef_induction_lower_concrete data()[169] 3.819s passed
jdiv_one data()[16] 3.575s passed
seqDef_split_in_three data()[170] 4.098s passed
seqDef_empty data()[171] 3.813s passed
seqDef_one_summand data()[172] 4.096s passed
seqDef_lower_equals_upper data()[173] 4.145s passed
seqDefOfSeq data()[174] 4.060s passed
seqSelfDefinitionEQ2 data()[175] 3.941s passed
indexOfSeqSingleton data()[176] 3.899s passed
indexOfSeqConcatFirst data()[177] 3.955s passed
indexOfSeqConcatSecond data()[178] 3.892s passed
indexOfSeqSub data()[179] 3.925s passed
div_zero data()[17] 3.896s passed
lenOfArray2seq data()[180] 3.887s passed
getAnyOfArray2seq data()[181] 3.880s passed
getOfArray2seq data()[182] 3.818s passed
getAnyOfNPermInv data()[183] 3.879s passed
seqNPermRange data()[184] 3.996s passed
seqPermTrans data()[185] 3.962s passed
seqPermRefl data()[186] 3.628s passed
seqPermSplit data()[187] 3.669s passed
seqNPermRight data()[188] 4.255s passed
seqPermFromSwap data()[189] 3.930s passed
divResZero1 data()[18] 3.914s passed
seqPermTransAlt0 data()[190] 3.845s passed
seqPermTransAlt1 data()[191] 3.892s passed
seqPermTransAlt2 data()[192] 3.713s passed
seqPermTransAlt3 data()[193] 3.857s passed
schiffl_lemma_2 data()[194] 24.656s passed
schiffl_thm_1 data()[195] 4.439s passed
eqSameSeq data()[196] 3.792s passed
divResZero2 data()[19] 3.922s passed
eqTermCut data()[1] 4.738s passed
divResOne1 data()[20] 3.639s passed
divResOne2 data()[21] 3.651s passed
div_cancel1 data()[22] 3.564s passed
div_cancel2 data()[23] 3.588s passed
divAddMultDenom data()[24] 3.855s passed
divMinus data()[25] 3.651s passed
divMinusDenom data()[26] 3.655s passed
divLeastDPos data()[27] 3.581s passed
divLeastDNeg data()[28] 3.591s passed
divGreatestDPos data()[29] 3.600s passed
equivAllRight data()[2] 4.174s passed
divGreatestDNeg data()[30] 3.952s passed
divIncreasingPos data()[31] 3.699s passed
divIncreasingNeg data()[32] 3.765s passed
jdiv_zero data()[33] 3.676s passed
jdivPulloutMinusNum data()[34] 3.596s passed
jdivPulloutMinusDenom data()[35] 3.714s passed
jdiv_uniquePosPos data()[36] 3.581s passed
jdiv_uniquePosNeg data()[37] 3.682s passed
jdiv_uniqueNegPos data()[38] 3.731s passed
jdiv_uniqueNegNeg data()[39] 3.759s passed
irrflConcrete1 data()[3] 4.589s passed
jdivMultDenom1 data()[40] 3.776s passed
jdivMultDenom2 data()[41] 3.539s passed
mod_geZero data()[42] 3.632s passed
mod_lessDenom data()[43] 3.728s passed
jmod_NumPos data()[44] 3.635s passed
jmod_NumNeg data()[45] 3.614s passed
jmod_geZero data()[46] 3.581s passed
jmodNumZero data()[47] 3.567s passed
jmod_pulloutminusNum data()[48] 3.695s passed
jmod_pulloutminusDenom data()[49] 3.571s passed
irrflConcrete2 data()[4] 3.792s passed
jmodUnique1 data()[50] 3.774s passed
jmodUnique2 data()[51] 3.816s passed
intDivRem data()[52] 3.681s passed
jmodjmod data()[53] 3.682s passed
jmodDivisible data()[54] 3.675s passed
jmodDivisibleRep data()[55] 3.775s passed
jdivAddMultDenom data()[56] 3.904s passed
jmodAltZero data()[57] 3.738s passed
jmodAddMultDenomZero data()[58] 3.656s passed
polyDiv_zero data()[59] 3.650s passed
cancel_gtPos data()[5] 3.824s passed
polyMod_ltdivDenom data()[60] 3.734s passed
bsum_empty data()[61] 3.730s passed
bsum_induction_upper data()[62] 3.732s passed
bsum_induction_lower data()[63] 3.771s passed
bsum_num_of_bounds data()[64] 3.706s passed
bsum_num_of_bounds2 data()[65] 3.703s passed
bsum_induction_upper2 data()[66] 3.688s passed
bsum_induction_upper_concrete data()[67] 3.796s passed
bsum_induction_upper_concrete_2 data()[68] 3.751s passed
bsum_induction_upper2_concrete data()[69] 3.816s passed
cancel_gtNeg data()[6] 3.741s passed
bsum_induction_lower_concrete data()[70] 3.872s passed
bsum_induction_lower2 data()[71] 3.816s passed
bsum_induction_lower2_concrete data()[72] 3.760s passed
bsum_positive data()[73] 3.833s passed
bsum_upper_bound data()[74] 3.918s passed
bsum_lower_bound data()[75] 3.999s passed
bsum_positive_lower_bound_element data()[76] 3.925s passed
bsum_sub_same_index data()[77] 3.913s passed
bsum_less_same_index data()[78] 3.892s passed
bsum_equal_except_one_index data()[79] 3.700s passed
moduloIntIsInInt data()[7] 3.778s passed
bsum_num_of_is_max data()[80] 3.816s passed
bsum_num_of_is_max2 data()[81] 3.751s passed
bsum_num_of_is_max3 data()[82] 3.833s passed
bsum_num_of_is_max4 data()[83] 3.731s passed
bsum_num_of_lt_max data()[84] 3.791s passed
bsum_num_of_lt_max2 data()[85] 3.776s passed
bsum_num_of_lt_max3 data()[86] 3.701s passed
bsum_num_of_lt_max4 data()[87] 3.689s passed
bsum_num_of_gt0 data()[88] 3.623s passed
bsum_num_of_gt0_alt data()[89] 3.636s passed
moduloLongIsInLong data()[8] 3.895s passed
bsum_add_concrete data()[90] 3.738s passed
bprod_all_positive data()[91] 3.628s passed
bprod_split data()[92] 3.756s passed
powConcrete0 data()[93] 3.707s passed
powConcrete1 data()[94] 3.638s passed
powSplitFactor data()[95] 3.866s passed
powAdd data()[96] 3.744s passed
powMono data()[97] 3.687s passed
powMonoConcrete data()[98] 3.649s passed
powMonoConcreteRight data()[99] 3.619s passed
moduloShortIsInShort data()[9] 3.766s passed

Standard output

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

14215      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
18559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
23105      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
27028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30819      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34580      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38351      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42242      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
49769      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
53365      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
57047      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
60736      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
64619      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
68731      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
72320      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
76017      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
80050      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
84026      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
87666      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
91361      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
94927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
98446      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
102314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
105919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
109603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
113225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
116810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
120433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
124237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
128008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
131787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
135520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
139108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
142747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
146364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
150096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
153767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
157566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
161242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
164931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
168494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
172243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
175855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
179510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
183087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
186681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
190298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
193908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
197558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
201257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
205235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
208807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
212493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
216328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
219983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
223953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
227624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
231277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
234942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
238694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
242466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
246210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
249894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
253621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
257330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
261149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
264877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
268637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
272516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
276330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
280173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
283887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
287756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
291791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
295722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
299670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
303553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
307283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
311080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
314860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
318647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
322426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
326151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
329964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
333691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
337390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
341034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
344675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
348424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
352038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
355711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
359498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
363172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
366983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
370756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
374412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
378102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
381721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
385344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
388994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
392750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
396409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
399982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
403581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
407422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
411105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
414774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
418483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
422226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
425825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
429542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
433514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
437222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
440893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
444733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
448344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
452054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
455737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
459415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
463131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
466774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
470336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
473887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
477486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
481139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
484734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
488404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
492147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
496077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
499870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
503513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
507233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
510893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
514561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
518206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
521899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
525583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
529294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
533151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
537096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
540924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
544595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
548493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
552231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
556124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
559807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
563499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
567202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
571020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
574713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
578351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
582219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
585881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
589544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
593214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
596986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
600886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
604762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
608673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
612455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
616199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
619892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
623575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
627402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
631267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
635216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
638928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
642693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
646530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
650679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
654648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
658833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
662920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
666841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
670766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
674722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
678642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
682524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
686447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
690368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
694125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
698049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
701942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
705907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
709662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
713316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
717086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
721378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
725307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
729172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
732956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
736840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
740698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
741659     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
741728     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
741749     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
741757     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
741765     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
741770     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
741771     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
741775     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
741780     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
741783     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
741787     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
741789     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
742048     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
742050     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
742052     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
742054     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
742055     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
742225     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
742227     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
742232     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
742234     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
742236     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
742237     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
742446     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
742449     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
742450     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
742451     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
742461     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
742462     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
742608     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
742613     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
742615     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
742616     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
742617     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
742618     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
742625     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
742627     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
742628     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
742630     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
742632     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
742633     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
742640     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
742642     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
742643     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
742644     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
742645     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
742646     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
742787     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
742788     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
742790     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
742922     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
742924     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)'' 
742927     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
742928     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
742931     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
742932     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
742933     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
742934     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
742941     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
742945     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
742947     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
742948     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
742949     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
743071     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
743076     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
743078     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
743079     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
743080     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
743081     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
743082     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
743205     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
743207     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
743208     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
743211     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
743213     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
743215     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
743216     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
743217     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
743312     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
743314     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
743424     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
743429     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
743433     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
743434     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
743435     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
743437     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
743437     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
743438     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
743439     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
743440     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
743448     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
743453     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
743542     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
743544     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
743545     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
743546     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
743547     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
743548     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
743548     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
743549     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
743600     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
743606     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
743708     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
743710     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
743712     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
743714     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
743715     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
743717     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
743844     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
743849     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
743850     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)'' 
743852     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
743853     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
743854     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
743855     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
743856     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
743864     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
743866     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
743867     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
743868     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
743965     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
743967     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
743972     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
743974     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
743975     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
743975     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
744077     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
744079     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
744080     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
744082     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
744083     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
744083     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
744084     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
744085     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
744169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
744171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
744298     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
744298     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
744299     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
744303     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
744307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
744311     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
744432     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
744433     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
744434     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
744435     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
744446     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
744530     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
748345     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
748347     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)'' 
748353     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
748354     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
748355     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
748358     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
748358     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
748367     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
748369     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
748371     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
748372     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
748373     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
748474     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
748479     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
748481     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
748481     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
748482     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
748483     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
748484     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
748585     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
748587     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
748588     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
748591     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
748593     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
748593     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
748594     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
748595     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
748723     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
748724     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
748802     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
748806     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
748811     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
748812     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
748812     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
748813     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
748824     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
748907     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
748908     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
748909     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
748910     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
748987     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
748997     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
748998     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)'' 
749000     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
749001     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
749002     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
749003     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
749003     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
749015     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
749016     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
749018     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
749018     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
749019     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
749111     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
749113     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
749114     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
749115     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
749116     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
749212     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
749217     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
749218     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
749219     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
749219     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
749220     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
749221     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
749324     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
749325     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
749326     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
749328     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
749328     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
749329     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
749329     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
749330     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
749331     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
749332     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
749333     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
749334     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
749334     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
749335     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
749336     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
749429     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
749430     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
749436     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
749519     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
749605     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
749606     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
749607     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
749608     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
749609     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
749610     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
749610     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
749610     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
749611     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
749704     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
749710     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
749806     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
749808     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
749808     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
749810     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
749810     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
749810     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
749811     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
749812     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
749817     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
749818     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
749905     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
749911     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
749917     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
750023     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
750025     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
750026     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
750027     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
750028     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
750028     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
750029     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
750030     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
750088     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
750090     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
750091     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
750092     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
750093     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
750099     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
750105     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
750231     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
750325     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
750327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
750328     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
750329     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
750573     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
750668     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
750669     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
753948     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
753954     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
753956     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
753956     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
753957     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
754136     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
754138     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
754139     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
754140     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
754140     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
754253     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
757535     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
761005     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
761011     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
761012     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
761013     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
761014     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
761137     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
761138     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
761139     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
761140     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)' ...' 
761142     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
765180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
766126     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
766133     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
766145     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
766148     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
766150     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
766151     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
766156     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
766158     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
766160     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
766164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
766164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
766175     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
766177     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
766178     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
766260     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
766261     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
766262     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
766262     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
766263     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
766327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
766327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
766329     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
766330     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
766331     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
766334     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
766335     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
766335     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
766337     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
766338     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
766338     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
766414     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
766416     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
766416     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
766420     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
766421     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
766422     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
766503     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
766504     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
766505     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
766506     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
766507     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
766508     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
766509     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
766509     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
766510     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
766512     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
766513     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
766513     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
766514     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
766515     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
766515     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
766516     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
766517     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
766518     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
766519     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
766523     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
766559     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
766561     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
766611     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
766613     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
766615     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
766616     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
766617     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
766618     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
766665     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
766667     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
766669     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
766671     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
766672     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
766673     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
766674     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
766721     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
766724     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
766727     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
766789     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
769625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq