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

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

tests
1

failures
0

ignored
10m11.29s

duration
99%

successful

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.006s passed
powPositiveConcrete data()[101] 3.009s passed
powGeq1Concrete data()[102] 2.999s passed
pow2InIntLower data()[103] 3.002s passed
pow2InIntUpper data()[104] 3.003s passed
logSelfConcrete data()[105] 3.014s passed
log1Concrete data()[106] 3.015s passed
logProduct data()[107] 3.020s passed
logTimesBaseConcrete data()[108] 3.009s passed
logProdIdentity data()[109] 3.054s passed
moduloByteIsInByte data()[10] 3.133s passed
logProdIdentityConcrete data()[110] 3.024s passed
logPowIdentity data()[111] 3.024s passed
logPowIdentityConcrete data()[112] 3.021s passed
logPositive data()[113] 3.034s passed
logPositiveConcrete data()[114] 3.037s passed
logMono data()[115] 3.051s passed
logMonoConcrete data()[116] 3.018s passed
powLogLess data()[117] 3.032s passed
powLogMore2 data()[118] 3.024s passed
logLessThanPow data()[119] 3.015s passed
moduloCharIsInChar data()[11] 3.082s passed
logLessThanPowConcrete data()[120] 3.035s passed
logSqueeze data()[121] 3.021s passed
ifthenelse_equals data()[122] 3.006s passed
ifthenelse_equals_1 data()[123] 3.013s passed
ifthenelse_equals_2 data()[124] 3.010s passed
disjointWithSingleton1 data()[125] 3.020s passed
disjointWithSingleton2 data()[126] 3.006s passed
disjointArrayRanges data()[127] 3.009s passed
disjointArrayRangeAllFields1 data()[128] 3.019s passed
disjointArrayRangeAllFields2 data()[129] 3.010s passed
div_unique1 data()[12] 3.095s passed
seqSelfDefinition data()[130] 3.023s passed
seqOutsideValue data()[131] 3.025s passed
castedGetAny data()[132] 3.020s passed
seqGetAlphaCast data()[133] 3.022s passed
getOfSeqSingleton data()[134] 3.014s passed
getOfSeqSingletonConcrete data()[135] 3.063s passed
getOfSeqConcat data()[136] 3.027s passed
getOfSeqSub data()[137] 3.026s passed
getOfSeqReverse data()[138] 3.016s passed
lenOfSeqEmpty data()[139] 3.011s passed
div_unique2 data()[13] 3.127s passed
lenOfSeqSingleton data()[140] 3.018s passed
lenOfSeqConcat data()[141] 3.020s passed
lenOfSeqSub data()[142] 3.036s passed
lenOfSeqReverse data()[143] 3.019s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.015s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.014s passed
getOfSeqSingletonEQ data()[146] 3.010s passed
getOfSeqConcatEQ data()[147] 3.039s passed
getOfSeqSubEQ data()[148] 3.020s passed
getOfSeqReverseEQ data()[149] 3.017s passed
div_exists data()[14] 3.211s passed
lenOfSeqEmptyEQ data()[150] 3.012s passed
lenOfSeqSingletonEQ data()[151] 3.039s passed
lenOfSeqConcatEQ data()[152] 3.013s passed
lenOfSeqSubEQ data()[153] 3.018s passed
lenOfSeqReverseEQ data()[154] 3.007s passed
getOfSeqDefEQ data()[155] 3.036s passed
lenOfSeqDefEQ data()[156] 3.035s passed
seqConcatWithSeqEmpty1 data()[157] 3.029s passed
seqConcatWithSeqEmpty2 data()[158] 3.052s passed
seqReverseOfSeqEmpty data()[159] 3.013s passed
div_one data()[15] 3.083s passed
subSeqComplete data()[160] 3.010s passed
subSeqTailR data()[161] 3.031s passed
subSeqTailL data()[162] 3.019s passed
subSeqTailEQR data()[163] 3.012s passed
subSeqTailEQL data()[164] 3.031s passed
seqDef_split data()[165] 3.033s passed
seqDef_induction_upper data()[166] 3.045s passed
seqDef_induction_upper_concrete data()[167] 3.031s passed
seqDef_induction_lower data()[168] 3.036s passed
seqDef_induction_lower_concrete data()[169] 3.059s passed
jdiv_one data()[16] 3.080s passed
seqDef_split_in_three data()[170] 3.069s passed
seqDef_empty data()[171] 3.041s passed
seqDef_one_summand data()[172] 3.022s passed
seqDef_lower_equals_upper data()[173] 3.039s passed
seqDefOfSeq data()[174] 3.025s passed
seqSelfDefinitionEQ2 data()[175] 3.034s passed
indexOfSeqSingleton data()[176] 3.022s passed
indexOfSeqConcatFirst data()[177] 3.031s passed
indexOfSeqConcatSecond data()[178] 3.013s passed
indexOfSeqSub data()[179] 3.051s passed
div_zero data()[17] 3.110s passed
lenOfArray2seq data()[180] 3.012s passed
getAnyOfArray2seq data()[181] 3.038s passed
getOfArray2seq data()[182] 3.028s passed
getAnyOfNPermInv data()[183] 3.041s passed
seqNPermRange data()[184] 3.087s passed
seqPermTrans data()[185] 3.051s passed
seqPermRefl data()[186] 3.044s passed
seqPermSplit data()[187] 3.043s passed
seqNPermRight data()[188] 3.117s passed
seqPermFromSwap data()[189] 3.079s passed
divResZero1 data()[18] 3.070s passed
seqPermTransAlt0 data()[190] 3.052s passed
seqPermTransAlt1 data()[191] 3.022s passed
seqPermTransAlt2 data()[192] 3.036s passed
seqPermTransAlt3 data()[193] 3.028s passed
seqPermForall data()[194] 3.151s passed
seqPermExists data()[195] 3.124s passed
schiffl_lemma_2 data()[196] 9.889s failed
schiffl_thm_1 data()[197] 3.763s passed
eqSameSeq data()[198] 3.166s passed
divResZero2 data()[19] 3.074s passed
eqTermCut data()[1] 3.662s passed
divResOne1 data()[20] 3.067s passed
divResOne2 data()[21] 3.110s passed
div_cancel1 data()[22] 3.076s passed
div_cancel2 data()[23] 3.040s passed
divAddMultDenom data()[24] 3.076s passed
divMinus data()[25] 3.109s passed
divMinusDenom data()[26] 3.077s passed
divLeastDPos data()[27] 3.054s passed
divLeastDNeg data()[28] 3.051s passed
divGreatestDPos data()[29] 3.056s passed
equivAllRight data()[2] 3.350s passed
divGreatestDNeg data()[30] 3.050s passed
divIncreasingPos data()[31] 3.047s passed
divIncreasingNeg data()[32] 3.046s passed
jdiv_zero data()[33] 3.034s passed
jdivPulloutMinusNum data()[34] 3.044s passed
jdivPulloutMinusDenom data()[35] 3.108s passed
jdiv_uniquePosPos data()[36] 3.088s passed
jdiv_uniquePosNeg data()[37] 3.067s passed
jdiv_uniqueNegPos data()[38] 3.082s passed
jdiv_uniqueNegNeg data()[39] 3.075s passed
irrflConcrete1 data()[3] 3.321s passed
jdivMultDenom1 data()[40] 3.052s passed
jdivMultDenom2 data()[41] 3.049s passed
mod_geZero data()[42] 3.077s passed
mod_lessDenom data()[43] 3.032s passed
jmod_NumPos data()[44] 3.037s passed
jmod_NumNeg data()[45] 3.029s passed
jmod_geZero data()[46] 3.039s passed
jmodNumZero data()[47] 3.043s passed
jmod_pulloutminusNum data()[48] 3.032s passed
jmod_pulloutminusDenom data()[49] 3.013s passed
irrflConcrete2 data()[4] 3.192s passed
jmodUnique1 data()[50] 3.086s passed
jmodUnique2 data()[51] 3.099s passed
intDivRem data()[52] 3.013s passed
jmodjmod data()[53] 3.035s passed
jmodDivisible data()[54] 3.023s passed
jmodDivisibleRep data()[55] 3.029s passed
jdivAddMultDenom data()[56] 3.115s passed
jmodAltZero data()[57] 3.024s passed
jmodAddMultDenomZero data()[58] 3.027s passed
polyDiv_zero data()[59] 3.055s passed
cancel_gtPos data()[5] 3.184s passed
polyMod_ltdivDenom data()[60] 3.029s passed
bsum_empty data()[61] 3.010s passed
bsum_induction_upper data()[62] 3.021s passed
bsum_induction_lower data()[63] 3.032s passed
bsum_num_of_bounds data()[64] 3.034s passed
bsum_num_of_bounds2 data()[65] 3.030s passed
bsum_induction_upper2 data()[66] 3.018s passed
bsum_induction_upper_concrete data()[67] 3.009s passed
bsum_induction_upper_concrete_2 data()[68] 3.016s passed
bsum_induction_upper2_concrete data()[69] 3.016s passed
cancel_gtNeg data()[6] 3.146s passed
bsum_induction_lower_concrete data()[70] 3.014s passed
bsum_induction_lower2 data()[71] 3.015s passed
bsum_induction_lower2_concrete data()[72] 3.019s passed
bsum_positive data()[73] 3.057s passed
bsum_upper_bound data()[74] 3.035s passed
bsum_lower_bound data()[75] 3.023s passed
bsum_positive_lower_bound_element data()[76] 3.032s passed
bsum_sub_same_index data()[77] 3.030s passed
bsum_less_same_index data()[78] 3.040s passed
bsum_equal_except_one_index data()[79] 3.033s passed
moduloIntIsInInt data()[7] 3.165s passed
bsum_num_of_is_max data()[80] 3.026s passed
bsum_num_of_is_max2 data()[81] 3.020s passed
bsum_num_of_is_max3 data()[82] 3.018s passed
bsum_num_of_is_max4 data()[83] 3.029s passed
bsum_num_of_lt_max data()[84] 3.159s passed
bsum_num_of_lt_max2 data()[85] 3.031s passed
bsum_num_of_lt_max3 data()[86] 3.030s passed
bsum_num_of_lt_max4 data()[87] 3.024s passed
bsum_num_of_gt0 data()[88] 3.017s passed
bsum_num_of_gt0_alt data()[89] 3.017s passed
moduloLongIsInLong data()[8] 3.146s passed
bsum_add_concrete data()[90] 3.004s passed
bprod_all_positive data()[91] 3.020s passed
bprod_split data()[92] 3.002s passed
powConcrete0 data()[93] 3.003s passed
powConcrete1 data()[94] 3.005s passed
powSplitFactor data()[95] 3.030s passed
powAdd data()[96] 3.017s passed
powMono data()[97] 3.018s passed
powMonoConcrete data()[98] 3.008s passed
powMonoConcreteRight data()[99] 3.008s passed
moduloShortIsInShort data()[9] 3.098s passed

Standard output

522        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
549        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 14.15ms 
883        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
900        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)

1771       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1774       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1779       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1779       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3442       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8467       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.58s 
8539       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8572       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.9ns 
8584       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8585       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.4ns 
8590       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
11310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12238      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.73ms 
12250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.4ns 
12252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
14762      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
15600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.9ns 
15602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18134      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
18135      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18912      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18919      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
18921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18921      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.5ns 
18923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21340      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
21341      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22111      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
22114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22114      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 743.81ns 
22116      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24507      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
24507      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25295      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.72ms 
25298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25298      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns 
25299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
27671      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms 
28444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28445      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.5ns 
28446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
30858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31607      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 599.51ns 
31609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.8ns 
31611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
34006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34753      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.61ns 
34756      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.4ns 
34757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
37110      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37852      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 716.81ns 
37854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns 
37855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40242      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
40242      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40985      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.01ns 
40987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40987      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.8ns 
40988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
43326      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44067      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.51ns 
44069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.4ns 
44070      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46392      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
46393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47162      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.15ms 
47166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47167      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 713.61ns 
47168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
49503      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50288      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.41ms 
50293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.5ns 
50296      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
52635      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53501      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 126.47ms 
53504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53504      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.2ns 
53505      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55844      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
55844      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56580      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56584      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
56586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns 
56587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58900      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
58901      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59664      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
59667      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.3ns 
59669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
61985      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
62740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62775      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.64ms 
62778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.6ns 
62779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
65079      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
65834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
65845      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
65848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
65848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.1ns 
65849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
68148      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
68908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
68918      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
68921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
68921      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.81ns 
68923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
71220      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
71975      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
71986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
71988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
71988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns 
71989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
74328      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75096      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
75098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.2ns 
75100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
77400      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78172      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.68ms 
78174      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.7ns 
78175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
80460      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
81209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
81212      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
81214      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
81214      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.5ns 
81215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83504      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
83504      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
84253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
84286      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.56ms 
84289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
84290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.23ns 
84291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86605      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
86605      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
87354      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.27ms 
87399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.5ns 
87401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89696      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
89696      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
90444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
90474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms 
90477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
90479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.54ms 
90481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92768      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
92770      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
93520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
93527      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
93531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
93531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 681.94ns 
93533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
95818      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
96566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
96578      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
96581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
96581      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.5ns 
96582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98863      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
98863      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
99622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
99635      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.57ms 
99642      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
99642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.81ns 
99643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
101927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
102682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
102689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
102690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
102691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 
102691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
104981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
105729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
105736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
105738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
105738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
105738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
108027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
108776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
108782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
108784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
108784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns 
108785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
111067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
111813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
111816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
111818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
111818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
111819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
114100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
114847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
114860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.15ms 
114862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
114862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.51ns 
114863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
117153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
117918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
117967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.05ms 
117971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
117971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.91ns 
117983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
120291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
121043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
121058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.88ms 
121059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
121059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 
121060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
123347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
124102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
124124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ms 
124127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
124127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.11ns 
124129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
126436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
127192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
127207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.12ms 
127208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
127209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
127209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
129518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
130268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
130282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.38ms 
130283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
130283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
130284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
132558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
133302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
133334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.99ms 
133336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
133336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
133336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
135625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
136380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
136383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
136384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
136384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
136385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
138685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
139456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
139460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
139462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
139462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
139462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
141739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
142485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
142492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
142494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
142494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
142495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
144769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
145522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
145529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
145531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
145531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
145531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
147796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
148538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
148558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.15ms 
148563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
148566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.33ms 
148567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
150847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
151590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
151598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
151599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
151599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
151600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
153876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
154636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
154640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
154643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
154643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.1ns 
154644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
156947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
157669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
157672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
157674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
157674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
157674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
159961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
160682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
160685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
160686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
160687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
160687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
162980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
163703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
163771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.32ms 
163774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
163774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
163775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
166079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
166801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
166870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.38ms 
166872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
166872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
166872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
169161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
169881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
169884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
169885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
169885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
169886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
172171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
172890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
172918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.93ms 
172920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
172920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.2ns 
172921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
175201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
175921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
175941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ms 
175942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
175942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
175943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
178246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
178968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
178971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
178972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
178972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
178973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
181266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
181987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
182085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.97ms 
182088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
182088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.4ns 
182089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
184380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
185100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
185109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.21ms 
185112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
185112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.3ns 
185115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
187409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
188130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
188136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
188138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
188139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.3ns 
188140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
190429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
191177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
191191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
191192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
191193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
191193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
193466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
194209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
194220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
194221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
194222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
194222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
196487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
197227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
197230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
197231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
197231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
197232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
199503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
200248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
200251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
200252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
200252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
200253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
202521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
203269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
203283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
203284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
203284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
203285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
205559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
206305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
206317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
206319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
206319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
206320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
208595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
209336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
209347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ms 
209349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
209349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
209349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
211620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
212363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
212365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 980.62ns 
212366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
212367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
212367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
214631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
215372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
215375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
215376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
215376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
215377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
217641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
218386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
218391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
218392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
218392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
218393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
220662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
221404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
221406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 903.01ns 
221408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
221408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
221409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
223677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
224418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
224420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 482.31ns 
224422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
224422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
224422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
226689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
227432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
227435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
227437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
227437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
227438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
229711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
230452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
230455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.3ns 
230456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
230456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
230457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
232720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
233469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
233511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.04ms 
233513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
233513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 
233514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
235784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
236525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
236546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.81ms 
236547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
236547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
236548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
238809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
239551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
239569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.78ms 
239570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
239570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
239571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
241834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
242577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
242601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.15ms 
242603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
242603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
242603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
244868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
245615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
245631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.86ms 
245632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
245632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
245633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
247898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
248641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
248671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.28ms 
248673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
248673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.2ns 
248674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
250945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
251689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
251705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
251706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
251706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
251707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
253974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
254718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
254731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.87ms 
254732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
254732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
254733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
256994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
257737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
257750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.33ms 
257752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
257752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
257753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
260014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
260757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
260768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms 
260770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
260770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
260770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
263031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
263781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
263797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
263799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
263799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
263800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
266201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
266942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
266957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms 
266958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
266958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
266959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
269225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
269971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
269987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.58ms 
269989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
269989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.2ns 
269990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
272262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
273004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
273018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 
273019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
273019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
273020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
275287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
276028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
276042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ms 
276043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
276043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
276044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
278303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
279044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
279058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.59ms 
279059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
279059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
279060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
281320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
282061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
282075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.59ms 
282077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
282077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
282077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
284333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
285074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
285079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
285080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
285080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
285081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
287368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
288089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
288099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
288101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
288101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
288101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
290379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
291098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
291101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
291103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
291103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
291103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
293383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
294102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
294104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.41ns 
294106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
294106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
294106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
296387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
297107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
297110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 692.51ns 
297111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
297111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
297111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
299409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
300134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
300139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
300141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
300141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.1ns 
300143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
302427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
303151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
303156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
303158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
303158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.6ns 
303159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
305446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
306165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
306175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.33ms 
306176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
306176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
306177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
308458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
309179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
309183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
309184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
309184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
309185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
311464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
312189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
312191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 428.31ns 
312192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
312192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
312192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
314472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
315192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
315196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
315198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
315198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
315198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
317483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
318203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
318205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.81ns 
318206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
318206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
318207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
320483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
321203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
321205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484.11ns 
321206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
321206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
321207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
323485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
324205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
324207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 512.38ns 
324208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
324208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
324209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
326487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
327207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
327210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
327212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
327212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
327212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
329498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
330218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
330225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
330226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
330226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
330227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
332516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
333236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
333240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
333241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
333241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
333242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
335530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
336255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
336260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
336261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
336261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
336261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
338546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
339265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
339269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
339270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
339270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
339271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
341559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
342308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
342323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.85ms 
342324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
342324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
342325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
344593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
345338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
345341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
345348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
345348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
345349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
347622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
348367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
348370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
348372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
348372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
348372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
350643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
351388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
351391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
351392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
351392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
351393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
353663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
354412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
354425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
354427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
354427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.9ns 
354428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
356714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
357458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
357462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 312.5ns 
357464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
357464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
357465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
359733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
360481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
360513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.05ms 
360515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
360516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.4ns 
360516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
362785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
363529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
363532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
363533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
363533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
363534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
365803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
366549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
366563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.78ms 
366565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
366565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
366566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
368832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
369574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
369587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 
369588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
369588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
369589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
371845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
372585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
372602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.63ms 
372604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
372604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
372604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
374893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
375635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
375637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 512.61ns 
375638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
375638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
375639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
377911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
378654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
378658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
378660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
378660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
378660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
380919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
381662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
381665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
381666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
381666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
381667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
383930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
384675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
384678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.11ns 
384679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
384679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
384680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
386939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
387685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
387687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.61ns 
387688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
387688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
387689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
389945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
390704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
390707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
390711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
390711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
390711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
392964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
393713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
393715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
393716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
393716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
393717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
395971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
396717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
396724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
396726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
396726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
396726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
398989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
399737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
399743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
399744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
399744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
399745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
402002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
402748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
402754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
402755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
402755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
402756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
405014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
405769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
405776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
405778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
405778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.9ns 
405778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
408043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
408797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
408801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
408803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
408803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
408803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
411087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
411818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
411822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
411823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
411823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
411824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
414108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
414841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
414843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.71ns 
414844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
414844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
414845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
417124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
417855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
417858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938.11ns 
417859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
417859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
417860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
420148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
420918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
420920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 764.91ns 
420922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
420922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
420922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
423186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
423940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
423948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
423949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
423949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
423950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
426219     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
426970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
426973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
426974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
426975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
426975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
429229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
429985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
429990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
429991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
429991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
429991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
432246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
432998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
433000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.61ns 
433001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
433001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
433002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
435279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
436013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
436014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.21ns 
436020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
436020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 
436021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
438304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
439036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
439038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
439040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
439040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
439040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
441321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
442072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
442074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 703.41ns 
442075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
442076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
442076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
444338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
445091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
445093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 907.91ns 
445094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
445095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
445095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
447355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
448106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
448108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.11ns 
448109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
448110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
448110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
450365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
451118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
451122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
451123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
451123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
451124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
453403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
454131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
454133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.61ns 
454134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
454134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
454135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
456412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
457164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
457171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
457173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
457173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
457173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
459436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
460189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
460191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.31ns 
460192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
460192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
460193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
462450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
463203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
463208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.29ms 
463209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
463209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
463210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
465489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
466218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
466221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757.01ns 
466222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
466222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
466223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
468505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
469257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
469259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.01ns 
469260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
469260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
469262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
471516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
472270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
472273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
472274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
472274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
472275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
474537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
475288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
475290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.01ns 
475292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
475292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
475292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
477565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
478295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
478297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
478298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
478298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
478299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
480577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
481331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
481333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
481335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
481335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
481335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
483605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
484364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
484368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
484369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
484369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
484371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
486635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
487390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
487397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
487398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
487399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 656.41ns 
487400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
489685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
490442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
490449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
490451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
490451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
490451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
492706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
493457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
493462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
493464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
493464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
493464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
495715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
496467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
496472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
496473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
496474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
496474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
498744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
499494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
499503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.31ms 
499505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
499505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
499505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
501761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
502514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
502523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.19ms 
502524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
502524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
502525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
504798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
505526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
505534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
505536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
505536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
505536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
507807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
508559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
508565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
508566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
508566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
508567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
510825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
511579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
511598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.79ms 
511599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
511599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
511600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
513874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
514623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
514643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.82ms 
514645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
514645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
514646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
516899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
517657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
517675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.26ms 
517676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
517676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
517677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
519962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
520693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
520710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
520712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
520712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
520713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
522997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
523751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
523770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.19ms 
523771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
523771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
523772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
526036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
526792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
526838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.28ms 
526840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
526840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
526841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
529124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
529873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
529879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
529882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
529882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.7ns 
529883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
532145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
532896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
532901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
532902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
532902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
532903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
535184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
535938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
535941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
535942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
535942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
535943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
538200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
538953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
538965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.35ms 
538967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
538967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
538967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
541244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
541993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
541999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
542000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
542001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
542001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
544268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
545019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
545021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
545023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
545023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
545023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
547292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
548043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
548052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.07ms 
548053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
548053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
548054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.25s 
550305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
551056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
551066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.47ms 
551071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
551072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.5ns 
551072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
553354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
554104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
554116     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.75ms 
554117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
554117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
554118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
556376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
557126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
557129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.61ns 
557130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
557130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
557130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
559408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
560163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
560166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
560167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
560167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
560168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
562454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
563189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
563194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
563195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
563195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
563196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
565479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
566231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
566235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
566236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
566236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
566237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
568525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
569283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
569322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.38ms 
569324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
569324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
569325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
571602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
572357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
572373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.37ms 
572374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
572374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
572375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
574655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
575407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
575418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
575419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
575419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
575420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
577700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
578458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
578460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 156.4ns 
578463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
578463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 
578464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
580751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
581504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
581578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.63ms 
581580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
581580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
581581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
583871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
584625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
584657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.27ms 
584658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
584658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
584659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
586952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
587707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
587709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291ns 
587712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
587712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.8ns 
587713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
589978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
590731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
590732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.7ns 
590734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
590734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
590734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
593012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
593767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
593769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 199.2ns 
593770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
593770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
593771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
596040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
596794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
596796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 323ns 
596797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
596797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
596798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
599082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
599842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
599947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.24ms 
599949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
599949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 
599950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
602272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
603025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
603071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.54ms 
603073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
603073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
603074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
605373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
606126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
606128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
606156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
606208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
606222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
606228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
606240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
606241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
606242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
606243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
606249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
606250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
606254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
606257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
606480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
606481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
606483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
606484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
606485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
606610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
606611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
606613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
606614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
606615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
606616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
606765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
606766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
606767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
606768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
606769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
606773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
606882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
606883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
606885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
606885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
606886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
606887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
606900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
606901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
606902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
606904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
606905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
606906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
606914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
606915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
606916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
606917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
606918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
606919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
607035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
607036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
607038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
607138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
607139     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)'' 
607141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
607143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
607144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
607145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
607146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
607148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
607155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
607156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
607158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
607159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
607160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
607290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
607296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
607297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
607298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
607299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
607300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
607302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
607399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
607401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
607402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
607403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
607404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
607405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
607408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
607410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
607491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
607492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
607592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
607596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
607602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
607603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
607604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
607605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
607606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
607607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
607607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
607608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
607615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
607620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
607706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
607707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
607709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
607711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
607711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
607712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
607713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
607713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
607759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
607764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
607843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
607845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
607846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
607847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
607849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
607850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
607957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
607961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
607963     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)'' 
607965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
607966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
607967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
607968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
607968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
607977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
607982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
607983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
607984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
608067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
608068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
608069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
608070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
608071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
608072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
608157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
608159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
608160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
608162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
608163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
608164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
608164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
608165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
608233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
608234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
608305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
608306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
608351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
608355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
608358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
608362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
608499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
608500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
608501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
608502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
608511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
608596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
611895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
611896     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)'' 
611900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
611901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
611902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
611903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
611904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
611912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
611912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
611913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
611914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
611915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
611995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
611999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
612000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
612001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
612002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
612003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
612004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
612083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
612085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
612086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
612088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
612089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
612090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
612090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
612091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
612159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
612161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
612224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
612228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
612232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
612233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
612233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
612234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
612242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
612312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
612313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
612314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
612315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
612377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
612386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
612387     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)'' 
612388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
612389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
612390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
612391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
612391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
612401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
612402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
612403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
612404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
612404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
612479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
612480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
612481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
612482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
612483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
612563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
612567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
612567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
612568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
612569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
612569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
612570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
612697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
612698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
612699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
612700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
612700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
612701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
612702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
612702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
612703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
612704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
612705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
612705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
612706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
612706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
612707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
612787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
612788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
612795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
612866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
612937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
612938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
612939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
612940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
612941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
612941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
612942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
612943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
612943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
612947     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)

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

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

612949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
612950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 8 
612951     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)))] 
612952     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)] 
612952     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)] 
612952     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)))] 
612952     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)))] 
612953     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)))] 
612953     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)))] 
612953     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))))] 
612964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
612965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
612965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
615404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
616185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
616186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
616187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
616195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
616203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
616205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
616207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
616209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
616213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
616214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
616218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
616218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
616220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
616228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
616228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
616230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
616270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
616271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
616272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
616272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
616273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
616325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
616325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
616326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
616327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
616327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
616330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
616331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
616331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
616331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
616332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
616333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
616397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
616398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
616398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
616399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
616400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
616400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
616462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
616462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
616463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
616463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
616464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
616464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
616465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
616465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
616466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
616466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
616466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
616467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
616467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
616467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
616468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
616468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
616468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
616469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
616470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
616472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
616498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
616506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
616541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
616541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
616542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
616543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
616544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
616544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
616593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
616595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
616596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
616596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
616597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
616598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
616599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
616634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
616636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
616639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
616682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
616728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
616728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
616728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
619079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
619877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
619892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.71ms