%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW074_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 : n026.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 01:39:10 PM UTC 2026 % Result : Timeout 300.36s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW074_1 : TPTP v9.3.1. Released v5.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n026.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 13:14:12 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/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 % 3.32/0.82 % (3842497)Will run a generic schedule for satisfiability detection. % 3.32/0.82 % (3842526)dis+10_1_sil=32000:sp=arity:random_seed=2355528924:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.32/0.82 % (3842524)% WARNING: option uhcvi not known. % 3.32/0.82 % (3842523)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=870234004_2999 on theBenchmark for (2999ds/0Mi) % 3.32/0.82 % (3842524)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4224959570:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.32/0.82 % (3842525)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3220035754:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.32/0.82 % (3842527)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1064002035:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.32/0.82 % (3842528)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3481451117:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.32/0.82 % (3842529)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2457125096:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.32/0.82 % (3842526)Instruction limit reached! % 3.32/0.82 % (3842526)------------------------------ % 3.32/0.82 % (3842526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.82 % (3842526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.82 % (3842526)CaDiCaL version: 2.1.3 % 3.32/0.82 % (3842526)Termination reason: Instruction limit % 3.32/0.82 % (3842526)Termination phase: Saturation % 3.32/0.82 % (3842526)Time elapsed: 0.027 s % 3.32/0.82 % (3842526)Peak memory usage: 15 MB % 3.32/0.82 % (3842526)Instructions burned: 106 (million) % 3.32/0.82 % (3842528)Instruction limit reached! % 3.32/0.82 % (3842528)------------------------------ % 3.32/0.82 % (3842528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.82 % (3842528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.82 % (3842528)CaDiCaL version: 2.1.3 % 3.32/0.82 % (3842528)Termination reason: Instruction limit % 3.32/0.82 % (3842528)Termination phase: Saturation % 3.32/0.82 % (3842528)Time elapsed: 0.049 s % 3.32/0.82 % (3842528)Peak memory usage: 15 MB % 3.32/0.82 % (3842528)Instructions burned: 136 (million) % 3.32/0.82 % (3842548)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3913272403:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.32/0.82 % (3842523)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.32/0.82 % (3842523)Terminated due to inappropriate strategy. % 3.32/0.82 % (3842523)------------------------------ % 3.32/0.82 % (3842523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.82 % (3842523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.82 % (3842523)CaDiCaL version: 2.1.3 % 3.32/0.82 % (3842523)Termination reason: Inappropriate % 3.32/0.82 % (3842523)Time elapsed: 0.052 s % 3.32/0.82 % (3842523)Peak memory usage: 14 MB % 3.32/0.82 % (3842523)Instructions burned: 95 (million) % 3.32/0.82 % (3842523)------------------------------ % 3.32/0.82 % (3842523)------------------------------ % 3.32/0.82 % (3842527)Instruction limit reached! % 3.32/0.82 % (3842527)------------------------------ % 3.32/0.82 % (3842527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.82 % (3842527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.82 % (3842527)CaDiCaL version: 2.1.3 % 3.32/0.82 % (3842527)Termination reason: Instruction limit % 3.32/0.82 % (3842527)Termination phase: Saturation % 3.32/0.82 % (3842527)Time elapsed: 0.054 s % 3.32/0.82 % (3842527)Peak memory usage: 16 MB % 3.32/0.82 % (3842527)Instructions burned: 117 (million) % 3.32/0.82 % (3842556)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3590458340:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.32/0.82 % (3842529)Instruction limit reached! % 3.32/0.82 % (3842529)------------------------------ % 3.32/0.82 % (3842529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.32/0.82 % (3842529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.32/0.82 % (3842529)CaDiCaL version: 2.1.3 % 3.32/0.82 % (3842529)Termination reason: Instruction limit % 3.32/0.82 % (3842529)Termination phase: Saturation % 3.32/0.82 % (3842529)Time elapsed: 0.067 s % 3.32/0.82 % (3842529)Peak memory usage: 16 MB % 3.32/0.82 % (3842529)Instructions burned: 160 (million) % 5.99/1.18 % (3842558)ott-21_1_sil=16000:fs=off:random_seed=815413608:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.99/1.18 % (3842557)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=82946888:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.99/1.18 % (3842560)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2966457988:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.99/1.18 % (3842548)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.99/1.18 % (3842548)Terminated due to inappropriate strategy. % 5.99/1.18 % (3842548)------------------------------ % 5.99/1.18 % (3842548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.18 % (3842548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.18 % (3842548)CaDiCaL version: 2.1.3 % 5.99/1.18 % (3842548)Termination reason: Inappropriate % 5.99/1.18 % (3842548)Time elapsed: 0.042 s % 5.99/1.18 % (3842548)Peak memory usage: 14 MB % 5.99/1.18 % (3842548)Instructions burned: 95 (million) % 5.99/1.18 % (3842548)------------------------------ % 5.99/1.18 % (3842548)------------------------------ % 5.99/1.18 % (3842556)Instruction limit reached! % 5.99/1.18 % (3842556)------------------------------ % 5.99/1.18 % (3842556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.18 % (3842556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.18 % (3842556)CaDiCaL version: 2.1.3 % 5.99/1.18 % (3842556)Termination reason: Instruction limit % 5.99/1.18 % (3842556)Termination phase: Saturation % 5.99/1.18 % (3842556)Time elapsed: 0.031 s % 5.99/1.18 % (3842556)Peak memory usage: 16 MB % 5.99/1.18 % (3842556)Instructions burned: 135 (million) % 5.99/1.18 % (3842574)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2951200948:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.99/1.18 % (3842573)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4073400379:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.99/1.18 % (3842558)Instruction limit reached! % 5.99/1.18 % (3842558)------------------------------ % 5.99/1.18 % (3842558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.18 % (3842558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.18 % (3842558)CaDiCaL version: 2.1.3 % 5.99/1.18 % (3842558)Termination reason: Instruction limit % 5.99/1.18 % (3842558)Termination phase: Saturation % 5.99/1.18 % (3842558)Time elapsed: 0.085 s % 5.99/1.18 % (3842558)Peak memory usage: 15 MB % 5.99/1.18 % (3842558)Instructions burned: 182 (million) % 5.99/1.18 % (3842573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.99/1.18 % (3842573)Terminated due to inappropriate strategy. % 5.99/1.18 % (3842573)------------------------------ % 5.99/1.18 % (3842573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.18 % (3842573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.18 % (3842573)CaDiCaL version: 2.1.3 % 5.99/1.18 % (3842573)Termination reason: Inappropriate % 5.99/1.18 % (3842573)Time elapsed: 0.053 s % 5.99/1.18 % (3842573)Peak memory usage: 14 MB % 5.99/1.18 % (3842573)Instructions burned: 94 (million) % 5.99/1.18 % (3842573)------------------------------ % 5.99/1.18 % (3842573)------------------------------ % 5.99/1.18 % (3842590)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2640900153:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 5.99/1.18 % (3842593)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=3710488903:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 5.99/1.18 % (3842590)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.99/1.18 % (3842590)Terminated due to inappropriate strategy. % 5.99/1.18 % (3842590)------------------------------ % 5.99/1.18 % (3842590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.99/1.18 % (3842590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.99/1.18 % (3842590)CaDiCaL version: 2.1.3 % 5.99/1.18 % (3842590)Termination reason: Inappropriate % 5.99/1.18 % (3842590)Time elapsed: 0.057 s % 5.99/1.18 % (3842590)Peak memory usage: 16 MB % 23.57/3.68 % (3842590)Instructions burned: 130 (million) % 23.57/3.68 % (3842590)------------------------------ % 23.57/3.68 % (3842590)------------------------------ % 23.57/3.68 % (3842611)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3018379921:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 23.57/3.68 % (3842560)Instruction limit reached! % 23.57/3.68 % (3842560)------------------------------ % 23.57/3.68 % (3842560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.57/3.68 % (3842560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.57/3.68 % (3842560)CaDiCaL version: 2.1.3 % 23.57/3.68 % (3842560)Termination reason: Instruction limit % 23.57/3.68 % (3842560)Termination phase: Saturation % 23.57/3.68 % (3842560)Time elapsed: 0.265 s % 23.57/3.68 % (3842560)Peak memory usage: 17 MB % 23.57/3.68 % (3842560)Instructions burned: 478 (million) % 23.57/3.68 % (3842621)fmb+10_1_sil=64000:random_seed=1066630669:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 23.57/3.68 % (3842621)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.57/3.68 % (3842621)Terminated due to inappropriate strategy. % 23.57/3.68 % (3842621)------------------------------ % 23.57/3.68 % (3842621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.57/3.68 % (3842621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.57/3.68 % (3842621)CaDiCaL version: 2.1.3 % 23.57/3.68 % (3842621)Termination reason: Inappropriate % 23.57/3.68 % (3842621)Time elapsed: 0.046 s % 23.57/3.68 % (3842621)Peak memory usage: 14 MB % 23.57/3.68 % (3842621)Instructions burned: 104 (million) % 23.57/3.68 % (3842621)------------------------------ % 23.57/3.68 % (3842621)------------------------------ % 23.57/3.68 % (3842574)Instruction limit reached! % 23.57/3.68 % (3842574)------------------------------ % 23.57/3.68 % (3842574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.57/3.68 % (3842574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.57/3.68 % (3842574)CaDiCaL version: 2.1.3 % 23.57/3.68 % (3842574)Termination reason: Instruction limit % 23.57/3.68 % (3842574)Termination phase: Saturation % 23.57/3.68 % (3842574)Time elapsed: 0.324 s % 23.57/3.68 % (3842574)Peak memory usage: 22 MB % 23.57/3.68 % (3842574)Instructions burned: 1181 (million) % 23.57/3.68 % (3842557)Instruction limit reached! % 23.57/3.68 % (3842557)------------------------------ % 23.57/3.68 % (3842557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.57/3.68 % (3842557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.57/3.68 % (3842557)CaDiCaL version: 2.1.3 % 23.57/3.68 % (3842557)Termination reason: Instruction limit % 23.57/3.68 % (3842557)Termination phase: Saturation % 23.57/3.68 % (3842557)Time elapsed: 0.367 s % 23.57/3.68 % (3842557)Peak memory usage: 20 MB % 23.57/3.68 % (3842557)Instructions burned: 685 (million) % 23.57/3.68 % (3842623)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3517318653:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 23.57/3.68 % (3842625)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2573928068:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 23.57/3.68 % (3842624)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3613821776:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 23.57/3.68 % (3842623)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.57/3.68 % (3842623)Terminated due to inappropriate strategy. % 23.57/3.68 % (3842623)------------------------------ % 23.57/3.68 % (3842623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.57/3.68 % (3842623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.57/3.68 % (3842623)CaDiCaL version: 2.1.3 % 23.57/3.68 % (3842623)Termination reason: Inappropriate % 23.57/3.68 % (3842623)Time elapsed: 0.041 s % 23.57/3.68 % (3842623)Peak memory usage: 14 MB % 23.57/3.68 % (3842623)Instructions burned: 95 (million) % 23.57/3.68 % (3842623)------------------------------ % 23.57/3.68 % (3842623)------------------------------ % 23.57/3.68 % (3842624)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 23.57/3.68 % (3842624)Terminated due to inappropriate strategy. % 23.57/3.68 % (3842624)------------------------------ % 23.57/3.68 % (3842624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.57/3.68 % (3842624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.27 % (3842624)CaDiCaL version: 2.1.3 % 27.84/4.27 % (3842624)Termination reason: Inappropriate % 27.84/4.27 % (3842624)Time elapsed: 0.042 s % 27.84/4.27 % (3842624)Peak memory usage: 14 MB % 27.84/4.27 % (3842624)Instructions burned: 95 (million) % 27.84/4.27 % (3842624)------------------------------ % 27.84/4.27 % (3842624)------------------------------ % 27.84/4.27 % (3842629)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1664462794:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 27.84/4.27 % (3842630)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2757076366:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 27.84/4.27 % (3842630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.84/4.27 % (3842630)Terminated due to inappropriate strategy. % 27.84/4.27 % (3842630)------------------------------ % 27.84/4.27 % (3842630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.84/4.27 % (3842630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.27 % (3842630)CaDiCaL version: 2.1.3 % 27.84/4.27 % (3842630)Termination reason: Inappropriate % 27.84/4.27 % (3842630)Time elapsed: 0.040 s % 27.84/4.27 % (3842630)Peak memory usage: 14 MB % 27.84/4.27 % (3842630)Instructions burned: 95 (million) % 27.84/4.27 % (3842630)------------------------------ % 27.84/4.27 % (3842630)------------------------------ % 27.84/4.27 % (3842633)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=855022659:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 27.84/4.27 % (3842633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.84/4.27 % (3842633)Terminated due to inappropriate strategy. % 27.84/4.27 % (3842633)------------------------------ % 27.84/4.27 % (3842633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.84/4.27 % (3842633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.27 % (3842633)CaDiCaL version: 2.1.3 % 27.84/4.27 % (3842633)Termination reason: Inappropriate % 27.84/4.27 % (3842633)Time elapsed: 0.040 s % 27.84/4.27 % (3842633)Peak memory usage: 14 MB % 27.84/4.27 % (3842633)Instructions burned: 95 (million) % 27.84/4.27 % (3842633)------------------------------ % 27.84/4.27 % (3842633)------------------------------ % 27.84/4.27 % (3842635)ott-2_1_sil=16000:newcnf=on:random_seed=341770351:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 27.84/4.27 % (3842611)Instruction limit reached! % 27.84/4.27 % (3842611)------------------------------ % 27.84/4.27 % (3842611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.84/4.27 % (3842611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.27 % (3842611)CaDiCaL version: 2.1.3 % 27.84/4.27 % (3842611)Termination reason: Instruction limit % 27.84/4.27 % (3842611)Termination phase: Saturation % 27.84/4.27 % (3842611)Time elapsed: 0.487 s % 27.84/4.27 % (3842611)Peak memory usage: 22 MB % 27.84/4.27 % (3842611)Instructions burned: 879 (million) % 27.84/4.27 % (3842637)ott+10_1_sil=32000:tgt=ground:random_seed=2757346481:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 27.84/4.27 % (3842593)Instruction limit reached! % 27.84/4.27 % (3842593)------------------------------ % 27.84/4.27 % (3842593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.84/4.27 % (3842593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.27 % (3842593)CaDiCaL version: 2.1.3 % 27.84/4.27 % (3842593)Termination reason: Instruction limit % 27.84/4.27 % (3842593)Termination phase: Saturation % 27.84/4.27 % (3842593)Time elapsed: 0.606 s % 27.84/4.27 % (3842593)Peak memory usage: 22 MB % 27.84/4.27 % (3842593)Instructions burned: 692 (million) % 27.84/4.27 % (3842639)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4104807441:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 27.84/4.27 % (3842639)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.84/4.27 % (3842639)Terminated due to inappropriate strategy. % 27.84/4.27 % (3842639)------------------------------ % 27.84/4.27 % (3842639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.84/4.27 % (3842639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.84/4.27 % (3842639)CaDiCaL version: 2.1.3 % 27.84/4.27 % (3842639)Termination reason: Inappropriate % 27.84/4.27 % (3842639)Time elapsed: 0.040 s % 27.84/4.27 % (3842639)Peak memory usage: 14 MB % 27.84/4.27 % (3842639)Instructions burned: 95 (million) % 93.84/13.59 % (3842639)------------------------------ % 93.84/13.59 % (3842639)------------------------------ % 93.84/13.59 % (3842641)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=40973043:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 93.84/13.59 % (3842629)Instruction limit reached! % 93.84/13.59 % (3842629)------------------------------ % 93.84/13.59 % (3842629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.84/13.59 % (3842629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.84/13.59 % (3842629)CaDiCaL version: 2.1.3 % 93.84/13.59 % (3842629)Termination reason: Instruction limit % 93.84/13.59 % (3842629)Termination phase: Saturation % 93.84/13.59 % (3842629)Time elapsed: 0.540 s % 93.84/13.59 % (3842629)Peak memory usage: 17 MB % 93.84/13.59 % (3842629)Instructions burned: 1473 (million) % 93.84/13.59 % (3842651)dis+21_1_sil=32000:sas=cadical:random_seed=704222378:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 93.84/13.59 % (3842635)Instruction limit reached! % 93.84/13.59 % (3842635)------------------------------ % 93.84/13.59 % (3842635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.84/13.59 % (3842635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.84/13.59 % (3842635)CaDiCaL version: 2.1.3 % 93.84/13.59 % (3842635)Termination reason: Instruction limit % 93.84/13.59 % (3842635)Termination phase: Saturation % 93.84/13.59 % (3842635)Time elapsed: 0.517 s % 93.84/13.59 % (3842635)Peak memory usage: 20 MB % 93.84/13.59 % (3842635)Instructions burned: 869 (million) % 93.84/13.59 % (3842656)ott+11_1_sil=16000:gs=on:random_seed=2678686821:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 93.84/13.59 % (3842625)Instruction limit reached! % 93.84/13.59 % (3842625)------------------------------ % 93.84/13.59 % (3842625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.84/13.59 % (3842625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.84/13.59 % (3842625)CaDiCaL version: 2.1.3 % 93.84/13.59 % (3842625)Termination reason: Instruction limit % 93.84/13.59 % (3842625)Termination phase: Saturation % 93.84/13.59 % (3842625)Time elapsed: 1.895 s % 93.84/13.59 % (3842625)Peak memory usage: 44 MB % 93.84/13.59 % (3842625)Instructions burned: 5131 (million) % 93.84/13.59 % (3842727)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2907760174:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi) % 93.84/13.59 % (3842727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 93.84/13.59 % (3842727)Terminated due to inappropriate strategy. % 93.84/13.59 % (3842727)------------------------------ % 93.84/13.59 % (3842727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.84/13.59 % (3842727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.84/13.59 % (3842727)CaDiCaL version: 2.1.3 % 93.84/13.59 % (3842727)Termination reason: Inappropriate % 93.84/13.59 % (3842727)Time elapsed: 0.055 s % 93.84/13.59 % (3842727)Peak memory usage: 14 MB % 93.84/13.59 % (3842727)Instructions burned: 128 (million) % 93.84/13.59 % (3842727)------------------------------ % 93.84/13.59 % (3842727)------------------------------ % 93.84/13.59 % (3842731)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2118989906:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi) % 93.84/13.59 % (3842656)Instruction limit reached! % 93.84/13.59 % (3842656)------------------------------ % 93.84/13.59 % (3842656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.84/13.59 % (3842656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.84/13.59 % (3842656)CaDiCaL version: 2.1.3 % 93.84/13.59 % (3842656)Termination reason: Instruction limit % 93.84/13.59 % (3842656)Termination phase: Saturation % 93.84/13.59 % (3842656)Time elapsed: 1.474 s % 93.84/13.59 % (3842656)Peak memory usage: 19 MB % 93.84/13.59 % (3842656)Instructions burned: 2252 (million) % 93.84/13.59 % (3842739)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3566596160:i=29340_2972 on theBenchmark for (2972ds/29340Mi) % 93.84/13.59 % (3842641)Instruction limit reached! % 93.84/13.59 % (3842641)------------------------------ % 93.84/13.59 % (3842641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 93.84/13.59 % (3842641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.84/13.59 % (3842641)CaDiCaL version: 2.1.3 % 93.84/13.59 % (3842641)Termination reason: Instruction limit % 117.97/16.98 % (3842641)Termination phase: Saturation % 117.97/16.98 % (3842641)Time elapsed: 2.484 s % 117.97/16.98 % (3842641)Peak memory usage: 31 MB % 117.97/16.98 % (3842641)Instructions burned: 3512 (million) % 117.97/16.98 % (3842786)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3962695871:i=5211_2965 on theBenchmark for (2965ds/5211Mi) % 117.97/16.98 % (3842651)Instruction limit reached! % 117.97/16.98 % (3842651)------------------------------ % 117.97/16.98 % (3842651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.97/16.98 % (3842651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.97/16.98 % (3842651)CaDiCaL version: 2.1.3 % 117.97/16.98 % (3842651)Termination reason: Instruction limit % 117.97/16.98 % (3842651)Termination phase: Saturation % 117.97/16.98 % (3842651)Time elapsed: 2.320 s % 117.97/16.98 % (3842651)Peak memory usage: 26 MB % 117.97/16.98 % (3842651)Instructions burned: 3773 (million) % 117.97/16.98 % (3842788)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3579086788:i=5497:nm=2_2965 on theBenchmark for (2965ds/5497Mi) % 117.97/16.98 % (3842788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.97/16.98 % (3842788)Terminated due to inappropriate strategy. % 117.97/16.98 % (3842788)------------------------------ % 117.97/16.98 % (3842788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.97/16.98 % (3842788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.97/16.98 % (3842788)CaDiCaL version: 2.1.3 % 117.97/16.98 % (3842788)Termination reason: Inappropriate % 117.97/16.98 % (3842788)Time elapsed: 0.040 s % 117.97/16.98 % (3842788)Peak memory usage: 14 MB % 117.97/16.98 % (3842788)Instructions burned: 95 (million) % 117.97/16.98 % (3842788)------------------------------ % 117.97/16.98 % (3842788)------------------------------ % 117.97/16.98 % (3842790)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3501422046:fmbsr=2:i=46332_2964 on theBenchmark for (2964ds/46332Mi) % 117.97/16.98 % (3842790)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.97/16.98 % (3842790)Terminated due to inappropriate strategy. % 117.97/16.98 % (3842790)------------------------------ % 117.97/16.98 % (3842790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.97/16.98 % (3842790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.97/16.98 % (3842790)CaDiCaL version: 2.1.3 % 117.97/16.98 % (3842790)Termination reason: Inappropriate % 117.97/16.98 % (3842790)Time elapsed: 0.054 s % 117.97/16.98 % (3842790)Peak memory usage: 14 MB % 117.97/16.98 % (3842790)Instructions burned: 132 (million) % 117.97/16.98 % (3842790)------------------------------ % 117.97/16.98 % (3842790)------------------------------ % 117.97/16.98 % (3842792)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=395775335:i=14071_2963 on theBenchmark for (2963ds/14071Mi) % 117.97/16.98 % (3842792)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 117.97/16.98 % (3842792)Terminated due to inappropriate strategy. % 117.97/16.98 % (3842792)------------------------------ % 117.97/16.98 % (3842792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.97/16.98 % (3842792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.97/16.98 % (3842792)CaDiCaL version: 2.1.3 % 117.97/16.98 % (3842792)Termination reason: Inappropriate % 117.97/16.98 % (3842792)Time elapsed: 0.056 s % 117.97/16.98 % (3842792)Peak memory usage: 14 MB % 117.97/16.98 % (3842792)Instructions burned: 132 (million) % 117.97/16.98 % (3842792)------------------------------ % 117.97/16.98 % (3842792)------------------------------ % 117.97/16.98 % (3842794)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1599568366:i=22565:add=on:rawr=on_2962 on theBenchmark for (2962ds/22565Mi) % 117.97/16.98 % (3842731)Instruction limit reached! % 117.97/16.98 % (3842731)------------------------------ % 117.97/16.98 % (3842731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 117.97/16.98 % (3842731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.97/16.98 % (3842731)CaDiCaL version: 2.1.3 % 117.97/16.98 % (3842731)Termination reason: Instruction limit % 117.97/16.98 % (3842731)Termination phase: Saturation % 117.97/16.98 % (3842731)Time elapsed: 1.492 s % 117.97/16.98 % (3842731)Peak memory usage: 47 MB % 117.97/16.98 % (3842731)Instructions burned: 4592 (million) % 117.97/16.98 % (3842796)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3905581711:i=8173:av=off_2959 on theBenchmark for (2959ds/8173Mi) % 120.75/17.33 % (3842637)Instruction limit reached! % 120.75/17.33 % (3842637)------------------------------ % 120.75/17.33 % (3842637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.75/17.33 % (3842637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.75/17.33 % (3842637)CaDiCaL version: 2.1.3 % 120.75/17.33 % (3842637)Termination reason: Instruction limit % 120.75/17.33 % (3842637)Termination phase: Saturation % 120.75/17.33 % (3842637)Time elapsed: 3.598 s % 120.75/17.33 % (3842637)Peak memory usage: 33 MB % 120.75/17.33 % (3842637)Instructions burned: 5115 (million) % 120.75/17.33 % (3842798)dis+10_16:1_sil=16000:random_seed=204557618:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi) % 120.75/17.33 % (3842796)Instruction limit reached! % 120.75/17.33 % (3842796)------------------------------ % 120.75/17.33 % (3842796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.75/17.33 % (3842796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.75/17.33 % (3842796)CaDiCaL version: 2.1.3 % 120.75/17.33 % (3842796)Termination reason: Instruction limit % 120.75/17.33 % (3842796)Termination phase: Saturation % 120.75/17.33 % (3842796)Time elapsed: 1.818 s % 120.75/17.33 % (3842796)Peak memory usage: 39 MB % 120.75/17.33 % (3842796)Instructions burned: 8178 (million) % 120.75/17.33 % (3842800)ott-3_8_sil=64000:random_seed=3329487461:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi) % 120.75/17.33 % (3842786)Instruction limit reached! % 120.75/17.33 % (3842786)------------------------------ % 120.75/17.33 % (3842786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.75/17.33 % (3842786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.75/17.33 % (3842786)CaDiCaL version: 2.1.3 % 120.75/17.33 % (3842786)Termination reason: Instruction limit % 120.75/17.33 % (3842786)Termination phase: Saturation % 120.75/17.33 % (3842786)Time elapsed: 2.794 s % 120.75/17.33 % (3842786)Peak memory usage: 52 MB % 120.75/17.33 % (3842786)Instructions burned: 5211 (million) % 120.75/17.33 % (3842802)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3521777735:fmbsr=2:i=32576_2937 on theBenchmark for (2937ds/32576Mi) % 120.75/17.33 % (3842802)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 120.75/17.33 % (3842802)Terminated due to inappropriate strategy. % 120.75/17.33 % (3842802)------------------------------ % 120.75/17.33 % (3842802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.75/17.33 % (3842802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.75/17.33 % (3842802)CaDiCaL version: 2.1.3 % 120.75/17.33 % (3842802)Termination reason: Inappropriate % 120.75/17.33 % (3842802)Time elapsed: 0.052 s % 120.75/17.33 % (3842802)Peak memory usage: 14 MB % 120.75/17.33 % (3842802)Instructions burned: 128 (million) % 120.75/17.33 % (3842802)------------------------------ % 120.75/17.33 % (3842802)------------------------------ % 120.75/17.33 % (3842804)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=778513042:i=11404_2936 on theBenchmark for (2936ds/11404Mi) % 120.75/17.33 % (3842798)Instruction limit reached! % 120.75/17.33 % (3842798)------------------------------ % 120.75/17.33 % (3842798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.75/17.33 % (3842798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.75/17.33 % (3842798)CaDiCaL version: 2.1.3 % 120.75/17.33 % (3842798)Termination reason: Instruction limit % 120.75/17.33 % (3842798)Termination phase: Saturation % 120.75/17.33 % (3842798)Time elapsed: 4.688 s % 120.75/17.33 % (3842798)Peak memory usage: 55 MB % 120.75/17.33 % (3842798)Instructions burned: 9157 (million) % 120.75/17.33 % (3842806)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=779491868:i=14134_2908 on theBenchmark for (2908ds/14134Mi) % 120.75/17.33 % (3842800)Instruction limit reached! % 120.75/17.33 % (3842800)------------------------------ % 120.75/17.33 % (3842800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.75/17.33 % (3842800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.75/17.33 % (3842800)CaDiCaL version: 2.1.3 % 120.75/17.33 % (3842800)Termination reason: Instruction limit % 120.75/17.33 % (3842800)Termination phase: Saturation % 120.75/17.33 % (3842800)Time elapsed: 5.494 s % 120.75/17.33 % (3842800)Peak memory usage: 59 MB % 120.75/17.33 % (3842800)Instructions burned: 20140 (million) % 120.75/17.33 % (3842808)dis+33_16_sil=32000:sac=on:random_seed=117135558:i=15851:nm=0_2886 on theBenchmark for (2886ds/15851Mi) % 120.75/17.33 % (3842794)Instruction limit reached! % 120.75/17.33 % (3842794)------------------------------ % 120.75/17.33 % (3842794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.85/21.45 % (3842794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.85/21.45 % (3842794)CaDiCaL version: 2.1.3 % 149.85/21.45 % (3842794)Termination reason: Instruction limit % 149.85/21.45 % (3842794)Termination phase: Saturation % 149.85/21.45 % (3842794)Time elapsed: 9.622 s % 149.85/21.45 % (3842794)Peak memory usage: 79 MB % 149.85/21.45 % (3842794)Instructions burned: 22568 (million) % 149.85/21.45 % (3842810)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=883123323:avsq=on:i=17627:add=on:amm=off_2866 on theBenchmark for (2866ds/17627Mi) % 149.85/21.45 % (3842804)Instruction limit reached! % 149.85/21.45 % (3842804)------------------------------ % 149.85/21.45 % (3842804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.85/21.45 % (3842804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.85/21.45 % (3842804)CaDiCaL version: 2.1.3 % 149.85/21.45 % (3842804)Termination reason: Instruction limit % 149.85/21.45 % (3842804)Termination phase: Saturation % 149.85/21.45 % (3842804)Time elapsed: 7.379 s % 149.85/21.45 % (3842804)Peak memory usage: 48 MB % 149.85/21.45 % (3842804)Instructions burned: 11405 (million) % 149.85/21.45 % (3842814)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4075777711:s2a=on:i=53295_2862 on theBenchmark for (2862ds/53295Mi) % 149.85/21.45 % (3842808)Instruction limit reached! % 149.85/21.45 % (3842808)------------------------------ % 149.85/21.45 % (3842808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.85/21.45 % (3842808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.85/21.45 % (3842808)CaDiCaL version: 2.1.3 % 149.85/21.45 % (3842808)Termination reason: Instruction limit % 149.85/21.45 % (3842808)Termination phase: Saturation % 149.85/21.45 % (3842808)Time elapsed: 3.622 s % 149.85/21.45 % (3842808)Peak memory usage: 35 MB % 149.85/21.45 % (3842808)Instructions burned: 15855 (million) % 149.85/21.45 % (3842816)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=364653016:i=26857:ins=20_2850 on theBenchmark for (2850ds/26857Mi) % 149.85/21.45 % (3842816)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.85/21.45 % (3842816)Terminated due to inappropriate strategy. % 149.85/21.45 % (3842816)------------------------------ % 149.85/21.45 % (3842816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.85/21.45 % (3842816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.85/21.45 % (3842816)CaDiCaL version: 2.1.3 % 149.85/21.45 % (3842816)Termination reason: Inappropriate % 149.85/21.45 % (3842816)Time elapsed: 0.022 s % 149.85/21.45 % (3842816)Peak memory usage: 14 MB % 149.85/21.45 % (3842816)Instructions burned: 95 (million) % 149.85/21.45 % (3842816)------------------------------ % 149.85/21.45 % (3842816)------------------------------ % 149.85/21.45 % (3842818)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3581298701:i=28120:bs=on:fsr=off_2849 on theBenchmark for (2849ds/28120Mi) % 149.85/21.45 % (3842739)Instruction limit reached! % 149.85/21.45 % (3842739)------------------------------ % 149.85/21.45 % (3842739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.85/21.45 % (3842739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.85/21.45 % (3842739)CaDiCaL version: 2.1.3 % 149.85/21.45 % (3842739)Termination reason: Instruction limit % 149.85/21.45 % (3842739)Termination phase: Saturation % 149.85/21.45 % (3842739)Time elapsed: 13.857 s % 149.85/21.45 % (3842739)Peak memory usage: 44 MB % 149.85/21.45 % (3842739)Instructions burned: 29342 (million) % 149.85/21.45 % (3842820)fmb+10_1_sil=256000:fmbss=7:random_seed=69881992:fmbsr=1.6:i=182295_2833 on theBenchmark for (2833ds/182295Mi) % 149.85/21.45 % (3842820)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 149.85/21.45 % (3842820)Terminated due to inappropriate strategy. % 149.85/21.45 % (3842820)------------------------------ % 149.85/21.45 % (3842820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.85/21.45 % (3842820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.85/21.45 % (3842820)CaDiCaL version: 2.1.3 % 149.85/21.45 % (3842820)Termination reason: Inappropriate % 149.85/21.45 % (3842820)Time elapsed: 0.040 s % 149.85/21.45 % (3842820)Peak memory usage: 14 MB % 149.85/21.45 % (3842820)Instructions burned: 95 (million) % 149.85/21.45 % (3842820)------------------------------ % 149.85/21.45 % (3842820)------------------------------ % 149.85/21.45 % (3842822)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2523831277:i=44625:gsp=on_2832 on theBenchmark for (2832ds/44625Mi) % 156.98/22.42 % (3842822)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.42 % (3842822)Terminated due to inappropriate strategy. % 156.98/22.42 % (3842822)------------------------------ % 156.98/22.42 % (3842822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.42 % (3842822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.42 % (3842822)CaDiCaL version: 2.1.3 % 156.98/22.42 % (3842822)Termination reason: Inappropriate % 156.98/22.42 % (3842822)Time elapsed: 0.045 s % 156.98/22.42 % (3842822)Peak memory usage: 15 MB % 156.98/22.42 % (3842822)Instructions burned: 100 (million) % 156.98/22.42 % (3842822)------------------------------ % 156.98/22.42 % (3842822)------------------------------ % 156.98/22.42 % (3842824)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=349181133:i=160505_2832 on theBenchmark for (2832ds/160505Mi) % 156.98/22.42 % (3842824)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.42 % (3842824)Terminated due to inappropriate strategy. % 156.98/22.42 % (3842824)------------------------------ % 156.98/22.42 % (3842824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.42 % (3842824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.42 % (3842824)CaDiCaL version: 2.1.3 % 156.98/22.42 % (3842824)Termination reason: Inappropriate % 156.98/22.42 % (3842824)Time elapsed: 0.040 s % 156.98/22.42 % (3842824)Peak memory usage: 14 MB % 156.98/22.42 % (3842824)Instructions burned: 95 (million) % 156.98/22.42 % (3842824)------------------------------ % 156.98/22.42 % (3842824)------------------------------ % 156.98/22.42 % (3842826)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1599984179:fmbsr=1.3:i=225729_2831 on theBenchmark for (2831ds/225729Mi) % 156.98/22.42 % (3842826)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.42 % (3842826)Terminated due to inappropriate strategy. % 156.98/22.42 % (3842826)------------------------------ % 156.98/22.42 % (3842826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.42 % (3842826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.42 % (3842826)CaDiCaL version: 2.1.3 % 156.98/22.42 % (3842826)Termination reason: Inappropriate % 156.98/22.42 % (3842826)Time elapsed: 0.054 s % 156.98/22.42 % (3842826)Peak memory usage: 14 MB % 156.98/22.42 % (3842826)Instructions burned: 132 (million) % 156.98/22.42 % (3842826)------------------------------ % 156.98/22.42 % (3842826)------------------------------ % 156.98/22.42 % (3842828)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=430183271:fmbsr=2:i=185024:ins=7_2830 on theBenchmark for (2830ds/185024Mi) % 156.98/22.42 % (3842828)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.42 % (3842828)Terminated due to inappropriate strategy. % 156.98/22.42 % (3842828)------------------------------ % 156.98/22.42 % (3842828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.42 % (3842828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.42 % (3842828)CaDiCaL version: 2.1.3 % 156.98/22.42 % (3842828)Termination reason: Inappropriate % 156.98/22.42 % (3842828)Time elapsed: 0.055 s % 156.98/22.42 % (3842828)Peak memory usage: 14 MB % 156.98/22.42 % (3842828)Instructions burned: 132 (million) % 156.98/22.42 % (3842828)------------------------------ % 156.98/22.42 % (3842828)------------------------------ % 156.98/22.42 % (3842830)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3966781083:rtra=on_2830 on theBenchmark for (2830ds/0Mi) % 156.98/22.42 % (3842830)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 156.98/22.42 % (3842830)Terminated due to inappropriate strategy. % 156.98/22.42 % (3842830)------------------------------ % 156.98/22.42 % (3842830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 156.98/22.42 % (3842830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.98/22.42 % (3842830)CaDiCaL version: 2.1.3 % 156.98/22.42 % (3842830)Termination reason: Inappropriate % 156.98/22.42 % (3842830)Time elapsed: 0.052 s % 156.98/22.42 % (3842830)Peak memory usage: 15 MB % 156.98/22.42 % (3842830)Instructions burned: 111 (million) % 156.98/22.42 % (3842830)------------------------------ % 156.98/22.42 % (3842830)------------------------------ % 156.98/22.42 % (3842832)% WARNING: option uhcvi not known. % 156.98/22.42 % (3842832)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=774892912:i=271062:add=off:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/271062Mi) % 165.20/23.79 % (3842806)Instruction limit reached! % 165.20/23.79 % (3842806)------------------------------ % 165.20/23.79 % (3842806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.20/23.79 % (3842806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.20/23.79 % (3842806)CaDiCaL version: 2.1.3 % 165.20/23.79 % (3842806)Termination reason: Instruction limit % 165.20/23.79 % (3842806)Termination phase: Saturation % 165.20/23.79 % (3842806)Time elapsed: 8.898 s % 165.20/23.79 % (3842806)Peak memory usage: 54 MB % 165.20/23.79 % (3842806)Instructions burned: 14134 (million) % 165.20/23.79 % (3842834)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2940467266:i=176048:add=on:rtra=on:rawr=on_2819 on theBenchmark for (2819ds/176048Mi) % 165.20/23.79 % (3842818)Instruction limit reached! % 165.20/23.79 % (3842818)------------------------------ % 165.20/23.79 % (3842818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.20/23.79 % (3842818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.20/23.79 % (3842818)CaDiCaL version: 2.1.3 % 165.20/23.79 % (3842818)Termination reason: Instruction limit % 165.20/23.79 % (3842818)Termination phase: Saturation % 165.20/23.79 % (3842818)Time elapsed: 5.834 s % 165.20/23.79 % (3842818)Peak memory usage: 25 MB % 165.20/23.79 % (3842818)Instructions burned: 28122 (million) % 165.20/23.79 % (3842836)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2467919129:i=206:fgj=on:rtra=on_2791 on theBenchmark for (2791ds/206Mi) % 165.20/23.79 % (3842836)Instruction limit reached! % 165.20/23.79 % (3842836)------------------------------ % 165.20/23.79 % (3842836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.20/23.79 % (3842836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.20/23.79 % (3842836)CaDiCaL version: 2.1.3 % 165.20/23.79 % (3842836)Termination reason: Instruction limit % 165.20/23.79 % (3842836)Termination phase: Saturation % 165.20/23.79 % (3842836)Time elapsed: 0.057 s % 165.20/23.79 % (3842836)Peak memory usage: 18 MB % 165.20/23.79 % (3842836)Instructions burned: 210 (million) % 165.20/23.79 % (3842838)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3115080279:i=232:rtra=on_2790 on theBenchmark for (2790ds/232Mi) % 165.20/23.79 % (3842838)Instruction limit reached! % 165.20/23.79 % (3842838)------------------------------ % 165.20/23.79 % (3842838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.20/23.79 % (3842838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.20/23.79 % (3842838)CaDiCaL version: 2.1.3 % 165.20/23.79 % (3842838)Termination reason: Instruction limit % 165.20/23.79 % (3842838)Termination phase: Saturation % 165.20/23.79 % (3842838)Time elapsed: 0.058 s % 165.20/23.79 % (3842838)Peak memory usage: 17 MB % 165.20/23.79 % (3842838)Instructions burned: 233 (million) % 165.20/23.79 % (3842840)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3373498040:i=262:rtra=on_2789 on theBenchmark for (2789ds/262Mi) % 165.20/23.79 % (3842840)Instruction limit reached! % 165.20/23.79 % (3842840)------------------------------ % 165.20/23.79 % (3842840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.20/23.79 % (3842840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.20/23.79 % (3842840)CaDiCaL version: 2.1.3 % 165.20/23.79 % (3842840)Termination reason: Instruction limit % 165.20/23.79 % (3842840)Termination phase: Saturation % 165.20/23.79 % (3842840)Time elapsed: 0.066 s % 165.20/23.79 % (3842840)Peak memory usage: 18 MB % 165.20/23.79 % (3842840)Instructions burned: 264 (million) % 165.20/23.79 % (3842842)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3332530319:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2789 on theBenchmark for (2789ds/318Mi) % 165.20/23.79 % (3842842)Instruction limit reached! % 165.20/23.79 % (3842842)------------------------------ % 165.20/23.79 % (3842842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.20/23.79 % (3842842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.20/23.79 % (3842842)CaDiCaL version: 2.1.3 % 165.20/23.79 % (3842842)Termination reason: Instruction limit % 165.20/23.79 % (3842842)Termination phase: Saturation % 165.20/23.79 % (3842842)Time elapsed: 0.089 s % 165.20/23.79 % (3842842)Peak memory usage: 20 MB % 165.20/23.79 % (3842842)Instructions burned: 320 (million) % 165.20/23.79 % (3842844)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4238911168:i=1428:nm=2:rtra=on_2788 on theBenchmark for (2788ds/1428Mi) % 179.68/25.64 % (3842844)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.68/25.64 % (3842844)Terminated due to inappropriate strategy. % 179.68/25.64 % (3842844)------------------------------ % 179.68/25.64 % (3842844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.68/25.64 % (3842844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.68/25.64 % (3842844)CaDiCaL version: 2.1.3 % 179.68/25.64 % (3842844)Termination reason: Inappropriate % 179.68/25.64 % (3842844)Time elapsed: 0.052 s % 179.68/25.64 % (3842844)Peak memory usage: 15 MB % 179.68/25.64 % (3842844)Instructions burned: 110 (million) % 179.68/25.64 % (3842844)------------------------------ % 179.68/25.64 % (3842844)------------------------------ % 179.68/25.64 % (3842846)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=121993906:i=262:bd=preordered:rtra=on:fsd=on_2787 on theBenchmark for (2787ds/262Mi) % 179.68/25.64 % (3842846)Instruction limit reached! % 179.68/25.64 % (3842846)------------------------------ % 179.68/25.64 % (3842846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.68/25.64 % (3842846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.68/25.64 % (3842846)CaDiCaL version: 2.1.3 % 179.68/25.64 % (3842846)Termination reason: Instruction limit % 179.68/25.64 % (3842846)Termination phase: Saturation % 179.68/25.64 % (3842846)Time elapsed: 0.065 s % 179.68/25.64 % (3842846)Peak memory usage: 18 MB % 179.68/25.64 % (3842846)Instructions burned: 266 (million) % 179.68/25.64 % (3842848)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=1052747405:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2786 on theBenchmark for (2786ds/1368Mi) % 179.68/25.64 % (3842848)Instruction limit reached! % 179.68/25.64 % (3842848)------------------------------ % 179.68/25.64 % (3842848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.68/25.64 % (3842848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.68/25.64 % (3842848)CaDiCaL version: 2.1.3 % 179.68/25.64 % (3842848)Termination reason: Instruction limit % 179.68/25.64 % (3842848)Termination phase: Saturation % 179.68/25.64 % (3842848)Time elapsed: 0.373 s % 179.68/25.64 % (3842848)Peak memory usage: 23 MB % 179.68/25.64 % (3842848)Instructions burned: 1369 (million) % 179.68/25.64 % (3842850)ott-21_1_sil=16000:si=on:fs=off:random_seed=1637430050:i=360:av=off:fsr=off:rtra=on_2782 on theBenchmark for (2782ds/360Mi) % 179.68/25.64 % (3842850)Instruction limit reached! % 179.68/25.64 % (3842850)------------------------------ % 179.68/25.64 % (3842850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.68/25.64 % (3842850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.68/25.64 % (3842850)CaDiCaL version: 2.1.3 % 179.68/25.64 % (3842850)Termination reason: Instruction limit % 179.68/25.64 % (3842850)Termination phase: Saturation % 179.68/25.64 % (3842850)Time elapsed: 0.096 s % 179.68/25.64 % (3842850)Peak memory usage: 17 MB % 179.68/25.64 % (3842850)Instructions burned: 362 (million) % 179.68/25.64 % (3842852)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3856761221:i=954:bd=all:rtra=on_2781 on theBenchmark for (2781ds/954Mi) % 179.68/25.64 % (3842852)Instruction limit reached! % 179.68/25.64 % (3842852)------------------------------ % 179.68/25.64 % (3842852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.68/25.64 % (3842852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.68/25.64 % (3842852)CaDiCaL version: 2.1.3 % 179.68/25.64 % (3842852)Termination reason: Instruction limit % 179.68/25.64 % (3842852)Termination phase: Saturation % 179.68/25.64 % (3842852)Time elapsed: 0.294 s % 179.68/25.64 % (3842852)Peak memory usage: 21 MB % 179.68/25.64 % (3842852)Instructions burned: 956 (million) % 179.68/25.64 % (3842854)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1656325205:fmbsr=1.3:i=1730:ins=25:rtra=on_2778 on theBenchmark for (2778ds/1730Mi) % 179.68/25.64 % (3842854)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 179.68/25.64 % (3842854)Terminated due to inappropriate strategy. % 179.68/25.64 % (3842854)------------------------------ % 179.68/25.64 % (3842854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 179.68/25.64 % (3842854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 179.68/25.64 % (3842854)CaDiCaL version: 2.1.3 % 179.68/25.64 % (3842854)Termination reason: Inappropriate % 219.01/31.14 % (3842854)Time elapsed: 0.028 s % 219.01/31.14 % (3842854)Peak memory usage: 15 MB % 219.01/31.14 % (3842854)Instructions burned: 109 (million) % 219.01/31.14 % (3842854)------------------------------ % 219.01/31.14 % (3842854)------------------------------ % 219.01/31.14 % (3842856)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1263767158:i=2358:rtra=on_2778 on theBenchmark for (2778ds/2358Mi) % 219.01/31.14 % (3842810)Instruction limit reached! % 219.01/31.14 % (3842810)------------------------------ % 219.01/31.14 % (3842810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.01/31.14 % (3842810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.01/31.14 % (3842810)CaDiCaL version: 2.1.3 % 219.01/31.14 % (3842810)Termination reason: Instruction limit % 219.01/31.14 % (3842810)Termination phase: Saturation % 219.01/31.14 % (3842810)Time elapsed: 9.461 s % 219.01/31.14 % (3842810)Peak memory usage: 88 MB % 219.01/31.14 % (3842810)Instructions burned: 17629 (million) % 219.01/31.14 % (3842858)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=354318868:i=1778:ins=1:rtra=on_2771 on theBenchmark for (2771ds/1778Mi) % 219.01/31.14 % (3842858)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.01/31.14 % (3842858)Terminated due to inappropriate strategy. % 219.01/31.14 % (3842858)------------------------------ % 219.01/31.14 % (3842858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.01/31.14 % (3842858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.01/31.14 % (3842858)CaDiCaL version: 2.1.3 % 219.01/31.14 % (3842858)Termination reason: Inappropriate % 219.01/31.14 % (3842858)Time elapsed: 0.072 s % 219.01/31.14 % (3842858)Peak memory usage: 18 MB % 219.01/31.14 % (3842858)Instructions burned: 149 (million) % 219.01/31.14 % (3842858)------------------------------ % 219.01/31.14 % (3842858)------------------------------ % 219.01/31.14 % (3842856)Instruction limit reached! % 219.01/31.14 % (3842856)------------------------------ % 219.01/31.14 % (3842856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.01/31.14 % (3842856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.01/31.14 % (3842856)CaDiCaL version: 2.1.3 % 219.01/31.14 % (3842856)Termination reason: Instruction limit % 219.01/31.14 % (3842856)Termination phase: Saturation % 219.01/31.14 % (3842856)Time elapsed: 0.748 s % 219.01/31.14 % (3842856)Peak memory usage: 27 MB % 219.01/31.14 % (3842856)Instructions burned: 2360 (million) % 219.01/31.14 % (3842861)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=791914328:i=1758:kws=inv_precedence:fsr=off:rtra=on_2770 on theBenchmark for (2770ds/1758Mi) % 219.01/31.14 % (3842860)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=4269877198:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2770 on theBenchmark for (2770ds/1384Mi) % 219.01/31.14 % (3842861)Instruction limit reached! % 219.01/31.14 % (3842861)------------------------------ % 219.01/31.14 % (3842861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.01/31.14 % (3842861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.01/31.14 % (3842861)CaDiCaL version: 2.1.3 % 219.01/31.14 % (3842861)Termination reason: Instruction limit % 219.01/31.14 % (3842861)Termination phase: Saturation % 219.01/31.14 % (3842861)Time elapsed: 0.539 s % 219.01/31.14 % (3842861)Peak memory usage: 29 MB % 219.01/31.14 % (3842861)Instructions burned: 1759 (million) % 219.01/31.14 % (3842864)fmb+10_1_sil=64000:si=on:random_seed=1751255284:i=44122:nm=2:rtra=on:gsp=on_2765 on theBenchmark for (2765ds/44122Mi) % 219.01/31.14 % (3842864)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 219.01/31.14 % (3842864)Terminated due to inappropriate strategy. % 219.01/31.14 % (3842864)------------------------------ % 219.01/31.14 % (3842864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.01/31.14 % (3842864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.01/31.14 % (3842864)CaDiCaL version: 2.1.3 % 219.01/31.14 % (3842864)Termination reason: Inappropriate % 219.01/31.14 % (3842864)Time elapsed: 0.031 s % 219.01/31.14 % (3842864)Peak memory usage: 15 MB % 219.01/31.14 % (3842864)Instructions burned: 120 (million) % 219.01/31.14 % (3842864)------------------------------ % 219.01/31.14 % (3842864)------------------------------ % 219.01/31.14 % (3842866)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2324112122:i=19030:nm=5:rtra=on_2764 on theBenchmark for (2764ds/19030Mi) % 252.79/35.91 % (3842866)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.79/35.91 % (3842866)Terminated due to inappropriate strategy. % 252.79/35.91 % (3842866)------------------------------ % 252.79/35.91 % (3842866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.79/35.91 % (3842866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.79/35.91 % (3842866)CaDiCaL version: 2.1.3 % 252.79/35.91 % (3842866)Termination reason: Inappropriate % 252.79/35.91 % (3842866)Time elapsed: 0.028 s % 252.79/35.91 % (3842866)Peak memory usage: 15 MB % 252.79/35.91 % (3842866)Instructions burned: 111 (million) % 252.79/35.91 % (3842866)------------------------------ % 252.79/35.91 % (3842866)------------------------------ % 252.79/35.91 % (3842868)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2637344349:fmbsr=1.7:i=1840:rtra=on_2764 on theBenchmark for (2764ds/1840Mi) % 252.79/35.91 % (3842868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.79/35.91 % (3842868)Terminated due to inappropriate strategy. % 252.79/35.91 % (3842868)------------------------------ % 252.79/35.91 % (3842868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.79/35.91 % (3842868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.79/35.91 % (3842868)CaDiCaL version: 2.1.3 % 252.79/35.91 % (3842868)Termination reason: Inappropriate % 252.79/35.91 % (3842868)Time elapsed: 0.028 s % 252.79/35.91 % (3842868)Peak memory usage: 15 MB % 252.79/35.91 % (3842868)Instructions burned: 110 (million) % 252.79/35.91 % (3842868)------------------------------ % 252.79/35.91 % (3842868)------------------------------ % 252.79/35.91 % (3842870)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2642986196:i=10262:rtra=on_2763 on theBenchmark for (2763ds/10262Mi) % 252.79/35.91 % (3842860)Instruction limit reached! % 252.79/35.91 % (3842860)------------------------------ % 252.79/35.91 % (3842860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.79/35.91 % (3842860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.79/35.91 % (3842860)CaDiCaL version: 2.1.3 % 252.79/35.91 % (3842860)Termination reason: Instruction limit % 252.79/35.91 % (3842860)Termination phase: Saturation % 252.79/35.91 % (3842860)Time elapsed: 0.809 s % 252.79/35.91 % (3842860)Peak memory usage: 26 MB % 252.79/35.91 % (3842860)Instructions burned: 1384 (million) % 252.79/35.91 % (3842872)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3409576702:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2762 on theBenchmark for (2762ds/2944Mi) % 252.79/35.91 % (3842872)Instruction limit reached! % 252.79/35.91 % (3842872)------------------------------ % 252.79/35.91 % (3842872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.79/35.91 % (3842872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.79/35.91 % (3842872)CaDiCaL version: 2.1.3 % 252.79/35.91 % (3842872)Termination reason: Instruction limit % 252.79/35.91 % (3842872)Termination phase: Saturation % 252.79/35.91 % (3842872)Time elapsed: 1.463 s % 252.79/35.91 % (3842872)Peak memory usage: 30 MB % 252.79/35.91 % (3842872)Instructions burned: 2945 (million) % 252.79/35.91 % (3842874)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=112933197:i=12648:rtra=on_2747 on theBenchmark for (2747ds/12648Mi) % 252.79/35.91 % (3842874)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.79/35.91 % (3842874)Terminated due to inappropriate strategy. % 252.79/35.91 % (3842874)------------------------------ % 252.79/35.91 % (3842874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 252.79/35.91 % (3842874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.79/35.91 % (3842874)CaDiCaL version: 2.1.3 % 252.79/35.91 % (3842874)Termination reason: Inappropriate % 252.79/35.91 % (3842874)Time elapsed: 0.052 s % 252.79/35.91 % (3842874)Peak memory usage: 16 MB % 252.79/35.91 % (3842874)Instructions burned: 111 (million) % 252.79/35.91 % (3842874)------------------------------ % 252.79/35.91 % (3842874)------------------------------ % 252.79/35.91 % (3842876)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=63731264:fmbsr=2.30978:i=4348:rtra=on_2746 on theBenchmark for (2746ds/4348Mi) % 252.79/35.91 % (3842876)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 252.79/35.91 % (3842876)Terminated due to inappropriate strategy. % 252.79/35.91 % (3842876)------------------------------ % 300.36/42.63 % (3842876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.63 % (3842876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.63 % (3842876)CaDiCaL version: 2.1.3 % 300.36/42.63 % (3842876)Termination reason: Inappropriate % 300.36/42.63 % (3842876)Time elapsed: 0.052 s % 300.36/42.63 % (3842876)Peak memory usage: 15 MB % 300.36/42.63 % (3842876)Instructions burned: 110 (million) % 300.36/42.63 % (3842876)------------------------------ % 300.36/42.63 % (3842876)------------------------------ % 300.36/42.63 % (3842878)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3629597849:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2746 on theBenchmark for (2746ds/1738Mi) % 300.36/42.63 % (3842878)Instruction limit reached! % 300.36/42.63 % (3842878)------------------------------ % 300.36/42.63 % (3842878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.63 % (3842878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.63 % (3842878)CaDiCaL version: 2.1.3 % 300.36/42.63 % (3842878)Termination reason: Instruction limit % 300.36/42.63 % (3842878)Termination phase: Saturation % 300.36/42.63 % (3842878)Time elapsed: 1.038 s % 300.36/42.63 % (3842878)Peak memory usage: 23 MB % 300.36/42.63 % (3842878)Instructions burned: 1739 (million) % 300.36/42.63 % (3842880)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1142796593:i=10228:av=off:rtra=on_2735 on theBenchmark for (2735ds/10228Mi) % 300.36/42.63 % (3842870)Instruction limit reached! % 300.36/42.63 % (3842870)------------------------------ % 300.36/42.63 % (3842870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.63 % (3842870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.63 % (3842870)CaDiCaL version: 2.1.3 % 300.36/42.63 % (3842870)Termination reason: Instruction limit % 300.36/42.63 % (3842870)Termination phase: Saturation % 300.36/42.63 % (3842870)Time elapsed: 3.166 s % 300.36/42.63 % (3842870)Peak memory usage: 66 MB % 300.36/42.63 % (3842870)Instructions burned: 10265 (million) % 300.36/42.63 % (3842882)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2176492928:i=108564:rtra=on_2732 on theBenchmark for (2732ds/108564Mi) % 300.36/42.63 % (3842882)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.36/42.63 % (3842882)Terminated due to inappropriate strategy. % 300.36/42.63 % (3842882)------------------------------ % 300.36/42.63 % (3842882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.63 % (3842882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.63 % (3842882)CaDiCaL version: 2.1.3 % 300.36/42.63 % (3842882)Termination reason: Inappropriate % 300.36/42.63 % (3842882)Time elapsed: 0.028 s % 300.36/42.63 % (3842882)Peak memory usage: 15 MB % 300.36/42.63 % (3842882)Instructions burned: 111 (million) % 300.36/42.63 % (3842882)------------------------------ % 300.36/42.63 % (3842882)------------------------------ % 300.36/42.63 % (3842884)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=963124490:i=7024:aac=none:rtra=on_2731 on theBenchmark for (2731ds/7024Mi) % 300.36/42.63 % (3842884)Instruction limit reached! % 300.36/42.63 % (3842884)------------------------------ % 300.36/42.63 % (3842884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.63 % (3842884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.63 % (3842884)CaDiCaL version: 2.1.3 % 300.36/42.63 % (3842884)Termination reason: Instruction limit % 300.36/42.63 % (3842884)Termination phase: Saturation % 300.36/42.63 % (3842884)Time elapsed: 2.139 s % 300.36/42.63 % (3842884)Peak memory usage: 48 MB % 300.36/42.63 % (3842884)Instructions burned: 7025 (million) % 300.36/42.63 % (3842886)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3508682573:i=7546:rtra=on:amm=off_2710 on theBenchmark for (2710ds/7546Mi) % 300.36/42.63 % (3842886)Instruction limit reached! % 300.36/42.63 % (3842886)------------------------------ % 300.36/42.63 % (3842886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.36/42.63 % (3842886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.36/42.63 % (3842886)CaDiCaL version: 2.1.3 % 300.36/42.63 % (3842886)Termination reason: Instruction limit % 300.36/42.63 % (3842886)Termination phase: Saturation % 300.36/42.63 % (3842886)Time elapsed: 1.878 s % 300.36/42.63 % (3842886)Peak memory usage: 28 MB % 300.36/42.63 % (3842886)Instructions burned: 7550 (million) % 300.36/42.63 % (3842888)ott+11_1_sil=16000:si=on:gs=on:random_seed=3611927201:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra= % 300.36/42.63 Terminated % 300.36/42.64 % Vampire exiting %------------------------------------------------------------------------------