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

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

198

tests

failures

ignored

10m58.83s

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.234s	passed
powPositiveConcrete	data()[101]	3.254s	passed
powGeq1Concrete	data()[102]	3.253s	passed
pow2InIntLower	data()[103]	3.242s	passed
pow2InIntUpper	data()[104]	3.250s	passed
logSelfConcrete	data()[105]	3.234s	passed
log1Concrete	data()[106]	3.235s	passed
logProduct	data()[107]	3.233s	passed
logTimesBaseConcrete	data()[108]	3.237s	passed
logProdIdentity	data()[109]	3.243s	passed
moduloByteIsInByte	data()[10]	3.334s	passed
logProdIdentityConcrete	data()[110]	3.242s	passed
logPowIdentity	data()[111]	3.261s	passed
logPowIdentityConcrete	data()[112]	3.250s	passed
logPositive	data()[113]	3.259s	passed
logPositiveConcrete	data()[114]	3.237s	passed
logMono	data()[115]	3.250s	passed
logMonoConcrete	data()[116]	3.246s	passed
powLogLess	data()[117]	3.268s	passed
powLogMore2	data()[118]	3.255s	passed
logLessThanPow	data()[119]	3.256s	passed
moduloCharIsInChar	data()[11]	3.342s	passed
logLessThanPowConcrete	data()[120]	3.247s	passed
logSqueeze	data()[121]	3.240s	passed
ifthenelse_equals	data()[122]	3.256s	passed
ifthenelse_equals_1	data()[123]	3.245s	passed
ifthenelse_equals_2	data()[124]	3.241s	passed
disjointWithSingleton1	data()[125]	3.248s	passed
disjointWithSingleton2	data()[126]	3.255s	passed
disjointArrayRanges	data()[127]	3.256s	passed
disjointArrayRangeAllFields1	data()[128]	3.252s	passed
disjointArrayRangeAllFields2	data()[129]	3.239s	passed
div_unique1	data()[12]	3.435s	passed
seqSelfDefinition	data()[130]	3.247s	passed
seqOutsideValue	data()[131]	3.267s	passed
castedGetAny	data()[132]	3.247s	passed
seqGetAlphaCast	data()[133]	3.247s	passed
getOfSeqSingleton	data()[134]	3.253s	passed
getOfSeqSingletonConcrete	data()[135]	3.273s	passed
getOfSeqConcat	data()[136]	3.266s	passed
getOfSeqSub	data()[137]	3.250s	passed
getOfSeqReverse	data()[138]	3.263s	passed
lenOfSeqEmpty	data()[139]	3.242s	passed
div_unique2	data()[13]	3.412s	passed
lenOfSeqSingleton	data()[140]	3.240s	passed
lenOfSeqConcat	data()[141]	3.261s	passed
lenOfSeqSub	data()[142]	3.245s	passed
lenOfSeqReverse	data()[143]	3.256s	passed
equalityToSeqGetAndSeqLenLeft	data()[144]	3.242s	passed
equalityToSeqGetAndSeqLenRight	data()[145]	3.266s	passed
getOfSeqSingletonEQ	data()[146]	3.246s	passed
getOfSeqConcatEQ	data()[147]	3.273s	passed
getOfSeqSubEQ	data()[148]	3.251s	passed
getOfSeqReverseEQ	data()[149]	3.265s	passed
div_exists	data()[14]	3.492s	passed
lenOfSeqEmptyEQ	data()[150]	3.261s	passed
lenOfSeqSingletonEQ	data()[151]	3.267s	passed
lenOfSeqConcatEQ	data()[152]	3.232s	passed
lenOfSeqSubEQ	data()[153]	3.266s	passed
lenOfSeqReverseEQ	data()[154]	3.259s	passed
getOfSeqDefEQ	data()[155]	3.245s	passed
lenOfSeqDefEQ	data()[156]	3.263s	passed
seqConcatWithSeqEmpty1	data()[157]	3.275s	passed
seqConcatWithSeqEmpty2	data()[158]	3.258s	passed
seqReverseOfSeqEmpty	data()[159]	3.282s	passed
div_one	data()[15]	3.322s	passed
subSeqComplete	data()[160]	3.280s	passed
subSeqTailR	data()[161]	3.271s	passed
subSeqTailL	data()[162]	3.244s	passed
subSeqTailEQR	data()[163]	3.257s	passed
subSeqTailEQL	data()[164]	3.265s	passed
seqDef_split	data()[165]	3.285s	passed
seqDef_induction_upper	data()[166]	3.279s	passed
seqDef_induction_upper_concrete	data()[167]	3.287s	passed
seqDef_induction_lower	data()[168]	3.291s	passed
seqDef_induction_lower_concrete	data()[169]	3.258s	passed
jdiv_one	data()[16]	3.321s	passed
seqDef_split_in_three	data()[170]	3.304s	passed
seqDef_empty	data()[171]	3.291s	passed
seqDef_one_summand	data()[172]	3.258s	passed
seqDef_lower_equals_upper	data()[173]	3.257s	passed
seqDefOfSeq	data()[174]	3.340s	passed
seqSelfDefinitionEQ2	data()[175]	3.265s	passed
indexOfSeqSingleton	data()[176]	3.281s	passed
indexOfSeqConcatFirst	data()[177]	3.261s	passed
indexOfSeqConcatSecond	data()[178]	3.332s	passed
indexOfSeqSub	data()[179]	3.262s	passed
div_zero	data()[17]	3.334s	passed
lenOfArray2seq	data()[180]	3.267s	passed
getAnyOfArray2seq	data()[181]	3.268s	passed
getOfArray2seq	data()[182]	3.254s	passed
getAnyOfNPermInv	data()[183]	3.271s	passed
seqNPermRange	data()[184]	3.308s	passed
seqPermTrans	data()[185]	3.291s	passed
seqPermRefl	data()[186]	3.252s	passed
seqPermSplit	data()[187]	3.252s	passed
seqNPermRight	data()[188]	3.350s	passed
seqPermFromSwap	data()[189]	3.296s	passed
divResZero1	data()[18]	3.360s	passed
seqPermTransAlt0	data()[190]	3.260s	passed
seqPermTransAlt1	data()[191]	3.268s	passed
seqPermTransAlt2	data()[192]	3.254s	passed
seqPermTransAlt3	data()[193]	3.331s	passed
seqPermForall	data()[194]	3.373s	passed
seqPermExists	data()[195]	3.336s	passed
schiffl_lemma_2	data()[196]	11.012s	failed
schiffl_thm_1	data()[197]	4.119s	passed
eqSameSeq	data()[198]	3.499s	passed
divResZero2	data()[19]	3.325s	passed
eqTermCut	data()[1]	4.013s	passed
divResOne1	data()[20]	3.293s	passed
divResOne2	data()[21]	3.309s	passed
div_cancel1	data()[22]	3.324s	passed
div_cancel2	data()[23]	3.301s	passed
divAddMultDenom	data()[24]	3.305s	passed
divMinus	data()[25]	3.338s	passed
divMinusDenom	data()[26]	3.318s	passed
divLeastDPos	data()[27]	3.252s	passed
divLeastDNeg	data()[28]	3.311s	passed
divGreatestDPos	data()[29]	3.302s	passed
equivAllRight	data()[2]	3.708s	passed
divGreatestDNeg	data()[30]	3.289s	passed
divIncreasingPos	data()[31]	3.286s	passed
divIncreasingNeg	data()[32]	3.263s	passed
jdiv_zero	data()[33]	3.253s	passed
jdivPulloutMinusNum	data()[34]	3.269s	passed
jdivPulloutMinusDenom	data()[35]	3.298s	passed
jdiv_uniquePosPos	data()[36]	3.298s	passed
jdiv_uniquePosNeg	data()[37]	3.271s	passed
jdiv_uniqueNegPos	data()[38]	3.276s	passed
jdiv_uniqueNegNeg	data()[39]	3.297s	passed
irrflConcrete1	data()[3]	3.519s	passed
jdivMultDenom1	data()[40]	3.286s	passed
jdivMultDenom2	data()[41]	3.257s	passed
mod_geZero	data()[42]	3.260s	passed
mod_lessDenom	data()[43]	3.245s	passed
jmod_NumPos	data()[44]	3.252s	passed
jmod_NumNeg	data()[45]	3.258s	passed
jmod_geZero	data()[46]	3.234s	passed
jmodNumZero	data()[47]	3.312s	passed
jmod_pulloutminusNum	data()[48]	3.267s	passed
jmod_pulloutminusDenom	data()[49]	3.239s	passed
irrflConcrete2	data()[4]	3.391s	passed
jmodUnique1	data()[50]	3.296s	passed
jmodUnique2	data()[51]	3.325s	passed
intDivRem	data()[52]	3.256s	passed
jmodjmod	data()[53]	3.267s	passed
jmodDivisible	data()[54]	3.306s	passed
jmodDivisibleRep	data()[55]	3.265s	passed
jdivAddMultDenom	data()[56]	3.356s	passed
jmodAltZero	data()[57]	3.258s	passed
jmodAddMultDenomZero	data()[58]	3.254s	passed
polyDiv_zero	data()[59]	3.251s	passed
cancel_gtPos	data()[5]	3.493s	passed
polyMod_ltdivDenom	data()[60]	3.255s	passed
bsum_empty	data()[61]	3.240s	passed
bsum_induction_upper	data()[62]	3.231s	passed
bsum_induction_lower	data()[63]	3.262s	passed
bsum_num_of_bounds	data()[64]	3.288s	passed
bsum_num_of_bounds2	data()[65]	3.265s	passed
bsum_induction_upper2	data()[66]	3.228s	passed
bsum_induction_upper_concrete	data()[67]	3.233s	passed
bsum_induction_upper_concrete_2	data()[68]	3.236s	passed
bsum_induction_upper2_concrete	data()[69]	3.238s	passed
cancel_gtNeg	data()[6]	3.484s	passed
bsum_induction_lower_concrete	data()[70]	3.247s	passed
bsum_induction_lower2	data()[71]	3.262s	passed
bsum_induction_lower2_concrete	data()[72]	3.249s	passed
bsum_positive	data()[73]	3.285s	passed
bsum_upper_bound	data()[74]	3.281s	passed
bsum_lower_bound	data()[75]	3.261s	passed
bsum_positive_lower_bound_element	data()[76]	3.308s	passed
bsum_sub_same_index	data()[77]	3.269s	passed
bsum_less_same_index	data()[78]	3.284s	passed
bsum_equal_except_one_index	data()[79]	3.251s	passed
moduloIntIsInInt	data()[7]	3.416s	passed
bsum_num_of_is_max	data()[80]	3.259s	passed
bsum_num_of_is_max2	data()[81]	3.254s	passed
bsum_num_of_is_max3	data()[82]	3.251s	passed
bsum_num_of_is_max4	data()[83]	3.255s	passed
bsum_num_of_lt_max	data()[84]	3.268s	passed
bsum_num_of_lt_max2	data()[85]	3.248s	passed
bsum_num_of_lt_max3	data()[86]	3.271s	passed
bsum_num_of_lt_max4	data()[87]	3.255s	passed
bsum_num_of_gt0	data()[88]	3.236s	passed
bsum_num_of_gt0_alt	data()[89]	3.261s	passed
moduloLongIsInLong	data()[8]	3.370s	passed
bsum_add_concrete	data()[90]	3.259s	passed
bprod_all_positive	data()[91]	3.262s	passed
bprod_split	data()[92]	3.244s	passed
powConcrete0	data()[93]	3.250s	passed
powConcrete1	data()[94]	3.233s	passed
powSplitFactor	data()[95]	3.229s	passed
powAdd	data()[96]	3.242s	passed
powMono	data()[97]	3.245s	passed
powMonoConcrete	data()[98]	3.240s	passed
powMonoConcreteRight	data()[99]	3.223s	passed
moduloShortIsInShort	data()[9]	3.346s	passed

Standard output

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

547        DEBUG Test worker     d.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 
578        DEBUG Test worker     d.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 
586        DEBUG Test worker     d.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 
601        DEBUG Test worker     d.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 
648        DEBUG Test worker     d.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 
661        DEBUG Test worker     d.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 
663        DEBUG Test worker     d.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 
673        DEBUG Test worker     d.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 
674        DEBUG Test worker     d.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 
676        DEBUG Test worker     d.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 
677        DEBUG Test worker     d.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 
679        DEBUG Test worker     d.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 
736        DEBUG Test worker     d.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 
737        DEBUG Test worker     d.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 
738        DEBUG Test worker     d.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 
891        DEBUG Test worker     d.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 
937        DEBUG Test worker     d.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 
969        DEBUG Test worker     d.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 
1021       DEBUG Test worker     d.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 
1117       DEBUG Test worker     d.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 
1135       DEBUG Test worker     d.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 
1246       DEBUG Test worker     d.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 
1286       DEBUG Test worker     d.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 
1306       DEBUG Test worker     d.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 
1318       DEBUG Test worker     d.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 
1346       DEBUG Test worker     d.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 
1547       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1549       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1553       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1553       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1602       DEBUG Test worker     d.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 
1632       DEBUG Test worker     d.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 
1762       DEBUG Test worker     d.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 
1835       DEBUG Test worker     d.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 
1839       DEBUG Test worker     d.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 
1844       DEBUG Test worker     d.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 
1861       DEBUG Test worker     d.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 
1884       DEBUG Test worker     d.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 
1886       DEBUG Test worker     d.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 
1887       DEBUG Test worker     d.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 
1906       DEBUG Test worker     d.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 
1926       DEBUG Test worker     d.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 
1930       DEBUG Test worker     d.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 
1936       DEBUG Test worker     d.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 
2001       DEBUG Test worker     d.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 
2042       DEBUG Test worker     d.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 
2100       DEBUG Test worker     d.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 
2129       DEBUG Test worker     d.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 
2133       DEBUG Test worker     d.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 
2173       DEBUG Test worker     d.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 
2203       DEBUG Test worker     d.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 
2209       DEBUG Test worker     d.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 
2311       DEBUG Test worker     d.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 
2852       DEBUG Test worker     d.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 
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/java5.key 
2875       DEBUG Test worker     d.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 
2917       DEBUG Test worker     d.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 
2948       DEBUG Test worker     d.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 
2962       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
2965       DEBUG Test worker     d.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 
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/precRules.key 
3009       DEBUG Test worker     d.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 
3026       DEBUG Test worker     d.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 
3029       DEBUG Test worker     d.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 
3030       DEBUG Test worker     d.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 
3036       DEBUG Test worker     d.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 
3044       DEBUG Test worker     d.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 
3052       DEBUG Test worker     d.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 
3060       DEBUG Test worker     d.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 
3064       DEBUG Test worker     d.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 
3066       DEBUG Test worker     d.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 
3068       DEBUG Test worker     d.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 
3073       DEBUG Test worker     d.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 
3100       DEBUG Test worker     d.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 
3108       DEBUG Test worker     d.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 
3112       DEBUG Test worker     d.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 
3115       DEBUG Test worker     d.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 
3119       DEBUG Test worker     d.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 
3123       DEBUG Test worker     d.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 
3125       DEBUG Test worker     d.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 
3142       DEBUG Test worker     d.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 
3146       DEBUG Test worker     d.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 
3149       DEBUG Test worker     d.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 
3225       DEBUG Test worker     d.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 
6197       DEBUG Test worker     d.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 
8484       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.3ns 
8486       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src/test/resources/testcase/dummyTrue.key 
8497       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9558       DEBUG Test worker     d.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 
11525      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12502      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ms 
12503      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_eqTermCut.proof 
12512      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13395      DEBUG Test worker     d.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 
15321      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16218      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
16218      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16221      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17089      DEBUG Test worker     d.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 
18875      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19737      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
19738      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19741      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20553      DEBUG Test worker     d.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 
22302      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23129      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
23130      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23133      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23957      DEBUG Test worker     d.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 
25708      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26623      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.15ms 
26624      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26641      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27458      DEBUG Test worker     d.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 
29203      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30108      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.59ms 
30109      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
30112      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30912      DEBUG Test worker     d.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 
32643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33525      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 811.5ns 
33526      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
33529      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34311      DEBUG Test worker     d.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 
36068      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36896      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.3ns 
36896      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
36898      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37695      DEBUG Test worker     d.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 
39424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.2ns 
40242      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
40244      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41036      DEBUG Test worker     d.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 
42761      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43576      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.8ns 
43576      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
43578      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44368      DEBUG Test worker     d.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 
46105      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46917      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.7ns 
46918      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
46920      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 
47724      DEBUG Test worker     d.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 
49456      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50348      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.39ms 
50353      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique1.proof 
50357      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 
51157      DEBUG Test worker     d.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 
52879      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53766      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.02ms 
53766      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_unique2.proof 
53768      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 
54583      DEBUG Test worker     d.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 
56353      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57257      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.15ms 
57258      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_exists.proof 
57261      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 
58066      DEBUG Test worker     d.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 
59775      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60580      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
60580      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_one.proof 
60582      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 
61378      DEBUG Test worker     d.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 
63086      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63901      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
63901      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_one.proof 
63905      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 
64707      DEBUG Test worker     d.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 
66417      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67236      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.33ms 
67237      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_zero.proof 
67239      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 
68049      DEBUG Test worker     d.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 
69783      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70596      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
70597      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero1.proof 
70599      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 
71395      DEBUG Test worker     d.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 
73104      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73922      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.06ms 
73922      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResZero2.proof 
73924      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 
74723      DEBUG Test worker     d.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 
76420      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77215      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
77215      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne1.proof 
77216      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 
78012      DEBUG Test worker     d.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 
79713      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80524      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
80525      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divResOne2.proof 
80527      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 
81321      DEBUG Test worker     d.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 
83025      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83847      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.86ms 
83848      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel1.proof 
83851      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 
84649      DEBUG Test worker     d.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 
86348      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87149      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
87149      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_div_cancel2.proof 
87150      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
87924      DEBUG Test worker     d.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 
89626      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90454      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.24ms 
90455      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
90456      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 
91249      DEBUG Test worker     d.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 
92940      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.12ms 
93792      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinus.proof 
93794      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
94589      DEBUG Test worker     d.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 
96281      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97111      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.84ms 
97111      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
97112      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
97900      DEBUG Test worker     d.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 
99563      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
100363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
100364     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
100365     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
101165     DEBUG Test worker     d.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 
102857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.46ms 
103674     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
103676     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
104471     DEBUG Test worker     d.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 
106170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
106976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
106977     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
106978     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
107781     DEBUG Test worker     d.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 
109481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
110265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
110266     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
110267     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
111048     DEBUG Test worker     d.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 
112740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
113551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
113552     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
113554     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
114337     DEBUG Test worker     d.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 
116016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
116815     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
116816     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
117595     DEBUG Test worker     d.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 
119279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
120066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
120068     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
120069     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
120851     DEBUG Test worker     d.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 
122534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
123337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
123337     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
123338     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
124119     DEBUG Test worker     d.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 
125808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
126634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.46ms 
126634     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
126635     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
127419     DEBUG Test worker     d.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 
129102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
129932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
129933     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
129934     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
130697     DEBUG Test worker     d.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 
132391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
133203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
133204     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
133205     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
133986     DEBUG Test worker     d.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 
135673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
136479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
136479     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
136480     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
137263     DEBUG Test worker     d.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 
138952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.14ms 
139776     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
139778     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
140541     DEBUG Test worker     d.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 
142236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
143062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.55ms 
143063     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
143064     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
143850     DEBUG Test worker     d.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 
145523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
146315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
146319     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
146324     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 
147101     DEBUG Test worker     d.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 
148779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
149577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
149577     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_geZero.proof 
149581     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
150366     DEBUG Test worker     d.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 
152029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
152824     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
152825     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
153601     DEBUG Test worker     d.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 
155279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
156077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
156077     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
156078     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
156853     DEBUG Test worker     d.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 
158530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
159334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
159334     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
159335     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
160113     DEBUG Test worker     d.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 
161789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
162568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.95ms 
162568     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
162570     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
163345     DEBUG Test worker     d.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 
165033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
165880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.9ns 
165880     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
165882     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
166665     DEBUG Test worker     d.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 
168342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
169148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
169148     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
169149     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
169931     DEBUG Test worker     d.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 
171610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
172386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
172386     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
172387     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
173164     DEBUG Test worker     d.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 
174836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
175682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.09ms 
175683     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
175684     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
176463     DEBUG Test worker     d.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 
178137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
179006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.02ms 
179007     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
179009     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 
179786     DEBUG Test worker     d.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 
181461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
182263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
182263     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_intDivRem.proof 
182265     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 
183028     DEBUG Test worker     d.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 
184708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
185529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.05ms 
185530     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodjmod.proof 
185532     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
186318     DEBUG Test worker     d.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 
188006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
188835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.91ms 
188836     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
188838     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
189628     DEBUG Test worker     d.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 
191307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
192101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 940.2ns 
192101     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
192102     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
192889     DEBUG Test worker     d.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 
194564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
195456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 91.76ms 
195457     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
195459     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
196245     DEBUG Test worker     d.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 
197919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
198715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.63ms 
198715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
198716     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
199493     DEBUG Test worker     d.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 
201166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
201969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
201970     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
201971     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
202760     DEBUG Test worker     d.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 
204435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
205220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms 
205220     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
205222     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
206007     DEBUG Test worker     d.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 
207677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
208474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
208475     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
208477     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 
209259     DEBUG Test worker     d.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 
210920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
211715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
211715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_empty.proof 
211717     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
212498     DEBUG Test worker     d.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 
214171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
214946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
214947     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
214951     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
215735     DEBUG Test worker     d.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 
217407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
218212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
218212     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
218213     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
218990     DEBUG Test worker     d.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 
220689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
221500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
221500     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
221501     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
222285     DEBUG Test worker     d.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 
223965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
224765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.83ms 
224765     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
224766     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
225524     DEBUG Test worker     d.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 
227200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
227994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 890.5ns 
227994     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
227995     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
228769     DEBUG Test worker     d.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 
230437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
231226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
231226     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
231228     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
232002     DEBUG Test worker     d.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 
233670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
234462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
234462     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
234464     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
235230     DEBUG Test worker     d.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 
236904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
237701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 885.3ns 
237701     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
237702     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
238476     DEBUG Test worker     d.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 
240151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
240947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 459.7ns 
240948     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240949     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
241729     DEBUG Test worker     d.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 
243411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
244209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
244209     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
244211     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
244994     DEBUG Test worker     d.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 
246660     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
247458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.8ns 
247458     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
247459     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 
248239     DEBUG Test worker     d.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 
249920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
250743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.11ms 
250744     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive.proof 
250745     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
251528     DEBUG Test worker     d.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 
253208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
254024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20ms 
254024     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
254025     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
254808     DEBUG Test worker     d.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 
256490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
257285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.76ms 
257285     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
257287     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
258089     DEBUG Test worker     d.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 
259775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
260593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.99ms 
260593     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
260595     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
261385     DEBUG Test worker     d.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 
263056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
263862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
263862     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
263864     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
264643     DEBUG Test worker     d.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 
266313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
267147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.05ms 
267147     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
267148     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
267912     DEBUG Test worker     d.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 
269591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
270398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ms 
270398     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
270399     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
271176     DEBUG Test worker     d.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 
272855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
273656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.27ms 
273656     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273658     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
274433     DEBUG Test worker     d.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 
276107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
276910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ms 
276911     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
276913     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
277671     DEBUG Test worker     d.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 
279359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
280161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.84ms 
280161     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
280163     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
280937     DEBUG Test worker     d.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 
282608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
283416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.75ms 
283416     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
283418     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
284198     DEBUG Test worker     d.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 
285879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
286684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.74ms 
286684     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
286686     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
287460     DEBUG Test worker     d.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 
289141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
289932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
289933     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
289935     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
290725     DEBUG Test worker     d.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 
292396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
293203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.38ms 
293203     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
293205     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
293985     DEBUG Test worker     d.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 
295655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
296458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.29ms 
296458     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
296459     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
297240     DEBUG Test worker     d.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 
298910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
299695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.07ms 
299695     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
299696     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300476     DEBUG Test worker     d.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 
302151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
302955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.63ms 
302955     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
302957     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303733     DEBUG Test worker     d.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 
305413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
306214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
306215     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
306217     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 
306994     DEBUG Test worker     d.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 
308670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
309476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
309477     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_all_positive.proof 
309479     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 
310243     DEBUG Test worker     d.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 
311927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
312721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
312721     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/bprod/Taclet_bprod_split.proof 
312722     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 
313501     DEBUG Test worker     d.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 
315180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
315972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567ns 
315972     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete0.proof 
315973     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 
316746     DEBUG Test worker     d.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 
318415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
319204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.3ns 
319204     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powConcrete1.proof 
319205     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 
319986     DEBUG Test worker     d.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 
321658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
322433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
322434     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powSplitFactor.proof 
322435     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 
323212     DEBUG Test worker     d.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 
324881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
325676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
325676     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powAdd.proof 
325677     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 
326453     DEBUG Test worker     d.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 
328124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
328921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
328921     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMono.proof 
328922     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 
329699     DEBUG Test worker     d.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 
331369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
332160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
332160     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcrete.proof 
332161     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
332939     DEBUG Test worker     d.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 
334612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
335384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 423.1ns 
335384     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
335385     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 
336158     DEBUG Test worker     d.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 
337822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
338617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
338618     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositive.proof 
338619     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
339396     DEBUG Test worker     d.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 
341079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
341872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.5ns 
341872     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
341873     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
342652     DEBUG Test worker     d.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 
344333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
345124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 443.9ns 
345124     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
345125     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 
345900     DEBUG Test worker     d.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 
347574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
348366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 507.1ns 
348366     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntLower.proof 
348367     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
349148     DEBUG Test worker     d.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 
350823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
351616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
351617     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
351618     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 
352374     DEBUG Test worker     d.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 
354071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
354850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
354850     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSelfConcrete.proof 
354851     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 
355625     DEBUG Test worker     d.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 
357293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
358085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
358085     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_log1Concrete.proof 
358086     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 
358862     DEBUG Test worker     d.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 
360523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
361318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
361319     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProduct.proof 
361320     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
362095     DEBUG Test worker     d.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 
363763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
364555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
364556     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
364557     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 
365332     DEBUG Test worker     d.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 
366994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
367798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
367799     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentity.proof 
367800     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
368576     DEBUG Test worker     d.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 
370246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
371040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
371041     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
371042     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 
371824     DEBUG Test worker     d.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 
373506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
374301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 900.1ns 
374301     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentity.proof 
374303     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
375085     DEBUG Test worker     d.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 
376757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
377551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
377551     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
377552     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 
378331     DEBUG Test worker     d.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 
380008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
380811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
380811     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositive.proof 
380812     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
381590     DEBUG Test worker     d.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 
383256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
384047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 326.7ns 
384047     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
384049     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 
384822     DEBUG Test worker     d.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 
386487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
387297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.92ms 
387297     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMono.proof 
387298     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 
388070     DEBUG Test worker     d.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 
389749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
390544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
390544     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logMonoConcrete.proof 
390546     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 
391326     DEBUG Test worker     d.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 
393005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
393811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
393811     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogLess.proof 
393812     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 
394591     DEBUG Test worker     d.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 
396265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
397067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.18ms 
397067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_powLogMore2.proof 
397068     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 
397847     DEBUG Test worker     d.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 
399517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
400322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.82ms 
400322     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPow.proof 
400324     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
401098     DEBUG Test worker     d.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 
402776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
403569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 423.6ns 
403570     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
403581     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 
404356     DEBUG Test worker     d.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 
406017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
406810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
406810     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/intPow/Taclet_logSqueeze.proof 
406811     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
407586     DEBUG Test worker     d.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 
409260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
410066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
410066     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
410067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
410844     DEBUG Test worker     d.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 
412518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
413311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.2ns 
413311     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
413312     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
414088     DEBUG Test worker     d.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 
415758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
416551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.3ns 
416551     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
416553     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
417331     DEBUG Test worker     d.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 
419023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
419800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
419800     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
419801     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
420577     DEBUG Test worker     d.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 
422258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
423054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
423054     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
423055     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
423831     DEBUG Test worker     d.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 
425506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
426310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
426310     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
426312     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
427093     DEBUG Test worker     d.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 
428762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
429562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
429563     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
429564     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
430336     DEBUG Test worker     d.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 
431999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
432801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
432802     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
432803     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
433577     DEBUG Test worker     d.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 
435243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
436048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.26ms 
436048     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
436050     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
436828     DEBUG Test worker     d.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 
438514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
439316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
439316     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
439317     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 
440091     DEBUG Test worker     d.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 
441758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
442562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
442562     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_castedGetAny.proof 
442564     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
443337     DEBUG Test worker     d.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 
445008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
445810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 763.12ns 
445810     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
445811     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
446588     DEBUG Test worker     d.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 
448262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
449062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.9ns 
449063     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
449064     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
449844     DEBUG Test worker     d.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 
451533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
452335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.9ns 
452335     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
452336     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
453116     DEBUG Test worker     d.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 
454791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
455602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.54ms 
455602     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
455603     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
456377     DEBUG Test worker     d.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 
458050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
458851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
458851     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
458852     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
459625     DEBUG Test worker     d.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 
461312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
462114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
462114     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
462115     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
462893     DEBUG Test worker     d.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 
464558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
465356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 664.3ns 
465356     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
465358     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
466130     DEBUG Test worker     d.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 
467796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
468596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.9ns 
468596     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
468598     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
469385     DEBUG Test worker     d.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 
471057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
471857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
471857     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
471858     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
472634     DEBUG Test worker     d.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 
474303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
475102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.1ns 
475102     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
475103     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
475875     DEBUG Test worker     d.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 
477560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
478359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 914.6ns 
478359     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
478360     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
479134     DEBUG Test worker     d.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 
480800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
481600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 866.3ns 
481601     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
481602     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
482374     DEBUG Test worker     d.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 
484066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
484866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
484866     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
484867     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
485643     DEBUG Test worker     d.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 
487312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
488112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 754.2ns 
488113     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
488114     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
488890     DEBUG Test worker     d.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 
490580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
491385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
491385     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
491387     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
492163     DEBUG Test worker     d.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 
493837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
494636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
494637     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
494638     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
495412     DEBUG Test worker     d.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 
497100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
497901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
497901     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
497902     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
498678     DEBUG Test worker     d.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 
500363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
501161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 776.9ns 
501161     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
501164     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
501942     DEBUG Test worker     d.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 
503630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
504429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.7ns 
504429     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
504430     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
505203     DEBUG Test worker     d.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 
506863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
507661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
507662     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
507663     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
508440     DEBUG Test worker     d.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 
510131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
510927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.4ns 
510927     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
510929     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
511703     DEBUG Test worker     d.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 
513384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
514186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
514186     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
514187     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
514962     DEBUG Test worker     d.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 
516630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
517431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
517432     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
517433     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
518206     DEBUG Test worker     d.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 
519893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
520694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
520694     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
520696     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
521469     DEBUG Test worker     d.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 
523163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
523969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
523969     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
523970     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
524743     DEBUG Test worker     d.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 
526420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
527227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
527228     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
527229     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
528007     DEBUG Test worker     d.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 
529705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
530509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
530510     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
530511     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 
531293     DEBUG Test worker     d.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 
532986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
533789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
533790     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqComplete.proof 
533791     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 
534567     DEBUG Test worker     d.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 
536236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
537060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
537061     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailR.proof 
537062     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 
537835     DEBUG Test worker     d.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 
539500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
540304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.29ms 
540305     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailL.proof 
540306     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
541080     DEBUG Test worker     d.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 
542756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
543561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.03ms 
543561     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
543562     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
544336     DEBUG Test worker     d.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 
546021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
546827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
546827     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
546828     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 
547601     DEBUG Test worker     d.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 
549295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
550111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.13ms 
550111     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split.proof 
550112     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
550888     DEBUG Test worker     d.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 
552572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
553390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.88ms 
553391     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
553392     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
554170     DEBUG Test worker     d.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 
555840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
556677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.75ms 
556677     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
556678     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
557459     DEBUG Test worker     d.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 
559134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
559969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.73ms 
559969     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
559970     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
560745     DEBUG Test worker     d.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 
562409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
563226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.55ms 
563226     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
563227     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
564021     DEBUG Test worker     d.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 
565684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
566530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.93ms 
566530     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
566532     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 
567320     DEBUG Test worker     d.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 
569016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
569821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
569821     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_empty.proof 
569823     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
570611     DEBUG Test worker     d.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 
572276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
573079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
573079     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
573081     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
573869     DEBUG Test worker     d.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 
575537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
576337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
576337     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
576338     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.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 
578864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
579677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.55ms 
579677     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
579678     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
580465     DEBUG Test worker     d.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 
582136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
582941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
582942     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
582943     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
583736     DEBUG Test worker     d.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 
585404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
586222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
586222     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
586223     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
586997     DEBUG Test worker     d.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 
588659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
589483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.57ms 
589484     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
589485     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
590259     DEBUG Test worker     d.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 
592003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
592815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.87ms 
592815     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
592817     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
593593     DEBUG Test worker     d.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 
595267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
596077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
596077     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
596078     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
596869     DEBUG Test worker     d.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 
598544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
599344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.5ns 
599344     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
599345     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
600118     DEBUG Test worker     d.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 
601806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
602612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
602612     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
602613     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
603391     DEBUG Test worker     d.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 
605063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
605866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 
605866     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
605868     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
606655     DEBUG Test worker     d.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 
608333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
609137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
609137     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
609138     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
609914     DEBUG Test worker     d.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 
611604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
612445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.92ms 
612446     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
612447     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
613221     DEBUG Test worker     d.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 
614918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
615736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
615737     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
615738     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
616515     DEBUG Test worker     d.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 
618182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
618989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
618989     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
618990     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
619773     DEBUG Test worker     d.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 
621441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
622240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 253.3ns 
622241     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
622242     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 
623016     DEBUG Test worker     d.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 
624713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
625590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.7ms 
625590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_seqNPermRight.proof 
625591     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
626374     DEBUG Test worker     d.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 
628056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
628886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.57ms 
628886     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
628888     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
629665     DEBUG Test worker     d.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 
631346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
632146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 237ns 
632146     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
632148     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
632923     DEBUG Test worker     d.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 
634597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
635414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 208.8ns 
635414     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
635416     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
636192     DEBUG Test worker     d.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 
637863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
638668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.5ns 
638668     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
638669     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
639483     DEBUG Test worker     d.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 
641198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
641999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.4ns 
641999     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
642000     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 
642777     DEBUG Test worker     d.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 
644469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
645371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.82ms 
645372     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermForall.proof 
645374     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 
646168     DEBUG Test worker     d.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 
647873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
648708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.25ms 
648708     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm/Taclet_seqPermExists.proof 
648709     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
649493     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 
649494     DEBUG Test worker     d.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 
651190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
652009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
652009     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
652033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
652073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
652085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
652090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
652100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
652101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
652103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
652104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
652109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
652110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
652112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
652113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
652262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
652262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
652263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
652264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
652265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
652358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
652359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
652360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
652361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
652362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
652363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
652524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
652525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
652526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
652527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
652527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
652528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
652660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
652661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
652663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
652664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
652664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
652666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
652675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
652677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
652679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
652681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
652684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
652685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
652694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
652695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
652696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
652696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
652698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
652699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
652834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
652835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
652837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
652966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
652967     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)'' 
652968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
652971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
652971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
652972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
652973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
652975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
652979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
652980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
652982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
652982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
652983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
653126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
653129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
653131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
653132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
653132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
653133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
653135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
653255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
653256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
653257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
653258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
653259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
653260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
653261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
653262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
653354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
653355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
653447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
653455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
653464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
653465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
653466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
653467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
653467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
653468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
653468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
653469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
653481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
653489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
653599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
653600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
653601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
653602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
653603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
653603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
653604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
653604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
653654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
653659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
653757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
653758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
653759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
653761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
653762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
653763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
653888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
653892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
653893     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)'' 
653894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
653895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
653896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
653897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
653897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
653906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
653907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
653909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
653910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
654028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
654029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
654031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
654032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
654033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
654034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
654196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
654197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
654199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
654200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
654200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
654201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
654202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
654202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
654291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
654292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
654369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
654370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
654371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
654375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
654379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
654384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
654504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
654505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
654506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
654507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
654517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
654606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
658624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
658625     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)'' 
658629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
658631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
658632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
658632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
658633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
658640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
658640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
658642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
658643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
658643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
658728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
658731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
658732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
658733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
658734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
658734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
658735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
658821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
658822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
658823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
658824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
658825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
658825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
658826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
658826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
658896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
658897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
658965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
658970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
658975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
658975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
658976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
658977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
658986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
659094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
659095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
659096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
659097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
659163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
659172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
659173     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)'' 
659174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
659176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
659176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
659177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
659177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
659187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
659188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
659189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
659190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
659190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
659269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
659270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
659271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
659272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
659273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
659356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
659360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
659361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
659362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
659362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
659363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
659364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
659459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
659460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
659461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
659462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
659462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
659463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
659463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
659464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
659464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
659465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
659466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
659466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
659467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
659467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
659468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
659553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
659554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
659561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
659633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
659706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
659707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
659708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
659708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
659709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
659710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
659710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
659710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
659711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
659714     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)

659715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
659715     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)

659715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
659715     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)

659716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
659717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 8 
659717     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)))] 
659718     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)] 
659718     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)] 
659718     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)))] 
659718     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)))] 
659718     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)))] 
659719     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)))] 
659719     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))))] 
659722     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
660640     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 
660640     DEBUG Test worker     d.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 
662384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
663207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
663207     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
663207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
663213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
663222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
663224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
663227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
663229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
663233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
663234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
663237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
663238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
663240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
663248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
663249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
663250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
663291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
663292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
663293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
663293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
663294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
663353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
663353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
663354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
663355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
663355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
663359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
663359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
663359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
663360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
663361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
663363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
663441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
663442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
663442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
663443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
663444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
663445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
663563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
663564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
663564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
663565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
663565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
663566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
663566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
663566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
663567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
663567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
663567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
663568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
663568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
663568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
663569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
663569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
663569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
663570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
663570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
663573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
663605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
663606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
663648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
663649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
663649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
663651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
663652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
663652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
663703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
663704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
663705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
663706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
663707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
663708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
663708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
663745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
663747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
663750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
663794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
663841     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof 
664644     DEBUG Test worker     d.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 
666476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
667338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.63ms 
667338     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file tacletProofs/seqRules/Taclet_eqSameSeq.proof