%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : LAT360+2 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 11:48:37 AM UTC 2026 % Result : Timeout 295.75s 42.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LAT360+2 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.38 % Computer : n007.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Sun Sep 27 14:58:27 UTC 2026 % 0.11/0.39 % CPUTime : % 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.42 Running first-order model finding % 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.94/4.58 % (1551161)Will run a generic schedule for satisfiability detection. % 25.94/4.58 % (1551169)dis+10_1_sil=32000:sp=arity:random_seed=1184122689:i=103:fgj=on_2995 on theBenchmark for (2995ds/103Mi) % 25.94/4.58 % (1551167)% WARNING: option uhcvi not known. % 25.94/4.58 % (1551166)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3675208074_2995 on theBenchmark for (2995ds/0Mi) % 25.94/4.58 % (1551167)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=266164178:i=135531:add=off:rawr=on_2995 on theBenchmark for (2995ds/135531Mi) % 25.94/4.58 % (1551168)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3998747824:i=88024:add=on:rawr=on_2995 on theBenchmark for (2995ds/88024Mi) % 25.94/4.58 % (1551170)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1466407306:i=116_2995 on theBenchmark for (2995ds/116Mi) % 25.94/4.58 % (1551171)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3349153107:i=131_2995 on theBenchmark for (2995ds/131Mi) % 25.94/4.58 % (1551172)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3802499782:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2995 on theBenchmark for (2995ds/159Mi) % 25.94/4.58 % (1551169)Instruction limit reached! % 25.94/4.58 % (1551169)------------------------------ % 25.94/4.58 % (1551169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.94/4.58 % (1551169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.58 % (1551169)CaDiCaL version: 2.1.3 % 25.94/4.58 % (1551169)Termination reason: Instruction limit % 25.94/4.58 % (1551169)Termination phase: Unused predicate definition removal % 25.94/4.58 % (1551169)Time elapsed: 0.047 s % 25.94/4.58 % (1551169)Peak memory usage: 31 MB % 25.94/4.58 % (1551169)Instructions burned: 103 (million) % 25.94/4.58 % (1551180)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3302139965:i=714:nm=2_2994 on theBenchmark for (2994ds/714Mi) % 25.94/4.58 % (1551170)Instruction limit reached! % 25.94/4.58 % (1551170)------------------------------ % 25.94/4.58 % (1551170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.94/4.58 % (1551170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.58 % (1551170)CaDiCaL version: 2.1.3 % 25.94/4.58 % (1551170)Termination reason: Instruction limit % 25.94/4.58 % (1551170)Termination phase: Preprocessing 2 % 25.94/4.58 % (1551170)Time elapsed: 0.099 s % 25.94/4.58 % (1551170)Peak memory usage: 34 MB % 25.94/4.58 % (1551170)Instructions burned: 116 (million) % 25.94/4.58 % (1551171)Instruction limit reached! % 25.94/4.58 % (1551171)------------------------------ % 25.94/4.58 % (1551171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.94/4.58 % (1551171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.58 % (1551171)CaDiCaL version: 2.1.3 % 25.94/4.58 % (1551171)Termination reason: Instruction limit % 25.94/4.58 % (1551171)Termination phase: Preprocessing 2 % 25.94/4.58 % (1551171)Time elapsed: 0.106 s % 25.94/4.58 % (1551171)Peak memory usage: 34 MB % 25.94/4.58 % (1551171)Instructions burned: 131 (million) % 25.94/4.58 % (1551182)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4279322345:i=131:bd=preordered:fsd=on_2993 on theBenchmark for (2993ds/131Mi) % 25.94/4.58 % (1551172)Instruction limit reached! % 25.94/4.58 % (1551172)------------------------------ % 25.94/4.58 % (1551172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.94/4.58 % (1551172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.58 % (1551172)CaDiCaL version: 2.1.3 % 25.94/4.58 % (1551172)Termination reason: Instruction limit % 25.94/4.58 % (1551172)Termination phase: Preprocessing 2 % 25.94/4.58 % (1551172)Time elapsed: 0.127 s % 25.94/4.58 % (1551172)Peak memory usage: 40 MB % 25.94/4.58 % (1551172)Instructions burned: 159 (million) % 25.94/4.58 % (1551183)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3772021839:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2993 on theBenchmark for (2993ds/684Mi) % 25.94/4.58 % (1551186)ott-21_1_sil=16000:fs=off:random_seed=3414842365:i=180:av=off:fsr=off_2993 on theBenchmark for (2993ds/180Mi) % 25.94/4.58 % (1551182)Instruction limit reached! % 25.94/4.58 % (1551182)------------------------------ % 25.94/4.58 % (1551182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.94/4.58 % (1551182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.89/7.09 % (1551182)CaDiCaL version: 2.1.3 % 43.89/7.09 % (1551182)Termination reason: Instruction limit % 43.89/7.09 % (1551182)Termination phase: Preprocessing 2 % 43.89/7.09 % (1551182)Time elapsed: 0.101 s % 43.89/7.09 % (1551182)Peak memory usage: 34 MB % 43.89/7.09 % (1551182)Instructions burned: 131 (million) % 43.89/7.09 % (1551188)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4119340346:i=477:bd=all_2992 on theBenchmark for (2992ds/477Mi) % 43.89/7.09 % (1551186)Instruction limit reached! % 43.89/7.09 % (1551186)------------------------------ % 43.89/7.09 % (1551186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.89/7.09 % (1551186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.89/7.09 % (1551186)CaDiCaL version: 2.1.3 % 43.89/7.09 % (1551186)Termination reason: Instruction limit % 43.89/7.09 % (1551186)Termination phase: Naming % 43.89/7.09 % (1551186)Time elapsed: 0.141 s % 43.89/7.09 % (1551186)Peak memory usage: 40 MB % 43.89/7.09 % (1551186)Instructions burned: 180 (million) % 43.89/7.09 % (1551190)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3558699112:fmbsr=1.3:i=865:ins=25_2991 on theBenchmark for (2991ds/865Mi) % 43.89/7.09 % (1551180)Instruction limit reached! % 43.89/7.09 % (1551180)------------------------------ % 43.89/7.09 % (1551180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.89/7.09 % (1551180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.89/7.09 % (1551180)CaDiCaL version: 2.1.3 % 43.89/7.09 % (1551180)Termination reason: Instruction limit % 43.89/7.09 % (1551180)Termination phase: Property scanning % 43.89/7.09 % (1551180)Time elapsed: 0.268 s % 43.89/7.09 % (1551180)Peak memory usage: 67 MB % 43.89/7.09 % (1551180)Instructions burned: 718 (million) % 43.89/7.09 % (1551192)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=44542475:i=1179_2991 on theBenchmark for (2991ds/1179Mi) % 43.89/7.09 % (1551183)Instruction limit reached! % 43.89/7.09 % (1551183)------------------------------ % 43.89/7.09 % (1551183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.89/7.09 % (1551183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.89/7.09 % (1551183)CaDiCaL version: 2.1.3 % 43.89/7.09 % (1551183)Termination reason: Instruction limit % 43.89/7.09 % (1551183)Termination phase: NewCNF % 43.89/7.09 % (1551183)Time elapsed: 0.409 s % 43.89/7.09 % (1551183)Peak memory usage: 54 MB % 43.89/7.09 % (1551183)Instructions burned: 685 (million) % 43.89/7.09 % (1551188)Instruction limit reached! % 43.89/7.09 % (1551188)------------------------------ % 43.89/7.09 % (1551188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.89/7.09 % (1551188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.89/7.09 % (1551188)CaDiCaL version: 2.1.3 % 43.89/7.09 % (1551188)Termination reason: Instruction limit % 43.89/7.09 % (1551188)Termination phase: Preprocessing 3 % 43.89/7.09 % (1551188)Time elapsed: 0.311 s % 43.89/7.09 % (1551188)Peak memory usage: 51 MB % 43.89/7.09 % (1551188)Instructions burned: 478 (million) % 43.89/7.09 % (1551194)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=656431762:i=889:ins=1_2989 on theBenchmark for (2989ds/889Mi) % 43.89/7.09 % (1551196)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2323837735:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi) % 43.89/7.09 % (1551192)Instruction limit reached! % 43.89/7.09 % (1551192)------------------------------ % 43.89/7.09 % (1551192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.89/7.09 % (1551192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.89/7.09 % (1551192)CaDiCaL version: 2.1.3 % 43.89/7.09 % (1551192)Termination reason: Instruction limit % 43.89/7.09 % (1551192)Termination phase: Property scanning % 43.89/7.09 % (1551192)Time elapsed: 0.360 s % 43.89/7.09 % (1551192)Peak memory usage: 62 MB % 43.89/7.09 % (1551192)Instructions burned: 1181 (million) % 43.89/7.09 % (1551198)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=968127452:i=879:kws=inv_precedence:fsr=off_2987 on theBenchmark for (2987ds/879Mi) % 43.89/7.09 % (1551190)Instruction limit reached! % 43.89/7.09 % (1551190)------------------------------ % 43.89/7.09 % (1551190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.89/7.09 % (1551190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551190)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551190)Termination reason: Instruction limit % 76.35/11.61 % (1551190)Termination phase: Function definition elimination % 76.35/11.61 % (1551190)Time elapsed: 0.480 s % 76.35/11.61 % (1551190)Peak memory usage: 58 MB % 76.35/11.61 % (1551190)Instructions burned: 867 (million) % 76.35/11.61 % (1551200)fmb+10_1_sil=64000:random_seed=1666089727:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi) % 76.35/11.61 % (1551198)Instruction limit reached! % 76.35/11.61 % (1551198)------------------------------ % 76.35/11.61 % (1551198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.35/11.61 % (1551198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551198)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551198)Termination reason: Instruction limit % 76.35/11.61 % (1551198)Termination phase: NewCNF % 76.35/11.61 % (1551198)Time elapsed: 0.268 s % 76.35/11.61 % (1551198)Peak memory usage: 62 MB % 76.35/11.61 % (1551198)Instructions burned: 883 (million) % 76.35/11.61 % (1551196)Instruction limit reached! % 76.35/11.61 % (1551196)------------------------------ % 76.35/11.61 % (1551196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.35/11.61 % (1551196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551196)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551196)Termination reason: Instruction limit % 76.35/11.61 % (1551196)Termination phase: NewCNF % 76.35/11.61 % (1551196)Time elapsed: 0.412 s % 76.35/11.61 % (1551196)Peak memory usage: 55 MB % 76.35/11.61 % (1551196)Instructions burned: 693 (million) % 76.35/11.61 % (1551202)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2300425075:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi) % 76.35/11.61 % (1551204)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1206388085:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi) % 76.35/11.61 % (1551194)Instruction limit reached! % 76.35/11.61 % (1551194)------------------------------ % 76.35/11.61 % (1551194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.35/11.61 % (1551194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551194)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551194)Termination reason: Instruction limit % 76.35/11.61 % (1551194)Termination phase: Function definition elimination % 76.35/11.61 % (1551194)Time elapsed: 0.494 s % 76.35/11.61 % (1551194)Peak memory usage: 58 MB % 76.35/11.61 % (1551194)Instructions burned: 889 (million) % 76.35/11.61 % (1551206)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4135629990:i=5131_2984 on theBenchmark for (2984ds/5131Mi) % 76.35/11.61 % (1551204)Instruction limit reached! % 76.35/11.61 % (1551204)------------------------------ % 76.35/11.61 % (1551204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.35/11.61 % (1551204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551204)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551204)Termination reason: Instruction limit % 76.35/11.61 % (1551204)Termination phase: Function definition elimination % 76.35/11.61 % (1551204)Time elapsed: 0.510 s % 76.35/11.61 % (1551204)Peak memory usage: 59 MB % 76.35/11.61 % (1551204)Instructions burned: 921 (million) % 76.35/11.61 % (1551208)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1620102585:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi) % 76.35/11.61 % (1551208)Instruction limit reached! % 76.35/11.61 % (1551208)------------------------------ % 76.35/11.61 % (1551208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.35/11.61 % (1551208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551208)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551208)Termination reason: Instruction limit % 76.35/11.61 % (1551208)Termination phase: Saturation % 76.35/11.61 % (1551208)Time elapsed: 0.747 s % 76.35/11.61 % (1551208)Peak memory usage: 60 MB % 76.35/11.61 % (1551208)Instructions burned: 1473 (million) % 76.35/11.61 % (1551210)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1866912968:i=6324_2971 on theBenchmark for (2971ds/6324Mi) % 76.35/11.61 % (1551202)Instruction limit reached! % 76.35/11.61 % (1551202)------------------------------ % 76.35/11.61 % (1551202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 76.35/11.61 % (1551202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.35/11.61 % (1551202)CaDiCaL version: 2.1.3 % 76.35/11.61 % (1551202)Termination reason: Instruction limit % 125.35/18.55 % (1551202)Termination phase: Finite model building preprocessing % 125.35/18.55 % (1551202)Time elapsed: 2.631 s % 125.35/18.55 % (1551202)Peak memory usage: 143 MB % 125.35/18.55 % (1551202)Instructions burned: 9517 (million) % 125.35/18.55 % (1551212)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3676908088:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi) % 125.35/18.55 % (1551206)Instruction limit reached! % 125.35/18.55 % (1551206)------------------------------ % 125.35/18.55 % (1551206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.35/18.55 % (1551206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.35/18.55 % (1551206)CaDiCaL version: 2.1.3 % 125.35/18.55 % (1551206)Termination reason: Instruction limit % 125.35/18.55 % (1551206)Termination phase: Saturation % 125.35/18.55 % (1551206)Time elapsed: 2.787 s % 125.35/18.55 % (1551206)Peak memory usage: 109 MB % 125.35/18.55 % (1551206)Instructions burned: 5132 (million) % 125.35/18.55 % (1551214)ott-2_1_sil=16000:newcnf=on:random_seed=1017376305:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi) % 125.35/18.55 % (1551212)Instruction limit reached! % 125.35/18.55 % (1551212)------------------------------ % 125.35/18.55 % (1551212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.35/18.55 % (1551212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.35/18.55 % (1551212)CaDiCaL version: 2.1.3 % 125.35/18.55 % (1551212)Termination reason: Instruction limit % 125.35/18.55 % (1551212)Termination phase: Finite model building preprocessing % 125.35/18.55 % (1551212)Time elapsed: 0.603 s % 125.35/18.55 % (1551212)Peak memory usage: 83 MB % 125.35/18.55 % (1551212)Instructions burned: 2175 (million) % 125.35/18.55 % (1551216)ott+10_1_sil=32000:tgt=ground:random_seed=236815512:i=5114:av=off_2952 on theBenchmark for (2952ds/5114Mi) % 125.35/18.55 % (1551214)Instruction limit reached! % 125.35/18.55 % (1551214)------------------------------ % 125.35/18.55 % (1551214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.35/18.55 % (1551214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.35/18.55 % (1551214)CaDiCaL version: 2.1.3 % 125.35/18.55 % (1551214)Termination reason: Instruction limit % 125.35/18.55 % (1551214)Termination phase: NewCNF % 125.35/18.55 % (1551214)Time elapsed: 0.470 s % 125.35/18.55 % (1551214)Peak memory usage: 60 MB % 125.35/18.55 % (1551214)Instructions burned: 870 (million) % 125.35/18.55 % (1551218)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=386777193:i=54282_2950 on theBenchmark for (2950ds/54282Mi) % 125.35/18.55 % (1551210)Instruction limit reached! % 125.35/18.55 % (1551210)------------------------------ % 125.35/18.55 % (1551210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.35/18.55 % (1551210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.35/18.55 % (1551210)CaDiCaL version: 2.1.3 % 125.35/18.55 % (1551210)Termination reason: Instruction limit % 125.35/18.55 % (1551210)Termination phase: Finite model building preprocessing % 125.35/18.55 % (1551210)Time elapsed: 3.236 s % 125.35/18.55 % (1551210)Peak memory usage: 116 MB % 125.35/18.55 % (1551210)Instructions burned: 6324 (million) % 125.35/18.55 % (1551220)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1612030805:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi) % 125.35/18.55 % (1551216)Instruction limit reached! % 125.35/18.55 % (1551216)------------------------------ % 125.35/18.55 % (1551216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.35/18.55 % (1551216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.35/18.55 % (1551216)CaDiCaL version: 2.1.3 % 125.35/18.55 % (1551216)Termination reason: Instruction limit % 125.35/18.55 % (1551216)Termination phase: Saturation % 125.35/18.55 % (1551216)Time elapsed: 1.572 s % 125.35/18.55 % (1551216)Peak memory usage: 119 MB % 125.35/18.55 % (1551216)Instructions burned: 5116 (million) % 125.35/18.55 % (1551222)dis+21_1_sil=32000:sas=cadical:random_seed=645412528:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi) % 125.35/18.55 % Detected minimum model sizes of [5] % 125.35/18.55 % Detected maximum model sizes of [max] % 125.35/18.55 % (1551200)Cannot represent all propositional literals internally % 125.35/18.55 % (1551200)Refutation not found, incomplete strategy % 125.35/18.55 % (1551200)------------------------------ % 125.35/18.55 % (1551200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 125.35/18.55 % (1551200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.35/18.55 % (1551200)CaDiCaL version: 2.1.3 % 177.15/25.89 % (1551200)Termination reason: Refutation not found, incomplete strategy % 177.15/25.89 % (1551200)Time elapsed: 5.318 s % 177.15/25.89 % (1551200)Peak memory usage: 184 MB % 177.15/25.89 % (1551200)Instructions burned: 10334 (million) % 177.15/25.89 % (1551200)------------------------------ % 177.15/25.89 % (1551200)------------------------------ % 177.15/25.89 % (1551224)ott+11_1_sil=16000:gs=on:random_seed=466436098:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi) % 177.15/25.89 % (1551222)Instruction limit reached! % 177.15/25.89 % (1551222)------------------------------ % 177.15/25.89 % (1551222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.89 % (1551222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.89 % (1551222)CaDiCaL version: 2.1.3 % 177.15/25.89 % (1551222)Termination reason: Instruction limit % 177.15/25.89 % (1551222)Termination phase: Saturation % 177.15/25.89 % (1551222)Time elapsed: 1.044 s % 177.15/25.89 % (1551222)Peak memory usage: 88 MB % 177.15/25.89 % (1551222)Instructions burned: 3777 (million) % 177.15/25.89 % (1551226)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1065316255:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi) % 177.15/25.89 % (1551220)Instruction limit reached! % 177.15/25.89 % (1551220)------------------------------ % 177.15/25.89 % (1551220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.89 % (1551220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.89 % (1551220)CaDiCaL version: 2.1.3 % 177.15/25.89 % (1551220)Termination reason: Instruction limit % 177.15/25.89 % (1551220)Termination phase: Saturation % 177.15/25.89 % (1551220)Time elapsed: 1.811 s % 177.15/25.89 % (1551220)Peak memory usage: 84 MB % 177.15/25.89 % (1551220)Instructions burned: 3512 (million) % 177.15/25.89 % (1551228)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1616699549:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi) % 177.15/25.89 % (1551224)Instruction limit reached! % 177.15/25.89 % (1551224)------------------------------ % 177.15/25.89 % (1551224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.89 % (1551224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.89 % (1551224)CaDiCaL version: 2.1.3 % 177.15/25.89 % (1551224)Termination reason: Instruction limit % 177.15/25.89 % (1551224)Termination phase: Saturation % 177.15/25.89 % (1551224)Time elapsed: 1.291 s % 177.15/25.89 % (1551224)Peak memory usage: 85 MB % 177.15/25.89 % (1551224)Instructions burned: 2252 (million) % 177.15/25.89 % (1551230)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1187680317:i=29340_2919 on theBenchmark for (2919ds/29340Mi) % 177.15/25.89 % Detected minimum model sizes of [5] % 177.15/25.89 % Detected maximum model sizes of [max] % 177.15/25.89 % (1551166)Cannot represent all propositional literals internally % 177.15/25.89 % (1551166)Refutation not found, incomplete strategy % 177.15/25.89 % (1551166)------------------------------ % 177.15/25.89 % (1551166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.89 % (1551166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.89 % (1551166)CaDiCaL version: 2.1.3 % 177.15/25.89 % (1551166)Termination reason: Refutation not found, incomplete strategy % 177.15/25.89 % (1551166)Time elapsed: 8.345 s % 177.15/25.89 % (1551166)Peak memory usage: 244 MB % 177.15/25.89 % (1551166)Instructions burned: 16334 (million) % 177.15/25.89 % (1551166)------------------------------ % 177.15/25.89 % (1551166)------------------------------ % 177.15/25.89 % (1551232)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3124534201:i=5211_2910 on theBenchmark for (2910ds/5211Mi) % 177.15/25.89 % (1551228)Instruction limit reached! % 177.15/25.89 % (1551228)------------------------------ % 177.15/25.89 % (1551228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 177.15/25.89 % (1551228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.15/25.89 % (1551228)CaDiCaL version: 2.1.3 % 177.15/25.89 % (1551228)Termination reason: Instruction limit % 177.15/25.89 % (1551228)Termination phase: Saturation % 177.15/25.89 % (1551228)Time elapsed: 2.282 s % 177.15/25.89 % (1551228)Peak memory usage: 93 MB % 177.15/25.89 % (1551228)Instructions burned: 4591 (million) % 177.15/25.89 % (1551234)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3205517647:i=5497:nm=2_2897 on theBenchmark for (2897ds/5497Mi) % 177.15/25.89 % (1551232)Instruction limit reached! % 177.15/25.89 % (1551232)------------------------------ % 245.38/35.43 % (1551232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.38/35.43 % (1551232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.38/35.43 % (1551232)CaDiCaL version: 2.1.3 % 245.38/35.43 % (1551232)Termination reason: Instruction limit % 245.38/35.43 % (1551232)Termination phase: Saturation % 245.38/35.43 % (1551232)Time elapsed: 2.236 s % 245.38/35.43 % (1551232)Peak memory usage: 105 MB % 245.38/35.43 % (1551232)Instructions burned: 5213 (million) % 245.38/35.43 % (1551236)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1198640397:fmbsr=2:i=46332_2888 on theBenchmark for (2888ds/46332Mi) % 245.38/35.43 % Detected minimum model sizes of [5] % 245.38/35.43 % Detected maximum model sizes of [max] % 245.38/35.43 % (1551226)Cannot represent all propositional literals internally % 245.38/35.43 % (1551226)Refutation not found, incomplete strategy % 245.38/35.43 % (1551226)------------------------------ % 245.38/35.43 % (1551226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.38/35.43 % (1551226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.38/35.43 % (1551226)CaDiCaL version: 2.1.3 % 245.38/35.43 % (1551226)Termination reason: Refutation not found, incomplete strategy % 245.38/35.43 % (1551226)Time elapsed: 4.181 s % 245.38/35.43 % (1551226)Peak memory usage: 205 MB % 245.38/35.43 % (1551226)Instructions burned: 15633 (million) % 245.38/35.43 % (1551226)------------------------------ % 245.38/35.43 % (1551226)------------------------------ % 245.38/35.43 % (1551238)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2756139455:i=14071_2883 on theBenchmark for (2883ds/14071Mi) % 245.38/35.43 % (1551234)Instruction limit reached! % 245.38/35.43 % (1551234)------------------------------ % 245.38/35.43 % (1551234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.38/35.43 % (1551234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.38/35.43 % (1551234)CaDiCaL version: 2.1.3 % 245.38/35.43 % (1551234)Termination reason: Instruction limit % 245.38/35.43 % (1551234)Termination phase: Finite model building preprocessing % 245.38/35.43 % (1551234)Time elapsed: 2.989 s % 245.38/35.43 % (1551234)Peak memory usage: 123 MB % 245.38/35.43 % (1551234)Instructions burned: 5498 (million) % 245.38/35.43 % Detected minimum model sizes of [5] % 245.38/35.43 % Detected maximum model sizes of [max] % 245.38/35.43 % (1551218)Cannot represent all propositional literals internally % 245.38/35.43 % (1551218)Refutation not found, incomplete strategy % 245.38/35.43 % (1551218)------------------------------ % 245.38/35.43 % (1551218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.38/35.43 % (1551218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.38/35.43 % (1551218)CaDiCaL version: 2.1.3 % 245.38/35.43 % (1551218)Termination reason: Refutation not found, incomplete strategy % 245.38/35.43 % (1551218)Time elapsed: 8.362 s % 245.38/35.43 % (1551218)Peak memory usage: 244 MB % 245.38/35.43 % (1551218)Instructions burned: 16338 (million) % 245.38/35.43 % (1551240)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2704296367:i=22565:add=on:rawr=on_2867 on theBenchmark for (2867ds/22565Mi) % 245.38/35.43 % (1551218)------------------------------ % 245.38/35.43 % (1551218)------------------------------ % 245.38/35.43 % (1551242)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1197488099:i=8173:av=off_2866 on theBenchmark for (2866ds/8173Mi) % 245.38/35.43 % (1551238)Instruction limit reached! % 245.38/35.43 % (1551238)------------------------------ % 245.38/35.43 % (1551238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.38/35.43 % (1551238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.38/35.43 % (1551238)CaDiCaL version: 2.1.3 % 245.38/35.43 % (1551238)Termination reason: Instruction limit % 245.38/35.43 % (1551238)Termination phase: Finite model building preprocessing % 245.38/35.43 % (1551238)Time elapsed: 3.912 s % 245.38/35.43 % (1551238)Peak memory usage: 230 MB % 245.38/35.43 % (1551238)Instructions burned: 14073 (million) % 245.38/35.43 % (1551244)dis+10_16:1_sil=16000:random_seed=2703051253:i=9155:fsr=off_2843 on theBenchmark for (2843ds/9155Mi) % 245.38/35.43 % (1551244)Instruction limit reached! % 245.38/35.43 % (1551244)------------------------------ % 245.38/35.43 % (1551244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 245.38/35.43 % (1551244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.38/35.43 % (1551244)CaDiCaL version: 2.1.3 % 245.38/35.43 % (1551244)Termination reason: Instruction limit % 295.75/42.58 % (1551244)Termination phase: Saturation % 295.75/42.58 % (1551244)Time elapsed: 2.474 s % 295.75/42.58 % (1551244)Peak memory usage: 125 MB % 295.75/42.58 % (1551244)Instructions burned: 9157 (million) % 295.75/42.58 % (1551242)Instruction limit reached! % 295.75/42.58 % (1551242)------------------------------ % 295.75/42.58 % (1551242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.75/42.58 % (1551242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.75/42.58 % (1551242)CaDiCaL version: 2.1.3 % 295.75/42.58 % (1551242)Termination reason: Instruction limit % 295.75/42.58 % (1551242)Termination phase: Saturation % 295.75/42.58 % (1551242)Time elapsed: 4.774 s % 295.75/42.58 % (1551242)Peak memory usage: 170 MB % 295.75/42.58 % (1551242)Instructions burned: 8173 (million) % 295.75/42.58 % (1551246)ott-3_8_sil=64000:random_seed=1444998143:i=20139:bs=on_2818 on theBenchmark for (2818ds/20139Mi) % 295.75/42.58 % (1551248)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1372432785:fmbsr=2:i=32576_2818 on theBenchmark for (2818ds/32576Mi) % 295.75/42.58 % Detected minimum model sizes of [5] % 295.75/42.58 % Detected maximum model sizes of [max] % 295.75/42.58 % (1551236)Cannot represent all propositional literals internally % 295.75/42.58 % (1551236)Refutation not found, incomplete strategy % 295.75/42.58 % (1551236)------------------------------ % 295.75/42.58 % (1551236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.75/42.58 % (1551236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.75/42.58 % (1551236)CaDiCaL version: 2.1.3 % 295.75/42.58 % (1551236)Termination reason: Refutation not found, incomplete strategy % 295.75/42.58 % (1551236)Time elapsed: 7.691 s % 295.75/42.58 % (1551236)Peak memory usage: 205 MB % 295.75/42.58 % (1551236)Instructions burned: 15632 (million) % 295.75/42.58 % (1551236)------------------------------ % 295.75/42.58 % (1551236)------------------------------ % 295.75/42.58 % (1551250)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=732682147:i=11404_2810 on theBenchmark for (2810ds/11404Mi) % 295.75/42.58 % (1551240)Instruction limit reached! % 295.75/42.58 % (1551240)------------------------------ % 295.75/42.58 % (1551240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.75/42.58 % (1551240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.75/42.58 % (1551240)CaDiCaL version: 2.1.3 % 295.75/42.58 % (1551240)Termination reason: Instruction limit % 295.75/42.58 % (1551240)Termination phase: Saturation % 295.75/42.58 % (1551240)Time elapsed: 8.384 s % 295.75/42.58 % (1551240)Peak memory usage: 242 MB % 295.75/42.58 % (1551240)Instructions burned: 22567 (million) % 295.75/42.58 % (1551252)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3721830687:i=14134_2782 on theBenchmark for (2782ds/14134Mi) % 295.75/42.58 % (1551230)Instruction limit reached! % 295.75/42.58 % (1551230)------------------------------ % 295.75/42.58 % (1551230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.75/42.58 % (1551230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.75/42.58 % (1551230)CaDiCaL version: 2.1.3 % 295.75/42.58 % (1551230)Termination reason: Instruction limit % 295.75/42.58 % (1551230)Termination phase: Saturation % 295.75/42.58 % (1551230)Time elapsed: 15.434 s % 295.75/42.58 % (1551230)Peak memory usage: 403 MB % 295.75/42.58 % (1551230)Instructions burned: 29341 (million) % 295.75/42.58 % (1551254)dis+33_16_sil=32000:sac=on:random_seed=118149299:i=15851:nm=0_2764 on theBenchmark for (2764ds/15851Mi) % 295.75/42.58 % (1551246)Instruction limit reached! % 295.75/42.58 % (1551246)------------------------------ % 295.75/42.58 % (1551246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.75/42.58 % (1551246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.75/42.58 % (1551246)CaDiCaL version: 2.1.3 % 295.75/42.58 % (1551246)Termination reason: Instruction limit % 295.75/42.58 % (1551246)Termination phase: Saturation % 295.75/42.58 % (1551246)Time elapsed: 7.161 s % 295.75/42.58 % (1551246)Peak memory usage: 177 MB % 295.75/42.58 % (1551246)Instructions burned: 20143 (million) % 295.75/42.58 % (1551256)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2187883521:avsq=on:i=17627:add=on:amm=off_2746 on theBenchmark for (2746ds/17627Mi) % 295.75/42.58 % (1551250)Instruction limit reached! % 295.75/42.58 % (1551250)------------------------------ % 295.75/42.58 % (1551250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.75/42.58 % (1551250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.75/42.58 % (1551250)CaDiCaL version: Terminated % 300.27/43.18 % Vampire exiting % 300.27/43.18 Terminated %------------------------------------------------------------------------------