%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : LCL916^1 : TPTP v9.3.1. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n013.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 : Wed Sep 30 08:15:14 AM UTC 2026 % Result : Satisfiable 2.55s 0.68s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL916^1 : TPTP v9.3.1. Released v6.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.20 % Computer : n013.cluster.edu % 0.10/0.20 % Model : x86_64 x86_64 % 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.20 % Memory : 8046.5625MB % 0.10/0.20 % OS : Linux 6.8.0-71-generic % 0.10/0.20 % CPULimit : 300 % 0.10/0.20 % WCLimit : 300 % 0.10/0.20 % DateTime : Tue Sep 29 11:04:02 UTC 2026 % 0.10/0.20 % CPUTime : % 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.23 Running first-order model finding % 0.10/0.24 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 % 2.55/0.68 % (1956324)Will run a generic schedule for satisfiability detection. % 2.55/0.68 % (1956332)dis+10_1_sil=32000:sp=arity:random_seed=57802477:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.55/0.68 % (1956329)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3373780414_2999 on theBenchmark for (2999ds/0Mi) % 2.55/0.68 % (1956331)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2567488904:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.55/0.68 % (1956333)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4095905649:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.55/0.68 % (1956333)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 2.55/0.68 % Detected minimum model sizes of [1] % 2.55/0.68 % Detected maximum model sizes of [2] % 2.55/0.68 % TRYING [1] % 2.55/0.68 % TRYING [2] % 2.55/0.68 % Finite Model Found! % 2.55/0.68 % SZS status Satisfiable for theBenchmark % 2.55/0.68 % (1956329)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.55/0.68 % (1956329)------------------------------ % 2.55/0.68 % (1956329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.55/0.68 % (1956329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.55/0.68 % (1956329)CaDiCaL version: 2.1.3 % 2.55/0.68 % (1956329)Termination reason: Unknown % 2.55/0.68 % (1956329)Termination phase: Finite model building constraint generation % 2.55/0.68 % (1956329)Time elapsed: 0.002 s % 2.55/0.68 % (1956329)Peak memory usage: 11 MB % 2.55/0.68 % (1956329)Instructions burned: 2 (million) % 2.55/0.68 % (1956330)% WARNING: option uhcvi not known. % 2.55/0.68 % (1956334)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4291557000:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.55/0.68 % (1956330)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2192686749:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.55/0.68 % (1956330)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 2.55/0.68 % (1956335)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=131772191:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.55/0.68 % (1956340)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4266608438:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.55/0.68 % Detected minimum model sizes of [1] % 2.55/0.68 % Detected maximum model sizes of [3] % 2.55/0.68 % TRYING [1] % 2.55/0.68 % TRYING [2] % 2.55/0.68 % Finite Model Found! % 2.55/0.68 % SZS status Satisfiable for theBenchmark % 2.55/0.68 % (1956340)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.55/0.68 % (1956340)------------------------------ % 2.55/0.68 % (1956340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.55/0.68 % (1956340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.55/0.68 % (1956340)CaDiCaL version: 2.1.3 % 2.55/0.68 % (1956340)Termination reason: Unknown % 2.55/0.68 % (1956340)Termination phase: Finite model building constraint generation % 2.55/0.68 % (1956340)Time elapsed: 0.002 s % 2.55/0.68 % (1956340)Peak memory usage: 11 MB % 2.55/0.68 % (1956340)Instructions burned: 2 (million) % 2.55/0.68 % (1956330)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 2.55/0.68 % (1956332)Instruction limit reached! % 2.55/0.68 % (1956332)------------------------------ % 2.55/0.68 % (1956332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.55/0.68 % (1956332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.55/0.68 % (1956332)CaDiCaL version: 2.1.3 % 2.55/0.68 % (1956332)Termination reason: Instruction limit % 2.55/0.68 % (1956332)Termination phase: Saturation % 2.55/0.68 % (1956332)Time elapsed: 0.041 s % 2.55/0.68 % (1956332)Peak memory usage: 11 MB % 2.55/0.68 % (1956332)Instructions burned: 104 (million) % 2.55/0.68 % (1956345)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2664252797:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.55/0.68 % (1956333)Instruction limit reached! % 2.55/0.68 % (1956333)------------------------------ % 2.55/0.68 % (1956333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.55/0.68 % (1956333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.55/0.68 % (1956333)CaDiCaL version: 2.1.3 % 2.55/0.68 % (1956333)Termination reason: Instruction limit % 2.55/0.68 % (1956333)Termination phase: Saturation % 3.55/0.88 % (1956333)Time elapsed: 0.053 s % 3.55/0.88 % (1956333)Peak memory usage: 12 MB % 3.55/0.88 % (1956333)Instructions burned: 116 (million) % 3.55/0.88 % (1956346)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=1742002886:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.55/0.88 % (1956346)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.55/0.88 % (1956346)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 3.55/0.88 % (1956348)ott-21_1_sil=16000:fs=off:random_seed=81908467:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.55/0.88 % (1956335)Instruction limit reached! % 3.55/0.88 % (1956335)------------------------------ % 3.55/0.88 % (1956335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (1956335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (1956335)CaDiCaL version: 2.1.3 % 3.55/0.88 % (1956335)Termination reason: Instruction limit % 3.55/0.88 % (1956335)Termination phase: Saturation % 3.55/0.88 % (1956335)Time elapsed: 0.066 s % 3.55/0.88 % (1956335)Peak memory usage: 11 MB % 3.55/0.88 % (1956335)Instructions burned: 159 (million) % 3.55/0.88 % (1956334)Instruction limit reached! % 3.55/0.88 % (1956334)------------------------------ % 3.55/0.88 % (1956334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (1956334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (1956334)CaDiCaL version: 2.1.3 % 3.55/0.88 % (1956334)Termination reason: Instruction limit % 3.55/0.88 % (1956334)Termination phase: Saturation % 3.55/0.88 % (1956334)Time elapsed: 0.082 s % 3.55/0.88 % (1956334)Peak memory usage: 11 MB % 3.55/0.88 % (1956334)Instructions burned: 132 (million) % 3.55/0.88 % (1956345)Instruction limit reached! % 3.55/0.88 % (1956345)------------------------------ % 3.55/0.88 % (1956345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (1956345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (1956345)CaDiCaL version: 2.1.3 % 3.55/0.88 % (1956345)Termination reason: Instruction limit % 3.55/0.88 % (1956345)Termination phase: Saturation % 3.55/0.88 % (1956345)Time elapsed: 0.056 s % 3.55/0.88 % (1956345)Peak memory usage: 11 MB % 3.55/0.88 % (1956345)Instructions burned: 133 (million) % 3.55/0.88 % (1956352)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3193081812:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 3.55/0.88 % Detected minimum model sizes of [1] % 3.55/0.88 % Detected maximum model sizes of [2] % 3.55/0.88 % TRYING [1] % 3.55/0.88 % TRYING [2] % 3.55/0.88 % Finite Model Found! % 3.55/0.88 % SZS status Satisfiable for theBenchmark % 3.55/0.88 % (1956352)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.55/0.88 % (1956352)------------------------------ % 3.55/0.88 % (1956352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.55/0.88 % (1956352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.55/0.88 % (1956352)CaDiCaL version: 2.1.3 % 3.55/0.88 % (1956352)Termination reason: Unknown % 3.55/0.88 % (1956352)Termination phase: Finite model building constraint generation % 3.55/0.88 % (1956352)Time elapsed: 0.001 s % 3.55/0.88 % (1956352)Peak memory usage: 10 MB % 3.55/0.88 % (1956352)Instructions burned: 2 (million) % 3.55/0.88 % (1956351)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3299537699:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 3.55/0.88 % (1956353)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3871002287:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 3.55/0.88 % (1956355)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4183984681:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 3.55/0.88 % Exception at run slice level % 3.55/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 3.55/0.88 % (1956359)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=4190622145:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 3.55/0.88 % (1956359)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 3.55/0.88 % (1956348)Instruction limit reached! % 13.64/2.22 % (1956348)------------------------------ % 13.64/2.22 % (1956348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.64/2.22 % (1956348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.64/2.22 % (1956348)CaDiCaL version: 2.1.3 % 13.64/2.22 % (1956348)Termination reason: Instruction limit % 13.64/2.22 % (1956348)Termination phase: Saturation % 13.64/2.22 % (1956348)Time elapsed: 0.120 s % 13.64/2.22 % (1956348)Peak memory usage: 13 MB % 13.64/2.22 % (1956348)Instructions burned: 181 (million) % 13.64/2.22 % (1956361)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3933732845:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 13.64/2.22 % (1956361)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 13.64/2.22 % (1956346)Instruction limit reached! % 13.64/2.22 % (1956346)------------------------------ % 13.64/2.22 % (1956346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.64/2.22 % (1956346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.64/2.22 % (1956346)CaDiCaL version: 2.1.3 % 13.64/2.22 % (1956346)Termination reason: Instruction limit % 13.64/2.22 % (1956346)Termination phase: Saturation % 13.64/2.22 % (1956346)Time elapsed: 0.269 s % 13.64/2.22 % (1956346)Peak memory usage: 13 MB % 13.64/2.22 % (1956346)Instructions burned: 686 (million) % 13.64/2.22 % (1956363)fmb+10_1_sil=64000:random_seed=1262051949:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 13.64/2.22 % (1956363)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.64/2.22 % Detected minimum model sizes of [1] % 13.64/2.22 % Detected maximum model sizes of [2] % 13.64/2.22 % TRYING [1] % 13.64/2.22 % TRYING [2] % 13.64/2.22 % Finite Model Found! % 13.64/2.22 % SZS status Satisfiable for theBenchmark % 13.64/2.22 % (1956363)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.64/2.22 % (1956363)------------------------------ % 13.64/2.22 % (1956363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.64/2.22 % (1956363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.64/2.22 % (1956363)CaDiCaL version: 2.1.3 % 13.64/2.22 % (1956363)Termination reason: Unknown % 13.64/2.22 % (1956363)Termination phase: Finite model building constraint generation % 13.64/2.22 % (1956363)Time elapsed: 0.001 s % 13.64/2.22 % (1956363)Peak memory usage: 10 MB % 13.64/2.22 % (1956363)Instructions burned: 2 (million) % 13.64/2.22 % (1956365)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4269186266:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 13.64/2.22 % Detected minimum model sizes of [1] % 13.64/2.22 % Detected maximum model sizes of [2] % 13.64/2.22 % fmb_start_size (= 20) larger than a detected sort maximum size! % 13.64/2.22 % (1956365)Refutation not found, incomplete strategy % 13.64/2.22 % (1956365)------------------------------ % 13.64/2.22 % (1956365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.64/2.22 % (1956365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.64/2.22 % (1956365)CaDiCaL version: 2.1.3 % 13.64/2.22 % (1956365)Termination reason: Refutation not found, incomplete strategy % 13.64/2.22 % (1956365)Time elapsed: 0.001 s % 13.64/2.22 % (1956365)Peak memory usage: 10 MB % 13.64/2.22 % (1956365)Instructions burned: 2 (million) % 13.64/2.22 % (1956365)------------------------------ % 13.64/2.22 % (1956365)------------------------------ % 13.64/2.22 % (1956351)Instruction limit reached! % 13.64/2.22 % (1956351)------------------------------ % 13.64/2.22 % (1956351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.64/2.22 % (1956351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.64/2.22 % (1956351)CaDiCaL version: 2.1.3 % 13.64/2.22 % (1956351)Termination reason: Instruction limit % 13.64/2.22 % (1956351)Termination phase: Saturation % 13.64/2.22 % (1956351)Time elapsed: 0.277 s % 13.64/2.22 % (1956351)Peak memory usage: 12 MB % 13.64/2.22 % (1956351)Instructions burned: 477 (million) % 13.64/2.22 % (1956367)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4291825673:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 13.64/2.22 % Detected minimum model sizes of [1] % 13.64/2.22 % Detected maximum model sizes of [2] % 13.64/2.22 % fmb_start_size (= 8) larger than a detected sort maximum size! % 13.64/2.22 % (1956367)Refutation not found, incomplete strategy % 13.64/2.22 % (1956367)------------------------------ % 13.64/2.22 % (1956367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.64/2.22 % (1956367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/2.83 % (1956367)CaDiCaL version: 2.1.3 % 16.74/2.83 % (1956367)Termination reason: Refutation not found, incomplete strategy % 16.74/2.83 % (1956367)Time elapsed: 0.001 s % 16.74/2.83 % (1956367)Peak memory usage: 10 MB % 16.74/2.83 % (1956367)Instructions burned: 2 (million) % 16.74/2.83 % (1956367)------------------------------ % 16.74/2.83 % (1956367)------------------------------ % 16.74/2.83 % (1956368)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2795075852:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 16.74/2.83 % (1956368)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 16.74/2.83 % (1956370)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1106972953:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 16.74/2.83 % (1956370)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 16.74/2.83 % (1956370)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 16.74/2.83 % (1956361)Instruction limit reached! % 16.74/2.83 % (1956361)------------------------------ % 16.74/2.83 % (1956361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.74/2.83 % (1956361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/2.83 % (1956361)CaDiCaL version: 2.1.3 % 16.74/2.83 % (1956361)Termination reason: Instruction limit % 16.74/2.83 % (1956361)Termination phase: Saturation % 16.74/2.83 % (1956361)Time elapsed: 0.319 s % 16.74/2.83 % (1956361)Peak memory usage: 12 MB % 16.74/2.83 % (1956361)Instructions burned: 882 (million) % 16.74/2.83 % (1956353)Instruction limit reached! % 16.74/2.83 % (1956353)------------------------------ % 16.74/2.83 % (1956353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.74/2.83 % (1956353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/2.83 % (1956353)CaDiCaL version: 2.1.3 % 16.74/2.83 % (1956353)Termination reason: Instruction limit % 16.74/2.83 % (1956353)Termination phase: Saturation % 16.74/2.83 % (1956353)Time elapsed: 0.447 s % 16.74/2.83 % (1956353)Peak memory usage: 11 MB % 16.74/2.83 % (1956353)Instructions burned: 1179 (million) % 16.74/2.83 % (1956374)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3080421795:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 16.74/2.83 % TRYING [16] % 16.74/2.83 % (1956373)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4025250600:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 16.74/2.83 % Finite Model Found! % 16.74/2.83 % SZS status Satisfiable for theBenchmark % 16.74/2.83 % (1956374)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.74/2.83 % (1956374)------------------------------ % 16.74/2.83 % (1956374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.74/2.83 % (1956374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/2.83 % (1956374)CaDiCaL version: 2.1.3 % 16.74/2.83 % (1956374)Termination reason: Unknown % 16.74/2.83 % (1956374)Termination phase: Finite model building constraint generation % 16.74/2.83 % (1956374)Time elapsed: 0.003 s % 16.74/2.83 % (1956374)Peak memory usage: 11 MB % 16.74/2.83 % (1956374)Instructions burned: 5 (million) % 16.74/2.83 % Detected minimum model sizes of [1] % 16.74/2.83 % Detected maximum model sizes of [2] % 16.74/2.83 % fmb_start_size (= 77) larger than a detected sort maximum size! % 16.74/2.83 % (1956373)Refutation not found, incomplete strategy % 16.74/2.83 % (1956373)------------------------------ % 16.74/2.83 % (1956373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.74/2.83 % (1956373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/2.83 % (1956373)CaDiCaL version: 2.1.3 % 16.74/2.83 % (1956373)Termination reason: Refutation not found, incomplete strategy % 16.74/2.83 % (1956373)Time elapsed: 0.001 s % 16.74/2.83 % (1956373)Peak memory usage: 10 MB % 16.74/2.83 % (1956373)Instructions burned: 2 (million) % 16.74/2.83 % (1956373)------------------------------ % 16.74/2.83 % (1956373)------------------------------ % 16.74/2.83 % (1956359)Instruction limit reached! % 16.74/2.83 % (1956359)------------------------------ % 16.74/2.83 % (1956359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 16.74/2.83 % (1956359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/2.83 % (1956359)CaDiCaL version: 2.1.3 % 16.74/2.83 % (1956359)Termination reason: Instruction limit % 47.04/6.99 % (1956359)Termination phase: Saturation % 47.04/6.99 % (1956359)Time elapsed: 0.441 s % 47.04/6.99 % (1956359)Peak memory usage: 12 MB % 47.04/6.99 % (1956359)Instructions burned: 692 (million) % 47.04/6.99 % (1956379)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3273674303:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 47.04/6.99 % Detected minimum model sizes of [1] % 47.04/6.99 % Detected maximum model sizes of [2] % 47.04/6.99 % TRYING [1] % 47.04/6.99 % TRYING [2] % 47.04/6.99 % Finite Model Found! % 47.04/6.99 % SZS status Satisfiable for theBenchmark % 47.04/6.99 % (1956379)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.04/6.99 % (1956379)------------------------------ % 47.04/6.99 % (1956379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.04/6.99 % (1956379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.04/6.99 % (1956379)CaDiCaL version: 2.1.3 % 47.04/6.99 % (1956379)Termination reason: Unknown % 47.04/6.99 % (1956379)Termination phase: Finite model building constraint generation % 47.04/6.99 % (1956379)Time elapsed: 0.002 s % 47.04/6.99 % (1956379)Peak memory usage: 11 MB % 47.04/6.99 % (1956379)Instructions burned: 2 (million) % 47.04/6.99 % (1956377)ott-2_1_sil=16000:newcnf=on:random_seed=3504374437:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 47.04/6.99 % (1956377)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 47.04/6.99 % (1956378)ott+10_1_sil=32000:tgt=ground:random_seed=1759990215:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 47.04/6.99 % (1956382)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=513448824:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi) % 47.04/6.99 % (1956382)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 47.04/6.99 % (1956377)Instruction limit reached! % 47.04/6.99 % (1956377)------------------------------ % 47.04/6.99 % (1956377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.04/6.99 % (1956377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.04/6.99 % (1956377)CaDiCaL version: 2.1.3 % 47.04/6.99 % (1956377)Termination reason: Instruction limit % 47.04/6.99 % (1956377)Termination phase: Saturation % 47.04/6.99 % (1956377)Time elapsed: 0.471 s % 47.04/6.99 % (1956377)Peak memory usage: 11 MB % 47.04/6.99 % (1956377)Instructions burned: 870 (million) % 47.04/6.99 % (1956370)Instruction limit reached! % 47.04/6.99 % (1956370)------------------------------ % 47.04/6.99 % (1956370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.04/6.99 % (1956370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.04/6.99 % (1956370)CaDiCaL version: 2.1.3 % 47.04/6.99 % (1956370)Termination reason: Instruction limit % 47.04/6.99 % (1956370)Termination phase: Saturation % 47.04/6.99 % (1956370)Time elapsed: 0.682 s % 47.04/6.99 % (1956370)Peak memory usage: 12 MB % 47.04/6.99 % (1956370)Instructions burned: 1474 (million) % 47.04/6.99 % (1956387)dis+21_1_sil=32000:sas=cadical:random_seed=186281170:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 47.04/6.99 % (1956388)ott+11_1_sil=16000:gs=on:random_seed=3565728670:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 47.04/6.99 % (1956388)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 47.04/6.99 % (1956388)Instruction limit reached! % 47.04/6.99 % (1956388)------------------------------ % 47.04/6.99 % (1956388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 47.04/6.99 % (1956388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.04/6.99 % (1956388)CaDiCaL version: 2.1.3 % 47.04/6.99 % (1956388)Termination reason: Instruction limit % 47.04/6.99 % (1956388)Termination phase: Saturation % 47.04/6.99 % (1956388)Time elapsed: 0.795 s % 47.04/6.99 % (1956388)Peak memory usage: 12 MB % 47.04/6.99 % (1956388)Instructions burned: 2254 (million) % 47.04/6.99 % (1956391)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1940084909:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 47.04/6.99 % Detected minimum model sizes of [1] % 47.04/6.99 % Detected maximum model sizes of [3] % 47.04/6.99 % fmb_start_size (= 7) larger than a detected sort maximum size! % 47.04/6.99 % (1956391)Refutation not found, incomplete strategy % 47.04/6.99 % (1956391)------------------------------ % 47.04/6.99 % (1956391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.01/13.62 % (1956391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.01/13.62 % (1956391)CaDiCaL version: 2.1.3 % 94.01/13.62 % (1956391)Termination reason: Refutation not found, incomplete strategy % 94.01/13.62 % (1956391)Time elapsed: 0.001 s % 94.01/13.62 % (1956391)Peak memory usage: 10 MB % 94.01/13.62 % (1956391)Instructions burned: 2 (million) % 94.01/13.62 % (1956391)------------------------------ % 94.01/13.62 % (1956391)------------------------------ % 94.01/13.62 % (1956393)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1313271554:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 94.01/13.62 % (1956378)Instruction limit reached! % 94.01/13.62 % (1956378)------------------------------ % 94.01/13.62 % (1956378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.01/13.62 % (1956378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.01/13.62 % (1956378)CaDiCaL version: 2.1.3 % 94.01/13.62 % (1956378)Termination reason: Instruction limit % 94.01/13.62 % (1956378)Termination phase: Saturation % 94.01/13.62 % (1956378)Time elapsed: 1.507 s % 94.01/13.62 % (1956378)Peak memory usage: 11 MB % 94.01/13.62 % (1956378)Instructions burned: 5118 (million) % 94.01/13.62 % (1956395)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=390403172:i=29340_2978 on theBenchmark for (2978ds/29340Mi) % 94.01/13.62 % (1956382)Instruction limit reached! % 94.01/13.62 % (1956382)------------------------------ % 94.01/13.62 % (1956382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.01/13.62 % (1956382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.01/13.62 % (1956382)CaDiCaL version: 2.1.3 % 94.01/13.62 % (1956382)Termination reason: Instruction limit % 94.01/13.62 % (1956382)Termination phase: Saturation % 94.01/13.62 % (1956382)Time elapsed: 1.648 s % 94.01/13.62 % (1956382)Peak memory usage: 14 MB % 94.01/13.62 % (1956382)Instructions burned: 3513 (million) % 94.01/13.62 % (1956397)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1952985477:i=5211_2976 on theBenchmark for (2976ds/5211Mi) % 94.01/13.62 % (1956368)Instruction limit reached! % 94.01/13.62 % (1956368)------------------------------ % 94.01/13.62 % (1956368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.01/13.62 % (1956368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.01/13.62 % (1956368)CaDiCaL version: 2.1.3 % 94.01/13.62 % (1956368)Termination reason: Instruction limit % 94.01/13.62 % (1956368)Termination phase: Saturation % 94.01/13.62 % (1956368)Time elapsed: 2.087 s % 94.01/13.62 % (1956368)Peak memory usage: 13 MB % 94.01/13.62 % (1956368)Instructions burned: 5133 (million) % 94.01/13.62 % (1956399)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2042817124:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi) % 94.01/13.62 % Detected minimum model sizes of [1] % 94.01/13.62 % Detected maximum model sizes of [2] % 94.01/13.62 % fmb_start_size (= 17) larger than a detected sort maximum size! % 94.01/13.62 % (1956399)Refutation not found, incomplete strategy % 94.01/13.62 % (1956399)------------------------------ % 94.01/13.62 % (1956399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.01/13.62 % (1956399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.01/13.62 % (1956399)CaDiCaL version: 2.1.3 % 94.01/13.62 % (1956399)Termination reason: Refutation not found, incomplete strategy % 94.01/13.62 % (1956399)Time elapsed: 0.001 s % 94.01/13.62 % (1956399)Peak memory usage: 10 MB % 94.01/13.62 % (1956399)Instructions burned: 2 (million) % 94.01/13.62 % (1956399)------------------------------ % 94.01/13.62 % (1956399)------------------------------ % 94.01/13.62 % (1956401)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2748382741:fmbsr=2:i=46332_2974 on theBenchmark for (2974ds/46332Mi) % 94.01/13.62 % Detected minimum model sizes of [1] % 94.01/13.62 % Detected maximum model sizes of [3] % 94.01/13.62 % fmb_start_size (= 15) larger than a detected sort maximum size! % 94.01/13.62 % (1956401)Refutation not found, incomplete strategy % 94.01/13.62 % (1956401)------------------------------ % 94.01/13.62 % (1956401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 94.01/13.62 % (1956401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.01/13.62 % (1956401)CaDiCaL version: 2.1.3 % 94.01/13.62 % (1956401)Termination reason: Refutation not found, incomplete strategy % 94.01/13.62 % (1956401)Time elapsed: 0.001 s % 94.01/13.62 % (1956401)Peak memory usage: 10 MB % 98.88/14.28 % (1956401)Instructions burned: 2 (million) % 98.88/14.28 % (1956401)------------------------------ % 98.88/14.28 % (1956401)------------------------------ % 98.88/14.28 % (1956403)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1215296505:i=14071_2974 on theBenchmark for (2974ds/14071Mi) % 98.88/14.28 % Detected minimum model sizes of [1] % 98.88/14.28 % Detected maximum model sizes of [2] % 98.88/14.28 % fmb_start_size (= 12) larger than a detected sort maximum size! % 98.88/14.28 % (1956403)Refutation not found, incomplete strategy % 98.88/14.28 % (1956403)------------------------------ % 98.88/14.28 % (1956403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.88/14.28 % (1956403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.88/14.28 % (1956403)CaDiCaL version: 2.1.3 % 98.88/14.28 % (1956403)Termination reason: Refutation not found, incomplete strategy % 98.88/14.28 % (1956403)Time elapsed: 0.001 s % 98.88/14.28 % (1956403)Peak memory usage: 11 MB % 98.88/14.28 % (1956403)Instructions burned: 2 (million) % 98.88/14.28 % (1956403)------------------------------ % 98.88/14.28 % (1956403)------------------------------ % 98.88/14.28 % (1956405)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3289424833:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi) % 98.88/14.28 % (1956387)Instruction limit reached! % 98.88/14.28 % (1956387)------------------------------ % 98.88/14.28 % (1956387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.88/14.28 % (1956387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.88/14.28 % (1956387)CaDiCaL version: 2.1.3 % 98.88/14.28 % (1956387)Termination reason: Instruction limit % 98.88/14.28 % (1956387)Termination phase: Saturation % 98.88/14.28 % (1956387)Time elapsed: 2.056 s % 98.88/14.28 % (1956387)Peak memory usage: 15 MB % 98.88/14.28 % (1956387)Instructions burned: 3773 (million) % 98.88/14.28 % (1956408)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2163521556:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 98.88/14.28 % (1956393)Instruction limit reached! % 98.88/14.28 % (1956393)------------------------------ % 98.88/14.28 % (1956393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.88/14.28 % (1956393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.88/14.28 % (1956393)CaDiCaL version: 2.1.3 % 98.88/14.28 % (1956393)Termination reason: Instruction limit % 98.88/14.28 % (1956393)Termination phase: Saturation % 98.88/14.28 % (1956393)Time elapsed: 1.779 s % 98.88/14.28 % (1956393)Peak memory usage: 13 MB % 98.88/14.28 % (1956393)Instructions burned: 4594 (million) % 98.88/14.28 % (1956411)dis+10_16:1_sil=16000:random_seed=1382681440:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 98.88/14.28 % (1956397)Instruction limit reached! % 98.88/14.28 % (1956397)------------------------------ % 98.88/14.28 % (1956397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.88/14.28 % (1956397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.88/14.28 % (1956397)CaDiCaL version: 2.1.3 % 98.88/14.28 % (1956397)Termination reason: Instruction limit % 98.88/14.28 % (1956397)Termination phase: Saturation % 98.88/14.28 % (1956397)Time elapsed: 2.669 s % 98.88/14.28 % (1956397)Peak memory usage: 15 MB % 98.88/14.28 % (1956397)Instructions burned: 5213 (million) % 98.88/14.28 % (1956414)ott-3_8_sil=64000:random_seed=2461180302:i=20139:bs=on_2949 on theBenchmark for (2949ds/20139Mi) % 98.88/14.28 % (1956408)Instruction limit reached! % 98.88/14.28 % (1956408)------------------------------ % 98.88/14.28 % (1956408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.88/14.28 % (1956408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.88/14.28 % (1956408)CaDiCaL version: 2.1.3 % 98.88/14.28 % (1956408)Termination reason: Instruction limit % 98.88/14.28 % (1956408)Termination phase: Saturation % 98.88/14.28 % (1956408)Time elapsed: 3.496 s % 98.88/14.28 % (1956408)Peak memory usage: 12 MB % 98.88/14.28 % (1956408)Instructions burned: 8174 (million) % 98.88/14.28 % (1956417)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1286361992:fmbsr=2:i=32576_2932 on theBenchmark for (2932ds/32576Mi) % 98.88/14.28 % Detected minimum model sizes of [1] % 98.88/14.28 % Detected maximum model sizes of [2] % 98.88/14.28 % fmb_start_size (= 9) larger than a detected sort maximum size! % 98.88/14.28 % (1956417)Refutation not found, incomplete strategy % 98.88/14.28 % (1956417)------------------------------ % 98.88/14.28 % (1956417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.73/17.74 % (1956417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.73/17.74 % (1956417)CaDiCaL version: 2.1.3 % 123.73/17.74 % (1956417)Termination reason: Refutation not found, incomplete strategy % 123.73/17.74 % (1956417)Time elapsed: 0.001 s % 123.73/17.74 % (1956417)Peak memory usage: 11 MB % 123.73/17.74 % (1956417)Instructions burned: 2 (million) % 123.73/17.74 % (1956417)------------------------------ % 123.73/17.74 % (1956417)------------------------------ % 123.73/17.74 % (1956419)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=779994655:i=11404_2932 on theBenchmark for (2932ds/11404Mi) % 123.73/17.74 % (1956411)Instruction limit reached! % 123.73/17.74 % (1956411)------------------------------ % 123.73/17.74 % (1956411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.73/17.74 % (1956411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.73/17.74 % (1956411)CaDiCaL version: 2.1.3 % 123.73/17.74 % (1956411)Termination reason: Instruction limit % 123.73/17.74 % (1956411)Termination phase: Saturation % 123.73/17.74 % (1956411)Time elapsed: 3.788 s % 123.73/17.74 % (1956411)Peak memory usage: 16 MB % 123.73/17.74 % (1956411)Instructions burned: 9157 (million) % 123.73/17.74 % (1956427)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2386478601:i=14134_2924 on theBenchmark for (2924ds/14134Mi) % 123.73/17.74 % (1956427)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 123.73/17.74 % (1956405)Instruction limit reached! % 123.73/17.74 % (1956405)------------------------------ % 123.73/17.74 % (1956405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.73/17.74 % (1956405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.73/17.74 % (1956405)CaDiCaL version: 2.1.3 % 123.73/17.74 % (1956405)Termination reason: Instruction limit % 123.73/17.74 % (1956405)Termination phase: Saturation % 123.73/17.74 % (1956405)Time elapsed: 7.074 s % 123.73/17.74 % (1956405)Peak memory usage: 14 MB % 123.73/17.74 % (1956405)Instructions burned: 22567 (million) % 123.73/17.74 % (1956433)dis+33_16_sil=32000:sac=on:random_seed=1769727997:i=15851:nm=0_2903 on theBenchmark for (2903ds/15851Mi) % 123.73/17.74 % (1956395)Instruction limit reached! % 123.73/17.74 % (1956395)------------------------------ % 123.73/17.74 % (1956395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.73/17.74 % (1956395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.73/17.74 % (1956395)CaDiCaL version: 2.1.3 % 123.73/17.74 % (1956395)Termination reason: Instruction limit % 123.73/17.74 % (1956395)Termination phase: Saturation % 123.73/17.74 % (1956395)Time elapsed: 8.114 s % 123.73/17.74 % (1956395)Peak memory usage: 16 MB % 123.73/17.74 % (1956395)Instructions burned: 29341 (million) % 123.73/17.74 % (1956435)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3171468410:avsq=on:i=17627:add=on:amm=off_2897 on theBenchmark for (2897ds/17627Mi) % 123.73/17.74 % (1956419)Instruction limit reached! % 123.73/17.74 % (1956419)------------------------------ % 123.73/17.74 % (1956419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.73/17.74 % (1956419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.73/17.74 % (1956419)CaDiCaL version: 2.1.3 % 123.73/17.74 % (1956419)Termination reason: Instruction limit % 123.73/17.74 % (1956419)Termination phase: Saturation % 123.73/17.74 % (1956419)Time elapsed: 6.0000 s % 123.73/17.74 % (1956419)Peak memory usage: 13 MB % 123.73/17.74 % (1956419)Instructions burned: 11404 (million) % 123.73/17.74 % (1956438)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3371310261:s2a=on:i=53295_2872 on theBenchmark for (2872ds/53295Mi) % 123.73/17.74 % (1956427)Instruction limit reached! % 123.73/17.74 % (1956427)------------------------------ % 123.73/17.74 % (1956427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.73/17.74 % (1956427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.73/17.74 % (1956427)CaDiCaL version: 2.1.3 % 123.73/17.74 % (1956427)Termination reason: Instruction limit % 123.73/17.74 % (1956427)Termination phase: Saturation % 123.73/17.74 % (1956427)Time elapsed: 5.746 s % 123.73/17.74 % (1956427)Peak memory usage: 12 MB % 123.73/17.74 % (1956427)Instructions burned: 14136 (million) % 123.73/17.74 % (1956441)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=592072748:i=26857:ins=20_2866 on theBenchmark for (2866ds/26857Mi) % 123.73/17.74 % Detected minimum model sizes of [1] % 123.73/17.74 % Detected maximum model sizes of [2] % 123.73/17.74 % fmb_start_size (= 16) larger than a detected sort maximum size! % 123.73/17.74 % (1956441)Refutation not found, incomplete strategy % 126.08/18.10 % (1956441)------------------------------ % 126.08/18.10 % (1956441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.10 % (1956441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.10 % (1956441)CaDiCaL version: 2.1.3 % 126.08/18.10 % (1956441)Termination reason: Refutation not found, incomplete strategy % 126.08/18.10 % (1956441)Time elapsed: 0.001 s % 126.08/18.10 % (1956441)Peak memory usage: 10 MB % 126.08/18.10 % (1956441)Instructions burned: 2 (million) % 126.08/18.10 % (1956441)------------------------------ % 126.08/18.10 % (1956441)------------------------------ % 126.08/18.10 % (1956443)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3384274738:i=28120:bs=on:fsr=off_2866 on theBenchmark for (2866ds/28120Mi) % 126.08/18.10 % (1956414)Instruction limit reached! % 126.08/18.10 % (1956414)------------------------------ % 126.08/18.10 % (1956414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.10 % (1956414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.10 % (1956414)CaDiCaL version: 2.1.3 % 126.08/18.10 % (1956414)Termination reason: Instruction limit % 126.08/18.10 % (1956414)Termination phase: Saturation % 126.08/18.10 % (1956414)Time elapsed: 8.912 s % 126.08/18.10 % (1956414)Peak memory usage: 14 MB % 126.08/18.10 % (1956414)Instructions burned: 20139 (million) % 126.08/18.10 % (1956445)fmb+10_1_sil=256000:fmbss=7:random_seed=3135866638:fmbsr=1.6:i=182295_2860 on theBenchmark for (2860ds/182295Mi) % 126.08/18.10 % Detected minimum model sizes of [1] % 126.08/18.10 % Detected maximum model sizes of [2] % 126.08/18.10 % fmb_start_size (= 7) larger than a detected sort maximum size! % 126.08/18.10 % (1956445)Refutation not found, incomplete strategy % 126.08/18.10 % (1956445)------------------------------ % 126.08/18.10 % (1956445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.10 % (1956445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.10 % (1956445)CaDiCaL version: 2.1.3 % 126.08/18.10 % (1956445)Termination reason: Refutation not found, incomplete strategy % 126.08/18.10 % (1956445)Time elapsed: 0.001 s % 126.08/18.10 % (1956445)Peak memory usage: 10 MB % 126.08/18.10 % (1956445)Instructions burned: 2 (million) % 126.08/18.10 % (1956445)------------------------------ % 126.08/18.10 % (1956445)------------------------------ % 126.08/18.10 % (1956447)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1675870039:i=44625:gsp=on_2860 on theBenchmark for (2860ds/44625Mi) % 126.08/18.10 % (1956447)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 126.08/18.10 % (1956447)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 126.08/18.10 % Detected minimum model sizes of [1] % 126.08/18.10 % Detected maximum model sizes of [2] % 126.08/18.10 % fmb_start_size (= 21) larger than a detected sort maximum size! % 126.08/18.10 % (1956447)Refutation not found, incomplete strategy % 126.08/18.10 % (1956447)------------------------------ % 126.08/18.10 % (1956447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.10 % (1956447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.10 % (1956447)CaDiCaL version: 2.1.3 % 126.08/18.10 % (1956447)Termination reason: Refutation not found, incomplete strategy % 126.08/18.10 % (1956447)Time elapsed: 0.001 s % 126.08/18.10 % (1956447)Peak memory usage: 10 MB % 126.08/18.10 % (1956447)Instructions burned: 2 (million) % 126.08/18.10 % (1956447)------------------------------ % 126.08/18.10 % (1956447)------------------------------ % 126.08/18.10 % (1956449)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=413027941:i=160505_2860 on theBenchmark for (2860ds/160505Mi) % 126.08/18.10 % Detected minimum model sizes of [1] % 126.08/18.10 % Detected maximum model sizes of [2] % 126.08/18.10 % fmb_start_size (= 15) larger than a detected sort maximum size! % 126.08/18.10 % (1956449)Refutation not found, incomplete strategy % 126.08/18.10 % (1956449)------------------------------ % 126.08/18.10 % (1956449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.10 % (1956449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.10 % (1956449)CaDiCaL version: 2.1.3 % 126.08/18.10 % (1956449)Termination reason: Refutation not found, incomplete strategy % 126.08/18.10 % (1956449)Time elapsed: 0.001 s % 126.08/18.10 % (1956449)Peak memory usage: 10 MB % 126.08/18.10 % (1956449)Instructions burned: 2 (million) % 126.08/18.10 % (1956449)------------------------------ % 126.08/18.10 % (1956449)------------------------------ % 126.08/18.10 % (1956451)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1727863639:fmbsr=1.3:i=225729_2859 on theBenchmark for (2859ds/225729Mi) % 135.10/19.38 % Detected minimum model sizes of [1] % 135.10/19.38 % Detected maximum model sizes of [2] % 135.10/19.38 % fmb_start_size (= 10) larger than a detected sort maximum size! % 135.10/19.38 % (1956451)Refutation not found, incomplete strategy % 135.10/19.38 % (1956451)------------------------------ % 135.10/19.38 % (1956451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.38 % (1956451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.38 % (1956451)CaDiCaL version: 2.1.3 % 135.10/19.38 % (1956451)Termination reason: Refutation not found, incomplete strategy % 135.10/19.38 % (1956451)Time elapsed: 0.002 s % 135.10/19.38 % (1956451)Peak memory usage: 11 MB % 135.10/19.38 % (1956451)Instructions burned: 2 (million) % 135.10/19.38 % (1956451)------------------------------ % 135.10/19.38 % (1956451)------------------------------ % 135.10/19.38 % (1956453)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2979516187:fmbsr=2:i=185024:ins=7_2859 on theBenchmark for (2859ds/185024Mi) % 135.10/19.38 % Detected minimum model sizes of [1] % 135.10/19.38 % Detected maximum model sizes of [2] % 135.10/19.38 % fmb_start_size (= 10) larger than a detected sort maximum size! % 135.10/19.38 % (1956453)Refutation not found, incomplete strategy % 135.10/19.38 % (1956453)------------------------------ % 135.10/19.38 % (1956453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.38 % (1956453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.38 % (1956453)CaDiCaL version: 2.1.3 % 135.10/19.38 % (1956453)Termination reason: Refutation not found, incomplete strategy % 135.10/19.38 % (1956453)Time elapsed: 0.001 s % 135.10/19.38 % (1956453)Peak memory usage: 11 MB % 135.10/19.38 % (1956453)Instructions burned: 2 (million) % 135.10/19.38 % (1956453)------------------------------ % 135.10/19.38 % (1956453)------------------------------ % 135.10/19.38 % (1956455)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2503375782:rtra=on_2859 on theBenchmark for (2859ds/0Mi) % 135.10/19.38 % Detected minimum model sizes of [1] % 135.10/19.38 % Detected maximum model sizes of [2] % 135.10/19.38 % TRYING [1] % 135.10/19.38 % TRYING [2] % 135.10/19.38 % Finite Model Found! % 135.10/19.38 % SZS status Satisfiable for theBenchmark % 135.10/19.38 % (1956455)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 135.10/19.38 % (1956455)------------------------------ % 135.10/19.38 % (1956455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.38 % (1956455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.38 % (1956455)CaDiCaL version: 2.1.3 % 135.10/19.38 % (1956455)Termination reason: Unknown % 135.10/19.38 % (1956455)Termination phase: Finite model building constraint generation % 135.10/19.38 % (1956455)Time elapsed: 0.002 s % 135.10/19.38 % (1956455)Peak memory usage: 11 MB % 135.10/19.38 % (1956455)Instructions burned: 2 (million) % 135.10/19.38 % (1956457)% WARNING: option uhcvi not known. % 135.10/19.38 % (1956457)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=703663487:i=271062:add=off:rtra=on:rawr=on_2859 on theBenchmark for (2859ds/271062Mi) % 135.10/19.38 % (1956457)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 135.10/19.38 % (1956457)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 135.10/19.38 % (1956435)Instruction limit reached! % 135.10/19.38 % (1956435)------------------------------ % 135.10/19.38 % (1956435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.38 % (1956435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.38 % (1956435)CaDiCaL version: 2.1.3 % 135.10/19.38 % (1956435)Termination reason: Instruction limit % 135.10/19.38 % (1956435)Termination phase: Saturation % 135.10/19.38 % (1956435)Time elapsed: 4.802 s % 135.10/19.38 % (1956435)Peak memory usage: 22 MB % 135.10/19.38 % (1956435)Instructions burned: 17630 (million) % 135.10/19.38 % (1956460)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3452273569:i=176048:add=on:rtra=on:rawr=on_2848 on theBenchmark for (2848ds/176048Mi) % 135.10/19.38 % (1956433)Instruction limit reached! % 135.10/19.38 % (1956433)------------------------------ % 135.10/19.38 % (1956433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.38 % (1956433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.38 % (1956433)CaDiCaL version: 2.1.3 % 135.10/19.38 % (1956433)Termination reason: Instruction limit % 143.27/20.55 % (1956433)Termination phase: Saturation % 143.27/20.55 % (1956433)Time elapsed: 7.781 s % 143.27/20.55 % (1956433)Peak memory usage: 14 MB % 143.27/20.55 % (1956433)Instructions burned: 15851 (million) % 143.27/20.55 % (1956463)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2048369770:i=206:fgj=on:rtra=on_2824 on theBenchmark for (2824ds/206Mi) % 143.27/20.55 % (1956463)Instruction limit reached! % 143.27/20.55 % (1956463)------------------------------ % 143.27/20.55 % (1956463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.27/20.55 % (1956463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.27/20.55 % (1956463)CaDiCaL version: 2.1.3 % 143.27/20.55 % (1956463)Termination reason: Instruction limit % 143.27/20.55 % (1956463)Termination phase: Saturation % 143.27/20.55 % (1956463)Time elapsed: 0.054 s % 143.27/20.55 % (1956463)Peak memory usage: 12 MB % 143.27/20.55 % (1956463)Instructions burned: 211 (million) % 143.27/20.55 % (1956465)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=842074637:i=232:rtra=on_2824 on theBenchmark for (2824ds/232Mi) % 143.27/20.55 % (1956465)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 143.27/20.55 % (1956465)Instruction limit reached! % 143.27/20.55 % (1956465)------------------------------ % 143.27/20.55 % (1956465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.27/20.55 % (1956465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.27/20.55 % (1956465)CaDiCaL version: 2.1.3 % 143.27/20.55 % (1956465)Termination reason: Instruction limit % 143.27/20.55 % (1956465)Termination phase: Saturation % 143.27/20.55 % (1956465)Time elapsed: 0.051 s % 143.27/20.55 % (1956465)Peak memory usage: 11 MB % 143.27/20.55 % (1956465)Instructions burned: 236 (million) % 143.27/20.55 % (1956467)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1454088174:i=262:rtra=on_2823 on theBenchmark for (2823ds/262Mi) % 143.27/20.55 % (1956467)Instruction limit reached! % 143.27/20.55 % (1956467)------------------------------ % 143.27/20.55 % (1956467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.27/20.55 % (1956467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.27/20.55 % (1956467)CaDiCaL version: 2.1.3 % 143.27/20.55 % (1956467)Termination reason: Instruction limit % 143.27/20.55 % (1956467)Termination phase: Saturation % 143.27/20.55 % (1956467)Time elapsed: 0.056 s % 143.27/20.55 % (1956467)Peak memory usage: 11 MB % 143.27/20.55 % (1956467)Instructions burned: 264 (million) % 143.27/20.55 % (1956469)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2237910686:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2823 on theBenchmark for (2823ds/318Mi) % 143.27/20.55 % (1956469)Instruction limit reached! % 143.27/20.55 % (1956469)------------------------------ % 143.27/20.55 % (1956469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.27/20.55 % (1956469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.27/20.55 % (1956469)CaDiCaL version: 2.1.3 % 143.27/20.55 % (1956469)Termination reason: Instruction limit % 143.27/20.55 % (1956469)Termination phase: Saturation % 143.27/20.55 % (1956469)Time elapsed: 0.066 s % 143.27/20.55 % (1956469)Peak memory usage: 12 MB % 143.27/20.55 % (1956469)Instructions burned: 320 (million) % 143.27/20.55 % (1956471)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1126016964:i=1428:nm=2:rtra=on_2822 on theBenchmark for (2822ds/1428Mi) % 143.27/20.55 % Detected minimum model sizes of [1] % 143.27/20.55 % Detected maximum model sizes of [3] % 143.27/20.55 % TRYING [1] % 143.27/20.55 % TRYING [2] % 143.27/20.55 % Finite Model Found! % 143.27/20.55 % SZS status Satisfiable for theBenchmark % 143.27/20.55 % (1956471)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 143.27/20.55 % (1956471)------------------------------ % 143.27/20.55 % (1956471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 143.27/20.55 % (1956471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.27/20.55 % (1956471)CaDiCaL version: 2.1.3 % 143.27/20.55 % (1956471)Termination reason: Unknown % 143.27/20.55 % (1956471)Termination phase: Finite model building constraint generation % 143.27/20.55 % (1956471)Time elapsed: 0.001 s % 143.27/20.55 % (1956471)Peak memory usage: 11 MB % 143.27/20.55 % (1956471)Instructions burned: 2 (million) % 143.27/20.55 % (1956473)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3952701367:i=262:bd=preordered:rtra=on:fsd=on_2822 on theBenchmark for (2822ds/262Mi) % 143.27/20.55 % (1956473)Instruction limit reached! % 143.27/20.55 % (1956473)------------------------------ % 165.49/23.72 % (1956473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.49/23.72 % (1956473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.49/23.72 % (1956473)CaDiCaL version: 2.1.3 % 165.49/23.72 % (1956473)Termination reason: Instruction limit % 165.49/23.72 % (1956473)Termination phase: Saturation % 165.49/23.72 % (1956473)Time elapsed: 0.059 s % 165.49/23.72 % (1956473)Peak memory usage: 11 MB % 165.49/23.72 % (1956473)Instructions burned: 268 (million) % 165.49/23.72 % (1956475)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1202129008:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2821 on theBenchmark for (2821ds/1368Mi) % 165.49/23.72 % (1956475)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 165.49/23.72 % (1956475)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 165.49/23.72 % (1956475)Instruction limit reached! % 165.49/23.72 % (1956475)------------------------------ % 165.49/23.72 % (1956475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.49/23.72 % (1956475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.49/23.72 % (1956475)CaDiCaL version: 2.1.3 % 165.49/23.72 % (1956475)Termination reason: Instruction limit % 165.49/23.72 % (1956475)Termination phase: Saturation % 165.49/23.72 % (1956475)Time elapsed: 0.414 s % 165.49/23.72 % (1956475)Peak memory usage: 13 MB % 165.49/23.72 % (1956475)Instructions burned: 1370 (million) % 165.49/23.72 % (1956477)ott-21_1_sil=16000:si=on:fs=off:random_seed=1927220918:i=360:av=off:fsr=off:rtra=on_2817 on theBenchmark for (2817ds/360Mi) % 165.49/23.72 % (1956477)Instruction limit reached! % 165.49/23.72 % (1956477)------------------------------ % 165.49/23.72 % (1956477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.49/23.72 % (1956477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.49/23.72 % (1956477)CaDiCaL version: 2.1.3 % 165.49/23.72 % (1956477)Termination reason: Instruction limit % 165.49/23.72 % (1956477)Termination phase: Saturation % 165.49/23.72 % (1956477)Time elapsed: 0.107 s % 165.49/23.72 % (1956477)Peak memory usage: 14 MB % 165.49/23.72 % (1956477)Instructions burned: 364 (million) % 165.49/23.72 % (1956479)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3831385096:i=954:bd=all:rtra=on_2815 on theBenchmark for (2815ds/954Mi) % 165.49/23.72 % (1956479)Instruction limit reached! % 165.49/23.72 % (1956479)------------------------------ % 165.49/23.72 % (1956479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.49/23.72 % (1956479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.49/23.72 % (1956479)CaDiCaL version: 2.1.3 % 165.49/23.72 % (1956479)Termination reason: Instruction limit % 165.49/23.72 % (1956479)Termination phase: Saturation % 165.49/23.72 % (1956479)Time elapsed: 0.217 s % 165.49/23.72 % (1956479)Peak memory usage: 12 MB % 165.49/23.72 % (1956479)Instructions burned: 955 (million) % 165.49/23.72 % (1956482)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3585028168:fmbsr=1.3:i=1730:ins=25:rtra=on_2813 on theBenchmark for (2813ds/1730Mi) % 165.49/23.72 % Detected minimum model sizes of [1] % 165.49/23.72 % Detected maximum model sizes of [2] % 165.49/23.72 % TRYING [1] % 165.49/23.72 % TRYING [2] % 165.49/23.72 % Finite Model Found! % 165.49/23.72 % SZS status Satisfiable for theBenchmark % 165.49/23.72 % (1956482)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 165.49/23.72 % (1956482)------------------------------ % 165.49/23.72 % (1956482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.49/23.72 % (1956482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.49/23.72 % (1956482)CaDiCaL version: 2.1.3 % 165.49/23.72 % (1956482)Termination reason: Unknown % 165.49/23.72 % (1956482)Termination phase: Finite model building constraint generation % 165.49/23.72 % (1956482)Time elapsed: 0.001 s % 165.49/23.72 % (1956482)Peak memory usage: 10 MB % 165.49/23.72 % (1956482)Instructions burned: 2 (million) % 165.49/23.72 % (1956484)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3183010036:i=2358:rtra=on_2813 on theBenchmark for (2813ds/2358Mi) % 165.49/23.72 % (1956484)Instruction limit reached! % 165.49/23.72 % (1956484)------------------------------ % 165.49/23.72 % (1956484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.49/23.72 % (1956484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.49/23.72 % (1956484)CaDiCaL version: 2.1.3 % 200.00/28.52 % (1956484)Termination reason: Instruction limit % 200.00/28.52 % (1956484)Termination phase: Saturation % 200.00/28.52 % (1956484)Time elapsed: 0.478 s % 200.00/28.52 % (1956484)Peak memory usage: 11 MB % 200.00/28.52 % (1956484)Instructions burned: 2362 (million) % 200.00/28.52 % (1956486)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=911981995:i=1778:ins=1:rtra=on_2808 on theBenchmark for (2808ds/1778Mi) % 200.00/28.52 % Exception at run slice level % 200.00/28.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 200.00/28.52 % (1956488)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=724407568:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/1384Mi) % 200.00/28.52 % (1956488)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 200.00/28.52 % (1956488)Instruction limit reached! % 200.00/28.52 % (1956488)------------------------------ % 200.00/28.52 % (1956488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.00/28.52 % (1956488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.00/28.52 % (1956488)CaDiCaL version: 2.1.3 % 200.00/28.52 % (1956488)Termination reason: Instruction limit % 200.00/28.52 % (1956488)Termination phase: Saturation % 200.00/28.52 % (1956488)Time elapsed: 0.584 s % 200.00/28.52 % (1956488)Peak memory usage: 12 MB % 200.00/28.52 % (1956488)Instructions burned: 1386 (million) % 200.00/28.52 % (1956491)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3479712547:i=1758:kws=inv_precedence:fsr=off:rtra=on_2802 on theBenchmark for (2802ds/1758Mi) % 200.00/28.52 % (1956491)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 200.00/28.52 % (1956491)Instruction limit reached! % 200.00/28.52 % (1956491)------------------------------ % 200.00/28.52 % (1956491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.00/28.52 % (1956491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.00/28.52 % (1956491)CaDiCaL version: 2.1.3 % 200.00/28.52 % (1956491)Termination reason: Instruction limit % 200.00/28.52 % (1956491)Termination phase: Saturation % 200.00/28.52 % (1956491)Time elapsed: 0.432 s % 200.00/28.52 % (1956491)Peak memory usage: 13 MB % 200.00/28.52 % (1956491)Instructions burned: 1759 (million) % 200.00/28.52 % (1956493)fmb+10_1_sil=64000:si=on:random_seed=555794569:i=44122:nm=2:rtra=on:gsp=on_2797 on theBenchmark for (2797ds/44122Mi) % 200.00/28.52 % (1956493)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 200.00/28.52 % Detected minimum model sizes of [1] % 200.00/28.52 % Detected maximum model sizes of [2] % 200.00/28.52 % TRYING [1] % 200.00/28.52 % TRYING [2] % 200.00/28.52 % Finite Model Found! % 200.00/28.52 % SZS status Satisfiable for theBenchmark % 200.00/28.52 % (1956493)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 200.00/28.52 % (1956493)------------------------------ % 200.00/28.52 % (1956493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.00/28.52 % (1956493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.00/28.52 % (1956493)CaDiCaL version: 2.1.3 % 200.00/28.52 % (1956493)Termination reason: Unknown % 200.00/28.52 % (1956493)Termination phase: Finite model building constraint generation % 200.00/28.52 % (1956493)Time elapsed: 0.001 s % 200.00/28.52 % (1956493)Peak memory usage: 10 MB % 200.00/28.52 % (1956493)Instructions burned: 2 (million) % 200.00/28.52 % (1956495)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1435931634:i=19030:nm=5:rtra=on_2797 on theBenchmark for (2797ds/19030Mi) % 200.00/28.52 % Detected minimum model sizes of [1] % 200.00/28.52 % Detected maximum model sizes of [2] % 200.00/28.52 % fmb_start_size (= 20) larger than a detected sort maximum size! % 200.00/28.52 % (1956495)Refutation not found, incomplete strategy % 200.00/28.52 % (1956495)------------------------------ % 200.00/28.52 % (1956495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.00/28.52 % (1956495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.00/28.52 % (1956495)CaDiCaL version: 2.1.3 % 200.00/28.52 % (1956495)Termination reason: Refutation not found, incomplete strategy % 200.00/28.52 % (1956495)Time elapsed: 0.001 s % 200.00/28.52 % (1956495)Peak memory usage: 11 MB % 200.00/28.52 % (1956495)Instructions burned: 2 (million) % 200.00/28.52 % (1956495)------------------------------ % 200.00/28.52 % (1956495)------------------------------ % 200.00/28.52 % (1956497)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=427846520:fmbsr=1.7:i=1840:rtra=on_2797 on theBenchmark for (2797ds/1840Mi) % 221.66/31.66 % Detected minimum model sizes of [1] % 221.66/31.66 % Detected maximum model sizes of [2] % 221.66/31.66 % fmb_start_size (= 8) larger than a detected sort maximum size! % 221.66/31.66 % (1956497)Refutation not found, incomplete strategy % 221.66/31.66 % (1956497)------------------------------ % 221.66/31.66 % (1956497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.66/31.66 % (1956497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.66/31.66 % (1956497)CaDiCaL version: 2.1.3 % 221.66/31.66 % (1956497)Termination reason: Refutation not found, incomplete strategy % 221.66/31.66 % (1956497)Time elapsed: 0.001 s % 221.66/31.66 % (1956497)Peak memory usage: 10 MB % 221.66/31.66 % (1956497)Instructions burned: 2 (million) % 221.66/31.66 % (1956497)------------------------------ % 221.66/31.66 % (1956497)------------------------------ % 221.66/31.66 % (1956499)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=362577944:i=10262:rtra=on_2796 on theBenchmark for (2796ds/10262Mi) % 221.66/31.66 % (1956499)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 221.66/31.66 % (1956499)Instruction limit reached! % 221.66/31.66 % (1956499)------------------------------ % 221.66/31.66 % (1956499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.66/31.66 % (1956499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.66/31.66 % (1956499)CaDiCaL version: 2.1.3 % 221.66/31.66 % (1956499)Termination reason: Instruction limit % 221.66/31.66 % (1956499)Termination phase: Saturation % 221.66/31.66 % (1956499)Time elapsed: 2.674 s % 221.66/31.66 % (1956499)Peak memory usage: 13 MB % 221.66/31.66 % (1956499)Instructions burned: 10262 (million) % 221.66/31.66 % (1956506)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3388741265:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2769 on theBenchmark for (2769ds/2944Mi) % 221.66/31.66 % (1956506)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 221.66/31.66 % (1956506)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 221.66/31.66 % (1956443)Instruction limit reached! % 221.66/31.66 % (1956443)------------------------------ % 221.66/31.66 % (1956443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.66/31.66 % (1956443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.66/31.66 % (1956443)CaDiCaL version: 2.1.3 % 221.66/31.66 % (1956443)Termination reason: Instruction limit % 221.66/31.66 % (1956443)Termination phase: Saturation % 221.66/31.66 % (1956443)Time elapsed: 10.031 s % 221.66/31.66 % (1956443)Peak memory usage: 15 MB % 221.66/31.66 % (1956443)Instructions burned: 28120 (million) % 221.66/31.66 % (1956510)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2310396095:i=12648:rtra=on_2765 on theBenchmark for (2765ds/12648Mi) % 221.66/31.66 % Detected minimum model sizes of [1] % 221.66/31.66 % Detected maximum model sizes of [2] % 221.66/31.66 % fmb_start_size (= 77) larger than a detected sort maximum size! % 221.66/31.66 % (1956510)Refutation not found, incomplete strategy % 221.66/31.66 % (1956510)------------------------------ % 221.66/31.66 % (1956510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.66/31.66 % (1956510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.66/31.66 % (1956510)CaDiCaL version: 2.1.3 % 221.66/31.66 % (1956510)Termination reason: Refutation not found, incomplete strategy % 221.66/31.66 % (1956510)Time elapsed: 0.001 s % 221.66/31.66 % (1956510)Peak memory usage: 10 MB % 221.66/31.66 % (1956510)Instructions burned: 2 (million) % 221.66/31.66 % (1956510)------------------------------ % 221.66/31.66 % (1956510)------------------------------ % 221.66/31.66 % (1956512)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=4064322376:fmbsr=2.30978:i=4348:rtra=on_2765 on theBenchmark for (2765ds/4348Mi) % 221.66/31.66 % TRYING [16] % 221.66/31.66 % Finite Model Found! % 221.66/31.66 % SZS status Satisfiable for theBenchmark % 221.66/31.66 % (1956512)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.66/31.66 % (1956512)------------------------------ % 221.66/31.66 % (1956512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.66/31.66 % (1956512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.66/31.66 % (1956512)CaDiCaL version: 2.1.3 % 221.66/31.66 % (1956512)Termination reason: Unknown % 270.04/38.41 % (1956512)Termination phase: Finite model building constraint generation % 270.04/38.41 % (1956512)Time elapsed: 0.003 s % 270.04/38.41 % (1956512)Peak memory usage: 11 MB % 270.04/38.41 % (1956512)Instructions burned: 6 (million) % 270.04/38.41 % (1956514)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=2341138962:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2765 on theBenchmark for (2765ds/1738Mi) % 270.04/38.41 % (1956514)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 270.04/38.41 % (1956514)Instruction limit reached! % 270.04/38.41 % (1956514)------------------------------ % 270.04/38.41 % (1956514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.04/38.41 % (1956514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.04/38.41 % (1956514)CaDiCaL version: 2.1.3 % 270.04/38.41 % (1956514)Termination reason: Instruction limit % 270.04/38.41 % (1956514)Termination phase: Saturation % 270.04/38.41 % (1956514)Time elapsed: 0.626 s % 270.04/38.41 % (1956514)Peak memory usage: 12 MB % 270.04/38.41 % (1956514)Instructions burned: 1740 (million) % 270.04/38.41 % (1956516)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1766139946:i=10228:av=off:rtra=on_2758 on theBenchmark for (2758ds/10228Mi) % 270.04/38.41 % (1956506)Instruction limit reached! % 270.04/38.41 % (1956506)------------------------------ % 270.04/38.41 % (1956506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.04/38.41 % (1956506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.04/38.41 % (1956506)CaDiCaL version: 2.1.3 % 270.04/38.41 % (1956506)Termination reason: Instruction limit % 270.04/38.41 % (1956506)Termination phase: Saturation % 270.04/38.41 % (1956506)Time elapsed: 1.446 s % 270.04/38.41 % (1956506)Peak memory usage: 13 MB % 270.04/38.41 % (1956506)Instructions burned: 2945 (million) % 270.04/38.41 % (1956518)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3032807071:i=108564:rtra=on_2755 on theBenchmark for (2755ds/108564Mi) % 270.04/38.41 % Detected minimum model sizes of [1] % 270.04/38.41 % Detected maximum model sizes of [2] % 270.04/38.41 % TRYING [1] % 270.04/38.41 % TRYING [2] % 270.04/38.41 % Finite Model Found! % 270.04/38.41 % SZS status Satisfiable for theBenchmark % 270.04/38.41 % (1956518)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 270.04/38.41 % (1956518)------------------------------ % 270.04/38.41 % (1956518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.04/38.41 % (1956518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.04/38.41 % (1956518)CaDiCaL version: 2.1.3 % 270.04/38.41 % (1956518)Termination reason: Unknown % 270.04/38.41 % (1956518)Termination phase: Finite model building constraint generation % 270.04/38.41 % (1956518)Time elapsed: 0.002 s % 270.04/38.41 % (1956518)Peak memory usage: 11 MB % 270.04/38.41 % (1956518)Instructions burned: 2 (million) % 270.04/38.41 % (1956520)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4204636522:i=7024:aac=none:rtra=on_2754 on theBenchmark for (2754ds/7024Mi) % 270.04/38.41 % (1956520)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 270.04/38.41 % (1956331)Instruction limit reached! % 270.04/38.41 % (1956331)------------------------------ % 270.04/38.41 % (1956331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.04/38.41 % (1956331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.04/38.41 % (1956331)CaDiCaL version: 2.1.3 % 270.04/38.41 % (1956331)Termination reason: Instruction limit % 270.04/38.41 % (1956331)Termination phase: Saturation % 270.04/38.41 % (1956331)Time elapsed: 28.185 s % 270.04/38.41 % (1956331)Peak memory usage: 14 MB % 270.04/38.41 % (1956331)Instructions burned: 88026 (million) % 270.04/38.41 % (1956527)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3806773130:i=7546:rtra=on:amm=off_2717 on theBenchmark for (2717ds/7546Mi) % 270.04/38.41 % (1956516)Instruction limit reached! % 270.04/38.41 % (1956516)------------------------------ % 270.04/38.41 % (1956516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.04/38.41 % (1956516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.04/38.41 % (1956516)CaDiCaL version: 2.1.3 % 270.04/38.41 % (1956516)Termination reason: Instruction limit % 270.04/38.41 % (1956516)Termination phase: Saturation % 270.04/38.41 % (1956516)Time elapsed: 4.110 s % 270.04/38.41 % (1956516)Peak memory usage: 11 MB % 270.04/38.41 % (1956516)Instructions burned: 10229 (million) % 270.04/38.41 % (1956529)ott+11_1_sil=16000:si=on:gs=on:random_seed=3368024601:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2717 on theBenchmark for (2717ds/4502Mi) % 300.60/42.74 % (1956529)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 300.60/42.74 % (1956520)Instruction limit reached! % 300.60/42.74 % (1956520)------------------------------ % 300.60/42.74 % (1956520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.60/42.74 % (1956520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/42.74 % (1956520)CaDiCaL version: 2.1.3 % 300.60/42.74 % (1956520)Termination reason: Instruction limit % 300.60/42.74 % (1956520)Termination phase: Saturation % 300.60/42.74 % (1956520)Time elapsed: 4.757 s % 300.60/42.74 % (1956520)Peak memory usage: 16 MB % 300.60/42.74 % (1956520)Instructions burned: 7025 (million) % 300.60/42.74 % (1956531)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1917733391:fmbsr=1.6:i=135068:rtra=on_2707 on theBenchmark for (2707ds/135068Mi) % 300.60/42.74 % Detected minimum model sizes of [1] % 300.60/42.74 % Detected maximum model sizes of [3] % 300.60/42.74 % fmb_start_size (= 7) larger than a detected sort maximum size! % 300.60/42.74 % (1956531)Refutation not found, incomplete strategy % 300.60/42.74 % (1956531)------------------------------ % 300.60/42.74 % (1956531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.60/42.74 % (1956531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/42.74 % (1956531)CaDiCaL version: 2.1.3 % 300.60/42.74 % (1956531)Termination reason: Refutation not found, incomplete strategy % 300.60/42.74 % (1956531)Time elapsed: 0.001 s % 300.60/42.74 % (1956531)Peak memory usage: 11 MB % 300.60/42.74 % (1956531)Instructions burned: 2 (million) % 300.60/42.74 % (1956531)------------------------------ % 300.60/42.74 % (1956531)------------------------------ % 300.60/42.74 % (1956533)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2001846928:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2706 on theBenchmark for (2706ds/9182Mi) % 300.60/42.74 % (1956529)Instruction limit reached! % 300.60/42.74 % (1956529)------------------------------ % 300.60/42.74 % (1956529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.60/42.74 % (1956529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/42.74 % (1956529)CaDiCaL version: 2.1.3 % 300.60/42.74 % (1956529)Termination reason: Instruction limit % 300.60/42.74 % (1956529)Termination phase: Saturation % 300.60/42.74 % (1956529)Time elapsed: 1.692 s % 300.60/42.74 % (1956529)Peak memory usage: 12 MB % 300.60/42.74 % (1956529)Instructions burned: 4505 (million) % 300.60/42.74 % (1956536)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=4230195474:i=58680:rtra=on_2700 on theBenchmark for (2700ds/58680Mi) % 300.60/42.74 % (1956438)Instruction limit reached! % 300.60/42.74 % (1956438)------------------------------ % 300.60/42.74 % (1956438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.60/42.74 % (1956438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/42.74 % (1956438)CaDiCaL version: 2.1.3 % 300.60/42.74 % (1956438)Termination reason: Instruction limit % 300.60/42.74 % (1956438)Termination phase: Saturation % 300.60/42.74 % (1956438)Time elapsed: 18.188 s % 300.60/42.74 % (1956438)Peak memory usage: 19 MB % 300.60/42.74 % (1956438)Instructions burned: 53296 (million) % 300.60/42.74 % (1956539)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=2105902365:i=10422:rtra=on_2689 on theBenchmark for (2689ds/10422Mi) % 300.60/42.74 % (1956527)Instruction limit reached! % 300.60/42.74 % (1956527)------------------------------ % 300.60/42.74 % (1956527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.60/42.74 % (1956527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/42.74 % (1956527)CaDiCaL version: 2.1.3 % 300.60/42.74 % (1956527)Termination reason: Instruction limit % 300.60/42.74 % (1956527)Termination phase: Saturation % 300.60/42.74 % (1956527)Time elapsed: 3.159 s % 300.60/42.74 % (1956527)Peak memory usage: 16 MB % 300.60/42.74 % (1956527)Instructions burned: 7547 (million) % 300.60/42.74 % (1956541)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=779722265:i=10994:nm=2:rtra=on_2686 on theBenchmark for (2686ds/10994Mi) % 300.60/42.74 % Detected minimum model sizes of [1] % 300.60/42.74 % Detected maximum model sizes of [2] % 300.60/42.74 % fmb_start_size (= 17) larger than a detected sort maximum size! % 300.60/42.74 % (1956541)Refutation not found, incomplete strategy % 300.60/42.74 % (1956541)------------------------------ % 300.60/42.74 % (1956541)Version: Vamp % 300.60/42.74 Terminated % 300.60/42.74 % Vampire exiting % 300.60/42.74 Terminated %------------------------------------------------------------------------------