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

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

tests
0

failures
0

ignored
10m42.20s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.127s passed
powPositiveConcrete data()[101] 3.159s passed
powGeq1Concrete data()[102] 3.129s passed
pow2InIntLower data()[103] 3.125s passed
pow2InIntUpper data()[104] 3.122s passed
logSelfConcrete data()[105] 3.148s passed
log1Concrete data()[106] 3.142s passed
logProduct data()[107] 3.165s passed
logTimesBaseConcrete data()[108] 3.126s passed
logProdIdentity data()[109] 3.155s passed
moduloByteIsInByte data()[10] 3.271s passed
logProdIdentityConcrete data()[110] 3.166s passed
logPowIdentity data()[111] 3.180s passed
logPowIdentityConcrete data()[112] 3.127s passed
logPositive data()[113] 3.140s passed
logPositiveConcrete data()[114] 3.126s passed
logMono data()[115] 3.213s passed
logMonoConcrete data()[116] 3.132s passed
powLogLess data()[117] 3.139s passed
powLogMore2 data()[118] 3.146s passed
logLessThanPow data()[119] 3.191s passed
moduloCharIsInChar data()[11] 3.234s passed
logLessThanPowConcrete data()[120] 3.137s passed
logSqueeze data()[121] 3.112s passed
ifthenelse_equals data()[122] 3.143s passed
ifthenelse_equals_1 data()[123] 3.128s passed
ifthenelse_equals_2 data()[124] 3.131s passed
disjointWithSingleton1 data()[125] 3.124s passed
disjointWithSingleton2 data()[126] 3.142s passed
disjointArrayRanges data()[127] 3.143s passed
disjointArrayRangeAllFields1 data()[128] 3.135s passed
disjointArrayRangeAllFields2 data()[129] 3.156s passed
div_unique1 data()[12] 3.306s passed
seqSelfDefinition data()[130] 3.132s passed
seqOutsideValue data()[131] 3.153s passed
castedGetAny data()[132] 3.129s passed
seqGetAlphaCast data()[133] 3.127s passed
getOfSeqSingleton data()[134] 3.156s passed
getOfSeqSingletonConcrete data()[135] 3.147s passed
getOfSeqConcat data()[136] 3.167s passed
getOfSeqSub data()[137] 3.157s passed
getOfSeqReverse data()[138] 3.142s passed
lenOfSeqEmpty data()[139] 3.165s passed
div_unique2 data()[13] 3.343s passed
lenOfSeqSingleton data()[140] 3.137s passed
lenOfSeqConcat data()[141] 3.180s passed
lenOfSeqSub data()[142] 3.135s passed
lenOfSeqReverse data()[143] 3.161s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.130s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.156s passed
getOfSeqSingletonEQ data()[146] 3.146s passed
getOfSeqConcatEQ data()[147] 3.160s passed
getOfSeqSubEQ data()[148] 3.165s passed
getOfSeqReverseEQ data()[149] 3.160s passed
div_exists data()[14] 3.500s passed
lenOfSeqEmptyEQ data()[150] 3.157s passed
lenOfSeqSingletonEQ data()[151] 3.139s passed
lenOfSeqConcatEQ data()[152] 3.163s passed
lenOfSeqSubEQ data()[153] 3.151s passed
lenOfSeqReverseEQ data()[154] 3.151s passed
getOfSeqDefEQ data()[155] 3.140s passed
lenOfSeqDefEQ data()[156] 3.137s passed
seqConcatWithSeqEmpty1 data()[157] 3.151s passed
seqConcatWithSeqEmpty2 data()[158] 3.185s passed
seqReverseOfSeqEmpty data()[159] 3.167s passed
div_one data()[15] 3.225s passed
subSeqComplete data()[160] 3.167s passed
subSeqTailR data()[161] 3.169s passed
subSeqTailL data()[162] 3.184s passed
subSeqTailEQR data()[163] 3.196s passed
subSeqTailEQL data()[164] 3.159s passed
seqDef_split data()[165] 3.209s passed
seqDef_induction_upper data()[166] 3.174s passed
seqDef_induction_upper_concrete data()[167] 3.187s passed
seqDef_induction_lower data()[168] 3.189s passed
seqDef_induction_lower_concrete data()[169] 3.188s passed
jdiv_one data()[16] 3.218s passed
seqDef_split_in_three data()[170] 3.367s passed
seqDef_empty data()[171] 3.176s passed
seqDef_one_summand data()[172] 3.157s passed
seqDef_lower_equals_upper data()[173] 3.140s passed
seqDefOfSeq data()[174] 3.159s passed
seqSelfDefinitionEQ2 data()[175] 3.154s passed
indexOfSeqSingleton data()[176] 3.152s passed
indexOfSeqConcatFirst data()[177] 3.157s passed
indexOfSeqConcatSecond data()[178] 3.194s passed
indexOfSeqSub data()[179] 3.185s passed
div_zero data()[17] 3.244s passed
lenOfArray2seq data()[180] 3.157s passed
getAnyOfArray2seq data()[181] 3.150s passed
getOfArray2seq data()[182] 3.158s passed
getAnyOfNPermInv data()[183] 3.146s passed
seqNPermRange data()[184] 3.225s passed
seqPermTrans data()[185] 3.240s passed
seqPermRefl data()[186] 3.167s passed
seqPermSplit data()[187] 3.156s passed
seqNPermRight data()[188] 3.503s passed
seqPermFromSwap data()[189] 3.324s passed
divResZero1 data()[18] 3.228s passed
seqPermTransAlt0 data()[190] 3.167s passed
seqPermTransAlt1 data()[191] 3.158s passed
seqPermTransAlt2 data()[192] 3.159s passed
seqPermTransAlt3 data()[193] 3.147s passed
schiffl_lemma_2 data()[194] 20.481s passed
schiffl_thm_1 data()[195] 3.889s passed
eqSameSeq data()[196] 3.386s passed
divResZero2 data()[19] 3.194s passed
eqTermCut data()[1] 3.872s passed
divResOne1 data()[20] 3.208s passed
divResOne2 data()[21] 3.169s passed
div_cancel1 data()[22] 3.206s passed
div_cancel2 data()[23] 3.174s passed
divAddMultDenom data()[24] 3.210s passed
divMinus data()[25] 3.234s passed
divMinusDenom data()[26] 3.191s passed
divLeastDPos data()[27] 3.193s passed
divLeastDNeg data()[28] 3.171s passed
divGreatestDPos data()[29] 3.191s passed
equivAllRight data()[2] 3.574s passed
divGreatestDNeg data()[30] 3.226s passed
divIncreasingPos data()[31] 3.148s passed
divIncreasingNeg data()[32] 3.167s passed
jdiv_zero data()[33] 3.152s passed
jdivPulloutMinusNum data()[34] 3.165s passed
jdivPulloutMinusDenom data()[35] 3.233s passed
jdiv_uniquePosPos data()[36] 3.184s passed
jdiv_uniquePosNeg data()[37] 3.200s passed
jdiv_uniqueNegPos data()[38] 3.210s passed
jdiv_uniqueNegNeg data()[39] 3.169s passed
irrflConcrete1 data()[3] 3.467s passed
jdivMultDenom1 data()[40] 3.186s passed
jdivMultDenom2 data()[41] 3.134s passed
mod_geZero data()[42] 3.159s passed
mod_lessDenom data()[43] 3.166s passed
jmod_NumPos data()[44] 3.176s passed
jmod_NumNeg data()[45] 3.186s passed
jmod_geZero data()[46] 3.163s passed
jmodNumZero data()[47] 3.226s passed
jmod_pulloutminusNum data()[48] 3.162s passed
jmod_pulloutminusDenom data()[49] 3.145s passed
irrflConcrete2 data()[4] 3.323s passed
jmodUnique1 data()[50] 3.257s passed
jmodUnique2 data()[51] 3.325s passed
intDivRem data()[52] 3.150s passed
jmodjmod data()[53] 3.226s passed
jmodDivisible data()[54] 3.184s passed
jmodDivisibleRep data()[55] 3.149s passed
jdivAddMultDenom data()[56] 3.367s passed
jmodAltZero data()[57] 3.151s passed
jmodAddMultDenomZero data()[58] 3.137s passed
polyDiv_zero data()[59] 3.142s passed
cancel_gtPos data()[5] 3.350s passed
polyMod_ltdivDenom data()[60] 3.161s passed
bsum_empty data()[61] 3.136s passed
bsum_induction_upper data()[62] 3.125s passed
bsum_induction_lower data()[63] 3.159s passed
bsum_num_of_bounds data()[64] 3.172s passed
bsum_num_of_bounds2 data()[65] 3.171s passed
bsum_induction_upper2 data()[66] 3.162s passed
bsum_induction_upper_concrete data()[67] 3.122s passed
bsum_induction_upper_concrete_2 data()[68] 3.126s passed
bsum_induction_upper2_concrete data()[69] 3.136s passed
cancel_gtNeg data()[6] 3.268s passed
bsum_induction_lower_concrete data()[70] 3.116s passed
bsum_induction_lower2 data()[71] 3.119s passed
bsum_induction_lower2_concrete data()[72] 3.124s passed
bsum_positive data()[73] 3.201s passed
bsum_upper_bound data()[74] 3.203s passed
bsum_lower_bound data()[75] 3.166s passed
bsum_positive_lower_bound_element data()[76] 3.185s passed
bsum_sub_same_index data()[77] 3.148s passed
bsum_less_same_index data()[78] 3.197s passed
bsum_equal_except_one_index data()[79] 3.163s passed
moduloIntIsInInt data()[7] 3.274s passed
bsum_num_of_is_max data()[80] 3.163s passed
bsum_num_of_is_max2 data()[81] 3.179s passed
bsum_num_of_is_max3 data()[82] 3.160s passed
bsum_num_of_is_max4 data()[83] 3.178s passed
bsum_num_of_lt_max data()[84] 3.163s passed
bsum_num_of_lt_max2 data()[85] 3.151s passed
bsum_num_of_lt_max3 data()[86] 3.183s passed
bsum_num_of_lt_max4 data()[87] 3.171s passed
bsum_num_of_gt0 data()[88] 3.153s passed
bsum_num_of_gt0_alt data()[89] 3.150s passed
moduloLongIsInLong data()[8] 3.255s passed
bsum_add_concrete data()[90] 3.135s passed
bprod_all_positive data()[91] 3.169s passed
bprod_split data()[92] 3.179s passed
powConcrete0 data()[93] 3.119s passed
powConcrete1 data()[94] 3.116s passed
powSplitFactor data()[95] 3.117s passed
powAdd data()[96] 3.147s passed
powMono data()[97] 3.144s passed
powMonoConcrete data()[98] 3.118s passed
powMonoConcreteRight data()[99] 3.117s passed
moduloShortIsInShort data()[9] 3.226s passed

Standard output

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

11292      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15003      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18492      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21873      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25215      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28495      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
31775      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
35023      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
38295      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41541      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44780      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47989      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51323      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58160      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
61354      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64562      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67854      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
71041      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
74252      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80613      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86985      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90197      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93412      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
96641      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99826      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
106233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
109381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
122033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
150686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
153859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
166577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
169715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
173015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
176306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
179478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
182687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
185887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
189039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
192379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
195523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
198675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
201809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
204967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
208090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
211246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
214399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
217570     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
220759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
223883     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
227024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
230146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
233264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
236374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
239505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
242660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
245870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
249040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
252213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
255402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
258550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
261730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
264902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
268063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
271264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
274418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
277575     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
280731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
283931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
287084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
290239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
293388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
296569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
299699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
302849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
306021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
309135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
312269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
315399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
318524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
321661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
324778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
327919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
331066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
334192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
337315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
340459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
343598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
346728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
349887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
353018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
356168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
359333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
362520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
365647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
368767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
371933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
375064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
378259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
381374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
384543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
387680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
390877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
393984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
397126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
400254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
403383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
406529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
409650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
412780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
415938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
419076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
422204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
425354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
428491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
431638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
434772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
437920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
441080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
444240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
447399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
450540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
453707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
456865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
459999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
463164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
466297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
469451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
472613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
475752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
478924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
482078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
485240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
488379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
491539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
494693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
497843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
500987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
504119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
507259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
510435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
513615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
516784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
519937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
523125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
526314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
529488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
532649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
535857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
539032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
542221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
545404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
548597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
551975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
555140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
558302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
561428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
564591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
567746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
570891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
574065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
577255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
580441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
583592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
586746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
589894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
593043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
596266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
599509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
602683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
605836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
609403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
612674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
615833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
618995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
622142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
625317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
626132     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
626192     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
626213     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
626220     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
626229     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
626231     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
626232     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
626236     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
626242     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
626244     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
626249     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
626251     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
626485     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
626488     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
626490     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
626491     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
626493     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
626607     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
626608     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
626612     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
626614     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
626615     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
626616     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
626777     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
626780     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
626782     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
626783     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
626783     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
626787     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
626908     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
626911     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
626913     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
626915     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
626916     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
626917     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
626926     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
626928     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
626929     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
626931     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
626934     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
626935     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
626943     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
626944     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
626945     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
626946     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
626947     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
626948     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
627067     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
627069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
627070     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
627168     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
627171     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)'' 
627173     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
627175     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
627177     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
627178     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
627179     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
627180     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
627192     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
627195     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
627197     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
627197     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
627199     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
627290     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
627294     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
627296     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
627297     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
627298     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
627299     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
627300     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
627398     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
627400     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
627401     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
627403     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
627404     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
627405     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
627406     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
627408     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
627483     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
627485     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
627572     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
627576     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
627580     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
627582     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
627583     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
627584     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
627585     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
627585     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
627586     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
627587     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
627594     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
627598     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
627687     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
627689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
627690     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
627691     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
627692     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
627692     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
627693     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
627694     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
627739     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
627744     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
627825     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
627827     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
627829     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
627831     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
627832     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
627833     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
627949     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
627953     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
627955     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)'' 
627957     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
627958     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
627959     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
627959     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
627960     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
627968     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
627970     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
627971     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
627972     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
628060     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
628062     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
628063     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
628064     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
628064     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
628065     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
628163     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
628165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
628166     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
628167     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
628168     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
628169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
628169     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
628171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
628247     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
628248     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
628316     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
628317     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
628318     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
628322     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
628326     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
628330     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
628437     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
628439     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
628440     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
628441     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
628450     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
628565     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
631854     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
631855     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)'' 
631860     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
631861     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
631862     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
631863     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
631863     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
631870     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
631872     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
631873     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
631874     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
631874     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
631958     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
631962     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
631963     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
631965     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
631965     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
631966     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
631967     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
632051     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
632053     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
632054     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
632055     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
632056     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
632057     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
632057     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
632059     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
632127     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
632129     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
632237     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
632241     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
632245     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
632246     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
632247     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
632248     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
632257     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
632327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
632328     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
632329     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
632332     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
632395     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
632403     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
632404     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)'' 
632406     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
632407     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
632407     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
632408     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
632408     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
632418     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
632419     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
632420     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
632420     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
632421     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
632497     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
632499     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
632500     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
632501     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
632502     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
632590     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
632594     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
632595     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
632596     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
632597     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
632597     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
632598     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
632684     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
632685     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
632687     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
632688     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
632689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
632691     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
632693     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
632694     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
632695     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
632696     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
632697     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
632697     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
632698     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
632699     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
632700     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
632778     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
632779     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
632785     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
632853     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
632923     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
632925     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
632926     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
632926     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
632927     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
632928     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
632928     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
632928     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
632930     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
633006     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
633011     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
633091     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
633092     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
633093     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
633094     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
633094     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
633094     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
633095     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
633095     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
633100     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
633101     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
633171     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
633176     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
633181     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
633272     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
633273     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
633274     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
633275     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
633276     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
633276     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
633276     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
633277     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
633326     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
633327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
633327     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
633328     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
633329     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
633334     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
633338     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
633441     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
633519     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
633520     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
633521     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
633522     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
633671     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
633793     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
633794     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
636476     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
636481     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
636482     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
636482     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
636483     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
636584     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
636585     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
636586     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
636587     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
636588     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
636682     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
639410     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
642262     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
642267     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
642268     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
642268     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
642269     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
642369     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
642370     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
642371     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
642372     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)' ...' 
642374     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
645831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
646678     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
646689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
646700     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
646703     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
646704     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
646705     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
646710     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
646711     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
646714     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
646717     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
646718     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
646726     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
646728     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
646729     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
646775     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
646781     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
646784     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
646784     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
646785     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
646846     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
646847     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
646849     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
646849     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
646850     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
646853     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
646854     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
646855     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
646856     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
646857     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
646857     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
646934     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
646935     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
646936     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
646938     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
646939     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
646939     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
647012     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
647013     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
647014     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
647015     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
647015     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
647017     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
647017     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
647018     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
647019     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
647019     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
647019     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
647020     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
647021     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
647021     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
647022     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
647022     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
647023     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
647024     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
647025     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
647027     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
647060     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
647061     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
647108     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
647110     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
647111     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
647113     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
647113     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
647114     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
647157     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
647159     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
647161     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
647162     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
647163     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
647164     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
647165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
647206     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
647208     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
647211     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
647256     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
649741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq