%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM875_1 : TPTP v9.3.1. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:25:59 PM UTC 2026 % Result : Timeout 300.42s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM875_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.60 % Computer : n006.cluster.edu % 0.10/0.60 % Model : x86_64 x86_64 % 0.10/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.60 % Memory : 8046.5625MB % 0.10/0.60 % OS : Linux 6.8.0-71-generic % 0.10/0.60 % CPULimit : 300 % 0.10/0.60 % WCLimit : 300 % 0.10/0.60 % DateTime : Sun Sep 27 21:37:11 UTC 2026 % 0.10/0.60 % CPUTime : % 0.10/0.60 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.15/0.63 Running first-order model finding % 0.15/0.63 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.76/1.08 % (3337589)Will run a generic schedule for satisfiability detection. % 2.76/1.08 % (3337595)% WARNING: option uhcvi not known. % 2.76/1.08 % (3337594)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1811652982_2999 on theBenchmark for (2999ds/0Mi) % 2.76/1.08 % (3337595)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=165926668:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 2.76/1.08 % (3337596)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3901754798:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 2.76/1.08 % (3337597)dis+10_1_sil=32000:sp=arity:random_seed=1291182985:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 2.76/1.08 % (3337598)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1449771567:i=116_2999 on theBenchmark for (2999ds/116Mi) % 2.76/1.08 % (3337599)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3059211839:i=131_2999 on theBenchmark for (2999ds/131Mi) % 2.76/1.08 % (3337600)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2704618949:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 2.76/1.08 % (3337594)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.76/1.08 % (3337594)Terminated due to inappropriate strategy. % 2.76/1.08 % (3337594)------------------------------ % 2.76/1.08 % (3337594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.76/1.08 % (3337594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.76/1.08 % (3337594)CaDiCaL version: 2.1.3 % 2.76/1.08 % (3337594)Termination reason: Inappropriate % 2.76/1.08 % (3337594)Time elapsed: 0.0000 s % 2.76/1.08 % (3337594)Peak memory usage: 10 MB % 2.76/1.08 % (3337594)------------------------------ % 2.76/1.08 % (3337594)------------------------------ % 2.76/1.08 % (3337608)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=618692044:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 2.76/1.08 % (3337608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 2.76/1.08 % (3337608)Terminated due to inappropriate strategy. % 2.76/1.08 % (3337608)------------------------------ % 2.76/1.08 % (3337608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.76/1.08 % (3337608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.76/1.08 % (3337608)CaDiCaL version: 2.1.3 % 2.76/1.08 % (3337608)Termination reason: Inappropriate % 2.76/1.08 % (3337608)Time elapsed: 0.0000 s % 2.76/1.08 % (3337608)Peak memory usage: 10 MB % 2.76/1.08 % (3337608)------------------------------ % 2.76/1.08 % (3337608)------------------------------ % 2.76/1.08 % (3337610)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1904780604:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 2.76/1.08 % (3337597)Instruction limit reached! % 2.76/1.08 % (3337597)------------------------------ % 2.76/1.08 % (3337597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.76/1.08 % (3337597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.76/1.08 % (3337597)CaDiCaL version: 2.1.3 % 2.76/1.08 % (3337597)Termination reason: Instruction limit % 2.76/1.08 % (3337597)Termination phase: Saturation % 2.76/1.08 % (3337597)Time elapsed: 0.065 s % 2.76/1.08 % (3337597)Peak memory usage: 12 MB % 2.76/1.08 % (3337597)Instructions burned: 104 (million) % 2.76/1.08 % (3337598)Instruction limit reached! % 2.76/1.08 % (3337598)------------------------------ % 2.76/1.08 % (3337598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.76/1.08 % (3337598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.76/1.08 % (3337598)CaDiCaL version: 2.1.3 % 2.76/1.08 % (3337598)Termination reason: Instruction limit % 2.76/1.08 % (3337598)Termination phase: Saturation % 2.76/1.08 % (3337598)Time elapsed: 0.069 s % 2.76/1.08 % (3337598)Peak memory usage: 12 MB % 2.76/1.08 % (3337598)Instructions burned: 116 (million) % 2.76/1.08 % (3337599)Instruction limit reached! % 2.76/1.08 % (3337599)------------------------------ % 2.76/1.08 % (3337599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 2.76/1.08 % (3337599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 2.76/1.08 % (3337599)CaDiCaL version: 2.1.3 % 2.76/1.08 % (3337599)Termination reason: Instruction limit % 2.76/1.08 % (3337599)Termination phase: Saturation % 2.76/1.08 % (3337599)Time elapsed: 0.080 s % 4.74/1.55 % (3337599)Peak memory usage: 12 MB % 4.74/1.55 % (3337599)Instructions burned: 132 (million) % 4.74/1.55 % (3337612)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=2886221368:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.74/1.55 % (3337613)ott-21_1_sil=16000:fs=off:random_seed=3020500596:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 4.74/1.55 % (3337614)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3497628529:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 4.74/1.55 % (3337600)Instruction limit reached! % 4.74/1.55 % (3337600)------------------------------ % 4.74/1.55 % (3337600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.74/1.55 % (3337600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.74/1.55 % (3337600)CaDiCaL version: 2.1.3 % 4.74/1.55 % (3337600)Termination reason: Instruction limit % 4.74/1.55 % (3337600)Termination phase: Saturation % 4.74/1.55 % (3337600)Time elapsed: 0.102 s % 4.74/1.55 % (3337600)Peak memory usage: 13 MB % 4.74/1.55 % (3337600)Instructions burned: 159 (million) % 4.74/1.55 % (3337618)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2302799307:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 4.74/1.55 % (3337618)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.74/1.55 % (3337618)Terminated due to inappropriate strategy. % 4.74/1.55 % (3337618)------------------------------ % 4.74/1.55 % (3337618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.74/1.55 % (3337618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.74/1.55 % (3337618)CaDiCaL version: 2.1.3 % 4.74/1.55 % (3337618)Termination reason: Inappropriate % 4.74/1.55 % (3337618)Time elapsed: 0.0000 s % 4.74/1.55 % (3337618)Peak memory usage: 10 MB % 4.74/1.55 % (3337618)------------------------------ % 4.74/1.55 % (3337618)------------------------------ % 4.74/1.55 % (3337610)Instruction limit reached! % 4.74/1.55 % (3337610)------------------------------ % 4.74/1.55 % (3337610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.74/1.55 % (3337610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.74/1.55 % (3337610)CaDiCaL version: 2.1.3 % 4.74/1.55 % (3337610)Termination reason: Instruction limit % 4.74/1.55 % (3337610)Termination phase: Saturation % 4.74/1.55 % (3337610)Time elapsed: 0.086 s % 4.74/1.55 % (3337610)Peak memory usage: 12 MB % 4.74/1.55 % (3337610)Instructions burned: 132 (million) % 4.74/1.55 % (3337620)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2571619146:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 4.74/1.55 % (3337621)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3123135134:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 4.74/1.55 % (3337621)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.74/1.55 % (3337621)Terminated due to inappropriate strategy. % 4.74/1.55 % (3337621)------------------------------ % 4.74/1.55 % (3337621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.74/1.55 % (3337621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.74/1.55 % (3337621)CaDiCaL version: 2.1.3 % 4.74/1.55 % (3337621)Termination reason: Inappropriate % 4.74/1.55 % (3337621)Time elapsed: 0.0000 s % 4.74/1.55 % (3337621)Peak memory usage: 10 MB % 4.74/1.55 % (3337621)------------------------------ % 4.74/1.55 % (3337621)------------------------------ % 4.74/1.55 % (3337624)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=1034661539: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) % 4.74/1.55 % (3337613)Instruction limit reached! % 4.74/1.55 % (3337613)------------------------------ % 4.74/1.55 % (3337613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.74/1.55 % (3337613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.74/1.55 % (3337613)CaDiCaL version: 2.1.3 % 4.74/1.55 % (3337613)Termination reason: Instruction limit % 4.74/1.55 % (3337613)Termination phase: Saturation % 4.74/1.55 % (3337613)Time elapsed: 0.079 s % 4.74/1.55 % (3337613)Peak memory usage: 12 MB % 4.74/1.55 % (3337613)Instructions burned: 180 (million) % 4.74/1.55 % (3337626)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=639475811:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 22.20/3.80 % (3337624)Instruction limit reached! % 22.20/3.80 % (3337624)------------------------------ % 22.20/3.80 % (3337624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.20/3.80 % (3337624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.80 % (3337624)CaDiCaL version: 2.1.3 % 22.20/3.80 % (3337624)Termination reason: Instruction limit % 22.20/3.80 % (3337624)Termination phase: Saturation % 22.20/3.80 % (3337624)Time elapsed: 0.196 s % 22.20/3.80 % (3337624)Peak memory usage: 15 MB % 22.20/3.80 % (3337624)Instructions burned: 696 (million) % 22.20/3.80 % (3337628)fmb+10_1_sil=64000:random_seed=2549957510:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 22.20/3.80 % (3337628)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.20/3.80 % (3337628)Terminated due to inappropriate strategy. % 22.20/3.80 % (3337628)------------------------------ % 22.20/3.80 % (3337628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.20/3.80 % (3337628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.80 % (3337628)CaDiCaL version: 2.1.3 % 22.20/3.80 % (3337628)Termination reason: Inappropriate % 22.20/3.80 % (3337628)Time elapsed: 0.0000 s % 22.20/3.80 % (3337628)Peak memory usage: 10 MB % 22.20/3.80 % (3337628)------------------------------ % 22.20/3.80 % (3337628)------------------------------ % 22.20/3.80 % (3337630)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=725998884:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 22.20/3.80 % (3337630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.20/3.80 % (3337630)Terminated due to inappropriate strategy. % 22.20/3.80 % (3337630)------------------------------ % 22.20/3.80 % (3337630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.20/3.80 % (3337630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.80 % (3337630)CaDiCaL version: 2.1.3 % 22.20/3.80 % (3337630)Termination reason: Inappropriate % 22.20/3.80 % (3337630)Time elapsed: 0.0000 s % 22.20/3.80 % (3337630)Peak memory usage: 10 MB % 22.20/3.80 % (3337630)------------------------------ % 22.20/3.80 % (3337630)------------------------------ % 22.20/3.80 % (3337614)Instruction limit reached! % 22.20/3.80 % (3337614)------------------------------ % 22.20/3.80 % (3337614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.20/3.80 % (3337614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.80 % (3337614)CaDiCaL version: 2.1.3 % 22.20/3.80 % (3337614)Termination reason: Instruction limit % 22.20/3.80 % (3337614)Termination phase: Saturation % 22.20/3.80 % (3337614)Time elapsed: 0.291 s % 22.20/3.80 % (3337614)Peak memory usage: 14 MB % 22.20/3.80 % (3337614)Instructions burned: 478 (million) % 22.20/3.80 % (3337632)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3461713081:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.20/3.80 % (3337632)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 22.20/3.80 % (3337632)Terminated due to inappropriate strategy. % 22.20/3.80 % (3337632)------------------------------ % 22.20/3.80 % (3337632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.20/3.80 % (3337632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.80 % (3337632)CaDiCaL version: 2.1.3 % 22.20/3.80 % (3337632)Termination reason: Inappropriate % 22.20/3.80 % (3337632)Time elapsed: 0.0000 s % 22.20/3.80 % (3337632)Peak memory usage: 10 MB % 22.20/3.80 % (3337632)------------------------------ % 22.20/3.80 % (3337632)------------------------------ % 22.20/3.80 % (3337633)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=639578697:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 22.20/3.80 % (3337635)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2788959702:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 22.20/3.80 % (3337612)Instruction limit reached! % 22.20/3.80 % (3337612)------------------------------ % 22.20/3.80 % (3337612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.20/3.80 % (3337612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.80 % (3337612)CaDiCaL version: 2.1.3 % 22.20/3.80 % (3337612)Termination reason: Instruction limit % 26.94/4.57 % (3337612)Termination phase: Saturation % 26.94/4.57 % (3337612)Time elapsed: 0.333 s % 26.94/4.57 % (3337612)Peak memory usage: 14 MB % 26.94/4.57 % (3337612)Instructions burned: 685 (million) % 26.94/4.57 % (3337638)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2921940202:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 26.94/4.57 % (3337638)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.94/4.57 % (3337638)Terminated due to inappropriate strategy. % 26.94/4.57 % (3337638)------------------------------ % 26.94/4.57 % (3337638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.94/4.57 % (3337638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.57 % (3337638)CaDiCaL version: 2.1.3 % 26.94/4.57 % (3337638)Termination reason: Inappropriate % 26.94/4.57 % (3337638)Time elapsed: 0.0000 s % 26.94/4.57 % (3337638)Peak memory usage: 10 MB % 26.94/4.57 % (3337638)------------------------------ % 26.94/4.57 % (3337638)------------------------------ % 26.94/4.57 % (3337640)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3441657661:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 26.94/4.57 % (3337640)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.94/4.57 % (3337640)Terminated due to inappropriate strategy. % 26.94/4.57 % (3337640)------------------------------ % 26.94/4.57 % (3337640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.94/4.57 % (3337640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.57 % (3337640)CaDiCaL version: 2.1.3 % 26.94/4.57 % (3337640)Termination reason: Inappropriate % 26.94/4.57 % (3337640)Time elapsed: 0.0000 s % 26.94/4.57 % (3337640)Peak memory usage: 10 MB % 26.94/4.57 % (3337640)------------------------------ % 26.94/4.57 % (3337640)------------------------------ % 26.94/4.57 % (3337642)ott-2_1_sil=16000:newcnf=on:random_seed=4269326662:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 26.94/4.57 % (3337626)Instruction limit reached! % 26.94/4.57 % (3337626)------------------------------ % 26.94/4.57 % (3337626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.94/4.57 % (3337626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.57 % (3337626)CaDiCaL version: 2.1.3 % 26.94/4.57 % (3337626)Termination reason: Instruction limit % 26.94/4.57 % (3337626)Termination phase: Saturation % 26.94/4.57 % (3337626)Time elapsed: 0.500 s % 26.94/4.57 % (3337626)Peak memory usage: 18 MB % 26.94/4.57 % (3337626)Instructions burned: 880 (million) % 26.94/4.57 % (3337644)ott+10_1_sil=32000:tgt=ground:random_seed=2159956073:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 26.94/4.57 % (3337620)Instruction limit reached! % 26.94/4.57 % (3337620)------------------------------ % 26.94/4.57 % (3337620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.94/4.57 % (3337620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.57 % (3337620)CaDiCaL version: 2.1.3 % 26.94/4.57 % (3337620)Termination reason: Instruction limit % 26.94/4.57 % (3337620)Termination phase: Saturation % 26.94/4.57 % (3337620)Time elapsed: 0.723 s % 26.94/4.57 % (3337620)Peak memory usage: 16 MB % 26.94/4.57 % (3337620)Instructions burned: 1180 (million) % 26.94/4.57 % (3337635)Instruction limit reached! % 26.94/4.57 % (3337635)------------------------------ % 26.94/4.57 % (3337635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.94/4.57 % (3337635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.57 % (3337635)CaDiCaL version: 2.1.3 % 26.94/4.57 % (3337635)Termination reason: Instruction limit % 26.94/4.57 % (3337635)Termination phase: Saturation % 26.94/4.57 % (3337635)Time elapsed: 0.456 s % 26.94/4.57 % (3337635)Peak memory usage: 24 MB % 26.94/4.57 % (3337635)Instructions burned: 1473 (million) % 26.94/4.57 % (3337647)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=859041566:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 26.94/4.57 % (3337646)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1327127496:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 26.94/4.57 % (3337646)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.94/4.57 % (3337646)Terminated due to inappropriate strategy. % 26.94/4.57 % (3337646)------------------------------ % 26.94/4.57 % (3337646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.94/4.57 % (3337646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.18 % (3337646)CaDiCaL version: 2.1.3 % 103.06/15.18 % (3337646)Termination reason: Inappropriate % 103.06/15.18 % (3337646)Time elapsed: 0.0000 s % 103.06/15.18 % (3337646)Peak memory usage: 10 MB % 103.06/15.18 % (3337646)------------------------------ % 103.06/15.18 % (3337646)------------------------------ % 103.06/15.18 % (3337650)dis+21_1_sil=32000:sas=cadical:random_seed=2517813654:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 103.06/15.18 % (3337642)Instruction limit reached! % 103.06/15.18 % (3337642)------------------------------ % 103.06/15.18 % (3337642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.06/15.18 % (3337642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.18 % (3337642)CaDiCaL version: 2.1.3 % 103.06/15.18 % (3337642)Termination reason: Instruction limit % 103.06/15.18 % (3337642)Termination phase: Saturation % 103.06/15.18 % (3337642)Time elapsed: 0.546 s % 103.06/15.18 % (3337642)Peak memory usage: 15 MB % 103.06/15.18 % (3337642)Instructions burned: 869 (million) % 103.06/15.18 % (3337652)ott+11_1_sil=16000:gs=on:random_seed=2272436622:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi) % 103.06/15.18 % (3337647)Instruction limit reached! % 103.06/15.18 % (3337647)------------------------------ % 103.06/15.18 % (3337647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.06/15.18 % (3337647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.18 % (3337647)CaDiCaL version: 2.1.3 % 103.06/15.18 % (3337647)Termination reason: Instruction limit % 103.06/15.18 % (3337647)Termination phase: Saturation % 103.06/15.18 % (3337647)Time elapsed: 0.974 s % 103.06/15.18 % (3337647)Peak memory usage: 29 MB % 103.06/15.18 % (3337647)Instructions burned: 3514 (million) % 103.06/15.18 % (3337654)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3863212997:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 103.06/15.18 % (3337654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 103.06/15.18 % (3337654)Terminated due to inappropriate strategy. % 103.06/15.18 % (3337654)------------------------------ % 103.06/15.18 % (3337654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.06/15.18 % (3337654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.18 % (3337654)CaDiCaL version: 2.1.3 % 103.06/15.18 % (3337654)Termination reason: Inappropriate % 103.06/15.18 % (3337654)Time elapsed: 0.0000 s % 103.06/15.18 % (3337654)Peak memory usage: 10 MB % 103.06/15.18 % (3337654)------------------------------ % 103.06/15.18 % (3337654)------------------------------ % 103.06/15.18 % (3337656)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1190835024:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 103.06/15.18 % (3337652)Instruction limit reached! % 103.06/15.18 % (3337652)------------------------------ % 103.06/15.18 % (3337652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.06/15.18 % (3337652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.18 % (3337652)CaDiCaL version: 2.1.3 % 103.06/15.18 % (3337652)Termination reason: Instruction limit % 103.06/15.18 % (3337652)Termination phase: Saturation % 103.06/15.18 % (3337652)Time elapsed: 1.237 s % 103.06/15.18 % (3337652)Peak memory usage: 21 MB % 103.06/15.18 % (3337652)Instructions burned: 2252 (million) % 103.06/15.18 % (3337658)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1262554677:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 103.06/15.18 % (3337650)Instruction limit reached! % 103.06/15.18 % (3337650)------------------------------ % 103.06/15.18 % (3337650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.06/15.18 % (3337650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.18 % (3337650)CaDiCaL version: 2.1.3 % 103.06/15.18 % (3337650)Termination reason: Instruction limit % 103.06/15.18 % (3337650)Termination phase: Saturation % 103.06/15.18 % (3337650)Time elapsed: 2.0000 s % 103.06/15.18 % (3337650)Peak memory usage: 29 MB % 103.06/15.18 % (3337650)Instructions burned: 3774 (million) % 103.06/15.18 % (3337660)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1325756074:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 103.06/15.18 % (3337633)Instruction limit reached! % 103.06/15.18 % (3337633)------------------------------ % 103.06/15.18 % (3337633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.89/16.98 % (3337633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/16.98 % (3337633)CaDiCaL version: 2.1.3 % 114.89/16.98 % (3337633)Termination reason: Instruction limit % 114.89/16.98 % (3337633)Termination phase: Saturation % 114.89/16.98 % (3337633)Time elapsed: 2.728 s % 114.89/16.98 % (3337633)Peak memory usage: 39 MB % 114.89/16.98 % (3337633)Instructions burned: 5132 (million) % 114.89/16.98 % (3337662)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1951402806:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 114.89/16.98 % (3337662)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.89/16.98 % (3337662)Terminated due to inappropriate strategy. % 114.89/16.98 % (3337662)------------------------------ % 114.89/16.98 % (3337662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.89/16.98 % (3337662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/16.98 % (3337662)CaDiCaL version: 2.1.3 % 114.89/16.98 % (3337662)Termination reason: Inappropriate % 114.89/16.98 % (3337662)Time elapsed: 0.0000 s % 114.89/16.98 % (3337662)Peak memory usage: 10 MB % 114.89/16.98 % (3337662)------------------------------ % 114.89/16.98 % (3337662)------------------------------ % 114.89/16.98 % (3337664)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2134281882:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 114.89/16.98 % (3337664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.89/16.98 % (3337664)Terminated due to inappropriate strategy. % 114.89/16.98 % (3337664)------------------------------ % 114.89/16.98 % (3337664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.89/16.98 % (3337664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/16.98 % (3337664)CaDiCaL version: 2.1.3 % 114.89/16.98 % (3337664)Termination reason: Inappropriate % 114.89/16.98 % (3337664)Time elapsed: 0.0000 s % 114.89/16.98 % (3337664)Peak memory usage: 10 MB % 114.89/16.98 % (3337664)------------------------------ % 114.89/16.98 % (3337664)------------------------------ % 114.89/16.98 % (3337666)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1035149683:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 114.89/16.98 % (3337666)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 114.89/16.98 % (3337666)Terminated due to inappropriate strategy. % 114.89/16.98 % (3337666)------------------------------ % 114.89/16.98 % (3337666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.89/16.98 % (3337666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/16.98 % (3337666)CaDiCaL version: 2.1.3 % 114.89/16.98 % (3337666)Termination reason: Inappropriate % 114.89/16.98 % (3337666)Time elapsed: 0.0000 s % 114.89/16.98 % (3337666)Peak memory usage: 10 MB % 114.89/16.98 % (3337666)------------------------------ % 114.89/16.98 % (3337666)------------------------------ % 114.89/16.98 % (3337668)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4063069184:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 114.89/16.98 % (3337656)Instruction limit reached! % 114.89/16.98 % (3337656)------------------------------ % 114.89/16.98 % (3337656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.89/16.98 % (3337656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/16.98 % (3337656)CaDiCaL version: 2.1.3 % 114.89/16.98 % (3337656)Termination reason: Instruction limit % 114.89/16.98 % (3337656)Termination phase: Saturation % 114.89/16.98 % (3337656)Time elapsed: 1.493 s % 114.89/16.98 % (3337656)Peak memory usage: 46 MB % 114.89/16.98 % (3337656)Instructions burned: 4593 (million) % 114.89/16.98 % (3337670)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2352264884:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 114.89/16.98 % (3337644)Instruction limit reached! % 114.89/16.98 % (3337644)------------------------------ % 114.89/16.98 % (3337644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.89/16.98 % (3337644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.89/16.98 % (3337644)CaDiCaL version: 2.1.3 % 114.89/16.98 % (3337644)Termination reason: Instruction limit % 114.89/16.98 % (3337644)Termination phase: Saturation % 114.89/16.98 % (3337644)Time elapsed: 3.176 s % 114.89/16.98 % (3337644)Peak memory usage: 29 MB % 114.89/16.98 % (3337644)Instructions burned: 5115 (million) % 114.89/16.98 % (3337672)dis+10_16:1_sil=16000:random_seed=3919014533:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 182.35/26.34 % (3337660)Instruction limit reached! % 182.35/26.34 % (3337660)------------------------------ % 182.35/26.34 % (3337660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.35/26.34 % (3337660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.35/26.34 % (3337660)CaDiCaL version: 2.1.3 % 182.35/26.34 % (3337660)Termination reason: Instruction limit % 182.35/26.34 % (3337660)Termination phase: Saturation % 182.35/26.34 % (3337660)Time elapsed: 2.775 s % 182.35/26.34 % (3337660)Peak memory usage: 48 MB % 182.35/26.34 % (3337660)Instructions burned: 5211 (million) % 182.35/26.34 % (3337674)ott-3_8_sil=64000:random_seed=1990024453:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 182.35/26.34 % (3337670)Instruction limit reached! % 182.35/26.34 % (3337670)------------------------------ % 182.35/26.34 % (3337670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.35/26.34 % (3337670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.35/26.34 % (3337670)CaDiCaL version: 2.1.3 % 182.35/26.34 % (3337670)Termination reason: Instruction limit % 182.35/26.34 % (3337670)Termination phase: Saturation % 182.35/26.34 % (3337670)Time elapsed: 2.844 s % 182.35/26.34 % (3337670)Peak memory usage: 42 MB % 182.35/26.34 % (3337670)Instructions burned: 8176 (million) % 182.35/26.34 % (3337676)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1059727091:fmbsr=2:i=32576_2937 on theBenchmark for (2937ds/32576Mi) % 182.35/26.34 % (3337676)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 182.35/26.34 % (3337676)Terminated due to inappropriate strategy. % 182.35/26.34 % (3337676)------------------------------ % 182.35/26.34 % (3337676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.35/26.34 % (3337676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.35/26.34 % (3337676)CaDiCaL version: 2.1.3 % 182.35/26.34 % (3337676)Termination reason: Inappropriate % 182.35/26.34 % (3337676)Time elapsed: 0.0000 s % 182.35/26.34 % (3337676)Peak memory usage: 10 MB % 182.35/26.34 % (3337676)------------------------------ % 182.35/26.34 % (3337676)------------------------------ % 182.35/26.34 % (3337678)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2495533945:i=11404_2937 on theBenchmark for (2937ds/11404Mi) % 182.35/26.34 % (3337672)Instruction limit reached! % 182.35/26.34 % (3337672)------------------------------ % 182.35/26.34 % (3337672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.35/26.34 % (3337672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.35/26.34 % (3337672)CaDiCaL version: 2.1.3 % 182.35/26.34 % (3337672)Termination reason: Instruction limit % 182.35/26.34 % (3337672)Termination phase: Saturation % 182.35/26.34 % (3337672)Time elapsed: 4.714 s % 182.35/26.34 % (3337672)Peak memory usage: 47 MB % 182.35/26.34 % (3337672)Instructions burned: 9156 (million) % 182.35/26.34 % (3337680)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2541766041:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 182.35/26.34 % (3337678)Instruction limit reached! % 182.35/26.34 % (3337678)------------------------------ % 182.35/26.34 % (3337678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.35/26.34 % (3337678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.35/26.34 % (3337678)CaDiCaL version: 2.1.3 % 182.35/26.34 % (3337678)Termination reason: Instruction limit % 182.35/26.34 % (3337678)Termination phase: Saturation % 182.35/26.34 % (3337678)Time elapsed: 4.042 s % 182.35/26.34 % (3337678)Peak memory usage: 43 MB % 182.35/26.34 % (3337678)Instructions burned: 11406 (million) % 182.35/26.34 % (3337682)dis+33_16_sil=32000:sac=on:random_seed=2250269175:i=15851:nm=0_2896 on theBenchmark for (2896ds/15851Mi) % 182.35/26.34 % (3337668)Instruction limit reached! % 182.35/26.34 % (3337668)------------------------------ % 182.35/26.34 % (3337668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.35/26.34 % (3337668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.35/26.34 % (3337668)CaDiCaL version: 2.1.3 % 182.35/26.34 % (3337668)Termination reason: Instruction limit % 182.35/26.34 % (3337668)Termination phase: Saturation % 182.35/26.34 % (3337668)Time elapsed: 9.260 s % 182.35/26.34 % (3337668)Peak memory usage: 20 MB % 182.35/26.34 % (3337668)Instructions burned: 22565 (million) % 182.35/26.34 % (3337684)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4192555972:avsq=on:i=17627:add=on:amm=off_2874 on theBenchmark for (2874ds/17627Mi) % 182.35/26.34 % (3337682)Instruction limit reached! % 182.35/26.34 % (3337682)------------------------------ % 192.73/27.84 % (3337682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.73/27.84 % (3337682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.73/27.84 % (3337682)CaDiCaL version: 2.1.3 % 192.73/27.84 % (3337682)Termination reason: Instruction limit % 192.73/27.84 % (3337682)Termination phase: Saturation % 192.73/27.84 % (3337682)Time elapsed: 4.200 s % 192.73/27.84 % (3337682)Peak memory usage: 69 MB % 192.73/27.84 % (3337682)Instructions burned: 15852 (million) % 192.73/27.84 % (3337904)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1293574024:s2a=on:i=53295_2854 on theBenchmark for (2854ds/53295Mi) % 192.73/27.84 % (3337674)Instruction limit reached! % 192.73/27.84 % (3337674)------------------------------ % 192.73/27.84 % (3337674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.73/27.84 % (3337674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.73/27.84 % (3337674)CaDiCaL version: 2.1.3 % 192.73/27.84 % (3337674)Termination reason: Instruction limit % 192.73/27.84 % (3337674)Termination phase: Saturation % 192.73/27.84 % (3337674)Time elapsed: 9.885 s % 192.73/27.84 % (3337674)Peak memory usage: 49 MB % 192.73/27.84 % (3337674)Instructions burned: 20139 (million) % 192.73/27.84 % (3337969)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1730236305:i=26857:ins=20_2843 on theBenchmark for (2843ds/26857Mi) % 192.73/27.84 % (3337969)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.73/27.84 % (3337969)Terminated due to inappropriate strategy. % 192.73/27.84 % (3337969)------------------------------ % 192.73/27.84 % (3337969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.73/27.84 % (3337969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.73/27.84 % (3337969)CaDiCaL version: 2.1.3 % 192.73/27.84 % (3337969)Termination reason: Inappropriate % 192.73/27.84 % (3337969)Time elapsed: 0.001 s % 192.73/27.84 % (3337969)Peak memory usage: 10 MB % 192.73/27.84 % (3337969)------------------------------ % 192.73/27.84 % (3337969)------------------------------ % 192.73/27.84 % (3337971)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1455703508:i=28120:bs=on:fsr=off_2843 on theBenchmark for (2843ds/28120Mi) % 192.73/27.84 % (3337658)Instruction limit reached! % 192.73/27.84 % (3337658)------------------------------ % 192.73/27.84 % (3337658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.73/27.84 % (3337658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.73/27.84 % (3337658)CaDiCaL version: 2.1.3 % 192.73/27.84 % (3337658)Termination reason: Instruction limit % 192.73/27.84 % (3337658)Termination phase: Saturation % 192.73/27.84 % (3337658)Time elapsed: 13.877 s % 192.73/27.84 % (3337658)Peak memory usage: 143 MB % 192.73/27.84 % (3337658)Instructions burned: 29340 (million) % 192.73/27.84 % (3337980)fmb+10_1_sil=256000:fmbss=7:random_seed=123156075:fmbsr=1.6:i=182295_2837 on theBenchmark for (2837ds/182295Mi) % 192.73/27.84 % (3337980)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.73/27.84 % (3337980)Terminated due to inappropriate strategy. % 192.73/27.84 % (3337980)------------------------------ % 192.73/27.84 % (3337980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.73/27.84 % (3337980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.73/27.84 % (3337980)CaDiCaL version: 2.1.3 % 192.73/27.84 % (3337980)Termination reason: Inappropriate % 192.73/27.84 % (3337980)Time elapsed: 0.001 s % 192.73/27.84 % (3337980)Peak memory usage: 10 MB % 192.73/27.84 % (3337980)------------------------------ % 192.73/27.84 % (3337980)------------------------------ % 192.73/27.84 % (3337983)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1691440954:i=44625:gsp=on_2837 on theBenchmark for (2837ds/44625Mi) % 192.73/27.84 % (3337983)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 192.73/27.84 % (3337983)Terminated due to inappropriate strategy. % 192.73/27.84 % (3337983)------------------------------ % 192.73/27.84 % (3337983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.73/27.84 % (3337983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.73/27.84 % (3337983)CaDiCaL version: 2.1.3 % 192.73/27.84 % (3337983)Termination reason: Inappropriate % 192.73/27.84 % (3337983)Time elapsed: 0.001 s % 192.73/27.84 % (3337983)Peak memory usage: 10 MB % 192.73/27.84 % (3337983)------------------------------ % 192.73/27.84 % (3337983)------------------------------ % 192.73/27.84 % (3337985)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=556091441:i=160505_2836 on theBenchmark for (2836ds/160505Mi) % 229.22/32.91 % (3337985)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.22/32.91 % (3337985)Terminated due to inappropriate strategy. % 229.22/32.91 % (3337985)------------------------------ % 229.22/32.91 % (3337985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.22/32.91 % (3337985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.22/32.91 % (3337985)CaDiCaL version: 2.1.3 % 229.22/32.91 % (3337985)Termination reason: Inappropriate % 229.22/32.91 % (3337985)Time elapsed: 0.0000 s % 229.22/32.91 % (3337985)Peak memory usage: 10 MB % 229.22/32.91 % (3337985)------------------------------ % 229.22/32.91 % (3337985)------------------------------ % 229.22/32.91 % (3337987)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3533452744:fmbsr=1.3:i=225729_2836 on theBenchmark for (2836ds/225729Mi) % 229.22/32.91 % (3337987)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.22/32.91 % (3337987)Terminated due to inappropriate strategy. % 229.22/32.91 % (3337987)------------------------------ % 229.22/32.91 % (3337987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.22/32.91 % (3337987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.22/32.91 % (3337987)CaDiCaL version: 2.1.3 % 229.22/32.91 % (3337987)Termination reason: Inappropriate % 229.22/32.91 % (3337987)Time elapsed: 0.001 s % 229.22/32.91 % (3337987)Peak memory usage: 10 MB % 229.22/32.91 % (3337987)------------------------------ % 229.22/32.91 % (3337987)------------------------------ % 229.22/32.91 % (3337989)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2369862685:fmbsr=2:i=185024:ins=7_2836 on theBenchmark for (2836ds/185024Mi) % 229.22/32.91 % (3337989)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.22/32.91 % (3337989)Terminated due to inappropriate strategy. % 229.22/32.91 % (3337989)------------------------------ % 229.22/32.91 % (3337989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.22/32.91 % (3337989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.22/32.91 % (3337989)CaDiCaL version: 2.1.3 % 229.22/32.91 % (3337989)Termination reason: Inappropriate % 229.22/32.91 % (3337989)Time elapsed: 0.001 s % 229.22/32.91 % (3337989)Peak memory usage: 10 MB % 229.22/32.91 % (3337989)------------------------------ % 229.22/32.91 % (3337989)------------------------------ % 229.22/32.91 % (3337991)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1559734445:rtra=on_2835 on theBenchmark for (2835ds/0Mi) % 229.22/32.91 % (3337991)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 229.22/32.91 % (3337991)Terminated due to inappropriate strategy. % 229.22/32.91 % (3337991)------------------------------ % 229.22/32.91 % (3337991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.22/32.91 % (3337991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.22/32.91 % (3337991)CaDiCaL version: 2.1.3 % 229.22/32.91 % (3337991)Termination reason: Inappropriate % 229.22/32.91 % (3337991)Time elapsed: 0.0000 s % 229.22/32.91 % (3337991)Peak memory usage: 10 MB % 229.22/32.91 % (3337991)------------------------------ % 229.22/32.91 % (3337991)------------------------------ % 229.22/32.91 % (3337993)% WARNING: option uhcvi not known. % 229.22/32.91 % (3337993)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=344750961:i=271062:add=off:rtra=on:rawr=on_2835 on theBenchmark for (2835ds/271062Mi) % 229.22/32.91 % (3337680)Instruction limit reached! % 229.22/32.91 % (3337680)------------------------------ % 229.22/32.91 % (3337680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 229.22/32.91 % (3337680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.22/32.91 % (3337680)CaDiCaL version: 2.1.3 % 229.22/32.91 % (3337680)Termination reason: Instruction limit % 229.22/32.91 % (3337680)Termination phase: Saturation % 229.22/32.91 % (3337680)Time elapsed: 10.441 s % 229.22/32.91 % (3337680)Peak memory usage: 52 MB % 229.22/32.91 % (3337680)Instructions burned: 14135 (million) % 229.22/32.91 % (3338003)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2789194232:i=176048:add=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/176048Mi) % 229.22/32.91 % (3337684)Instruction limit reached! % 229.22/32.91 % (3337684)------------------------------ % 229.22/32.91 % (3337684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.61/36.13 % (3337684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.61/36.13 % (3337684)CaDiCaL version: 2.1.3 % 251.61/36.13 % (3337684)Termination reason: Instruction limit % 251.61/36.13 % (3337684)Termination phase: Saturation % 251.61/36.13 % (3337684)Time elapsed: 13.166 s % 251.61/36.13 % (3337684)Peak memory usage: 184 MB % 251.61/36.13 % (3337684)Instructions burned: 17628 (million) % 251.61/36.13 % (3338021)dis+10_1_sil=32000:si=on:sp=arity:random_seed=11580786:i=206:fgj=on:rtra=on_2742 on theBenchmark for (2742ds/206Mi) % 251.61/36.13 % (3338021)Instruction limit reached! % 251.61/36.13 % (3338021)------------------------------ % 251.61/36.13 % (3338021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.61/36.13 % (3338021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.61/36.13 % (3338021)CaDiCaL version: 2.1.3 % 251.61/36.13 % (3338021)Termination reason: Instruction limit % 251.61/36.13 % (3338021)Termination phase: Saturation % 251.61/36.13 % (3338021)Time elapsed: 0.182 s % 251.61/36.13 % (3338021)Peak memory usage: 13 MB % 251.61/36.13 % (3338021)Instructions burned: 206 (million) % 251.61/36.13 % (3338023)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4041262187:i=232:rtra=on_2740 on theBenchmark for (2740ds/232Mi) % 251.61/36.13 % (3338023)Instruction limit reached! % 251.61/36.13 % (3338023)------------------------------ % 251.61/36.13 % (3338023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.61/36.13 % (3338023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.61/36.13 % (3338023)CaDiCaL version: 2.1.3 % 251.61/36.13 % (3338023)Termination reason: Instruction limit % 251.61/36.13 % (3338023)Termination phase: Saturation % 251.61/36.13 % (3338023)Time elapsed: 0.215 s % 251.61/36.13 % (3338023)Peak memory usage: 13 MB % 251.61/36.13 % (3338023)Instructions burned: 232 (million) % 251.61/36.13 % (3338025)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=39322644:i=262:rtra=on_2737 on theBenchmark for (2737ds/262Mi) % 251.61/36.13 % (3338025)Instruction limit reached! % 251.61/36.13 % (3338025)------------------------------ % 251.61/36.13 % (3338025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.61/36.13 % (3338025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.61/36.13 % (3338025)CaDiCaL version: 2.1.3 % 251.61/36.13 % (3338025)Termination reason: Instruction limit % 251.61/36.13 % (3338025)Termination phase: Saturation % 251.61/36.13 % (3338025)Time elapsed: 0.261 s % 251.61/36.13 % (3338025)Peak memory usage: 13 MB % 251.61/36.13 % (3338025)Instructions burned: 263 (million) % 251.61/36.13 % (3338027)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2167525323:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2735 on theBenchmark for (2735ds/318Mi) % 251.61/36.13 % (3338027)Instruction limit reached! % 251.61/36.13 % (3338027)------------------------------ % 251.61/36.13 % (3338027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.61/36.13 % (3338027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.61/36.13 % (3338027)CaDiCaL version: 2.1.3 % 251.61/36.13 % (3338027)Termination reason: Instruction limit % 251.61/36.13 % (3338027)Termination phase: Saturation % 251.61/36.13 % (3338027)Time elapsed: 0.338 s % 251.61/36.13 % (3338027)Peak memory usage: 15 MB % 251.61/36.13 % (3338027)Instructions burned: 319 (million) % 251.61/36.13 % (3338033)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=50393460:i=1428:nm=2:rtra=on_2731 on theBenchmark for (2731ds/1428Mi) % 251.61/36.13 % (3338033)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 251.61/36.13 % (3338033)Terminated due to inappropriate strategy. % 251.61/36.13 % (3338033)------------------------------ % 251.61/36.13 % (3338033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 251.61/36.13 % (3338033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 251.61/36.13 % (3338033)CaDiCaL version: 2.1.3 % 251.61/36.13 % (3338033)Termination reason: Inappropriate % 251.61/36.13 % (3338033)Time elapsed: 0.0000 s % 251.61/36.13 % (3338033)Peak memory usage: 10 MB % 251.61/36.13 % (3338033)------------------------------ % 251.61/36.13 % (3338033)------------------------------ % 251.61/36.13 % (3338035)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1592149959:i=262:bd=preordered:rtra=on:fsd=on_2731 on theBenchmark for (2731ds/262Mi) % 251.61/36.13 % (3338035)Instruction limit reached! % 251.61/36.13 % (3338035)------------------------------ % 251.61/36.13 % (3338035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.63/40.40 % (3338035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.63/40.40 % (3338035)CaDiCaL version: 2.1.3 % 282.63/40.40 % (3338035)Termination reason: Instruction limit % 282.63/40.40 % (3338035)Termination phase: Saturation % 282.63/40.40 % (3338035)Time elapsed: 0.285 s % 282.63/40.40 % (3338035)Peak memory usage: 13 MB % 282.63/40.40 % (3338035)Instructions burned: 262 (million) % 282.63/40.40 % (3338037)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=2430190189:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2727 on theBenchmark for (2727ds/1368Mi) % 282.63/40.40 % (3338037)Instruction limit reached! % 282.63/40.40 % (3338037)------------------------------ % 282.63/40.40 % (3338037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.63/40.40 % (3338037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.63/40.40 % (3338037)CaDiCaL version: 2.1.3 % 282.63/40.40 % (3338037)Termination reason: Instruction limit % 282.63/40.40 % (3338037)Termination phase: Saturation % 282.63/40.40 % (3338037)Time elapsed: 1.181 s % 282.63/40.40 % (3338037)Peak memory usage: 16 MB % 282.63/40.40 % (3338037)Instructions burned: 1368 (million) % 282.63/40.40 % (3338039)ott-21_1_sil=16000:si=on:fs=off:random_seed=1697084454:i=360:av=off:fsr=off:rtra=on_2715 on theBenchmark for (2715ds/360Mi) % 282.63/40.40 % (3338039)Instruction limit reached! % 282.63/40.40 % (3338039)------------------------------ % 282.63/40.40 % (3338039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.63/40.40 % (3338039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.63/40.40 % (3338039)CaDiCaL version: 2.1.3 % 282.63/40.40 % (3338039)Termination reason: Instruction limit % 282.63/40.40 % (3338039)Termination phase: Saturation % 282.63/40.40 % (3338039)Time elapsed: 0.243 s % 282.63/40.40 % (3338039)Peak memory usage: 13 MB % 282.63/40.40 % (3338039)Instructions burned: 361 (million) % 282.63/40.40 % (3338041)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1154162866:i=954:bd=all:rtra=on_2713 on theBenchmark for (2713ds/954Mi) % 282.63/40.40 % (3338041)Instruction limit reached! % 282.63/40.40 % (3338041)------------------------------ % 282.63/40.40 % (3338041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.63/40.40 % (3338041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.63/40.40 % (3338041)CaDiCaL version: 2.1.3 % 282.63/40.40 % (3338041)Termination reason: Instruction limit % 282.63/40.40 % (3338041)Termination phase: Saturation % 282.63/40.40 % (3338041)Time elapsed: 0.933 s % 282.63/40.40 % (3338041)Peak memory usage: 17 MB % 282.63/40.40 % (3338041)Instructions burned: 955 (million) % 282.63/40.40 % (3338043)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2133524177:fmbsr=1.3:i=1730:ins=25:rtra=on_2703 on theBenchmark for (2703ds/1730Mi) % 282.63/40.40 % (3338043)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 282.63/40.40 % (3338043)Terminated due to inappropriate strategy. % 282.63/40.40 % (3338043)------------------------------ % 282.63/40.40 % (3338043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.63/40.40 % (3338043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.63/40.40 % (3338043)CaDiCaL version: 2.1.3 % 282.63/40.40 % (3338043)Termination reason: Inappropriate % 282.63/40.40 % (3338043)Time elapsed: 0.0000 s % 282.63/40.40 % (3338043)Peak memory usage: 10 MB % 282.63/40.40 % (3338043)------------------------------ % 282.63/40.40 % (3338043)------------------------------ % 282.63/40.40 % (3338045)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=239381667:i=2358:rtra=on_2703 on theBenchmark for (2703ds/2358Mi) % 282.63/40.40 % (3338045)Instruction limit reached! % 282.63/40.40 % (3338045)------------------------------ % 282.63/40.40 % (3338045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.63/40.40 % (3338045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.63/40.40 % (3338045)CaDiCaL version: 2.1.3 % 282.63/40.40 % (3338045)Termination reason: Instruction limit % 282.63/40.40 % (3338045)Termination phase: Saturation % 282.63/40.40 % (3338045)Time elapsed: 2.511 s % 282.63/40.40 % (3338045)Peak memory usage: 23 MB % 282.63/40.40 % (3338045)Instructions burned: 2358 (million) % 282.63/40.40 % (3338049)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1696849926:i=1778:ins=1:rtra=on_2677 on theBenchmark for (2677ds/1778Mi) % 282.63/40.40 % (3338049)WARNING: trying tTerminated % 300.42/42.94 % Vampire exiting % 300.42/42.94 Terminated %------------------------------------------------------------------------------