%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM923_30 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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 12:26:04 PM UTC 2026 % Result : Timeout 297.90s 42.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM923_30 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/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 21:37:40 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.42 Running first-order model finding % 0.16/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 14.95/2.77 % (1803028)Will run a generic schedule for satisfiability detection. % 14.95/2.77 % (1803033)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1502987974_2998 on theBenchmark for (2998ds/0Mi) % 14.95/2.77 % (1803034)% WARNING: option uhcvi not known. % 14.95/2.77 % (1803036)dis+10_1_sil=32000:sp=arity:random_seed=2319257788:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 14.95/2.77 % (1803035)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=949905794:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 14.95/2.77 % (1803034)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3242983309:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 14.95/2.77 % (1803038)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=257899995:i=131_2998 on theBenchmark for (2998ds/131Mi) % 14.95/2.77 % (1803037)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1163125996:i=116_2998 on theBenchmark for (2998ds/116Mi) % 14.95/2.77 % (1803039)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3007258757:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 14.95/2.77 % (1803036)Instruction limit reached! % 14.95/2.77 % (1803036)------------------------------ % 14.95/2.77 % (1803036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.95/2.77 % (1803036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.95/2.77 % (1803036)CaDiCaL version: 2.1.3 % 14.95/2.77 % (1803036)Termination reason: Instruction limit % 14.95/2.77 % (1803036)Termination phase: Saturation % 14.95/2.77 % (1803036)Time elapsed: 0.061 s % 14.95/2.77 % (1803036)Peak memory usage: 13 MB % 14.95/2.77 % (1803036)Instructions burned: 103 (million) % 14.95/2.77 % (1803038)Instruction limit reached! % 14.95/2.77 % (1803038)------------------------------ % 14.95/2.77 % (1803038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.95/2.77 % (1803038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.95/2.77 % (1803038)CaDiCaL version: 2.1.3 % 14.95/2.77 % (1803038)Termination reason: Instruction limit % 14.95/2.77 % (1803038)Termination phase: Saturation % 14.95/2.77 % (1803038)Time elapsed: 0.075 s % 14.95/2.77 % (1803038)Peak memory usage: 14 MB % 14.95/2.77 % (1803038)Instructions burned: 131 (million) % 14.95/2.77 % (1803037)Instruction limit reached! % 14.95/2.77 % (1803037)------------------------------ % 14.95/2.77 % (1803037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.95/2.77 % (1803037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.95/2.77 % (1803037)CaDiCaL version: 2.1.3 % 14.95/2.77 % (1803037)Termination reason: Instruction limit % 14.95/2.77 % (1803037)Termination phase: Blocked clause elimination % 14.95/2.77 % (1803037)Time elapsed: 0.077 s % 14.95/2.77 % (1803037)Peak memory usage: 13 MB % 14.95/2.77 % (1803037)Instructions burned: 117 (million) % 14.95/2.77 % (1803047)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2552765647:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi) % 14.95/2.77 % (1803048)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1810153288:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 14.95/2.77 % (1803049)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=3147031912:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 14.95/2.77 % (1803039)Instruction limit reached! % 14.95/2.77 % (1803039)------------------------------ % 14.95/2.77 % (1803039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.95/2.77 % (1803039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.95/2.77 % (1803039)CaDiCaL version: 2.1.3 % 14.95/2.77 % (1803039)Termination reason: Instruction limit % 14.95/2.77 % (1803039)Termination phase: Saturation % 14.95/2.77 % (1803039)Time elapsed: 0.132 s % 14.95/2.77 % (1803039)Peak memory usage: 15 MB % 14.95/2.77 % (1803039)Instructions burned: 160 (million) % 14.95/2.77 % (1803053)ott-21_1_sil=16000:fs=off:random_seed=2843086436:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 14.95/2.77 % (1803048)Instruction limit reached! % 14.95/2.77 % (1803048)------------------------------ % 14.95/2.77 % (1803048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.95/2.77 % (1803048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.07/4.72 % (1803048)CaDiCaL version: 2.1.3 % 29.07/4.72 % (1803048)Termination reason: Instruction limit % 29.07/4.72 % (1803048)Termination phase: Property scanning % 29.07/4.72 % (1803048)Time elapsed: 0.058 s % 29.07/4.72 % (1803048)Peak memory usage: 13 MB % 29.07/4.72 % (1803048)Instructions burned: 133 (million) % 29.07/4.72 % (1803055)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4229166084:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 29.07/4.72 % (1803053)Instruction limit reached! % 29.07/4.72 % (1803053)------------------------------ % 29.07/4.72 % (1803053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.07/4.72 % (1803053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.07/4.72 % (1803053)CaDiCaL version: 2.1.3 % 29.07/4.72 % (1803053)Termination reason: Instruction limit % 29.07/4.72 % (1803053)Termination phase: Saturation % 29.07/4.72 % (1803053)Time elapsed: 0.083 s % 29.07/4.72 % (1803053)Peak memory usage: 14 MB % 29.07/4.72 % (1803053)Instructions burned: 181 (million) % 29.07/4.72 % (1803057)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1698743368:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 29.07/4.72 % (1803047)Instruction limit reached! % 29.07/4.72 % (1803047)------------------------------ % 29.07/4.72 % (1803047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.07/4.72 % (1803047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.07/4.72 % (1803047)CaDiCaL version: 2.1.3 % 29.07/4.72 % (1803047)Termination reason: Instruction limit % 29.07/4.72 % (1803047)Termination phase: Finite model building preprocessing % 29.07/4.72 % (1803047)Time elapsed: 0.344 s % 29.07/4.72 % (1803047)Peak memory usage: 23 MB % 29.07/4.72 % (1803047)Instructions burned: 715 (million) % 29.07/4.72 % (1803055)Instruction limit reached! % 29.07/4.72 % (1803055)------------------------------ % 29.07/4.72 % (1803055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.07/4.72 % (1803055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.07/4.72 % (1803055)CaDiCaL version: 2.1.3 % 29.07/4.72 % (1803055)Termination reason: Instruction limit % 29.07/4.72 % (1803055)Termination phase: Saturation % 29.07/4.72 % (1803055)Time elapsed: 0.273 s % 29.07/4.72 % (1803055)Peak memory usage: 16 MB % 29.07/4.72 % (1803055)Instructions burned: 478 (million) % 29.07/4.72 % (1803059)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3506731600:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 29.07/4.72 % (1803049)Instruction limit reached! % 29.07/4.72 % (1803049)------------------------------ % 29.07/4.72 % (1803049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.07/4.72 % (1803049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.07/4.72 % (1803049)CaDiCaL version: 2.1.3 % 29.07/4.72 % (1803049)Termination reason: Instruction limit % 29.07/4.72 % (1803049)Termination phase: Saturation % 29.07/4.72 % (1803049)Time elapsed: 0.362 s % 29.07/4.72 % (1803049)Peak memory usage: 18 MB % 29.07/4.72 % (1803049)Instructions burned: 684 (million) % 29.07/4.72 % (1803061)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1513883023:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 29.07/4.72 % (1803062)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=181374967:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi) % 29.07/4.72 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 29.07/4.72 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 29.07/4.72 % TRYING [1,1,1,1,1,1,1] % 29.07/4.72 % (1803057)Instruction limit reached! % 29.07/4.72 % (1803057)------------------------------ % 29.07/4.72 % (1803057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.07/4.72 % (1803057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.07/4.72 % (1803057)CaDiCaL version: 2.1.3 % 29.07/4.72 % (1803057)Termination reason: Instruction limit % 29.07/4.72 % (1803057)Termination phase: Finite model building preprocessing % 29.07/4.72 % (1803057)Time elapsed: 0.427 s % 29.07/4.72 % (1803057)Peak memory usage: 29 MB % 29.07/4.72 % (1803057)Instructions burned: 867 (million) % 29.07/4.72 % TRYING [1,1,1,1,1,2,1] % 29.07/4.72 % (1803065)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3999782883:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi) % 29.07/4.72 % TRYING [1,1,1,1,2,2,1] % 29.07/4.72 % TRYING [1,1,1,1,3,2,1] % 29.07/4.72 % TRYING [1,1,1,1,4,2,1] % 72.94/10.84 % TRYING [1,1,1,1,5,2,1] % 72.94/10.84 % (1803062)Instruction limit reached! % 72.94/10.84 % (1803062)------------------------------ % 72.94/10.84 % (1803062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.94/10.84 % (1803062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.94/10.84 % (1803062)CaDiCaL version: 2.1.3 % 72.94/10.84 % (1803062)Termination reason: Instruction limit % 72.94/10.84 % (1803062)Termination phase: Saturation % 72.94/10.84 % (1803062)Time elapsed: 0.413 s % 72.94/10.84 % (1803062)Peak memory usage: 17 MB % 72.94/10.84 % (1803062)Instructions burned: 693 (million) % 72.94/10.84 % (1803061)Instruction limit reached! % 72.94/10.84 % (1803061)------------------------------ % 72.94/10.84 % (1803061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.94/10.84 % (1803061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.94/10.84 % (1803061)CaDiCaL version: 2.1.3 % 72.94/10.84 % (1803061)Termination reason: Instruction limit % 72.94/10.84 % (1803061)Termination phase: Finite model building preprocessing % 72.94/10.84 % (1803061)Time elapsed: 0.442 s % 72.94/10.84 % (1803061)Peak memory usage: 30 MB % 72.94/10.84 % (1803061)Instructions burned: 890 (million) % 72.94/10.84 % (1803067)fmb+10_1_sil=64000:random_seed=3827562684:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi) % 72.94/10.84 % (1803068)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1943586895:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 72.94/10.84 % TRYING [1,1,2,1,5,2,1] % 72.94/10.84 % (1803059)Instruction limit reached! % 72.94/10.84 % (1803059)------------------------------ % 72.94/10.84 % (1803059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.94/10.84 % (1803059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.94/10.84 % (1803059)CaDiCaL version: 2.1.3 % 72.94/10.84 % (1803059)Termination reason: Instruction limit % 72.94/10.84 % (1803059)Termination phase: Saturation % 72.94/10.84 % (1803059)Time elapsed: 0.673 s % 72.94/10.84 % (1803059)Peak memory usage: 23 MB % 72.94/10.84 % (1803059)Instructions burned: 1181 (million) % 72.94/10.84 % (1803071)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3089386911:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 72.94/10.84 % (1803065)Instruction limit reached! % 72.94/10.84 % (1803065)------------------------------ % 72.94/10.84 % (1803065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.94/10.84 % (1803065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.94/10.84 % (1803065)CaDiCaL version: 2.1.3 % 72.94/10.84 % (1803065)Termination reason: Instruction limit % 72.94/10.84 % (1803065)Termination phase: Saturation % 72.94/10.84 % (1803065)Time elapsed: 0.474 s % 72.94/10.84 % (1803065)Peak memory usage: 19 MB % 72.94/10.84 % (1803065)Instructions burned: 881 (million) % 72.94/10.84 % (1803073)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4178550535:i=5131_2986 on theBenchmark for (2986ds/5131Mi) % 72.94/10.84 % TRYING [1,2,2,1,5,2,1] % 72.94/10.84 % (1803071)Instruction limit reached! % 72.94/10.84 % (1803071)------------------------------ % 72.94/10.84 % (1803071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.94/10.84 % (1803071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.94/10.84 % (1803071)CaDiCaL version: 2.1.3 % 72.94/10.84 % (1803071)Termination reason: Instruction limit % 72.94/10.84 % (1803071)Termination phase: Finite model building preprocessing % 72.94/10.84 % (1803071)Time elapsed: 0.457 s % 72.94/10.84 % (1803071)Peak memory usage: 30 MB % 72.94/10.84 % (1803071)Instructions burned: 922 (million) % 72.94/10.84 % (1803075)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=183635073:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi) % 72.94/10.84 % TRYING [2,2,2,1,5,2,1] % 72.94/10.84 % TRYING [2,2,2,1,5,2,2] % 72.94/10.84 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 72.94/10.84 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 72.94/10.84 % TRYING [1,1,1,1,1,1,1] % 72.94/10.84 % TRYING [1,1,1,1,1,2,1] % 72.94/10.84 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 72.94/10.84 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 72.94/10.84 % fmb_start_size (= 20) larger than a detected sort maximum size! % 72.94/10.84 % (1803068)Refutation not found, incomplete strategy % 72.94/10.84 % (1803068)------------------------------ % 72.94/10.84 % (1803068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.94/10.84 % (1803068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/17.08 % (1803068)CaDiCaL version: 2.1.3 % 117.33/17.08 % (1803068)Termination reason: Refutation not found, incomplete strategy % 117.33/17.08 % (1803068)Time elapsed: 1.254 s % 117.33/17.08 % (1803068)Peak memory usage: 42 MB % 117.33/17.08 % (1803068)Instructions burned: 2694 (million) % 117.33/17.08 % (1803068)------------------------------ % 117.33/17.08 % (1803068)------------------------------ % 117.33/17.08 % (1803077)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3812998576:i=6324_2976 on theBenchmark for (2976ds/6324Mi) % 117.33/17.08 % TRYING [1,1,1,1,2,2,1] % 117.33/17.08 % TRYING [1,1,1,1,3,2,1] % 117.33/17.08 % TRYING [2,2,2,2,5,2,2] % 117.33/17.08 % (1803075)Instruction limit reached! % 117.33/17.08 % (1803075)------------------------------ % 117.33/17.08 % (1803075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/17.08 % (1803075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/17.08 % (1803075)CaDiCaL version: 2.1.3 % 117.33/17.08 % (1803075)Termination reason: Instruction limit % 117.33/17.08 % (1803075)Termination phase: Saturation % 117.33/17.08 % (1803075)Time elapsed: 0.907 s % 117.33/17.08 % (1803075)Peak memory usage: 34 MB % 117.33/17.08 % (1803075)Instructions burned: 1472 (million) % 117.33/17.08 % (1803079)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1061754526:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi) % 117.33/17.08 % TRYING [1,1,1,1,4,2,1] % 117.33/17.08 % TRYING [2,2,2,3,5,2,2] % 117.33/17.08 % TRYING [2,2,3,3,5,2,2] % 117.33/17.08 % TRYING [1,1,1,1,5,2,1] % 117.33/17.08 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 117.33/17.08 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 117.33/17.08 % fmb_start_size (= 77) larger than a detected sort maximum size! % 117.33/17.08 % (1803077)Refutation not found, incomplete strategy % 117.33/17.08 % (1803077)------------------------------ % 117.33/17.08 % (1803077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/17.08 % (1803077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/17.08 % (1803077)CaDiCaL version: 2.1.3 % 117.33/17.08 % (1803077)Termination reason: Refutation not found, incomplete strategy % 117.33/17.08 % (1803077)Time elapsed: 1.311 s % 117.33/17.08 % (1803077)Peak memory usage: 42 MB % 117.33/17.08 % (1803077)Instructions burned: 2799 (million) % 117.33/17.08 % (1803077)------------------------------ % 117.33/17.08 % (1803077)------------------------------ % 117.33/17.08 % (1803081)ott-2_1_sil=16000:newcnf=on:random_seed=2214172061:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2963 on theBenchmark for (2963ds/869Mi) % 117.33/17.08 % (1803079)Instruction limit reached! % 117.33/17.08 % (1803079)------------------------------ % 117.33/17.08 % (1803079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/17.08 % (1803079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/17.08 % (1803079)CaDiCaL version: 2.1.3 % 117.33/17.08 % (1803079)Termination reason: Instruction limit % 117.33/17.08 % (1803079)Termination phase: Finite model building preprocessing % 117.33/17.08 % (1803079)Time elapsed: 1.081 s % 117.33/17.08 % (1803079)Peak memory usage: 45 MB % 117.33/17.08 % (1803079)Instructions burned: 2175 (million) % 117.33/17.08 % (1803083)ott+10_1_sil=32000:tgt=ground:random_seed=2874450161:i=5114:av=off_2962 on theBenchmark for (2962ds/5114Mi) % 117.33/17.08 % TRYING [2,2,2,3,6,2,2] % 117.33/17.08 % (1803081)Instruction limit reached! % 117.33/17.08 % (1803081)------------------------------ % 117.33/17.08 % (1803081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/17.08 % (1803081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/17.08 % (1803081)CaDiCaL version: 2.1.3 % 117.33/17.08 % (1803081)Termination reason: Instruction limit % 117.33/17.08 % (1803081)Termination phase: Saturation % 117.33/17.08 % (1803081)Time elapsed: 0.437 s % 117.33/17.08 % (1803081)Peak memory usage: 18 MB % 117.33/17.08 % (1803081)Instructions burned: 869 (million) % 117.33/17.08 % (1803085)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=467431725:i=54282_2958 on theBenchmark for (2958ds/54282Mi) % 117.33/17.08 % (1803073)Instruction limit reached! % 117.33/17.08 % (1803073)------------------------------ % 117.33/17.08 % (1803073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.33/17.08 % (1803073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.33/17.08 % (1803073)CaDiCaL version: 2.1.3 % 117.33/17.08 % (1803073)Termination reason: Instruction limit % 117.33/17.08 % (1803073)Termination phase: Saturation % 117.33/17.08 % (1803073)Time elapsed: 2.912 s % 117.33/17.08 % (1803073)Peak memory usage: 41 MB % 117.33/17.08 % (1803073)Instructions burned: 5133 (million) % 117.33/17.08 % (1803087)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3043467211:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi) % 212.47/30.54 % TRYING [1,1,1,1,6,2,1] % 212.47/30.54 % TRYING [2,2,4,3,5,2,2] % 212.47/30.54 % TRYING [2,3,2,3,6,2,2] % 212.47/30.54 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 212.47/30.54 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 212.47/30.54 % TRYING [1,1,1,1,1,1,1] % 212.47/30.54 % TRYING [1,1,1,1,1,2,1] % 212.47/30.54 % TRYING [1,1,1,1,2,2,1] % 212.47/30.54 % TRYING [1,1,1,1,3,2,1] % 212.47/30.54 % TRYING [1,1,1,1,4,2,1] % 212.47/30.54 % TRYING [1,1,1,1,5,2,1] % 212.47/30.54 % TRYING [2,3,3,3,6,2,2] % 212.47/30.54 % TRYING [1,1,2,1,5,2,1] % 212.47/30.54 % (1803087)Instruction limit reached! % 212.47/30.54 % (1803087)------------------------------ % 212.47/30.54 % (1803087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.47/30.54 % (1803087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.54 % (1803087)CaDiCaL version: 2.1.3 % 212.47/30.54 % (1803087)Termination reason: Instruction limit % 212.47/30.54 % (1803087)Termination phase: Saturation % 212.47/30.54 % (1803087)Time elapsed: 1.997 s % 212.47/30.54 % (1803087)Peak memory usage: 35 MB % 212.47/30.54 % (1803087)Instructions burned: 3513 (million) % 212.47/30.54 % (1803089)dis+21_1_sil=32000:sas=cadical:random_seed=2923073886:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi) % 212.47/30.54 % TRYING [1,1,1,1,7,2,1] % 212.47/30.54 % TRYING [1,2,2,1,5,2,1] % 212.47/30.54 % TRYING [2,3,2,3,7,2,2] % 212.47/30.54 % (1803083)Instruction limit reached! % 212.47/30.54 % (1803083)------------------------------ % 212.47/30.54 % (1803083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.47/30.54 % (1803083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.54 % (1803083)CaDiCaL version: 2.1.3 % 212.47/30.54 % (1803083)Termination reason: Instruction limit % 212.47/30.54 % (1803083)Termination phase: Saturation % 212.47/30.54 % (1803083)Time elapsed: 3.107 s % 212.47/30.54 % (1803083)Peak memory usage: 44 MB % 212.47/30.54 % (1803083)Instructions burned: 5115 (million) % 212.47/30.54 % (1803091)ott+11_1_sil=16000:gs=on:random_seed=4121286824:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2930 on theBenchmark for (2930ds/2251Mi) % 212.47/30.54 % TRYING [2,2,2,1,5,2,1] % 212.47/30.54 % TRYING [2,3,4,3,5,2,2] % 212.47/30.54 % TRYING [2,2,2,1,5,2,2] % 212.47/30.54 % (1803091)Instruction limit reached! % 212.47/30.54 % (1803091)------------------------------ % 212.47/30.54 % (1803091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.47/30.54 % (1803091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.54 % (1803091)CaDiCaL version: 2.1.3 % 212.47/30.54 % (1803091)Termination reason: Instruction limit % 212.47/30.54 % (1803091)Termination phase: Saturation % 212.47/30.54 % (1803091)Time elapsed: 1.417 s % 212.47/30.54 % (1803091)Peak memory usage: 35 MB % 212.47/30.54 % (1803091)Instructions burned: 2252 (million) % 212.47/30.54 % (1803093)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1769806367:fmbsr=1.6:i=67534_2916 on theBenchmark for (2916ds/67534Mi) % 212.47/30.54 % (1803089)Instruction limit reached! % 212.47/30.54 % (1803089)------------------------------ % 212.47/30.54 % (1803089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.47/30.54 % (1803089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.54 % (1803089)CaDiCaL version: 2.1.3 % 212.47/30.54 % (1803089)Termination reason: Instruction limit % 212.47/30.54 % (1803089)Termination phase: Saturation % 212.47/30.54 % (1803089)Time elapsed: 2.144 s % 212.47/30.54 % (1803089)Peak memory usage: 36 MB % 212.47/30.54 % (1803089)Instructions burned: 3775 (million) % 212.47/30.54 % (1803095)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3227399335:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi) % 212.47/30.54 % TRYING [2,2,2,2,5,2,2] % 212.47/30.54 % TRYING [2,2,4,3,6,2,2] % 212.47/30.54 % TRYING [2,2,2,3,5,2,2] % 212.47/30.54 % TRYING [2,2,3,3,5,2,2] % 212.47/30.54 % TRYING [2,4,4,3,5,2,2] % 212.47/30.54 % (1803095)Instruction limit reached! % 212.47/30.54 % (1803095)------------------------------ % 212.47/30.54 % (1803095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 212.47/30.54 % (1803095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.54 % (1803095)CaDiCaL version: 2.1.3 % 212.47/30.54 % (1803095)Termination reason: Instruction limit % 212.47/30.54 % (1803095)Termination phase: Saturation % 212.47/30.54 % (1803095)Time elapsed: 1.905 s % 212.47/30.54 % (1803095)Peak memory usage: 29 MB % 212.47/30.54 % (1803095)Instructions burned: 4592 (million) % 212.47/30.54 % (1803097)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2621687655:i=29340_2896 on theBenchmark for (2896ds/29340Mi) % 297.90/42.58 % (1803067)Instruction limit reached! % 297.90/42.58 % (1803067)------------------------------ % 297.90/42.58 % (1803067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.90/42.58 % (1803067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.90/42.58 % (1803067)CaDiCaL version: 2.1.3 % 297.90/42.58 % (1803067)Termination reason: Instruction limit % 297.90/42.58 % (1803067)Termination phase: Finite model building constraint generation % 297.90/42.58 % (1803067)Time elapsed: 9.667 s % 297.90/42.58 % (1803067)Peak memory usage: 203 MB % 297.90/42.58 % (1803067)Instructions burned: 22062 (million) % 297.90/42.58 % (1803099)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3357977221:i=5211_2892 on theBenchmark for (2892ds/5211Mi) % 297.90/42.58 % TRYING [2,2,2,3,6,2,2] % 297.90/42.58 % TRYING [3,4,4,3,5,2,2] % 297.90/42.58 % TRYING [2,2,4,3,5,2,2] % 297.90/42.58 % TRYING [4,4,4,3,5,2,2] % 297.90/42.58 % (1803099)Instruction limit reached! % 297.90/42.58 % (1803099)------------------------------ % 297.90/42.58 % (1803099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.90/42.58 % (1803099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.90/42.58 % (1803099)CaDiCaL version: 2.1.3 % 297.90/42.58 % (1803099)Termination reason: Instruction limit % 297.90/42.58 % (1803099)Termination phase: Saturation % 297.90/42.58 % (1803099)Time elapsed: 2.771 s % 297.90/42.58 % (1803099)Peak memory usage: 49 MB % 297.90/42.58 % (1803099)Instructions burned: 5213 (million) % 297.90/42.58 % (1803101)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2428833522:i=5497:nm=2_2864 on theBenchmark for (2864ds/5497Mi) % 297.90/42.58 % TRYING [2,3,2,3,6,2,2] % 297.90/42.58 % TRYING [3,5,4,3,5,2,2] % 297.90/42.58 % TRYING [2,3,3,3,6,2,2] % 297.90/42.58 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 297.90/42.58 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 297.90/42.58 % fmb_start_size (= 17) larger than a detected sort maximum size! % 297.90/42.58 % (1803101)Refutation not found, incomplete strategy % 297.90/42.58 % (1803101)------------------------------ % 297.90/42.58 % (1803101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.90/42.58 % (1803101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.90/42.58 % (1803101)CaDiCaL version: 2.1.3 % 297.90/42.58 % (1803101)Termination reason: Refutation not found, incomplete strategy % 297.90/42.58 % (1803101)Time elapsed: 1.201 s % 297.90/42.58 % (1803101)Peak memory usage: 41 MB % 297.90/42.58 % (1803101)Instructions burned: 2604 (million) % 297.90/42.58 % (1803101)------------------------------ % 297.90/42.58 % (1803101)------------------------------ % 297.90/42.58 % (1803103)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=432641370:fmbsr=2:i=46332_2852 on theBenchmark for (2852ds/46332Mi) % 297.90/42.58 % (1803103)Cannot represent all propositional literals internally % 297.90/42.58 % (1803103)Refutation not found, incomplete strategy % 297.90/42.58 % (1803103)------------------------------ % 297.90/42.58 % (1803103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.90/42.58 % (1803103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.90/42.58 % (1803103)CaDiCaL version: 2.1.3 % 297.90/42.58 % (1803103)Termination reason: Refutation not found, incomplete strategy % 297.90/42.58 % (1803103)Time elapsed: 0.521 s % 297.90/42.58 % (1803103)Peak memory usage: 28 MB % 297.90/42.58 % (1803103)Instructions burned: 1094 (million) % 297.90/42.58 % (1803103)------------------------------ % 297.90/42.58 % (1803103)------------------------------ % 297.90/42.58 % (1803105)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=443884493:i=14071_2846 on theBenchmark for (2846ds/14071Mi) % 297.90/42.58 % TRYING [2,3,4,3,6,2,2] % 297.90/42.58 % TRYING [2,3,2,3,7,2,2] % 297.90/42.58 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 297.90/42.58 % Detected maximum model sizes of [max,max,max,max,max,2,max] % 297.90/42.58 % fmb_start_size (= 12) larger than a detected sort maximum size! % 297.90/42.58 % (1803105)Refutation not found, incomplete strategy % 297.90/42.58 % (1803105)------------------------------ % 297.90/42.58 % (1803105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 297.90/42.58 % (1803105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.90/42.58 % (1803105)CaDiCaL version: 2.1.3 % 297.90/42.58 % (1803105)Termination reason: Refutation not found, incomplete strategy % 297.90/42.58 % (1803105)Time elapsed: 1.290 s % 297.90/42.58 % (1803105)Peak memory usage: 42 MB % 297.90/42.58 % (1803105)Instructions burned: 2796 (million) % 297.90/42.58 % (1803105)------------------------------ % 297.90/42.58 % (1803105Terminated % 300.04/42.93 % Vampire exiting % 300.04/42.93 Terminated %------------------------------------------------------------------------------