# . * SAT 161 * UNSAT 43 * TIMEOUT 104 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: dio_no_dio_certora
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: 36a0006f595c746a98c133ba38671ab5659dacf6
Z3 branch: 
Z3 options: "-T:600 -st lp.dio=false"
Z3 inputs: inputs/certora
Z3 commit message: remove testing code in is_big_term_on_no_term

Signed-off-by: Lev Nachmanson
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |65782_cd31513fdcd15701933b_6_QF_UFNIA.smt2 | 0.101s | 20.872MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTLIA.smt2 | 0.104s | 21.492MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFDTNIA.smt2 | 0.113s | 20.816MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFNIA.smt2 | 0.150s | 23.196MiB| unsat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2 | 0.159s | 23.764MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_6_QF_UFLIA.smt2 | 0.164s | 21.784MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTLIA.smt2 | 0.164s | 23.316MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTLIA.smt2 | 0.183s | 24.52MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTNIA.smt2 | 0.185s | 22.796MiB| sat | 0 | | | |63058_aa742630eef64f949de269382c1f9035_25_UFDTNIA.smt2 | 0.204s | 23.696MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFLIA.smt2 | 0.236s | 25.42MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFDTLIA.smt2 | 0.238s | 23.268MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFLIA.smt2 | 0.240s | 23.824MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTNIA.smt2 | 0.286s | 27.412MiB| sat | 0 | | | |3106_1c933134166dbad31f79_40_QF_UFNIA.smt2 | 0.302s | 23.608MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTNIA.smt2 | 0.354s | 26.072MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFLIA.smt2 | 0.386s | 25.396MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTNIA.smt2 | 0.420s | 28.284MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFDTLIA.smt2 | 0.513s | 33.192MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTNIA.smt2 | 0.527s | 30.016MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTLIA.smt2 | 0.536s | 25.752MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFLIA.smt2 | 0.552s | 26.348MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTNIA.smt2 | 0.558s | 26.464MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTLIA.smt2 | 0.597s | 25.212MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFNIA.smt2 | 0.617s | 25.192MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTLIA.smt2 | 0.624s | 27.572MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTNIA.smt2 | 0.681s | 28.924MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFDTLIA.smt2 | 0.760s | 30.2MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFNIA.smt2 | 0.832s | 27.176MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTNIA.smt2 | 0.889s | 28.62MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFDTLIA.smt2 | 0.899s | 33.004MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTLIA.smt2 | 0.907s | 26.5MiB| unsat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFNIA.smt2 | 0.949s | 24.792MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTNIA.smt2 | 0.977s | 23.368MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTLIA.smt2 | 1.015s | 34.264MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFNIA.smt2 | 1.393s | 37.612MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFDTLIA.smt2 | 1.400s | 36.14MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTNIA.smt2 | 1.495s | 27.032MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFDTNIA.smt2 | 1.519s | 26.732MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_8_QF_UFDTNIA.smt2 | 1.549s | 25.016MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFLIA.smt2 | 1.647s | 33.992MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_43_QF_UFDTNIA.smt2 | 1.670s | 27.256MiB| unsat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFNIA.smt2 | 1.725s | 30.876MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTNIA.smt2 | 1.729s | 26.56MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFDTLIA.smt2 | 1.791s | 55.104MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTNIA.smt2 | 1.844s | 23.26MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFNIA.smt2 | 1.933s | 27.284MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2 | 2.091s | 35.764MiB| unsat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFLIA.smt2 | 2.167s | 31.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTNIA.smt2 | 2.174s | 41.544MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFLIA.smt2 | 2.255s | 39.744MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_58_QF_UFNIA.smt2 | 2.273s | 30.06MiB| sat | 0 | | | |11775_ad46e5b8db4748c51973_42_QF_UFDTLIA.smt2 | 2.322s | 36.048MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTNIA.smt2 | 2.368s | 55.68MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTLIA.smt2 | 2.699s | 50.752MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTLIA.smt2 | 2.707s | 57.592MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTNIA.smt2 | 3.124s | 57.388MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTLIA.smt2 | 3.431s | 47.96MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTLIA.smt2 | 3.465s | 50.528MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFNIA.smt2 | 3.465s | 45.568MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTLIA.smt2 | 3.520s | 37.62MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFDTNIA.smt2 | 3.633s | 58.576MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFNIA.smt2 | 4.039s | 23.152MiB| unsat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTNIA.smt2 | 4.236s | 46.488MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTLIA.smt2 | 4.254s | 31.544MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTNIA.smt2 | 4.285s | 43.528MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFDTLIA.smt2 | 4.458s | 57.568MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTLIA.smt2 | 4.508s | 65.524MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFNIA.smt2 | 4.564s | 26.872MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFDTLIA.smt2 | 4.586s | 28.5MiB| sat | 0 | | | |41958_45c688a4814eb926c254_60_QF_UFLIA.smt2 | 4.642s | 49.664MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFDTNIA.smt2 | 4.805s | 35.236MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTLIA.smt2 | 4.947s | 45.248MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTNIA.smt2 | 5.297s | 62.2MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTLIA.smt2 | 5.334s | 52.04MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTLIA.smt2 | 5.746s | 104.0MiB| unsat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFNIA.smt2 | 5.891s | 41.764MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFDTNIA.smt2 | 5.958s | 102.0MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFDTLIA.smt2 | 6.046s | 30.008MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFLIA.smt2 | 6.252s | 32.896MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTNIA.smt2 | 6.678s | 78.752MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTLIA.smt2 | 7.057s | 66.272MiB| unsat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFDTLIA.smt2 | 7.262s | 42.688MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFNIA.smt2 | 7.414s | 31.708MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFLIA.smt2 | 7.522s | 45.772MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFNIA.smt2 | 7.691s | 62.74MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFDTNIA.smt2 | 8.256s | 51.108MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFDTLIA.smt2 | 8.400s | 29.628MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTNIA.smt2 | 9.046s | 95.824MiB| sat | 0 | | | |65782_cd31513fdcd15701933b_7_QF_UFDTNIA.smt2 | 9.084s | 26.416MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFNIA.smt2 | 9.314s | 32.252MiB| unsat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFLIA.smt2 | 9.406s | 37.572MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFNIA.smt2 | 9.526s | 28.464MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFDTLIA.smt2 | 9.534s | 84.716MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFLIA.smt2 | 9.589s | 59.064MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFDTNIA.smt2 | 9.868s | 44.108MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFDTNIA.smt2 | 10.096s | 48.4MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTNIA.smt2 | 10.119s | 72.484MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTLIA.smt2 | 11.244s | 122.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_34_QF_UFDTNIA.smt2 | 11.526s | 26.544MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFLIA.smt2 | 12.111s | 72.348MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFDTNIA.smt2 | 12.367s | 53.424MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFNIA.smt2 | 13.602s | 25.792MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFNIA.smt2 | 13.922s | 43.976MiB| sat | 0 | | | |72658_63104dadde9c6026353f_70_QF_UFLIA.smt2 | 14.412s | 73.204MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFDTLIA.smt2 | 14.625s | 81.568MiB| sat | 0 | | | |41958_45c688a4814eb926c254_59_QF_UFLIA.smt2 | 15.314s | 85.628MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTNIA.smt2 | 15.347s | 74.796MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFNIA.smt2 | 16.447s | 91.864MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_48_QF_UFNIA.smt2 | 16.581s | 38.764MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFNIA.smt2 | 16.602s | 65.268MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFDTLIA.smt2 | 17.206s | 68.156MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFLIA.smt2 | 18.147s | 84.152MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFDTLIA.smt2 | 18.541s | 63.772MiB| unsat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFNIA.smt2 | 19.751s | 90.148MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTLIA.smt2 | 19.989s | 83.584MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTLIA.smt2 | 20.867s | 123.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFNIA.smt2 | 21.786s | 71.288MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTLIA.smt2 | 22.002s | 229.0MiB| unsat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFDTNIA.smt2 | 22.388s | 142.0MiB| unsat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFDTNIA.smt2 | 22.402s | 54.364MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFLIA.smt2 | 22.703s | 533.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTLIA.smt2 | 23.704s | 51.252MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTLIA.smt2 | 24.031s | 126.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_18_QF_UFLIA.smt2 | 24.227s | 87.68MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFDTNIA.smt2 | 24.584s | 57.296MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFLIA.smt2 | 24.782s | 60.964MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTLIA.smt2 | 25.143s | 76.028MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFLIA.smt2 | 25.766s | 90.148MiB| sat | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFLIA.smt2 | 26.807s | 46.476MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFDTNIA.smt2 | 27.820s | 133.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_14_QF_UFLIA.smt2 | 28.020s | 98.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTNIA.smt2 | 28.994s | 52.156MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFDTLIA.smt2 | 29.083s | 80.468MiB| sat | 0 | | | |17512_5c1021b0faa6b6e1791b_21_QF_UFDTNIA.smt2 | 32.795s | 36.608MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFNIA.smt2 | 32.982s | 254.0MiB| sat | 0 | | | |72771_f9d228efc97cf1458e38_64_QF_UFLIA.smt2 | 35.348s | 47.192MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTLIA.smt2 | 36.007s | 80.336MiB| sat | 0 | | | |3106_1c933134166dbad31f79_41_QF_UFNIA.smt2 | 36.292s | 50.5MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFLIA.smt2 | 42.607s | 161.0MiB| sat | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTNIA.smt2 | 44.382s | 54.256MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTNIA.smt2 | 44.708s | 46.148MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFLIA.smt2 | 48.250s | 117.0MiB| sat | 0 | | | |44289_e5a2e5c780236919ee6a_17_QF_UFNIA.smt2 | 50.200s | 108.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_13_QF_UFNIA.smt2 | 51.072s | 147.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTLIA.smt2 | 53.588s | 148.0MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTNIA.smt2 | 55.174s | 101.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFDTNIA.smt2 | 55.284s | 130.0MiB| unsat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFDTNIA.smt2 | 58.735s | 99.752MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFNIA.smt2 | 62.694s | 156.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFNIA.smt2 | 64.297s | 50.736MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTNIA.smt2 | 65.074s | 195.0MiB| sat | 0 | | | |39657_2866defdd1f2434b69ab_47_QF_UFLIA.smt2 | 66.244s | 46.56MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTNIA.smt2 | 67.429s | 93.168MiB| unsat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTNIA.smt2 | 68.592s | 51.292MiB| unsat | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFLIA.smt2 | 69.343s | 193.0MiB| sat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFLIA.smt2 | 69.766s | 284.0MiB| unsat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFNIA.smt2 | 72.344s | 245.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTLIA.smt2 | 72.442s | 50.412MiB| sat | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2 | 73.454s | 194.0MiB| unsat | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTNIA.smt2 | 74.889s | 37.428MiB| unsat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFNIA.smt2 | 82.750s | 114.0MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFNIA.smt2 | 84.757s | 158.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTLIA.smt2 | 92.808s | 159.0MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFNIA.smt2 | 93.911s | 236.0MiB| sat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFNIA.smt2 | 94.200s | 143.0MiB| sat | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFNIA.smt2 | 99.443s | 131.0MiB| sat | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFDTNIA.smt2 | 99.598s | 100.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTNIA.smt2 | 108.129s | 164.0MiB| sat | 0 | | | |52759_af0c476fe3b544b9a8507f3e42472c43_12_QF_UFLIA.smt2 | 109.858s | 148.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFLIA.smt2 | 111.393s | 149.0MiB| sat | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFDTLIA.smt2 | 112.814s | 143.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFLIA.smt2 | 115.999s | 79.596MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_23_QF_UFNIA.smt2 | 120.252s | 189.0MiB| sat | 0 | | | |63058_64ab9a7ef7b6c3492507_22_QF_UFNIA.smt2 | 120.381s | 186.0MiB| sat | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFLIA.smt2 | 127.855s | 1714.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFLIA.smt2 | 128.232s | 122.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFLIA.smt2 | 143.743s | 193.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFNIA.smt2 | 148.076s | 417.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_27_QF_UFLIA.smt2 | 148.178s | 460.0MiB| unsat | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTLIA.smt2 | 150.695s | 117.0MiB| sat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFDTNIA.smt2 | 151.977s | 140.0MiB| unsat | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFDTNIA.smt2 | 153.377s | 123.0MiB| sat | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFDTNIA.smt2 | 160.284s | 34.508MiB| unsat | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFNIA.smt2 | 161.259s | 445.0MiB| sat | 0 | | | |63058_55d6bef5390186355f11_26_QF_UFNIA.smt2 | 167.863s | 216.0MiB| sat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFNIA.smt2 | 195.553s | 155.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTNIA.smt2 | 208.404s | 235.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_46_QF_UFNIA.smt2 | 211.529s | 115.0MiB| sat | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTLIA.smt2 | 215.093s | 25.772MiB| unsat | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTLIA.smt2 | 249.816s | 419.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFLIA.smt2 | 251.780s | 476.0MiB| unsat | 0 | | | |30078_f817a923328f75af7e60_28_QF_UFNIA.smt2 | 261.523s | 432.0MiB| unsat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFDTLIA.smt2 | 267.096s | 247.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_44_QF_UFNIA.smt2 | 297.515s | 134.0MiB| sat | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFNIA.smt2 | 305.479s | 352.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_0_UFLIA.smt2 | 327.351s | 189.0MiB| sat | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFNIA.smt2 | 328.214s | 596.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFDTNIA.smt2 | 329.625s | 110.0MiB| sat | 0 | | | |39657_1c7158801cd59dc13f05_45_QF_UFNIA.smt2 | 383.693s | 120.0MiB| sat | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFNIA.smt2 | 388.331s | 318.0MiB| sat | 0 | | | |52759_b3ecd2335fd16ec2eee2_9_UFNIA.smt2 | 440.949s | 138.0MiB| sat | 0 | | | |83314_a702bf8b823398c9e37a_3_UFDTLIA.smt2 | 523.125s | 852.0MiB| unsat | 0 | | | |3106_1c933134166dbad31f79_39_QF_UFDTNIA.smt2 | 577.501s | 182.0MiB| sat | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFLIA.smt2 | 596.592s | 313.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFLIA.smt2 | 598.419s | 396.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFLIA.smt2 | 598.490s | 157.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFNIA.smt2 | 598.802s | 303.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFLIA.smt2 | 599.036s | 1151.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTNIA.smt2 | 599.192s | 186.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTNIA.smt2 | 599.329s | 276.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFDTLIA.smt2 | 599.336s | 266.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFNIA.smt2 | 599.339s | 85.784MiB| timeout | 0 | | | |44289_b077fc096b3d41cba49f8628caff7fa5_16_QF_UFLIA.smt2 | 599.342s | 212.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFDTLIA.smt2 | 599.344s | 700.0MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_11_QF_UFLIA.smt2 | 599.369s | 384.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTNIA.smt2 | 599.383s | 99.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFLIA.smt2 | 599.395s | 1345.0MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFLIA.smt2 | 599.398s | 277.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFNIA.smt2 | 599.425s | 33.94MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFNIA.smt2 | 599.426s | 123.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_61_QF_UFDTNIA.smt2 | 599.430s | 57.496MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFLIA.smt2 | 599.437s | 712.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFLIA.smt2 | 599.445s | 765.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTNIA.smt2 | 599.446s | 243.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFLIA.smt2 | 599.471s | 273.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_56_QF_UFLIA.smt2 | 599.474s | 228.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFDTLIA.smt2 | 599.477s | 1216.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFNIA.smt2 | 599.497s | 962.0MiB| timeout | 0 | | | |63058_64ab9a7ef7b6c3492507_24_QF_UFNIA.smt2 | 599.503s | 319.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFDTLIA.smt2 | 599.509s | 342.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFNIA.smt2 | 599.509s | 108.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFDTNIA.smt2 | 599.522s | 63.352MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFLIA.smt2 | 599.527s | 628.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFLIA.smt2 | 599.552s | 384.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2 | 599.553s | 57.848MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFDTLIA.smt2 | 599.561s | 920.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTNIA.smt2 | 599.566s | 92.528MiB| timeout | 0 | | | |93493_5990a6bf5f2740164f77_50_QF_UFLIA.smt2 | 599.568s | 345.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_1_UFDTLIA.smt2 | 599.569s | 702.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTNIA.smt2 | 599.577s | 142.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFNIA.smt2 | 599.577s | 75.44MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTNIA.smt2 | 599.577s | 94.336MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFLIA.smt2 | 599.582s | 399.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFNIA.smt2 | 599.586s | 682.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFNIA.smt2 | 599.594s | 358.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTLIA.smt2 | 599.599s | 342.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFDTLIA.smt2 | 599.603s | 223.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFNIA.smt2 | 599.605s | 632.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFLIA.smt2 | 599.607s | 2063.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_65_QF_UFDTLIA.smt2 | 599.611s | 1420.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFLIA.smt2 | 599.612s | 426.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_30_QF_UFDTLIA.smt2 | 599.617s | 516.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFDTLIA.smt2 | 599.626s | 398.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTLIA.smt2 | 599.631s | 32.644MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFDTLIA.smt2 | 599.636s | 332.0MiB| timeout | 0 | | | |93493_1fdb6cc8eb9c4363b5838af9eb8c7f1f_53_QF_UFLIA.smt2 | 599.639s | 155.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFNIA.smt2 | 599.640s | 316.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_36_QF_UFDTNIA.smt2 | 599.641s | 94.572MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_75_QF_UFLIA.smt2 | 599.649s | 1248.0MiB| timeout | 0 | | | |3106_afb7bc55417e43d7a22790c3576f04fc_37_QF_UFLIA.smt2 | 599.651s | 166.0MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFNIA.smt2 | 599.653s | 90.704MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_73_QF_UFLIA.smt2 | 599.656s | 749.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFLIA.smt2 | 599.657s | 300.0MiB| timeout | 0 | | | |93493_798593962ee29ad45ac8_52_QF_UFDTLIA.smt2 | 599.663s | 221.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_31_QF_UFLIA.smt2 | 599.675s | 217.0MiB| timeout | 0 | | | |3106_1c933134166dbad31f79_38_QF_UFDTNIA.smt2 | 599.676s | 470.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFLIA.smt2 | 599.686s | 157.0MiB| timeout | 0 | | | |93493_27ab26d56d60426da02e50231269b6ff_51_QF_UFLIA.smt2 | 599.688s | 258.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFNIA.smt2 | 599.689s | 358.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTLIA.smt2 | 599.695s | 1173.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_29_QF_UFLIA.smt2 | 599.698s | 542.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFDTNIA.smt2 | 599.700s | 189.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_63_QF_UFNIA.smt2 | 599.704s | 44.248MiB| timeout | 0 | | | |52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFLIA.smt2 | 599.705s | 437.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_67_QF_UFDTNIA.smt2 | 599.708s | 114.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTNIA.smt2 | 599.715s | 275.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFNIA.smt2 | 599.717s | 99.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_72_QF_UFNIA.smt2 | 599.717s | 572.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_66_QF_UFNIA.smt2 | 599.723s | 87.332MiB| timeout | 0 | | | |65782_cd31513fdcd15701933b_5_QF_UFDTLIA.smt2 | 599.744s | 271.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFDTLIA.smt2 | 599.744s | 340.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_33_QF_UFDTLIA.smt2 | 599.748s | 485.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTLIA.smt2 | 599.755s | 233.0MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFDTNIA.smt2 | 599.762s | 254.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_2_UFNIA.smt2 | 599.770s | 243.0MiB| timeout | 0 | | | |44289_4066055e0f64d96da11a_15_QF_UFLIA.smt2 | 599.771s | 636.0MiB| timeout | 0 | | | |41958_32933c5a1384696720a2_62_QF_UFNIA.smt2 | 599.773s | 49.856MiB| timeout | 0 | | | |72658_63104dadde9c6026353f_71_QF_UFNIA.smt2 | 599.776s | 51.124MiB| timeout | 0 | | | |93493_4ea6163ed03941199c785278ccc42812_49_QF_UFLIA.smt2 | 599.777s | 278.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFNIA.smt2 | 599.804s | 130.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFDTLIA.smt2 | 599.806s | 790.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFNIA.smt2 | 599.810s | 640.0MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_19_QF_UFLIA.smt2 | 599.811s | 194.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFDTLIA.smt2 | 599.813s | 2141.0MiB| timeout | 0 | | | |940_590f27b1c3c800d3243e_32_QF_UFDTLIA.smt2 | 599.823s | 631.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_3_UFNIA.smt2 | 599.827s | 118.0MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_68_QF_UFLIA.smt2 | 599.832s | 955.0MiB| timeout | 0 | | | |83314_a702bf8b823398c9e37a_4_UFNIA.smt2 | 599.836s | 249.0MiB| timeout | 0 | | | |44788_1965f0d6d94d5d8054ba_35_QF_UFDTNIA.smt2 | 599.839s | 60.32MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFDTLIA.smt2 | 599.846s | 766.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_57_QF_UFDTNIA.smt2 | 599.851s | 33.536MiB| timeout | 0 | | | |25959_5dee2e2f6ef44465a2bea4b085818948_69_QF_UFLIA.smt2 | 599.866s | 975.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_74_QF_UFLIA.smt2 | 599.866s | 582.0MiB| timeout | 0 | | | |38347_092cc73601c78e45f4f9_55_QF_UFDTNIA.smt2 | 599.868s | 25.356MiB| timeout | 0 | | | |17512_5c1021b0faa6b6e1791b_20_QF_UFLIA.smt2 | 599.869s | 585.0MiB| timeout | 0 | | | |66603_accdadf23a1cf70ae043_76_QF_UFNIA.smt2 | 599.893s | 1545.0MiB| timeout | 0 | | | |38347_525a1ca0331f2bcbf520_54_QF_UFLIA.smt2 | 599.922s | 2218.0MiB| timeout | 0 | | |