# . * SAT 272 * UNSAT 279 * TIMEOUT 0 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_AX.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_AX.tar.zst-down
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_AX.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_002.cvc.smt2 | 0.025s | 20.02MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00006_001.cvc.smt2 | 0.026s | 20.152MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00005_007.cvc.smt2 | 0.029s | 20.16MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_007.cvc.smt2 | 0.030s | 19.956MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_001.cvc.smt2 | 0.031s | 20.36MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00030_003.cvc.smt2 | 0.031s | 20.676MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00040_008.cvc.smt2 | 0.033s | 21.096MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_005.cvc.smt2 | 0.034s | 20.128MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_006.cvc.smt2 | 0.034s | 20.636MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_005.cvc.smt2 | 0.035s | 20.892MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00010_001.cvc.smt2 | 0.035s | 20.092MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00007_001.cvc.smt2 | 0.035s | 20.336MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00002_001.cvc.smt2 | 0.035s | 20.244MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00006_003.cvc.smt2 | 0.036s | 19.968MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00009_005.cvc.smt2 | 0.036s | 20.292MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00040_009.cvc.smt2 | 0.036s | 21.004MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_sf_ai_00007_001.cvc.smt2 | 0.036s | 20.324MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00006_001.cvc.smt2 | 0.036s | 20.356MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00004_002.cvc.smt2 | 0.038s | 20.076MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00060_002.cvc.smt2 | 0.038s | 21.74MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00050_003.cvc.smt2 | 0.038s | 21.2MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00008_001.cvc.smt2 | 0.038s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00006_001.cvc.smt2 | 0.038s | 20.148MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_009.cvc.smt2 | 0.039s | 20.624MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00009_008.cvc.smt2 | 0.040s | 20.36MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00009_001.cvc.smt2 | 0.041s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00004_008.cvc.smt2 | 0.043s | 19.856MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00008_004.cvc.smt2 | 0.044s | 20.012MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_009.cvc.smt2 | 0.044s | 20.336MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00001_001.cvc.smt2 | 0.045s | 19.832MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00010_001.cvc.smt2 | 0.045s | 20.616MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_007.cvc.smt2 | 0.046s | 20.172MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00020_004.cvc.smt2 | 0.046s | 20.372MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00050_006.cvc.smt2 | 0.046s | 21.7MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00010_001.cvc.smt2 | 0.046s | 20.104MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00005_001.cvc.smt2 | 0.046s | 20.068MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00006_001.cvc.smt2 | 0.046s | 20.376MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_009.cvc.smt2 | 0.047s | 20.356MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_001.cvc.smt2 | 0.047s | 20.268MiB| unsat | 0 | | | |non-incremental/QF_AX/cvc/read5.smt2 | 0.047s | 20.352MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00060_004.cvc.smt2 | 0.047s | 21.604MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00040_001.cvc.smt2 | 0.047s | 21.108MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00003_001.cvc.smt2 | 0.047s | 19.916MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_004.cvc.smt2 | 0.048s | 20.048MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00004_006.cvc.smt2 | 0.049s | 19.896MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00006_002.cvc.smt2 | 0.049s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_008.cvc.smt2 | 0.049s | 20.104MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00020_003.cvc.smt2 | 0.049s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00005_001.cvc.smt2 | 0.049s | 20.292MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_009.cvc.smt2 | 0.050s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00010_004.cvc.smt2 | 0.050s | 20.164MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_007.cvc.smt2 | 0.050s | 20.152MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00005_001.cvc.smt2 | 0.050s | 20.144MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00008_001.cvc.smt2 | 0.050s | 20.208MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_003.cvc.smt2 | 0.051s | 20.368MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00002_002.cvc.smt2 | 0.051s | 19.748MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00006_006.cvc.smt2 | 0.051s | 20.144MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00008_008.cvc.smt2 | 0.051s | 20.372MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_003.cvc.smt2 | 0.051s | 19.42MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00004_001.cvc.smt2 | 0.051s | 20.124MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_002.cvc.smt2 | 0.052s | 20.752MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_005.cvc.smt2 | 0.052s | 19.892MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00010_001.cvc.smt2 | 0.052s | 20.608MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_007.cvc.smt2 | 0.053s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_008.cvc.smt2 | 0.054s | 20.236MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_003.cvc.smt2 | 0.054s | 19.912MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_008.cvc.smt2 | 0.054s | 19.972MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_002.cvc.smt2 | 0.054s | 19.96MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_009.cvc.smt2 | 0.054s | 20.88MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_nf_ai_00009_001.cvc.smt2 | 0.054s | 20.408MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_009.cvc.smt2 | 0.055s | 20.348MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_008.cvc.smt2 | 0.055s | 20.856MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_005.cvc.smt2 | 0.056s | 21.676MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00005_001.cvc.smt2 | 0.056s | 20.12MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00002_006.cvc.smt2 | 0.057s | 19.828MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_002.cvc.smt2 | 0.057s | 20.18MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_009.cvc.smt2 | 0.057s | 20.06MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_004.cvc.smt2 | 0.058s | 20.136MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_009.cvc.smt2 | 0.058s | 20.12MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_009.cvc.smt2 | 0.058s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_003.cvc.smt2 | 0.058s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_007.cvc.smt2 | 0.058s | 21.116MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00040_002.cvc.smt2 | 0.058s | 20.84MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_004.cvc.smt2 | 0.059s | 20.288MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_008.cvc.smt2 | 0.059s | 20.28MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_005.cvc.smt2 | 0.059s | 20.52MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00002_006.cvc.smt2 | 0.059s | 19.904MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00002_005.cvc.smt2 | 0.059s | 19.932MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_005.cvc.smt2 | 0.059s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_001.cvc.smt2 | 0.059s | 19.94MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00008_001.cvc.smt2 | 0.059s | 20.196MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00007_004.cvc.smt2 | 0.060s | 20.164MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00010_006.cvc.smt2 | 0.060s | 20.212MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00003_006.cvc.smt2 | 0.060s | 19.88MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_003.cvc.smt2 | 0.060s | 19.528MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00007_009.cvc.smt2 | 0.060s | 20.356MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_002.cvc.smt2 | 0.060s | 21.112MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_009.cvc.smt2 | 0.060s | 21.64MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_008.cvc.smt2 | 0.060s | 20.388MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_001.cvc.smt2 | 0.061s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_006.cvc.smt2 | 0.061s | 20.628MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_006.cvc.smt2 | 0.062s | 20.128MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_003.cvc.smt2 | 0.062s | 20.132MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00002_005.cvc.smt2 | 0.062s | 19.956MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00008_002.cvc.smt2 | 0.062s | 20.264MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_006.cvc.smt2 | 0.062s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_007.cvc.smt2 | 0.062s | 20.572MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00060_009.cvc.smt2 | 0.062s | 21.848MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_001.cvc.smt2 | 0.062s | 20.336MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00006_003.cvc.smt2 | 0.063s | 20.136MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_006.cvc.smt2 | 0.063s | 20.176MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_003.cvc.smt2 | 0.063s | 20.344MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00007_001.cvc.smt2 | 0.063s | 20.24MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00005_007.cvc.smt2 | 0.063s | 19.988MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00050_008.cvc.smt2 | 0.063s | 21.784MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_007.cvc.smt2 | 0.063s | 20.028MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_009.cvc.smt2 | 0.064s | 19.976MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_003.cvc.smt2 | 0.064s | 20.4MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_003.cvc.smt2 | 0.064s | 20.104MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_004.cvc.smt2 | 0.064s | 21.1MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_002.cvc.smt2 | 0.064s | 22.296MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00020_002.cvc.smt2 | 0.064s | 20.528MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00009_001.cvc.smt2 | 0.064s | 20.404MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00002_001.cvc.smt2 | 0.064s | 19.944MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_004.cvc.smt2 | 0.065s | 20.12MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00006_009.cvc.smt2 | 0.065s | 20.392MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_007.cvc.smt2 | 0.065s | 20.732MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00002_005.cvc.smt2 | 0.066s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_nf_ai_00003_001.cvc.smt2 | 0.066s | 19.872MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_007.cvc.smt2 | 0.067s | 20.628MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_004.cvc.smt2 | 0.067s | 19.92MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_004.cvc.smt2 | 0.067s | 20.596MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00003_006.cvc.smt2 | 0.067s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00030_001.cvc.smt2 | 0.067s | 21.1MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00020_001.cvc.smt2 | 0.067s | 20.36MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00005_003.cvc.smt2 | 0.068s | 19.848MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_004.cvc.smt2 | 0.068s | 20.508MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_006.cvc.smt2 | 0.068s | 20.284MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_007.cvc.smt2 | 0.068s | 20.368MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_006.cvc.smt2 | 0.068s | 19.936MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00004_005.cvc.smt2 | 0.068s | 20.132MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_009.cvc.smt2 | 0.068s | 20.404MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_001.cvc.smt2 | 0.068s | 20.1MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00060_006.cvc.smt2 | 0.068s | 21.736MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_007.cvc.smt2 | 0.069s | 20.256MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_001.cvc.smt2 | 0.069s | 20.056MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00002_003.cvc.smt2 | 0.069s | 20.404MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_008.cvc.smt2 | 0.069s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_003.cvc.smt2 | 0.070s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00009_007.cvc.smt2 | 0.070s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00009_002.cvc.smt2 | 0.070s | 20.212MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_005.cvc.smt2 | 0.070s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_004.cvc.smt2 | 0.070s | 20.072MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00040_005.cvc.smt2 | 0.070s | 20.836MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_006.cvc.smt2 | 0.071s | 20.328MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_005.cvc.smt2 | 0.071s | 20.592MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00010_003.cvc.smt2 | 0.071s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_003.cvc.smt2 | 0.071s | 20.524MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_001.cvc.smt2 | 0.072s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_003.cvc.smt2 | 0.072s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_004.cvc.smt2 | 0.072s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_007.cvc.smt2 | 0.072s | 19.932MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_009.cvc.smt2 | 0.072s | 20.132MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00040_001.cvc.smt2 | 0.072s | 21.068MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_005.cvc.smt2 | 0.072s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_002.cvc.smt2 | 0.073s | 20.136MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_001.cvc.smt2 | 0.073s | 20.38MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_004.cvc.smt2 | 0.073s | 20.316MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_008.cvc.smt2 | 0.073s | 20.104MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_004.cvc.smt2 | 0.073s | 20.604MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_001.cvc.smt2 | 0.073s | 20.396MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_005.cvc.smt2 | 0.073s | 20.86MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_003.cvc.smt2 | 0.073s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_005.cvc.smt2 | 0.073s | 20.368MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00050_008.cvc.smt2 | 0.073s | 21.372MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00004_001.cvc.smt2 | 0.073s | 20.132MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00003_005.cvc.smt2 | 0.074s | 19.844MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_008.cvc.smt2 | 0.074s | 20.3MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_008.cvc.smt2 | 0.074s | 20.272MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_007.cvc.smt2 | 0.074s | 20.324MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_006.cvc.smt2 | 0.074s | 20.404MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00002_001.cvc.smt2 | 0.074s | 19.584MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_009.cvc.smt2 | 0.074s | 20.12MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00007_001.cvc.smt2 | 0.074s | 20.404MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_008.cvc.smt2 | 0.075s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_004.cvc.smt2 | 0.075s | 19.892MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00006_001.cvc.smt2 | 0.075s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00003_005.cvc.smt2 | 0.075s | 20.1MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00007_002.cvc.smt2 | 0.075s | 20.42MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_001.cvc.smt2 | 0.075s | 20.024MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00002_006.cvc.smt2 | 0.075s | 19.972MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_sf_ai_00002_001.cvc.smt2 | 0.075s | 19.848MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_005.cvc.smt2 | 0.076s | 20.12MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00003_001.cvc.smt2 | 0.076s | 19.992MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_002.cvc.smt2 | 0.076s | 20.1MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00006_008.cvc.smt2 | 0.077s | 20.228MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_006.cvc.smt2 | 0.077s | 20.128MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_009.cvc.smt2 | 0.077s | 20.22MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_005.cvc.smt2 | 0.077s | 20.2MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_005.cvc.smt2 | 0.077s | 20.104MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_002.cvc.smt2 | 0.077s | 20.62MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_008.cvc.smt2 | 0.077s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_007.cvc.smt2 | 0.077s | 20.636MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00003_006.cvc.smt2 | 0.077s | 20.48MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00020_003.cvc.smt2 | 0.077s | 20.376MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_009.cvc.smt2 | 0.077s | 20.092MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_nf_ai_00007_001.cvc.smt2 | 0.077s | 20.16MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_009.cvc.smt2 | 0.078s | 20.352MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_001.cvc.smt2 | 0.078s | 19.924MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_004.cvc.smt2 | 0.078s | 20.4MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00005_006.cvc.smt2 | 0.078s | 19.772MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_006.cvc.smt2 | 0.078s | 19.82MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_009.cvc.smt2 | 0.078s | 20.48MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t2_np_sf_ai_00001_001.cvc.smt2 | 0.078s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_007.cvc.smt2 | 0.079s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_004.cvc.smt2 | 0.079s | 19.864MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_006.cvc.smt2 | 0.079s | 19.9MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_001.cvc.smt2 | 0.079s | 19.86MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00009_001.cvc.smt2 | 0.079s | 20.192MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_001.cvc.smt2 | 0.080s | 20.452MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_004.cvc.smt2 | 0.080s | 20.168MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00002_002.cvc.smt2 | 0.080s | 20.336MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00050_007.cvc.smt2 | 0.080s | 21.108MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00010_002.cvc.smt2 | 0.080s | 20.012MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_008.cvc.smt2 | 0.080s | 20.152MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_sf_ai_00004_001.cvc.smt2 | 0.080s | 19.896MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t1_np_nf_ai_00002_001.cvc.smt2 | 0.080s | 19.924MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_t3_np_sf_ai_00003_001.cvc.smt2 | 0.080s | 19.884MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00007_008.cvc.smt2 | 0.081s | 20.256MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_004.cvc.smt2 | 0.081s | 20.356MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_008.cvc.smt2 | 0.081s | 20.352MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00002_009.cvc.smt2 | 0.081s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_003.cvc.smt2 | 0.081s | 19.6MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00010_001.cvc.smt2 | 0.081s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_005.cvc.smt2 | 0.081s | 21.116MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_002.cvc.smt2 | 0.082s | 20.104MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00004_001.cvc.smt2 | 0.082s | 19.808MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00002_009.cvc.smt2 | 0.082s | 20.144MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_006.cvc.smt2 | 0.082s | 20.34MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00008_008.cvc.smt2 | 0.082s | 20.396MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_008.cvc.smt2 | 0.082s | 20.128MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_002.cvc.smt2 | 0.082s | 21.676MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_006.cvc.smt2 | 0.082s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00003_002.cvc.smt2 | 0.083s | 20.564MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00008_003.cvc.smt2 | 0.083s | 19.4MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00008_007.cvc.smt2 | 0.083s | 20.368MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00040_002.cvc.smt2 | 0.083s | 20.984MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_006.cvc.smt2 | 0.084s | 20.276MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00040_006.cvc.smt2 | 0.084s | 20.816MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_006.cvc.smt2 | 0.085s | 19.968MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00010_006.cvc.smt2 | 0.085s | 20.316MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00006_002.cvc.smt2 | 0.085s | 20.036MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_004.cvc.smt2 | 0.085s | 22.476MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_007.cvc.smt2 | 0.085s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_009.cvc.smt2 | 0.085s | 20.396MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00008_005.cvc.smt2 | 0.086s | 20.16MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00008_001.cvc.smt2 | 0.086s | 20.328MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_007.cvc.smt2 | 0.086s | 20.116MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_008.cvc.smt2 | 0.086s | 20.24MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00004_004.cvc.smt2 | 0.087s | 20.068MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00002_001.cvc.smt2 | 0.087s | 19.836MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_001.cvc.smt2 | 0.087s | 21.124MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_006.cvc.smt2 | 0.088s | 20.268MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_004.cvc.smt2 | 0.088s | 21.156MiB| unsat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t1_np_sf_ai_00008_001.cvc.smt2 | 0.088s | 20.572MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00008_001.cvc.smt2 | 0.089s | 20.112MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00060_001.cvc.smt2 | 0.089s | 21.616MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_008.cvc.smt2 | 0.089s | 21.096MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00003_001.cvc.smt2 | 0.090s | 20.004MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_007.cvc.smt2 | 0.090s | 20.016MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00007_007.cvc.smt2 | 0.090s | 20.184MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_sf_ai_00003_001.cvc.smt2 | 0.090s | 19.892MiB| sat | 0 | | | |non-incremental/QF_AX/storeinv/storeinv_invalid_t3_np_nf_ai_00004_001.cvc.smt2 | 0.090s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_007.cvc.smt2 | 0.091s | 20.336MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_002.cvc.smt2 | 0.091s | 20.364MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00005_004.cvc.smt2 | 0.091s | 19.948MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00040_004.cvc.smt2 | 0.091s | 21.24MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00020_002.cvc.smt2 | 0.091s | 20.368MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_008.cvc.smt2 | 0.091s | 20.74MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_003.cvc.smt2 | 0.092s | 20.152MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_004.cvc.smt2 | 0.093s | 20.452MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00003_004.cvc.smt2 | 0.093s | 19.98MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_009.cvc.smt2 | 0.093s | 20.284MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_001.cvc.smt2 | 0.093s | 20.368MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_005.cvc.smt2 | 0.093s | 20.18MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_001.cvc.smt2 | 0.093s | 19.996MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_003.cvc.smt2 | 0.093s | 20.088MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00003_007.cvc.smt2 | 0.093s | 19.872MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_006.cvc.smt2 | 0.093s | 21.528MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00040_003.cvc.smt2 | 0.093s | 20.952MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00005_009.cvc.smt2 | 0.094s | 20.004MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00007_005.cvc.smt2 | 0.094s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_007.cvc.smt2 | 0.094s | 20.608MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00004_001.cvc.smt2 | 0.094s | 19.796MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_008.cvc.smt2 | 0.094s | 19.752MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00060_009.cvc.smt2 | 0.094s | 21.852MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_007.cvc.smt2 | 0.095s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_006.cvc.smt2 | 0.095s | 20.368MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_002.cvc.smt2 | 0.095s | 20.256MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_005.cvc.smt2 | 0.095s | 20.18MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00006_009.cvc.smt2 | 0.095s | 19.98MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00006_004.cvc.smt2 | 0.095s | 19.884MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_003.cvc.smt2 | 0.095s | 19.904MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_004.cvc.smt2 | 0.095s | 19.96MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_004.cvc.smt2 | 0.095s | 19.904MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00002_009.cvc.smt2 | 0.095s | 19.94MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_003.cvc.smt2 | 0.096s | 20.156MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_009.cvc.smt2 | 0.096s | 20.048MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_002.cvc.smt2 | 0.096s | 20.092MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00009_001.cvc.smt2 | 0.096s | 20.896MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00009_003.cvc.smt2 | 0.097s | 20.512MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_005.cvc.smt2 | 0.097s | 20.052MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00010_005.cvc.smt2 | 0.097s | 20.388MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00003_002.cvc.smt2 | 0.097s | 19.956MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_006.cvc.smt2 | 0.097s | 20.264MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_005.cvc.smt2 | 0.097s | 21.628MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_007.cvc.smt2 | 0.098s | 20.512MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00060_009.cvc.smt2 | 0.098s | 22.576MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_004.cvc.smt2 | 0.099s | 20.072MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00007_002.cvc.smt2 | 0.099s | 20.268MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00002_002.cvc.smt2 | 0.099s | 19.856MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00030_003.cvc.smt2 | 0.099s | 20.36MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_003.cvc.smt2 | 0.099s | 21.2MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_009.cvc.smt2 | 0.100s | 20.144MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00003_004.cvc.smt2 | 0.101s | 20.076MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00004_005.cvc.smt2 | 0.101s | 20.04MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00050_006.cvc.smt2 | 0.101s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_003.cvc.smt2 | 0.102s | 20.44MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_007.cvc.smt2 | 0.102s | 20.18MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00007_002.cvc.smt2 | 0.102s | 20.356MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00030_004.cvc.smt2 | 0.102s | 20.4MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00003_005.cvc.smt2 | 0.103s | 19.932MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00005_009.cvc.smt2 | 0.103s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00008_002.cvc.smt2 | 0.103s | 20.256MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_006.cvc.smt2 | 0.103s | 19.888MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00004_002.cvc.smt2 | 0.104s | 19.888MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00004_002.cvc.smt2 | 0.104s | 20.004MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00005_002.cvc.smt2 | 0.104s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00040_006.cvc.smt2 | 0.104s | 20.844MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_008.cvc.smt2 | 0.104s | 22.312MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00009_005.cvc.smt2 | 0.105s | 20.136MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00004_009.cvc.smt2 | 0.105s | 20.096MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00008_005.cvc.smt2 | 0.105s | 20.028MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00007_007.cvc.smt2 | 0.107s | 20.124MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_009.cvc.smt2 | 0.107s | 20.376MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00007_007.cvc.smt2 | 0.107s | 20.348MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00020_005.cvc.smt2 | 0.107s | 20.104MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_002.cvc.smt2 | 0.107s | 20.572MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00010_008.cvc.smt2 | 0.107s | 20.152MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00007_005.cvc.smt2 | 0.108s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_001.cvc.smt2 | 0.108s | 19.508MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_007.cvc.smt2 | 0.108s | 20.772MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_002.cvc.smt2 | 0.108s | 20.152MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_002.cvc.smt2 | 0.108s | 21.288MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00006_002.cvc.smt2 | 0.109s | 20.372MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00008_003.cvc.smt2 | 0.109s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00005_007.cvc.smt2 | 0.110s | 20.356MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_002.cvc.smt2 | 0.111s | 20.3MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_008.cvc.smt2 | 0.111s | 20.38MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_008.cvc.smt2 | 0.112s | 20.604MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_009.cvc.smt2 | 0.112s | 20.796MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_006.cvc.smt2 | 0.112s | 21.104MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_003.cvc.smt2 | 0.113s | 19.856MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_001.cvc.smt2 | 0.113s | 19.488MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_004.cvc.smt2 | 0.113s | 20.14MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00004_007.cvc.smt2 | 0.113s | 19.844MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00003_008.cvc.smt2 | 0.113s | 19.864MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_001.cvc.smt2 | 0.114s | 20.104MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00004_005.cvc.smt2 | 0.114s | 20.064MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00006_003.cvc.smt2 | 0.114s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_008.cvc.smt2 | 0.114s | 19.928MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00005_008.cvc.smt2 | 0.114s | 19.848MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00005_008.cvc.smt2 | 0.114s | 19.892MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_009.cvc.smt2 | 0.114s | 20.532MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00004_008.cvc.smt2 | 0.114s | 20.004MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00050_004.cvc.smt2 | 0.114s | 21.464MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_009.cvc.smt2 | 0.114s | 22.24MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00002_002.cvc.smt2 | 0.115s | 19.852MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00007_005.cvc.smt2 | 0.115s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00007_008.cvc.smt2 | 0.115s | 20.1MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_001.cvc.smt2 | 0.115s | 20.12MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00005_005.cvc.smt2 | 0.115s | 20.124MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00020_002.cvc.smt2 | 0.115s | 20.244MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_002.cvc.smt2 | 0.116s | 20.316MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00003_008.cvc.smt2 | 0.116s | 19.9MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00005_001.cvc.smt2 | 0.116s | 19.892MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_006.cvc.smt2 | 0.117s | 20.348MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00050_005.cvc.smt2 | 0.117s | 21.252MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_009.cvc.smt2 | 0.118s | 20.372MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00007_003.cvc.smt2 | 0.118s | 20.112MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_008.cvc.smt2 | 0.118s | 20.36MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00006_005.cvc.smt2 | 0.118s | 20.144MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00009_001.cvc.smt2 | 0.118s | 20.636MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_005.cvc.smt2 | 0.118s | 20.104MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00010_004.cvc.smt2 | 0.118s | 19.888MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_005.cvc.smt2 | 0.119s | 20.112MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_009.cvc.smt2 | 0.120s | 20.552MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00008_006.cvc.smt2 | 0.120s | 20.868MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00060_005.cvc.smt2 | 0.120s | 22.324MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_001.cvc.smt2 | 0.120s | 21.552MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00009_008.cvc.smt2 | 0.121s | 20.396MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_007.cvc.smt2 | 0.122s | 21.668MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00009_006.cvc.smt2 | 0.123s | 20.624MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00050_009.cvc.smt2 | 0.124s | 21.028MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00008_001.cvc.smt2 | 0.125s | 20.38MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_001.cvc.smt2 | 0.127s | 21.208MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00009_009.cvc.smt2 | 0.131s | 20.632MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00010_002.cvc.smt2 | 0.132s | 20.652MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_006.cvc.smt2 | 0.132s | 20.584MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00010_004.cvc.smt2 | 0.133s | 20.628MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00050_004.cvc.smt2 | 0.133s | 21.616MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_008.cvc.smt2 | 0.136s | 20.48MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00009_003.cvc.smt2 | 0.138s | 20.568MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_003.cvc.smt2 | 0.139s | 20.836MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_008.cvc.smt2 | 0.141s | 20.624MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_006.cvc.smt2 | 0.141s | 20.124MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00020_005.cvc.smt2 | 0.141s | 20.1MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_001.cvc.smt2 | 0.143s | 20.62MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_002.cvc.smt2 | 0.144s | 20.432MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00020_006.cvc.smt2 | 0.144s | 20.164MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_007.cvc.smt2 | 0.145s | 20.588MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_005.cvc.smt2 | 0.145s | 20.188MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00040_003.cvc.smt2 | 0.146s | 20.776MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_sf_ai_00010_008.cvc.smt2 | 0.147s | 20.392MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_006.cvc.smt2 | 0.147s | 21.116MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_008.cvc.smt2 | 0.147s | 20.18MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00060_003.cvc.smt2 | 0.148s | 21.812MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00030_008.cvc.smt2 | 0.149s | 20.404MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00030_007.cvc.smt2 | 0.149s | 20.62MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00050_004.cvc.smt2 | 0.150s | 21.084MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_001.cvc.smt2 | 0.151s | 21.104MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00060_005.cvc.smt2 | 0.151s | 21.692MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00010_004.cvc.smt2 | 0.152s | 20.792MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_007.cvc.smt2 | 0.152s | 21.104MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_007.cvc.smt2 | 0.153s | 20.4MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00008_008.cvc.smt2 | 0.154s | 20.408MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_008.cvc.smt2 | 0.154s | 21.12MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_007.cvc.smt2 | 0.155s | 20.148MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_003.cvc.smt2 | 0.155s | 20.564MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00060_001.cvc.smt2 | 0.155s | 21.712MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00050_008.cvc.smt2 | 0.156s | 21.84MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00010_003.cvc.smt2 | 0.157s | 20.36MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00006_006.cvc.smt2 | 0.159s | 19.86MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00010_005.cvc.smt2 | 0.159s | 19.884MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_001.cvc.smt2 | 0.159s | 20.036MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00002_008.cvc.smt2 | 0.160s | 19.908MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_009.cvc.smt2 | 0.160s | 20.476MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00060_003.cvc.smt2 | 0.160s | 21.672MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00010_004.cvc.smt2 | 0.160s | 20.156MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00010_002.cvc.smt2 | 0.160s | 20.004MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00008_006.cvc.smt2 | 0.161s | 20.156MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_008.cvc.smt2 | 0.161s | 20.116MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00010_006.cvc.smt2 | 0.161s | 20.096MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00020_003.cvc.smt2 | 0.161s | 20.14MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_009.cvc.smt2 | 0.161s | 20.536MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_008.cvc.smt2 | 0.161s | 20.616MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00020_005.cvc.smt2 | 0.161s | 20.392MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_sf_ai_00010_003.cvc.smt2 | 0.162s | 20.388MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00006_007.cvc.smt2 | 0.162s | 20.184MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00010_002.cvc.smt2 | 0.162s | 20.116MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_006.cvc.smt2 | 0.162s | 20.4MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00020_009.cvc.smt2 | 0.162s | 20.228MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_006.cvc.smt2 | 0.163s | 20.112MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00006_005.cvc.smt2 | 0.163s | 20.084MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00060_008.cvc.smt2 | 0.163s | 22.604MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_004.cvc.smt2 | 0.163s | 20.44MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00005_005.cvc.smt2 | 0.164s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00003_001.cvc.smt2 | 0.164s | 19.868MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00010_008.cvc.smt2 | 0.164s | 20.664MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00060_001.cvc.smt2 | 0.164s | 22.384MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00010_008.cvc.smt2 | 0.164s | 19.888MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_005.cvc.smt2 | 0.164s | 20.644MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_004.cvc.smt2 | 0.165s | 20.72MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00010_006.cvc.smt2 | 0.165s | 20.108MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00030_004.cvc.smt2 | 0.165s | 20.568MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00020_007.cvc.smt2 | 0.165s | 20.152MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_002.cvc.smt2 | 0.165s | 20.836MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00030_007.cvc.smt2 | 0.165s | 20.36MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00010_005.cvc.smt2 | 0.165s | 20.404MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00020_004.cvc.smt2 | 0.165s | 20.448MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00030_001.cvc.smt2 | 0.166s | 20.664MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_001.cvc.smt2 | 0.166s | 20.864MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00030_009.cvc.smt2 | 0.166s | 20.616MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00040_004.cvc.smt2 | 0.166s | 21.128MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00020_004.cvc.smt2 | 0.166s | 20.108MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00030_002.cvc.smt2 | 0.167s | 20.94MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00020_002.cvc.smt2 | 0.167s | 20.204MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00020_001.cvc.smt2 | 0.167s | 20.308MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00030_007.cvc.smt2 | 0.167s | 20.728MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00030_005.cvc.smt2 | 0.167s | 20.68MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00030_006.cvc.smt2 | 0.167s | 20.364MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00010_005.cvc.smt2 | 0.168s | 20.396MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00006_007.cvc.smt2 | 0.168s | 19.988MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_001.cvc.smt2 | 0.168s | 20.412MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00050_003.cvc.smt2 | 0.168s | 21.516MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00030_004.cvc.smt2 | 0.168s | 20.716MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00040_003.cvc.smt2 | 0.168s | 21.132MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00040_009.cvc.smt2 | 0.169s | 21.088MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_002.cvc.smt2 | 0.169s | 21.212MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00040_007.cvc.smt2 | 0.169s | 21.06MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00050_005.cvc.smt2 | 0.169s | 21.112MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00030_002.cvc.smt2 | 0.169s | 20.58MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00040_005.cvc.smt2 | 0.169s | 21.3MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00030_006.cvc.smt2 | 0.169s | 20.616MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00040_009.cvc.smt2 | 0.170s | 21.004MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_002.cvc.smt2 | 0.170s | 21.644MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00040_004.cvc.smt2 | 0.171s | 20.924MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00040_007.cvc.smt2 | 0.171s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_sf_ai_00050_008.cvc.smt2 | 0.172s | 21.292MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00050_003.cvc.smt2 | 0.172s | 21.896MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00030_006.cvc.smt2 | 0.172s | 20.772MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00040_006.cvc.smt2 | 0.172s | 21.184MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_sf_ai_00040_003.cvc.smt2 | 0.172s | 21.104MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00060_007.cvc.smt2 | 0.172s | 21.728MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00050_001.cvc.smt2 | 0.172s | 21.648MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_nf_ai_00060_004.cvc.smt2 | 0.172s | 21.624MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00009_003.cvc.smt2 | 0.173s | 20.612MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00040_007.cvc.smt2 | 0.173s | 20.768MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_sf_ai_00050_009.cvc.smt2 | 0.173s | 21.1MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00050_002.cvc.smt2 | 0.174s | 21.224MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t1_np_nf_ai_00060_005.cvc.smt2 | 0.174s | 21.588MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t1_np_nf_ai_00010_004.cvc.smt2 | 0.175s | 20.416MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t3_np_sf_ai_00060_008.cvc.smt2 | 0.175s | 21.72MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_sf_ai_00050_009.cvc.smt2 | 0.176s | 21.584MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_001.cvc.smt2 | 0.178s | 22.344MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00060_004.cvc.smt2 | 0.178s | 22.352MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00060_006.cvc.smt2 | 0.179s | 22.244MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00050_007.cvc.smt2 | 0.179s | 21.716MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t1_np_nf_ai_00060_005.cvc.smt2 | 0.179s | 22.296MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_t2_np_nf_ai_00060_008.cvc.smt2 | 0.179s | 21.764MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_sf_ai_00060_003.cvc.smt2 | 0.180s | 22.34MiB| sat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t3_np_nf_ai_00060_003.cvc.smt2 | 0.180s | 22.632MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_invalid_t3_np_nf_ai_00010_009.cvc.smt2 | 0.182s | 20.228MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00009_006.cvc.smt2 | 0.183s | 21.028MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_001.cvc.smt2 | 0.183s | 20.388MiB| unsat | 0 | | | |non-incremental/QF_AX/storecomm/storecomm_invalid_t2_np_nf_ai_00060_007.cvc.smt2 | 0.184s | 22.256MiB| sat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00008_009.cvc.smt2 | 0.185s | 20.508MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_sf_ai_00010_005.cvc.smt2 | 0.196s | 20.7MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00009_006.cvc.smt2 | 0.223s | 20.972MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00010_001.cvc.smt2 | 0.249s | 21.384MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_sf_ai_00010_003.cvc.smt2 | 0.255s | 21.136MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00009_004.cvc.smt2 | 0.259s | 21.38MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00010_003.cvc.smt2 | 0.268s | 20.96MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00009_004.cvc.smt2 | 0.281s | 21.4MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_007.cvc.smt2 | 0.285s | 21.388MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_nf_ai_00010_007.cvc.smt2 | 0.295s | 21.212MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00010_009.cvc.smt2 | 0.405s | 22.08MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t1_np_nf_ai_00010_001.cvc.smt2 | 0.451s | 21.644MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_009.cvc.smt2 | 0.559s | 21.676MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t3_np_sf_ai_00010_002.cvc.smt2 | 1.685s | 23.244MiB| unsat | 0 | | | |non-incremental/QF_AX/swap/swap_t2_np_nf_ai_00010_002.cvc.smt2 | 2.400s | 23.44MiB| unsat | 0 | | |