# . * SAT 0 * UNSAT 0 * TIMEOUT 0 * UNKNOWN 208 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/UFBVLIA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-UFBVLIA.tar.zst-do
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/UFBVLIA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-189.smt2 | 0.063s | 21.172MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-015.smt2 | 0.082s | 21.88MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-190.smt2 | 0.093s | 21.152MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-193.smt2 | 0.097s | 21.216MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-004.smt2 | 0.097s | 21.532MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-184.smt2 | 0.098s | 21.3MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-202.smt2 | 0.101s | 21.304MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-006.smt2 | 0.105s | 20.104MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-016.smt2 | 0.112s | 22.016MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-196.smt2 | 0.117s | 21.256MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-188.smt2 | 0.124s | 21.132MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-198.smt2 | 0.125s | 21.344MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-182.smt2 | 0.127s | 20.124MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-057.smt2 | 0.127s | 23.96MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-010.smt2 | 0.129s | 21.468MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-013.smt2 | 0.131s | 21.836MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-197.smt2 | 0.132s | 21.268MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-192.smt2 | 0.132s | 21.176MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-050.smt2 | 0.133s | 23.724MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-191.smt2 | 0.134s | 21.412MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-003.smt2 | 0.135s | 21.296MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-011.smt2 | 0.139s | 21.376MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-185.smt2 | 0.140s | 21.464MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-204.smt2 | 0.142s | 22.12MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-000.smt2 | 0.142s | 21.168MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-045.smt2 | 0.144s | 23.764MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-035.smt2 | 0.144s | 22.7MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-019.smt2 | 0.144s | 22.148MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-181.smt2 | 0.147s | 21.168MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-001.smt2 | 0.150s | 21.192MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-186.smt2 | 0.151s | 21.256MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-183.smt2 | 0.152s | 21.148MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-027.smt2 | 0.155s | 22.852MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-005.smt2 | 0.155s | 21.236MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-043.smt2 | 0.159s | 22.668MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-076.smt2 | 0.159s | 24.564MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-063.smt2 | 0.159s | 25.136MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-034.smt2 | 0.159s | 22.688MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-007.smt2 | 0.161s | 21.308MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-026.smt2 | 0.162s | 22.412MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-018.smt2 | 0.162s | 22.332MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-207.smt2 | 0.164s | 21.936MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-022.smt2 | 0.164s | 22.16MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-206.smt2 | 0.165s | 22.288MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-187.smt2 | 0.167s | 21.256MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-012.smt2 | 0.167s | 21.36MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-002.smt2 | 0.167s | 21.184MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-201.smt2 | 0.168s | 21.432MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-025.smt2 | 0.169s | 22.424MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-009.smt2 | 0.169s | 21.388MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-194.smt2 | 0.170s | 21.28MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-030.smt2 | 0.173s | 22.476MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-060.smt2 | 0.173s | 25.12MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-048.smt2 | 0.176s | 23.5MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-024.smt2 | 0.177s | 22.564MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-199.smt2 | 0.177s | 21.356MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-205.smt2 | 0.178s | 21.888MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-200.smt2 | 0.179s | 21.428MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-065.smt2 | 0.179s | 24.228MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-061.smt2 | 0.180s | 24.044MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-028.smt2 | 0.181s | 22.448MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-014.smt2 | 0.181s | 21.776MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-008.smt2 | 0.182s | 21.212MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-041.smt2 | 0.183s | 23.62MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-203.smt2 | 0.184s | 21.424MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-036.smt2 | 0.184s | 23.664MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-020.smt2 | 0.187s | 22.292MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-017.smt2 | 0.189s | 22.044MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-023.smt2 | 0.189s | 22.316MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-108.smt2 | 0.196s | 27.16MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-053.smt2 | 0.198s | 23.984MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-032.smt2 | 0.198s | 24.716MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-031.smt2 | 0.199s | 22.472MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-088.smt2 | 0.199s | 27.244MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-038.smt2 | 0.199s | 23.492MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-055.smt2 | 0.200s | 24.208MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-195.smt2 | 0.201s | 21.332MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-054.smt2 | 0.204s | 24.128MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-074.smt2 | 0.206s | 24.748MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-096.smt2 | 0.208s | 27.044MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-040.smt2 | 0.214s | 23.556MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-092.smt2 | 0.216s | 27.636MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-106.smt2 | 0.218s | 27.384MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-059.smt2 | 0.221s | 24.632MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-044.smt2 | 0.223s | 23.692MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-037.smt2 | 0.224s | 23.324MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-046.smt2 | 0.226s | 23.464MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-107.smt2 | 0.226s | 26.356MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-098.smt2 | 0.228s | 27.424MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-085.smt2 | 0.229s | 26.444MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-047.smt2 | 0.231s | 23.424MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-021.smt2 | 0.233s | 22.384MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-058.smt2 | 0.233s | 24.964MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-073.smt2 | 0.234s | 25.092MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-033.smt2 | 0.238s | 22.728MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-056.smt2 | 0.239s | 24.352MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-109.smt2 | 0.241s | 25.78MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-093.smt2 | 0.241s | 25.392MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-029.smt2 | 0.242s | 22.34MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-052.smt2 | 0.246s | 25.112MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-039.smt2 | 0.248s | 24.472MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-083.smt2 | 0.251s | 25.972MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-078.smt2 | 0.255s | 26.492MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-068.smt2 | 0.257s | 25.452MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-062.smt2 | 0.259s | 25.06MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-082.smt2 | 0.262s | 27.276MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-042.smt2 | 0.263s | 23.472MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-049.smt2 | 0.264s | 23.08MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-084.smt2 | 0.266s | 27.628MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-127.smt2 | 0.267s | 29.78MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-067.smt2 | 0.268s | 24.732MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-079.smt2 | 0.271s | 26.504MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-075.smt2 | 0.272s | 26.42MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-066.smt2 | 0.275s | 26.54MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-070.smt2 | 0.275s | 25.212MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-072.smt2 | 0.278s | 26.68MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-091.smt2 | 0.279s | 27.76MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-125.smt2 | 0.280s | 28.072MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-094.smt2 | 0.281s | 28.244MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-089.smt2 | 0.281s | 26.656MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-080.smt2 | 0.285s | 26.612MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-142.smt2 | 0.290s | 28.224MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-104.smt2 | 0.298s | 27.18MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-069.smt2 | 0.299s | 24.876MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-064.smt2 | 0.300s | 25.12MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-051.smt2 | 0.303s | 25.0MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-105.smt2 | 0.306s | 28.152MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-077.smt2 | 0.310s | 25.164MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-140.smt2 | 0.310s | 29.4MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-121.smt2 | 0.317s | 29.848MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-086.smt2 | 0.323s | 27.62MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-100.smt2 | 0.323s | 27.896MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-099.smt2 | 0.325s | 28.452MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-081.smt2 | 0.325s | 27.752MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-133.smt2 | 0.325s | 30.396MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-090.smt2 | 0.326s | 28.384MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-071.smt2 | 0.327s | 26.772MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-095.smt2 | 0.329s | 27.696MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-102.smt2 | 0.331s | 27.492MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-114.smt2 | 0.337s | 29.876MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-135.smt2 | 0.338s | 31.688MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-122.smt2 | 0.338s | 28.688MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-103.smt2 | 0.339s | 27.684MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-101.smt2 | 0.340s | 28.628MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-118.smt2 | 0.342s | 30.068MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-155.smt2 | 0.348s | 32.84MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-126.smt2 | 0.348s | 28.916MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-087.smt2 | 0.351s | 26.5MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-110.smt2 | 0.355s | 27.548MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-116.smt2 | 0.358s | 31.188MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-124.smt2 | 0.363s | 29.936MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-111.smt2 | 0.371s | 29.608MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-119.smt2 | 0.373s | 30.3MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-097.smt2 | 0.377s | 30.34MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-130.smt2 | 0.378s | 33.148MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-120.smt2 | 0.379s | 31.152MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-164.smt2 | 0.382s | 35.056MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-138.smt2 | 0.384s | 35.692MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-137.smt2 | 0.386s | 32.524MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-112.smt2 | 0.386s | 28.692MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-113.smt2 | 0.392s | 34.288MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-115.smt2 | 0.394s | 33.628MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-117.smt2 | 0.409s | 29.2MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-139.smt2 | 0.410s | 34.644MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-168.smt2 | 0.416s | 35.084MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-123.smt2 | 0.416s | 32.372MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-129.smt2 | 0.428s | 34.12MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-169.smt2 | 0.431s | 36.796MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-146.smt2 | 0.442s | 34.396MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-136.smt2 | 0.445s | 36.8MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-141.smt2 | 0.449s | 34.968MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-143.smt2 | 0.456s | 42.756MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-154.smt2 | 0.461s | 35.816MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-149.smt2 | 0.463s | 35.548MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-147.smt2 | 0.471s | 35.612MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-144.smt2 | 0.472s | 35.352MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-167.smt2 | 0.476s | 36.74MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-132.smt2 | 0.478s | 36.408MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-131.smt2 | 0.480s | 33.884MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-158.smt2 | 0.482s | 36.332MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-145.smt2 | 0.493s | 36.388MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-156.smt2 | 0.505s | 37.948MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-150.smt2 | 0.506s | 37.296MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-148.smt2 | 0.514s | 36.476MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-159.smt2 | 0.514s | 37.112MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-153.smt2 | 0.524s | 39.4MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-162.smt2 | 0.528s | 40.82MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-160.smt2 | 0.529s | 38.92MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-128.smt2 | 0.545s | 38.536MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-134.smt2 | 0.546s | 38.48MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-180.smt2 | 0.548s | 43.132MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-151.smt2 | 0.549s | 40.028MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-157.smt2 | 0.579s | 39.616MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-172.smt2 | 0.581s | 47.408MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-163.smt2 | 0.586s | 41.46MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-170.smt2 | 0.592s | 43.948MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-174.smt2 | 0.612s | 44.588MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-165.smt2 | 0.616s | 41.312MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-161.smt2 | 0.618s | 43.048MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-152.smt2 | 0.634s | 46.64MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-166.smt2 | 0.687s | 57.628MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-173.smt2 | 0.694s | 58.128MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-171.smt2 | 0.786s | 61.364MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-177.smt2 | 0.807s | 62.964MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-175.smt2 | 0.814s | 63.924MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-176.smt2 | 0.815s | 63.204MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-178.smt2 | 1.730s | 143.0MiB| unknown | 0 | | | |non-incremental/UFBVLIA/20210106-Schett/uso/ebso-179.smt2 | 1.749s | 143.0MiB| unknown | 0 | | |