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

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

198

tests

failures

ignored

10m46.80s

duration

99%

successful

Failed tests
Tests
Standard output

Failed tests

schiffl_lemma_2

de.uka.ilkd.key.macros.scripts.ScriptException: Error while executing script: No matching applications.

Command: rule getOfSwap
	at app//de.uka.ilkd.key.macros.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:174)
	at app//de.uka.ilkd.key.proof.proverules.ProveRulesTest.loadTacletProof(ProveRulesTest.java:72)
	at app//de.uka.ilkd.key.proof.proverules.ProveRulesTest.lambda$data$0(ProveRulesTest.java:144)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.lambda$execute$0(DynamicTestTestDescriptor.java:53)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
	at app//org.junit.jupiter.api.extension.InvocationInterceptor.interceptDynamicTest(InvocationInterceptor.java:167)
	at app//org.junit.jupiter.api.extension.InvocationInterceptor.interceptDynamicTest(InvocationInterceptor.java:184)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.lambda$execute$1(DynamicTestTestDescriptor.java:61)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptorCall.lambda$ofVoid$0(InvocationInterceptorChain.java:78)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
	at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.execute(DynamicTestTestDescriptor.java:60)
	at app//org.junit.jupiter.engine.descriptor.DynamicTestTestDescriptor.execute(DynamicTestTestDescriptor.java:32)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:226)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask$DefaultDynamicTestExecutor.execute(NodeTestTask.java:204)
	at java.base@11.0.18/java.util.Optional.ifPresent(Optional.java:183)
	at app//org.junit.jupiter.engine.descriptor.TestFactoryTestDescriptor.lambda$invokeTestMethod$1(TestFactoryTestDescriptor.java:108)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.jupiter.engine.descriptor.TestFactoryTestDescriptor.invokeTestMethod(TestFactoryTestDescriptor.java:95)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at java.base@11.0.18/java.util.ArrayList.forEach(ArrayList.java:1541)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at java.base@11.0.18/java.util.ArrayList.forEach(ArrayList.java:1541)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
	at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
	at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
	at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
	at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
	at app//org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:110)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:90)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:85)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62)
	at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
	at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
	at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
	at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
	at com.sun.proxy.$Proxy2.stop(Unknown Source)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:193)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
	at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
	at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
	at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
	at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Caused by: de.uka.ilkd.key.macros.scripts.ScriptException: No matching applications.
	at app//de.uka.ilkd.key.macros.scripts.RuleCommand.findTacletApp(RuleCommand.java:225)
	at app//de.uka.ilkd.key.macros.scripts.RuleCommand.makeRuleApp(RuleCommand.java:99)
	at app//de.uka.ilkd.key.macros.scripts.RuleCommand.execute(RuleCommand.java:55)
	at app//de.uka.ilkd.key.macros.scripts.RuleCommand.execute(RuleCommand.java:35)
	at app//de.uka.ilkd.key.macros.scripts.ProofScriptEngine.execute(ProofScriptEngine.java:148)
	... 92 more

Tests

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

Standard output

525        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src/test/resources/testcase/dummyTrue.key 
754        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)

756        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/standardRules.key 
784        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key 
789        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/boolean.key 
798        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key 
836        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerHeader.key 
843        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatHeader.key 
845        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heap.key 
849        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSets.key 
850        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permission.key 
851        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reach.key 
852        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seq.key 
853        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/map.key 
882        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/freeADT.key 
883        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wellfound.key 
885        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListHeader.key 
988        DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/propRule.key 
1013       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/firstOrderRules.key 
1052       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ifThenElseRules.key 
1092       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/formulaNormalisationRules.key 
1242       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/updateRules.key 
1297       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerRulesCommon.key 
1412       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRules.key 
1429       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key 
1437       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesCheckedSemantics.key 
1448       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key 
1469       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key 
1606       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1608       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1612       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1612       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1671       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intDiv.key 
1707       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bsum.key 
1787       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bprod.key 
1841       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryAxioms.key 
1846       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryLemmas.key 
1856       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intPow.key 
1868       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesCommon.key 
1891       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRules.key 
1893       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key 
1894       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key 
1929       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/genericRules.key 
1945       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/booleanRules.key 
1949       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/epsilon.key 
1954       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSetsRules.key 
1999       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heapRules.key 
2067       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permissionRules.key 
2086       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reachRules.key 
2111       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqCoreRules.key 
2114       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqRules.key 
2151       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm.key 
2179       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm2.key 
2185       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/javaRules.key 
2277       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/assertions.key 
2793       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopRules.key 
2801       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/activeUse.key 
2849       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/instanceAllocation.key 
2867       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/java5.key 
2871       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key 
2902       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key 
2925       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bigint.key 
2954       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
2956       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/adtProgramDecompositionRules.key 
2971       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/precRules.key 
2974       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListRules.key 
2987       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExTheory.key 
2988       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExHeader.key 
2989       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExAxioms.key 
2993       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExLemmaProven.key 
2998       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqEq.key 
3005       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/infFlow.key 
3010       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/mapSize.key 
3014       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wd.key 
3015       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeader.key 
3016       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdGeneralRules.key 
3021       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdNumericalRules.key 
3040       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdLocSetRules.key 
3045       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeapRules.key 
3049       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdReachRules.key 
3050       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdSeqRules.key 
3053       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdStringRules.key 
3056       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdRegExRules.key 
3058       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdFormulaRules.key 
3096       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopInvariantRules.key 
3099       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/forLoopRules.key 
3101       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/execRules.key 
3160       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopScopeRules.key 
5864       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
8110       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.8ns 
8112       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src/test/resources/testcase/dummyTrue.key 
8122       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9049       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
10930      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11846      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
11847      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11855      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12717      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
14571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15478      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms 
15478      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15483      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16419      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
18210      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19080      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
19081      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19083      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19889      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
21691      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22561      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
22562      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22574      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23394      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
25136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25994      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.69ms 
25995      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26011      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26820      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
28532      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29374      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.31ms 
29374      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
29376      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30163      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
31866      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32660      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.01ns 
32661      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
32663      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33458      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
35149      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35938      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.5ns 
35939      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
35941      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36747      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
38414      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39231      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.01ns 
39232      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
39233      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40029      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
41685      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42491      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.3ns 
42491      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
42493      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43294      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
44965      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45783      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.81ns 
45784      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
45786      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 
46593      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
48246      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49108      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.54ms 
49108      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 
49114      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 
49889      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
51583      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52406      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.91ms 
52406      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 
52409      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 
53171      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
54853      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55773      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 134.29ms 
55774      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 
55778      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 
56570      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
58252      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59032      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
59032      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 
59034      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59817      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
61503      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62281      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
62282      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 
62285      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 
63068      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
64714      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65544      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.86ms 
65544      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 
65546      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 
66328      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
67983      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.95ms 
68792      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 
68794      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 
69591      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
71237      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72043      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
72043      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 
72044      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 
72805      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
74493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75299      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.07ms 
75300      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 
75302      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 
76074      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
77777      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
78586      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.03ms 
78587      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 
78589      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79350      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
81041      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81836      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.11ms 
81836      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 
81838      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82650      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
84327      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85101      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
85101      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 
85102      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85887      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
87549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
88349      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.31ms 
88350      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
88353      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 
89139      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
90785      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
91621      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.73ms 
91622      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 
91625      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92410      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
94055      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
94881      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.45ms 
94881      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
94884      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95666      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
97311      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98119      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
98119      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
98120      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98880      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
100562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
101366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
101367     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
101368     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102126     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
103793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
104595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ms 
104595     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
104596     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105355     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
107028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
107810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
107811     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
107816     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108614     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
110290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
111069     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
111070     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111851     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
113489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
114291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
114291     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
114292     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115075     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
116727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
117525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
117526     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
117527     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118305     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
119945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
120743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.13ms 
120744     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
120745     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121543     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
123188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.18ms 
124010     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
124012     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
124781     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
126443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
127248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.79ms 
127249     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
127250     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128017     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
129688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
130496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
130496     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
130497     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131253     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
132914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
133696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
133696     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
133697     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134474     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
136139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
136924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.83ms 
136925     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
136926     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
137703     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
139340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
140160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.66ms 
140161     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
140162     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
140941     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
142573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
143365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
143365     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
143366     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144143     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
145779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
146573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
146574     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 
146575     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147354     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
148984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
149778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
149778     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
149779     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
150533     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
152198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
152996     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 
152997     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
152998     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
153752     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
155415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
156196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
156197     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
156198     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
156993     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
158646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
159419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
159419     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
159420     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160198     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
161851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
162618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
162622     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
162625     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
163401     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
165049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
165844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
165845     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
165847     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
166623     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
168259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
169051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
169051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
169053     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
169841     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
171475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
172342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.82ms 
172343     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
172346     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
173127     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
174764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
175620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.84ms 
175621     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
175623     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 
176401     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
178064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
178857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
178857     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 
178859     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 
179612     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
181279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
182074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.75ms 
182074     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 
182076     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
182850     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
184506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
185291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.79ms 
185292     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
185293     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
186066     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
187721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
188494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 939.71ns 
188494     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
188495     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
189271     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
190901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
191794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.09ms 
191794     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
191796     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
192579     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
194211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
195010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
195010     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
195011     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
195787     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
197425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
198220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 
198221     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
198222     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
198998     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
200631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
201436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
201453     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
201454     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
202210     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
203870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
204667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
204668     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
204670     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 
205424     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
207085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
207858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
207858     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 
207860     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
208630     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
210278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
211045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
211045     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
211046     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
211820     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
213472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
214249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.98ms 
214249     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
214250     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
215029     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
216657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
217459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.19ms 
217459     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
217461     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
218244     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
219872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
220670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.84ms 
220671     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
220672     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
221446     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
223074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
223863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
223863     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
223864     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
224615     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
226275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
227064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
227064     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
227065     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
227818     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
229475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
230269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
230269     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
230271     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
231025     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
232680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
233447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 847.51ns 
233447     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
233448     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
234222     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
235875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
236640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 501.5ns 
236640     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
236641     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
237417     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
239066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
239832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
239832     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
239833     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
240609     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
242247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
243037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.4ns 
243037     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
243038     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 
243813     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
245449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
246283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.43ms 
246284     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 
246286     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
247066     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
248698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
249513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.53ms 
249513     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
249516     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
250276     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
251938     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
252746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.69ms 
252746     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
252748     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
253502     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
255161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
256004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.04ms 
256004     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
256007     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
256765     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
258429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
259211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.97ms 
259211     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
259212     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
259987     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
261644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
262442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.9ms 
262442     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
262443     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
263243     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
264874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
265678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.52ms 
265678     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
265679     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
266456     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
268086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
268885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
268886     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
268887     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
269660     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
271293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
272102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.64ms 
272102     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
272104     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
272883     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
274520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
275321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.71ms 
275322     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
275323     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
276080     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
277768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
278575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
278576     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
278577     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
279330     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
280993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
281821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
281821     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
281822     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
282574     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
284234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
285017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms 
285017     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
285018     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
285793     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
287448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
288227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.22ms 
288227     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
288228     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
289020     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
290650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
291461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.15ms 
291462     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
291463     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
292237     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
293867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
294668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.29ms 
294668     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
294670     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
295443     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
297079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
297880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
297880     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
297881     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
298656     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
300283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
301079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
301079     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
301080     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 
301833     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
303490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
304287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
304287     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 
304288     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 
305039     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
306692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
307501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
307501     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 
307502     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 
308253     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
309905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
310672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.8ns 
310672     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 
310673     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 
311444     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
313093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
313867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.9ns 
313868     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 
313869     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 
314645     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
316271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
317065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
317066     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 
317067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 
317843     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
319471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
320269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
320269     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 
320271     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 
321051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
322677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
323476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
323476     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 
323477     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 
324253     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
325877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
326666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
326666     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 
326667     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
327418     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
329072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
329863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 434.4ns 
329864     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
329865     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 
330617     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
332273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
333042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
333042     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 
333044     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
333816     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
335462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
336228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 550.2ns 
336228     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
336229     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
337002     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
338654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
339420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.4ns 
339420     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
339421     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 
340198     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
341822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
342612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 510.4ns 
342612     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 
342613     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
343387     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
345009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
345801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
345801     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
345802     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 
346577     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
348202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
349005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
349005     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 
349007     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 
349757     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
351406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
352199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
352199     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 
352200     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 
352949     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
354597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
355389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
355390     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 
355391     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
356140     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
357793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
358561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
358561     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
358562     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 
359334     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
360985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
361765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
361765     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 
361766     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
362538     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
364185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
364958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
364963     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
364964     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 
365742     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
367369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
368163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.9ns 
368163     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 
368165     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
368938     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
370564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
371354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
371355     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
371356     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 
372129     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
373752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
374552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.32ms 
374553     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 
374554     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
375303     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
376956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
377744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 422.4ns 
377745     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
377746     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 
378496     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
380151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
380962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.11ms 
380963     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 
380964     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 
381718     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
383371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
384140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
384140     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 
384141     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 
384918     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
386572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
387352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.52ms 
387352     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 
387353     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 
388128     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
389757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
390566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.99ms 
390566     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 
390568     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 
391343     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
392973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
393779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.22ms 
393779     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 
393780     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
394553     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
396182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
396973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.9ns 
396973     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
396974     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 
397749     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
399377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
400169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
400170     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 
400171     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
400921     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
402577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
403371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
403371     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
403372     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
404122     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
405790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
406560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 731.8ns 
406560     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
406561     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
407332     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
408979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
409749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 682.7ns 
409749     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
409754     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
410525     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
412180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
412952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
412952     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
412953     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
413727     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
415354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
416149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 956.5ns 
416150     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
416151     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
416932     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
418558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
419362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
419362     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
419363     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
420140     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
421768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
422568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
422568     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
422569     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
423347     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
424974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
425772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
425773     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
425774     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
426527     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
428181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
428984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
428984     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
428986     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
429735     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
431386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
432162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
432162     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
432163     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 
432936     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
434581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
435357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
435357     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 
435358     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
436128     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
437782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
438556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 663.4ns 
438556     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
438557     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
439336     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
440961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
441760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 790.5ns 
441760     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
441761     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
442536     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
444160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
444960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708ns 
444960     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
444963     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
445738     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
447364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
448167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
448168     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
448170     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
448919     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
450572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
451371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
451371     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
451372     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
452122     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
453777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
454585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
454585     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
454587     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
455339     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
456996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
457776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722ns 
457776     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
457777     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
458554     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
460203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
460977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 543.8ns 
460977     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
460978     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
461753     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
463403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
464179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
464179     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
464180     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
464954     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
466599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
467374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711ns 
467374     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
467375     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
468148     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
469776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
470574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 884.2ns 
470574     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
470575     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
471351     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
472976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
473774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.8ns 
473774     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
473776     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
474548     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
476176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
476979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
476979     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
476981     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
477763     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
479389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
480187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802ns 
480187     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
480188     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
480962     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
482592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
483396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
483396     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
483398     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
484174     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
485798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
486594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 446.1ns 
486594     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
486595     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
487368     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
488994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
489796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
489797     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
489798     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
490570     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
492191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
492989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.5ns 
492989     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
492990     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
493766     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
495395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
496191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.6ns 
496191     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
496192     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
496941     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
498589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
499384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
499385     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
499386     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
500134     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
501783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
502579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.8ns 
502579     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
502581     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
503356     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
504984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
505781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
505781     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
505782     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
506555     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
508185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
508983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.6ns 
508984     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
508985     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
509759     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
511382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
512183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
512183     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
512184     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
512957     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
514582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
515386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ms 
515386     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
515388     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
516162     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
517780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
518581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
518581     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
518582     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
519356     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
520978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
521777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
521777     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
521778     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 
522551     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
524173     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
524974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
524975     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 
524976     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 
525749     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
527370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
528176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.19ms 
528176     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 
528177     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 
528950     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
530574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
531380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.28ms 
531380     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 
531381     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
532158     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
533803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
534584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
534584     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
534585     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
535362     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
537009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
537790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
537790     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
537791     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 
538566     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
540210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
541002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.48ms 
541002     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 
541003     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
541782     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
543426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
544243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.71ms 
544243     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
544244     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
544993     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
546647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
547459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.92ms 
547460     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
547461     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
548211     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
549859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
550673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.25ms 
550674     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
550675     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
551448     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
553073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
553888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
553888     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
553889     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
554663     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
556296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
557138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.49ms 
557138     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
557139     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 
557917     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
559563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
560341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
560341     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 
560342     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
561116     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
562765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
563566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
563566     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
563567     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
564317     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
565964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
566763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
566763     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
566764     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
567514     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
569168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
569979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
569979     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
569980     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
570753     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
572377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
573180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
573181     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
573182     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
573953     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
575598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
576375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
576375     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
576376     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
577150     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
578798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
579581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
579581     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
579583     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
580355     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
581998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
582804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
582804     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
582805     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
583558     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
585218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
586027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
586027     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
586029     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
586806     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
588430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
589230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.7ns 
589230     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
589231     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
590003     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
591649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
592426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
592426     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
592427     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
593201     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
594842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
595644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
595644     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
595645     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
596396     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
598047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
598847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
598847     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
598848     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
599620     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
601243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
602077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.13ms 
602077     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
602078     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
602853     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
604521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
605339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
605339     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
605340     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
606091     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
607732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
608539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.17ms 
608539     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
608540     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
609311     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
610936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
611737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 245.8ns 
611737     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
611739     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 
612511     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
614154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
615000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.97ms 
615000     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 
615002     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
615780     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
617427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
618256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.07ms 
618256     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
618258     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
619028     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
620649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
621449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 215.1ns 
621449     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
621451     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
622223     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
623867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
624644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 191.9ns 
624644     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
624645     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
625416     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
627060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
627859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 182ns 
627859     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
627860     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
628631     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
630253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
631053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 295.7ns 
631053     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
631054     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 
631825     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
633471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
634356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.68ms 
634362     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 
634364     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 
635120     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
636777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
637618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.73ms 
637618     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 
637620     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
638402     DEBUG Test worker     d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 
638403     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
640068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
640846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 
640847     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
640872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
640925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
640940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
640943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
640950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
640951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
640952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
640953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
640957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
640957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
640959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
640960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
641159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
641160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
641161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
641162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
641163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
641274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
641275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
641276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
641277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
641278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
641279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
641416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
641417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
641418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
641419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
641420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
641421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
641518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
641519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
641520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
641521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
641522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
641523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
641528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
641529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
641530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
641532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
641532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
641534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
641544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
641545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
641546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
641550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
641551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
641552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
641664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
641665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
641666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
641802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
641803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
641804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
641806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
641807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
641808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
641809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
641812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
641816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
641817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
641818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
641819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
641820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
641911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
641914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
641915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
641916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
641917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
641919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
641920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
642024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
642027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
642028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
642030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
642031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
642032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
642033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
642034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
642121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
642123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
642203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
642207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
642212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
642213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
642214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
642215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
642216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
642217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
642217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
642218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
642225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
642230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
642320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
642321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
642323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
642325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
642326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
642326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
642327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
642329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
642375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
642381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
642464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
642465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
642466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
642467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
642468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
642469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
642579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
642583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
642585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
642587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
642589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
642589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
642590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
642591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
642599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
642604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
642605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
642606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
642692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
642693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
642694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
642695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
642695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
642696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
642791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
642792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
642793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
642794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
642795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
642796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
642796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
642797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
642883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
642884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
642956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
642957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
642958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
642962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
642974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
642979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
643096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
643097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
643098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
643099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
643109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
643188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
646393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
646394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
646397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
646399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
646399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
646400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
646401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
646409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
646409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
646410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
646411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
646412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
646495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
646499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
646500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
646501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
646501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
646502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
646503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
646590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
646592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
646593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
646595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
646596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
646597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
646597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
646598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
646667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
646670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
646790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
646795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
646799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
646800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
646800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
646802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
646814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
646886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
646889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
646890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
646891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
646958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
646968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
646969     DEBUG 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)'' 
646970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
646971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
646972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
646973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
646973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
646985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
646985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
646986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
646987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
646989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
647066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
647067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
647069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
647070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
647071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
647155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
647159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
647160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
647161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
647162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
647162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
647163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
647250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
647251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
647252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
647253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
647254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
647254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
647255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
647256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
647256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
647257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
647258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
647259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
647260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
647260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
647261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
647344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
647345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
647352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
647422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
647493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
647494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
647495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
647496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
647496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
647497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
647497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
647498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
647498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
647501     WARN  Test worker     d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
	at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)

647502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
647502     WARN  Test worker     d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
	at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)

647503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
647503     WARN  Test worker     d.u.i.k.p.i.ApplyStrategy doWork exception java.lang.AssertionError: Formula Term top level of equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,jv_0),int::seqGet(s_0,v_x_0),if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))) does not exist
	at de.uka.ilkd.key.strategy.BuiltInRuleAppContainer.<init>(BuiltInRuleAppContainer.java:42)

647503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
647504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 8 
647505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),exists{v_r:Seq}(and(and(and(and(equals(seqLen(v_r),seqLen(f_s)),seqNPerm(v_r)),all{v_iv:int}(imp(and(leq(Z(0(#)),v_iv),lt(v_iv,seqLen(f_s))),equals(any::seqGet(f_s,v_iv),any::seqGet(f_t,int::seqGet(v_r,v_iv)))))),equals(int::seqGet(v_r,v_x_0),v_x_0)),equals(int::seqGet(v_r,v_y_0),v_y_0)))] 
647505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(int::seqGet(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0),v_y_0),v_y_0)] 
647505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(int::seqGet(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0),v_x_0),v_x_0)] 
647505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),and(and(and(leq(Z(0(#)),jv_0),leq(Z(0(#)),v_y_0)),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0)))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0)))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(seqSwap(s_0,jv_0,v_x_0),v_iv_0)))] 
647506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(v_iv_0,v_y_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(seqSwap(s_0,jv_0,v_x_0),v_iv_0)))] 
647506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),and(and(and(leq(Z(0(#)),jv_0),leq(Z(0(#)),v_x_0)),lt(jv_0,seqLen(s_0))),lt(v_x_0,seqLen(s_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,jv_0)))] 
647506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [equals(jv_0,jv_0),lt(v_x_0,seqLen(s_0)),equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0)))] 
647506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [lt(v_x_0,seqLen(s_0)),equals(v_iv_0,v_y_0),lt(jv_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),lt(v_y_0,seqLen(seqSwap(s_0,jv_0,v_x_0))),leq(Z(0(#)),v_iv_0),lt(v_iv_0,seqLen(f_s)),equals(int::cast(any::seqGet(s_0,v_x_0)),v_y_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,v_x_0)),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,v_y_0)),leq(Z(0(#)),v_x_0),lt(v_x_0,seqLen(f_s)),leq(Z(0(#)),v_y_0),lt(v_y_0,seqLen(f_s)),equals(seqLen(f_s),seqLen(f_t)),equals(seqLen(s_0),seqLen(f_s)),leq(Z(0(#)),int::seqGet(s_0,v_x_0)),lt(int::seqGet(s_0,v_x_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_x_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,v_y_0)),lt(int::seqGet(s_0,v_y_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,v_y_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_0)),lt(int::seqGet(s_0,jv_0),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_0)),TRUE),leq(Z(0(#)),int::seqGet(s_0,jv_1)),lt(int::seqGet(s_0,jv_1),seqLen(s_0)),equals(int::instance(any::seqGet(s_0,jv_1)),TRUE),leq(Z(0(#)),jv_0),lt(jv_0,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_0)),v_x_0),leq(Z(0(#)),jv_1),lt(jv_1,seqLen(s_0)),equals(int::cast(any::seqGet(s_0,jv_1)),v_y_0),seqNPerm(s_0),equals(any::seqGet(f_s,v_x_0),any::seqGet(f_t,int::seqGet(s_0,v_x_0))),equals(any::seqGet(f_s,v_y_0),any::seqGet(f_t,int::seqGet(s_0,v_y_0))),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,int::seqGet(s_0,v_iv_0))),all{iv:int}(imp(and(leq(Z(0(#)),iv),lt(iv,seqLen(s_0))),equals(any::seqGet(f_s,iv),any::seqGet(f_t,int::seqGet(s_0,iv))))),seqPerm(f_s,f_t)]==>[equals(int::cast(any::seqGet(s_0,v_y_0)),v_y_0),equals(int::cast(any::seqGet(s_0,v_x_0)),v_x_0),equals(int::cast(any::seqGet(s_0,v_x_0)),int::cast(any::seqGet(s_0,v_y_0))),equals(v_x_0,v_y_0),equals(v_iv_0,jv_0),equals(jv_0,jv_0),equals(any::seqGet(f_s,v_iv_0),any::seqGet(f_t,if-then-else(equals(jv_0,v_x_0),int::seqGet(s_0,jv_0),int::seqGet(s_0,jv_0))))] 
647509     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
648430     DEBUG Test worker     d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 
648432     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
650140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
650926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
650926     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
650926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
650934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
650943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
650945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
650947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
650949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
650954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
650954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
650958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
650958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
650960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
650970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
650971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
650973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
651026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
651027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
651028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
651028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
651028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
651165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
651165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
651166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
651166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
651167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
651171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
651171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
651172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
651172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
651173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
651174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
651256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
651257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
651257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
651258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
651258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
651259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
651339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
651339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
651340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
651340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
651341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
651341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
651342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
651342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
651343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
651343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
651343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
651343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
651344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
651344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
651344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
651345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
651345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
651346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
651346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
651349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
651385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
651386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
651433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
651434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
651435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
651436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
651436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
651437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
651498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
651500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
651501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
651501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
651502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
651503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
651504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
651540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
651542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
651545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
651589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
651636     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof 
652433     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
654086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
654948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.43ms 
654948     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof