%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX145_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n014.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:46:33 PM UTC 2026 % Result : Timeout 300.27s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX145_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 % Computer : n014.cluster.edu % 0.08/0.21 % Model : x86_64 x86_64 % 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.21 % Memory : 8046.5625MB % 0.08/0.21 % OS : Linux 6.8.0-71-generic % 0.08/0.21 % CPULimit : 300 % 0.08/0.21 % WCLimit : 300 % 0.08/0.21 % DateTime : Mon Sep 28 15:04:20 UTC 2026 % 0.08/0.21 % CPUTime : % 0.08/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.25 Running first-order model finding % 0.08/0.25 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.65/1.13 % (1837295)Will run a generic schedule for satisfiability detection. % 3.65/1.13 % (1837304)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3406737688:i=116_2996 on theBenchmark for (2996ds/116Mi) % 3.65/1.13 % (1837301)% WARNING: option uhcvi not known. % 3.65/1.13 % (1837300)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1889318278_2996 on theBenchmark for (2996ds/0Mi) % 3.65/1.13 % (1837301)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3978944298:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 3.65/1.13 % (1837302)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=944765474:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 3.65/1.13 % (1837303)dis+10_1_sil=32000:sp=arity:random_seed=1777682553:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 3.65/1.13 % (1837305)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1075567523:i=131_2996 on theBenchmark for (2996ds/131Mi) % 3.65/1.13 % (1837306)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2237893456:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 3.65/1.13 % (1837304)Instruction limit reached! % 3.65/1.13 % (1837304)------------------------------ % 3.65/1.13 % (1837304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/1.13 % (1837304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/1.13 % (1837304)CaDiCaL version: 2.1.3 % 3.65/1.13 % (1837304)Termination reason: Instruction limit % 3.65/1.13 % (1837304)Termination phase: Property scanning % 3.65/1.13 % (1837304)Time elapsed: 0.026 s % 3.65/1.13 % (1837304)Peak memory usage: 10 MB % 3.65/1.13 % (1837304)Instructions burned: 120 (million) % 3.65/1.13 % (1837314)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2803480127:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi) % 3.65/1.13 % (1837303)Instruction limit reached! % 3.65/1.13 % (1837303)------------------------------ % 3.65/1.13 % (1837303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/1.13 % (1837303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/1.13 % (1837303)CaDiCaL version: 2.1.3 % 3.65/1.13 % (1837303)Termination reason: Instruction limit % 3.65/1.13 % (1837303)Termination phase: Property scanning % 3.65/1.13 % (1837303)Time elapsed: 0.042 s % 3.65/1.13 % (1837303)Peak memory usage: 10 MB % 3.65/1.13 % (1837303)Instructions burned: 105 (million) % 3.65/1.13 % (1837305)Instruction limit reached! % 3.65/1.13 % (1837305)------------------------------ % 3.65/1.13 % (1837305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/1.13 % (1837305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/1.13 % (1837305)CaDiCaL version: 2.1.3 % 3.65/1.13 % (1837305)Termination reason: Instruction limit % 3.65/1.13 % (1837305)Termination phase: Property scanning % 3.65/1.13 % (1837305)Time elapsed: 0.053 s % 3.65/1.13 % (1837305)Peak memory usage: 10 MB % 3.65/1.13 % (1837305)Instructions burned: 133 (million) % 3.65/1.13 % (1837316)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2421306584:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi) % 3.65/1.13 % (1837306)Instruction limit reached! % 3.65/1.13 % (1837306)------------------------------ % 3.65/1.13 % (1837306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/1.13 % (1837306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.65/1.13 % (1837306)CaDiCaL version: 2.1.3 % 3.65/1.13 % (1837306)Termination reason: Instruction limit % 3.65/1.13 % (1837306)Termination phase: Property scanning % 3.65/1.13 % (1837306)Time elapsed: 0.065 s % 3.65/1.13 % (1837306)Peak memory usage: 10 MB % 3.65/1.13 % (1837306)Instructions burned: 161 (million) % 3.65/1.13 % (1837317)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=3563051749:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi) % 3.65/1.13 % (1837319)ott-21_1_sil=16000:fs=off:random_seed=3321793991:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 3.65/1.13 % (1837316)Instruction limit reached! % 3.65/1.13 % (1837316)------------------------------ % 3.65/1.13 % (1837316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.65/1.13 % (1837316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.64 % (1837316)CaDiCaL version: 2.1.3 % 6.02/1.64 % (1837316)Termination reason: Instruction limit % 6.02/1.64 % (1837316)Termination phase: Property scanning % 6.02/1.64 % (1837316)Time elapsed: 0.052 s % 6.02/1.64 % (1837316)Peak memory usage: 10 MB % 6.02/1.64 % (1837316)Instructions burned: 132 (million) % 6.02/1.64 % (1837314)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.02/1.64 % (1837314)Terminated due to inappropriate strategy. % 6.02/1.64 % (1837314)------------------------------ % 6.02/1.64 % (1837314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.02/1.64 % (1837314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.64 % (1837314)CaDiCaL version: 2.1.3 % 6.02/1.64 % (1837314)Termination reason: Inappropriate % 6.02/1.64 % (1837314)Time elapsed: 0.094 s % 6.02/1.64 % (1837314)Peak memory usage: 11 MB % 6.02/1.64 % (1837314)Instructions burned: 467 (million) % 6.02/1.64 % (1837314)------------------------------ % 6.02/1.64 % (1837314)------------------------------ % 6.02/1.64 % (1837322)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=43484740:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi) % 6.02/1.64 % (1837323)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2809430004:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 6.02/1.64 % (1837319)Instruction limit reached! % 6.02/1.64 % (1837319)------------------------------ % 6.02/1.64 % (1837319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.02/1.64 % (1837319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.64 % (1837319)CaDiCaL version: 2.1.3 % 6.02/1.64 % (1837319)Termination reason: Instruction limit % 6.02/1.64 % (1837319)Termination phase: Property scanning % 6.02/1.64 % (1837319)Time elapsed: 0.071 s % 6.02/1.64 % (1837319)Peak memory usage: 10 MB % 6.02/1.64 % (1837319)Instructions burned: 182 (million) % 6.02/1.64 % (1837326)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=737832751:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 6.02/1.64 % (1837300)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.02/1.64 % (1837300)Terminated due to inappropriate strategy. % 6.02/1.64 % (1837300)------------------------------ % 6.02/1.64 % (1837300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.02/1.64 % (1837300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.64 % (1837300)CaDiCaL version: 2.1.3 % 6.02/1.64 % (1837300)Termination reason: Inappropriate % 6.02/1.64 % (1837300)Time elapsed: 0.177 s % 6.02/1.64 % (1837300)Peak memory usage: 11 MB % 6.02/1.64 % (1837300)Instructions burned: 467 (million) % 6.02/1.64 % (1837300)------------------------------ % 6.02/1.64 % (1837300)------------------------------ % 6.02/1.64 % (1837328)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2098593446:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 6.02/1.64 % (1837323)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.02/1.64 % (1837323)Terminated due to inappropriate strategy. % 6.02/1.64 % (1837323)------------------------------ % 6.02/1.64 % (1837323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.02/1.64 % (1837323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.64 % (1837323)CaDiCaL version: 2.1.3 % 6.02/1.64 % (1837323)Termination reason: Inappropriate % 6.02/1.64 % (1837323)Time elapsed: 0.071 s % 6.02/1.64 % (1837323)Peak memory usage: 11 MB % 6.02/1.64 % (1837323)Instructions burned: 354 (million) % 6.02/1.64 % (1837323)------------------------------ % 6.02/1.64 % (1837323)------------------------------ % 6.02/1.64 % (1837330)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=2833018902:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 6.02/1.64 % (1837322)Instruction limit reached! % 6.02/1.64 % (1837322)------------------------------ % 6.02/1.64 % (1837322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.02/1.64 % (1837322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.02/1.64 % (1837322)CaDiCaL version: 2.1.3 % 6.02/1.64 % (1837322)Termination reason: Instruction limit % 6.02/1.64 % (1837322)Termination phase: Saturation % 6.02/1.64 % (1837322)Time elapsed: 0.183 s % 6.02/1.64 % (1837322)Peak memory usage: 12 MB % 6.02/1.64 % (1837322)Instructions burned: 479 (million) % 18.59/3.14 % (1837328)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.59/3.14 % (1837328)Terminated due to inappropriate strategy. % 18.59/3.14 % (1837328)------------------------------ % 18.59/3.14 % (1837328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.59/3.14 % (1837328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.59/3.14 % (1837328)CaDiCaL version: 2.1.3 % 18.59/3.14 % (1837328)Termination reason: Inappropriate % 18.59/3.14 % (1837328)Time elapsed: 0.135 s % 18.59/3.14 % (1837328)Peak memory usage: 11 MB % 18.59/3.14 % (1837328)Instructions burned: 354 (million) % 18.59/3.14 % (1837328)------------------------------ % 18.59/3.14 % (1837328)------------------------------ % 18.59/3.14 % (1837332)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=269494454:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 18.59/3.14 % (1837317)Instruction limit reached! % 18.59/3.14 % (1837317)------------------------------ % 18.59/3.14 % (1837317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.59/3.14 % (1837317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.59/3.14 % (1837317)CaDiCaL version: 2.1.3 % 18.59/3.14 % (1837317)Termination reason: Instruction limit % 18.59/3.14 % (1837317)Termination phase: Saturation % 18.59/3.14 % (1837317)Time elapsed: 0.265 s % 18.59/3.14 % (1837317)Peak memory usage: 13 MB % 18.59/3.14 % (1837317)Instructions burned: 684 (million) % 18.59/3.14 % (1837333)fmb+10_1_sil=64000:random_seed=494811689:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 18.59/3.14 % (1837335)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=73877950:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 18.59/3.14 % (1837330)Instruction limit reached! % 18.59/3.14 % (1837330)------------------------------ % 18.59/3.14 % (1837330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.59/3.14 % (1837330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.59/3.14 % (1837330)CaDiCaL version: 2.1.3 % 18.59/3.14 % (1837330)Termination reason: Instruction limit % 18.59/3.14 % (1837330)Termination phase: Saturation % 18.59/3.14 % (1837330)Time elapsed: 0.179 s % 18.59/3.14 % (1837330)Peak memory usage: 13 MB % 18.59/3.14 % (1837330)Instructions burned: 696 (million) % 18.59/3.14 % (1837338)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3247238850:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 18.59/3.14 % (1837338)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.59/3.14 % (1837338)Terminated due to inappropriate strategy. % 18.59/3.14 % (1837338)------------------------------ % 18.59/3.14 % (1837338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.59/3.14 % (1837338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.59/3.14 % (1837338)CaDiCaL version: 2.1.3 % 18.59/3.14 % (1837338)Termination reason: Inappropriate % 18.59/3.14 % (1837338)Time elapsed: 0.094 s % 18.59/3.14 % (1837338)Peak memory usage: 11 MB % 18.59/3.14 % (1837338)Instructions burned: 467 (million) % 18.59/3.14 % (1837338)------------------------------ % 18.59/3.14 % (1837338)------------------------------ % 18.59/3.14 % (1837340)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2909789248:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 18.59/3.14 % (1837333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.59/3.14 % (1837333)Terminated due to inappropriate strategy. % 18.59/3.14 % (1837333)------------------------------ % 18.59/3.14 % (1837333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.59/3.14 % (1837333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.59/3.14 % (1837333)CaDiCaL version: 2.1.3 % 18.59/3.14 % (1837333)Termination reason: Inappropriate % 18.59/3.14 % (1837333)Time elapsed: 0.177 s % 18.59/3.14 % (1837333)Peak memory usage: 11 MB % 18.59/3.14 % (1837333)Instructions burned: 467 (million) % 18.59/3.14 % (1837333)------------------------------ % 18.59/3.14 % (1837333)------------------------------ % 18.59/3.14 % (1837335)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.59/3.14 % (1837335)Terminated due to inappropriate strategy. % 18.59/3.14 % (1837335)------------------------------ % 18.59/3.14 % (1837335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.59/3.14 % (1837335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/3.58 % (1837335)CaDiCaL version: 2.1.3 % 20.53/3.58 % (1837335)Termination reason: Inappropriate % 20.53/3.58 % (1837335)Time elapsed: 0.177 s % 20.53/3.58 % (1837335)Peak memory usage: 11 MB % 20.53/3.58 % (1837335)Instructions burned: 467 (million) % 20.53/3.58 % (1837335)------------------------------ % 20.53/3.58 % (1837335)------------------------------ % 20.53/3.58 % (1837342)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2288947788:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 20.53/3.58 % (1837343)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=445590966:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 20.53/3.58 % (1837326)Instruction limit reached! % 20.53/3.58 % (1837326)------------------------------ % 20.53/3.58 % (1837326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.53/3.58 % (1837326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/3.58 % (1837326)CaDiCaL version: 2.1.3 % 20.53/3.58 % (1837326)Termination reason: Instruction limit % 20.53/3.58 % (1837326)Termination phase: Saturation % 20.53/3.58 % (1837326)Time elapsed: 0.469 s % 20.53/3.58 % (1837326)Peak memory usage: 18 MB % 20.53/3.58 % (1837326)Instructions burned: 1179 (million) % 20.53/3.58 % (1837346)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=648365705:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 20.53/3.58 % (1837332)Instruction limit reached! % 20.53/3.58 % (1837332)------------------------------ % 20.53/3.58 % (1837332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.53/3.58 % (1837332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/3.58 % (1837332)CaDiCaL version: 2.1.3 % 20.53/3.58 % (1837332)Termination reason: Instruction limit % 20.53/3.58 % (1837332)Termination phase: Saturation % 20.53/3.58 % (1837332)Time elapsed: 0.348 s % 20.53/3.58 % (1837332)Peak memory usage: 15 MB % 20.53/3.58 % (1837332)Instructions burned: 881 (million) % 20.53/3.58 % (1837348)ott-2_1_sil=16000:newcnf=on:random_seed=481389517:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 20.53/3.58 % (1837343)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.53/3.58 % (1837343)Terminated due to inappropriate strategy. % 20.53/3.58 % (1837343)------------------------------ % 20.53/3.58 % (1837343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.53/3.58 % (1837343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/3.58 % (1837343)CaDiCaL version: 2.1.3 % 20.53/3.58 % (1837343)Termination reason: Inappropriate % 20.53/3.58 % (1837343)Time elapsed: 0.177 s % 20.53/3.58 % (1837343)Peak memory usage: 11 MB % 20.53/3.58 % (1837343)Instructions burned: 467 (million) % 20.53/3.58 % (1837343)------------------------------ % 20.53/3.58 % (1837343)------------------------------ % 20.53/3.58 % (1837350)ott+10_1_sil=32000:tgt=ground:random_seed=2669505091:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 20.53/3.58 % (1837346)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.53/3.58 % (1837346)Terminated due to inappropriate strategy. % 20.53/3.58 % (1837346)------------------------------ % 20.53/3.58 % (1837346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.53/3.58 % (1837346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/3.58 % (1837346)CaDiCaL version: 2.1.3 % 20.53/3.58 % (1837346)Termination reason: Inappropriate % 20.53/3.58 % (1837346)Time elapsed: 0.177 s % 20.53/3.58 % (1837346)Peak memory usage: 11 MB % 20.53/3.58 % (1837346)Instructions burned: 467 (million) % 20.53/3.58 % (1837346)------------------------------ % 20.53/3.58 % (1837346)------------------------------ % 20.53/3.58 % (1837352)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4291467199:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 20.53/3.58 % (1837352)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 20.53/3.58 % (1837352)Terminated due to inappropriate strategy. % 20.53/3.58 % (1837352)------------------------------ % 20.53/3.58 % (1837352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.53/3.58 % (1837352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.53/3.58 % (1837352)CaDiCaL version: 2.1.3 % 20.53/3.58 % (1837352)Termination reason: Inappropriate % 20.53/3.58 % (1837352)Time elapsed: 0.177 s % 20.53/3.58 % (1837352)Peak memory usage: 11 MB % 82.72/12.18 % (1837352)Instructions burned: 467 (million) % 82.72/12.18 % (1837352)------------------------------ % 82.72/12.18 % (1837352)------------------------------ % 82.72/12.18 % (1837354)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=57152451:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi) % 82.72/12.18 % (1837348)Instruction limit reached! % 82.72/12.18 % (1837348)------------------------------ % 82.72/12.18 % (1837348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.72/12.18 % (1837348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.72/12.18 % (1837348)CaDiCaL version: 2.1.3 % 82.72/12.18 % (1837348)Termination reason: Instruction limit % 82.72/12.18 % (1837348)Termination phase: Saturation % 82.72/12.18 % (1837348)Time elapsed: 0.371 s % 82.72/12.18 % (1837348)Peak memory usage: 17 MB % 82.72/12.18 % (1837348)Instructions burned: 870 (million) % 82.72/12.18 % (1837356)dis+21_1_sil=32000:sas=cadical:random_seed=2750419342:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 82.72/12.18 % (1837342)Instruction limit reached! % 82.72/12.18 % (1837342)------------------------------ % 82.72/12.18 % (1837342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.72/12.18 % (1837342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.72/12.18 % (1837342)CaDiCaL version: 2.1.3 % 82.72/12.18 % (1837342)Termination reason: Instruction limit % 82.72/12.18 % (1837342)Termination phase: Saturation % 82.72/12.18 % (1837342)Time elapsed: 0.598 s % 82.72/12.18 % (1837342)Peak memory usage: 18 MB % 82.72/12.18 % (1837342)Instructions burned: 1474 (million) % 82.72/12.18 % (1837358)ott+11_1_sil=16000:gs=on:random_seed=799042307:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 82.72/12.18 % (1837340)Instruction limit reached! % 82.72/12.18 % (1837340)------------------------------ % 82.72/12.18 % (1837340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.72/12.18 % (1837340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.72/12.18 % (1837340)CaDiCaL version: 2.1.3 % 82.72/12.18 % (1837340)Termination reason: Instruction limit % 82.72/12.18 % (1837340)Termination phase: Saturation % 82.72/12.18 % (1837340)Time elapsed: 1.201 s % 82.72/12.18 % (1837340)Peak memory usage: 21 MB % 82.72/12.19 % (1837340)Instructions burned: 5135 (million) % 82.72/12.19 % (1837360)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=321478837:fmbsr=1.6:i=67534_2979 on theBenchmark for (2979ds/67534Mi) % 82.72/12.19 % (1837360)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 82.72/12.19 % (1837360)Terminated due to inappropriate strategy. % 82.72/12.19 % (1837360)------------------------------ % 82.72/12.19 % (1837360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.72/12.19 % (1837360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.72/12.19 % (1837360)CaDiCaL version: 2.1.3 % 82.72/12.19 % (1837360)Termination reason: Inappropriate % 82.72/12.19 % (1837360)Time elapsed: 0.093 s % 82.72/12.19 % (1837360)Peak memory usage: 11 MB % 82.72/12.19 % (1837360)Instructions burned: 467 (million) % 82.72/12.19 % (1837360)------------------------------ % 82.72/12.19 % (1837360)------------------------------ % 82.72/12.19 % (1837362)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=46761952:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2978 on theBenchmark for (2978ds/4591Mi) % 82.72/12.19 % (1837358)Instruction limit reached! % 82.72/12.19 % (1837358)------------------------------ % 82.72/12.19 % (1837358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.72/12.19 % (1837358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.72/12.19 % (1837358)CaDiCaL version: 2.1.3 % 82.72/12.19 % (1837358)Termination reason: Instruction limit % 82.72/12.19 % (1837358)Termination phase: Saturation % 82.72/12.19 % (1837358)Time elapsed: 0.887 s % 82.72/12.19 % (1837358)Peak memory usage: 19 MB % 82.72/12.19 % (1837358)Instructions burned: 2253 (million) % 82.72/12.19 % (1837364)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3800607743:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 82.72/12.19 % (1837354)Instruction limit reached! % 82.72/12.19 % (1837354)------------------------------ % 82.72/12.19 % (1837354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.72/12.19 % (1837354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.72/12.19 % (1837354)CaDiCaL version: 2.1.3 % 101.27/15.05 % (1837354)Termination reason: Instruction limit % 101.27/15.05 % (1837354)Termination phase: Saturation % 101.27/15.05 % (1837354)Time elapsed: 1.483 s % 101.27/15.05 % (1837354)Peak memory usage: 20 MB % 101.27/15.05 % (1837354)Instructions burned: 3512 (million) % 101.27/15.05 % (1837366)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3097208658:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 101.27/15.05 % (1837356)Instruction limit reached! % 101.27/15.05 % (1837356)------------------------------ % 101.27/15.05 % (1837356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/15.05 % (1837356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/15.05 % (1837356)CaDiCaL version: 2.1.3 % 101.27/15.05 % (1837356)Termination reason: Instruction limit % 101.27/15.05 % (1837356)Termination phase: Saturation % 101.27/15.05 % (1837356)Time elapsed: 1.629 s % 101.27/15.05 % (1837356)Peak memory usage: 19 MB % 101.27/15.05 % (1837356)Instructions burned: 3773 (million) % 101.27/15.05 % (1837368)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=486074789:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 101.27/15.05 % (1837350)Instruction limit reached! % 101.27/15.05 % (1837350)------------------------------ % 101.27/15.05 % (1837350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/15.05 % (1837350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/15.05 % (1837350)CaDiCaL version: 2.1.3 % 101.27/15.05 % (1837350)Termination reason: Instruction limit % 101.27/15.05 % (1837350)Termination phase: Saturation % 101.27/15.05 % (1837350)Time elapsed: 2.020 s % 101.27/15.05 % (1837350)Peak memory usage: 29 MB % 101.27/15.05 % (1837350)Instructions burned: 5116 (million) % 101.27/15.05 % (1837370)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3454809328:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 101.27/15.05 % (1837362)Instruction limit reached! % 101.27/15.05 % (1837362)------------------------------ % 101.27/15.05 % (1837362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/15.05 % (1837362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/15.05 % (1837362)CaDiCaL version: 2.1.3 % 101.27/15.05 % (1837362)Termination reason: Instruction limit % 101.27/15.05 % (1837362)Termination phase: Saturation % 101.27/15.05 % (1837362)Time elapsed: 1.040 s % 101.27/15.05 % (1837362)Peak memory usage: 18 MB % 101.27/15.05 % (1837362)Instructions burned: 4597 (million) % 101.27/15.05 % (1837372)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2199451367:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 101.27/15.05 % (1837368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.27/15.05 % (1837368)Terminated due to inappropriate strategy. % 101.27/15.05 % (1837368)------------------------------ % 101.27/15.05 % (1837368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/15.05 % (1837368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/15.05 % (1837368)CaDiCaL version: 2.1.3 % 101.27/15.05 % (1837368)Termination reason: Inappropriate % 101.27/15.05 % (1837368)Time elapsed: 0.177 s % 101.27/15.05 % (1837368)Peak memory usage: 11 MB % 101.27/15.05 % (1837368)Instructions burned: 467 (million) % 101.27/15.05 % (1837368)------------------------------ % 101.27/15.05 % (1837368)------------------------------ % 101.27/15.05 % (1837374)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2576947559:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 101.27/15.05 % (1837370)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.27/15.05 % (1837370)Terminated due to inappropriate strategy. % 101.27/15.05 % (1837370)------------------------------ % 101.27/15.05 % (1837370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/15.05 % (1837370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/15.05 % (1837370)CaDiCaL version: 2.1.3 % 101.27/15.05 % (1837370)Termination reason: Inappropriate % 101.27/15.05 % (1837370)Time elapsed: 0.177 s % 101.27/15.05 % (1837370)Peak memory usage: 11 MB % 101.27/15.05 % (1837370)Instructions burned: 467 (million) % 101.27/15.05 % (1837370)------------------------------ % 101.27/15.05 % (1837370)------------------------------ % 101.27/15.05 % (1837372)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 101.27/15.05 % (1837372)Terminated due to inappropriate strategy. % 101.27/15.05 % (1837372)------------------------------ % 101.27/15.05 % (1837372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.08/16.96 % (1837372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.08/16.96 % (1837372)CaDiCaL version: 2.1.3 % 116.08/16.96 % (1837372)Termination reason: Inappropriate % 116.08/16.96 % (1837372)Time elapsed: 0.093 s % 116.08/16.96 % (1837372)Peak memory usage: 11 MB % 116.08/16.96 % (1837372)Instructions burned: 467 (million) % 116.08/16.96 % (1837372)------------------------------ % 116.08/16.96 % (1837372)------------------------------ % 116.08/16.96 % (1837376)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2308828561:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 116.08/16.96 % (1837377)dis+10_16:1_sil=16000:random_seed=1987182410:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi) % 116.08/16.96 % (1837366)Instruction limit reached! % 116.08/16.96 % (1837366)------------------------------ % 116.08/16.96 % (1837366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.08/16.96 % (1837366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.08/16.96 % (1837366)CaDiCaL version: 2.1.3 % 116.08/16.96 % (1837366)Termination reason: Instruction limit % 116.08/16.96 % (1837366)Termination phase: Saturation % 116.08/16.96 % (1837366)Time elapsed: 2.227 s % 116.08/16.96 % (1837366)Peak memory usage: 20 MB % 116.08/16.96 % (1837366)Instructions burned: 5211 (million) % 116.08/16.96 % (1837380)ott-3_8_sil=64000:random_seed=1769417777:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 116.08/16.96 % (1837377)Instruction limit reached! % 116.08/16.96 % (1837377)------------------------------ % 116.08/16.96 % (1837377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.08/16.96 % (1837377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.08/16.96 % (1837377)CaDiCaL version: 2.1.3 % 116.08/16.96 % (1837377)Termination reason: Instruction limit % 116.08/16.96 % (1837377)Termination phase: Saturation % 116.08/16.96 % (1837377)Time elapsed: 1.907 s % 116.08/16.96 % (1837377)Peak memory usage: 22 MB % 116.08/16.96 % (1837377)Instructions burned: 9157 (million) % 116.08/16.96 % (1837382)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2263998500:fmbsr=2:i=32576_2947 on theBenchmark for (2947ds/32576Mi) % 116.08/16.96 % (1837382)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 116.08/16.96 % (1837382)Terminated due to inappropriate strategy. % 116.08/16.96 % (1837382)------------------------------ % 116.08/16.96 % (1837382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.08/16.96 % (1837382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.08/16.96 % (1837382)CaDiCaL version: 2.1.3 % 116.08/16.96 % (1837382)Termination reason: Inappropriate % 116.08/16.96 % (1837382)Time elapsed: 0.094 s % 116.08/16.96 % (1837382)Peak memory usage: 11 MB % 116.08/16.96 % (1837382)Instructions burned: 467 (million) % 116.08/16.96 % (1837382)------------------------------ % 116.08/16.96 % (1837382)------------------------------ % 116.08/16.96 % (1837384)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1747795358:i=11404_2946 on theBenchmark for (2946ds/11404Mi) % 116.08/16.96 % (1837376)Instruction limit reached! % 116.08/16.96 % (1837376)------------------------------ % 116.08/16.96 % (1837376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.08/16.96 % (1837376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.08/16.96 % (1837376)CaDiCaL version: 2.1.3 % 116.08/16.96 % (1837376)Termination reason: Instruction limit % 116.08/16.96 % (1837376)Termination phase: Saturation % 116.08/16.96 % (1837376)Time elapsed: 3.151 s % 116.08/16.96 % (1837376)Peak memory usage: 29 MB % 116.08/16.96 % (1837376)Instructions burned: 8175 (million) % 116.08/16.96 % (1837386)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3006424689:i=14134_2935 on theBenchmark for (2935ds/14134Mi) % 116.08/16.96 % (1837384)Instruction limit reached! % 116.08/16.96 % (1837384)------------------------------ % 116.08/16.96 % (1837384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.08/16.96 % (1837384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.08/16.96 % (1837384)CaDiCaL version: 2.1.3 % 116.08/16.96 % (1837384)Termination reason: Instruction limit % 116.08/16.96 % (1837384)Termination phase: Saturation % 116.08/16.96 % (1837384)Time elapsed: 2.332 s % 116.08/16.96 % (1837384)Peak memory usage: 29 MB % 116.08/16.96 % (1837384)Instructions burned: 11404 (million) % 116.08/16.96 % (1837388)dis+33_16_sil=32000:sac=on:random_seed=1990213332:i=15851:nm=0_2923 on theBenchmark for (2923ds/15851Mi) % 116.08/16.96 % (1837388)Instruction limit reached! % 116.08/16.96 % (1837388)------------------------------ % 136.90/19.81 % (1837388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.90/19.81 % (1837388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.90/19.81 % (1837388)CaDiCaL version: 2.1.3 % 136.90/19.81 % (1837388)Termination reason: Instruction limit % 136.90/19.81 % (1837388)Termination phase: Saturation % 136.90/19.81 % (1837388)Time elapsed: 4.219 s % 136.90/19.81 % (1837388)Peak memory usage: 27 MB % 136.90/19.81 % (1837388)Instructions burned: 15851 (million) % 136.90/19.81 % (1837708)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3981812039:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi) % 136.90/19.81 % (1837386)Instruction limit reached! % 136.90/19.81 % (1837386)------------------------------ % 136.90/19.81 % (1837386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.90/19.81 % (1837386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.90/19.81 % (1837386)CaDiCaL version: 2.1.3 % 136.90/19.81 % (1837386)Termination reason: Instruction limit % 136.90/19.81 % (1837386)Termination phase: Saturation % 136.90/19.81 % (1837386)Time elapsed: 6.038 s % 136.90/19.81 % (1837386)Peak memory usage: 29 MB % 136.90/19.81 % (1837386)Instructions burned: 14137 (million) % 136.90/19.81 % (1837714)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1783825517:s2a=on:i=53295_2874 on theBenchmark for (2874ds/53295Mi) % 136.90/19.81 % (1837374)Instruction limit reached! % 136.90/19.81 % (1837374)------------------------------ % 136.90/19.81 % (1837374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.90/19.81 % (1837374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.90/19.81 % (1837374)CaDiCaL version: 2.1.3 % 136.90/19.81 % (1837374)Termination reason: Instruction limit % 136.90/19.81 % (1837374)Termination phase: Saturation % 136.90/19.81 % (1837374)Time elapsed: 10.368 s % 136.90/19.81 % (1837374)Peak memory usage: 18 MB % 136.90/19.81 % (1837374)Instructions burned: 22565 (million) % 136.90/19.81 % (1837720)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=832144801:i=26857:ins=20_2863 on theBenchmark for (2863ds/26857Mi) % 136.90/19.81 % (1837720)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.90/19.81 % (1837720)Terminated due to inappropriate strategy. % 136.90/19.81 % (1837720)------------------------------ % 136.90/19.81 % (1837720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.90/19.81 % (1837720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.90/19.81 % (1837720)CaDiCaL version: 2.1.3 % 136.90/19.81 % (1837720)Termination reason: Inappropriate % 136.90/19.81 % (1837720)Time elapsed: 0.354 s % 136.90/19.81 % (1837720)Peak memory usage: 11 MB % 136.90/19.81 % (1837720)Instructions burned: 467 (million) % 136.90/19.81 % (1837720)------------------------------ % 136.90/19.81 % (1837720)------------------------------ % 136.90/19.81 % (1837725)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3065220364:i=28120:bs=on:fsr=off_2859 on theBenchmark for (2859ds/28120Mi) % 136.90/19.81 % (1837380)Instruction limit reached! % 136.90/19.81 % (1837380)------------------------------ % 136.90/19.81 % (1837380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.90/19.81 % (1837380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.90/19.81 % (1837380)CaDiCaL version: 2.1.3 % 136.90/19.81 % (1837380)Termination reason: Instruction limit % 136.90/19.81 % (1837380)Termination phase: Saturation % 136.90/19.81 % (1837380)Time elapsed: 9.231 s % 136.90/19.81 % (1837380)Peak memory usage: 31 MB % 136.90/19.81 % (1837380)Instructions burned: 20139 (million) % 136.90/19.81 % (1837728)fmb+10_1_sil=256000:fmbss=7:random_seed=704553434:fmbsr=1.6:i=182295_2856 on theBenchmark for (2856ds/182295Mi) % 136.90/19.81 % (1837728)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 136.90/19.81 % (1837728)Terminated due to inappropriate strategy. % 136.90/19.81 % (1837728)------------------------------ % 136.90/19.81 % (1837728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 136.90/19.81 % (1837728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.90/19.81 % (1837728)CaDiCaL version: 2.1.3 % 136.90/19.81 % (1837728)Termination reason: Inappropriate % 136.90/19.81 % (1837728)Time elapsed: 0.373 s % 136.90/19.81 % (1837728)Peak memory usage: 11 MB % 136.90/19.81 % (1837728)Instructions burned: 467 (million) % 136.90/19.81 % (1837728)------------------------------ % 136.90/19.81 % (1837728)------------------------------ % 148.83/21.51 % (1837733)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=180266337:i=44625:gsp=on_2852 on theBenchmark for (2852ds/44625Mi) % 148.83/21.51 % (1837733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.51 % (1837733)Terminated due to inappropriate strategy. % 148.83/21.51 % (1837733)------------------------------ % 148.83/21.51 % (1837733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.51 % (1837733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.51 % (1837733)CaDiCaL version: 2.1.3 % 148.83/21.51 % (1837733)Termination reason: Inappropriate % 148.83/21.51 % (1837733)Time elapsed: 0.327 s % 148.83/21.51 % (1837733)Peak memory usage: 11 MB % 148.83/21.51 % (1837733)Instructions burned: 467 (million) % 148.83/21.51 % (1837733)------------------------------ % 148.83/21.51 % (1837733)------------------------------ % 148.83/21.51 % (1837741)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1964563399:i=160505_2848 on theBenchmark for (2848ds/160505Mi) % 148.83/21.51 % (1837741)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.51 % (1837741)Terminated due to inappropriate strategy. % 148.83/21.51 % (1837741)------------------------------ % 148.83/21.51 % (1837741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.51 % (1837741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.51 % (1837741)CaDiCaL version: 2.1.3 % 148.83/21.51 % (1837741)Termination reason: Inappropriate % 148.83/21.51 % (1837741)Time elapsed: 0.377 s % 148.83/21.51 % (1837741)Peak memory usage: 11 MB % 148.83/21.51 % (1837741)Instructions burned: 467 (million) % 148.83/21.51 % (1837741)------------------------------ % 148.83/21.51 % (1837741)------------------------------ % 148.83/21.51 % (1837746)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1763307206:fmbsr=1.3:i=225729_2844 on theBenchmark for (2844ds/225729Mi) % 148.83/21.51 % (1837746)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.51 % (1837746)Terminated due to inappropriate strategy. % 148.83/21.51 % (1837746)------------------------------ % 148.83/21.51 % (1837746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.51 % (1837746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.51 % (1837746)CaDiCaL version: 2.1.3 % 148.83/21.51 % (1837746)Termination reason: Inappropriate % 148.83/21.51 % (1837746)Time elapsed: 0.400 s % 148.83/21.51 % (1837746)Peak memory usage: 11 MB % 148.83/21.51 % (1837746)Instructions burned: 467 (million) % 148.83/21.51 % (1837746)------------------------------ % 148.83/21.51 % (1837746)------------------------------ % 148.83/21.51 % (1837748)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1590058581:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 148.83/21.51 % (1837748)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.51 % (1837748)Terminated due to inappropriate strategy. % 148.83/21.51 % (1837748)------------------------------ % 148.83/21.51 % (1837748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.51 % (1837748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.51 % (1837748)CaDiCaL version: 2.1.3 % 148.83/21.51 % (1837748)Termination reason: Inappropriate % 148.83/21.51 % (1837748)Time elapsed: 0.376 s % 148.83/21.51 % (1837748)Peak memory usage: 11 MB % 148.83/21.51 % (1837748)Instructions burned: 467 (million) % 148.83/21.51 % (1837748)------------------------------ % 148.83/21.51 % (1837748)------------------------------ % 148.83/21.51 % (1837750)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1368305326:rtra=on_2835 on theBenchmark for (2835ds/0Mi) % 148.83/21.51 % (1837750)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 148.83/21.51 % (1837750)Terminated due to inappropriate strategy. % 148.83/21.51 % (1837750)------------------------------ % 148.83/21.51 % (1837750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.83/21.51 % (1837750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.83/21.51 % (1837750)CaDiCaL version: 2.1.3 % 148.83/21.51 % (1837750)Termination reason: Inappropriate % 148.83/21.51 % (1837750)Time elapsed: 0.225 s % 148.83/21.51 % (1837750)Peak memory usage: 11 MB % 148.83/21.51 % (1837750)Instructions burned: 469 (million) % 148.83/21.51 % (1837750)------------------------------ % 148.83/21.51 % (1837750)------------------------------ % 148.83/21.51 % (1837752)% WARNING: option uhcvi not known. % 148.83/21.51 % (1837752)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=587156219:i=271062:add=off:rtra=on:rawr=on_2833 on theBenchmark for (2833ds/271062Mi) % 165.99/24.01 % (1837364)Instruction limit reached! % 165.99/24.01 % (1837364)------------------------------ % 165.99/24.01 % (1837364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.99/24.01 % (1837364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.99/24.01 % (1837364)CaDiCaL version: 2.1.3 % 165.99/24.01 % (1837364)Termination reason: Instruction limit % 165.99/24.01 % (1837364)Termination phase: Saturation % 165.99/24.01 % (1837364)Time elapsed: 15.076 s % 165.99/24.01 % (1837364)Peak memory usage: 17 MB % 165.99/24.01 % (1837364)Instructions burned: 29340 (million) % 165.99/24.01 % (1837754)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2897383789:i=176048:add=on:rtra=on:rawr=on_2825 on theBenchmark for (2825ds/176048Mi) % 165.99/24.01 % (1837708)Instruction limit reached! % 165.99/24.01 % (1837708)------------------------------ % 165.99/24.01 % (1837708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.99/24.01 % (1837708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.99/24.01 % (1837708)CaDiCaL version: 2.1.3 % 165.99/24.01 % (1837708)Termination reason: Instruction limit % 165.99/24.01 % (1837708)Termination phase: Saturation % 165.99/24.01 % (1837708)Time elapsed: 7.125 s % 165.99/24.01 % (1837708)Peak memory usage: 91 MB % 165.99/24.01 % (1837708)Instructions burned: 17628 (million) % 165.99/24.01 % (1837758)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2692063660:i=206:fgj=on:rtra=on_2809 on theBenchmark for (2809ds/206Mi) % 165.99/24.01 % (1837758)Instruction limit reached! % 165.99/24.01 % (1837758)------------------------------ % 165.99/24.01 % (1837758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.99/24.01 % (1837758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.99/24.01 % (1837758)CaDiCaL version: 2.1.3 % 165.99/24.01 % (1837758)Termination reason: Instruction limit % 165.99/24.01 % (1837758)Termination phase: Property scanning % 165.99/24.01 % (1837758)Time elapsed: 0.080 s % 165.99/24.01 % (1837758)Peak memory usage: 10 MB % 165.99/24.01 % (1837758)Instructions burned: 210 (million) % 165.99/24.01 % (1837761)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3721131718:i=232:rtra=on_2808 on theBenchmark for (2808ds/232Mi) % 165.99/24.01 % (1837761)Instruction limit reached! % 165.99/24.01 % (1837761)------------------------------ % 165.99/24.01 % (1837761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.99/24.01 % (1837761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.99/24.01 % (1837761)CaDiCaL version: 2.1.3 % 165.99/24.01 % (1837761)Termination reason: Instruction limit % 165.99/24.01 % (1837761)Termination phase: Property scanning % 165.99/24.01 % (1837761)Time elapsed: 0.052 s % 165.99/24.01 % (1837761)Peak memory usage: 10 MB % 165.99/24.01 % (1837761)Instructions burned: 233 (million) % 165.99/24.01 % (1837764)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4245895132:i=262:rtra=on_2807 on theBenchmark for (2807ds/262Mi) % 165.99/24.01 % (1837764)Instruction limit reached! % 165.99/24.01 % (1837764)------------------------------ % 165.99/24.01 % (1837764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.99/24.01 % (1837764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.99/24.01 % (1837764)CaDiCaL version: 2.1.3 % 165.99/24.01 % (1837764)Termination reason: Instruction limit % 165.99/24.01 % (1837764)Termination phase: Property scanning % 165.99/24.01 % (1837764)Time elapsed: 0.114 s % 165.99/24.01 % (1837764)Peak memory usage: 11 MB % 165.99/24.01 % (1837764)Instructions burned: 263 (million) % 165.99/24.01 % (1837768)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3923251958:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2806 on theBenchmark for (2806ds/318Mi) % 165.99/24.01 % (1837768)Instruction limit reached! % 165.99/24.01 % (1837768)------------------------------ % 165.99/24.01 % (1837768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.99/24.01 % (1837768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.99/24.01 % (1837768)CaDiCaL version: 2.1.3 % 165.99/24.01 % (1837768)Termination reason: Instruction limit % 165.99/24.01 % (1837768)Termination phase: Property scanning % 165.99/24.01 % (1837768)Time elapsed: 0.135 s % 165.99/24.01 % (1837768)Peak memory usage: 11 MB % 165.99/24.01 % (1837768)Instructions burned: 319 (million) % 165.99/24.01 % (1837770)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2621750898:i=1428:nm=2:rtra=on_2804 on theBenchmark for (2804ds/1428Mi) % 213.48/30.63 % (1837770)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.48/30.63 % (1837770)Terminated due to inappropriate strategy. % 213.48/30.63 % (1837770)------------------------------ % 213.48/30.63 % (1837770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.48/30.63 % (1837770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.48/30.63 % (1837770)CaDiCaL version: 2.1.3 % 213.48/30.63 % (1837770)Termination reason: Inappropriate % 213.48/30.63 % (1837770)Time elapsed: 0.199 s % 213.48/30.63 % (1837770)Peak memory usage: 11 MB % 213.48/30.63 % (1837770)Instructions burned: 468 (million) % 213.48/30.63 % (1837770)------------------------------ % 213.48/30.63 % (1837770)------------------------------ % 213.48/30.63 % (1837772)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1987127379:i=262:bd=preordered:rtra=on:fsd=on_2802 on theBenchmark for (2802ds/262Mi) % 213.48/30.63 % (1837772)Instruction limit reached! % 213.48/30.63 % (1837772)------------------------------ % 213.48/30.63 % (1837772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.48/30.63 % (1837772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.48/30.63 % (1837772)CaDiCaL version: 2.1.3 % 213.48/30.63 % (1837772)Termination reason: Instruction limit % 213.48/30.63 % (1837772)Termination phase: Property scanning % 213.48/30.63 % (1837772)Time elapsed: 0.112 s % 213.48/30.63 % (1837772)Peak memory usage: 11 MB % 213.48/30.63 % (1837772)Instructions burned: 263 (million) % 213.48/30.63 % (1837774)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=3743815488:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2801 on theBenchmark for (2801ds/1368Mi) % 213.48/30.63 % (1837774)Instruction limit reached! % 213.48/30.63 % (1837774)------------------------------ % 213.48/30.63 % (1837774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.48/30.63 % (1837774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.48/30.63 % (1837774)CaDiCaL version: 2.1.3 % 213.48/30.63 % (1837774)Termination reason: Instruction limit % 213.48/30.63 % (1837774)Termination phase: Saturation % 213.48/30.63 % (1837774)Time elapsed: 0.580 s % 213.48/30.63 % (1837774)Peak memory usage: 17 MB % 213.48/30.63 % (1837774)Instructions burned: 1368 (million) % 213.48/30.63 % (1837776)ott-21_1_sil=16000:si=on:fs=off:random_seed=2657996365:i=360:av=off:fsr=off:rtra=on_2795 on theBenchmark for (2795ds/360Mi) % 213.48/30.63 % (1837776)Instruction limit reached! % 213.48/30.63 % (1837776)------------------------------ % 213.48/30.63 % (1837776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.48/30.63 % (1837776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.48/30.63 % (1837776)CaDiCaL version: 2.1.3 % 213.48/30.63 % (1837776)Termination reason: Instruction limit % 213.48/30.63 % (1837776)Termination phase: Property scanning % 213.48/30.63 % (1837776)Time elapsed: 0.153 s % 213.48/30.63 % (1837776)Peak memory usage: 11 MB % 213.48/30.63 % (1837776)Instructions burned: 361 (million) % 213.48/30.63 % (1837778)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1887398700:i=954:bd=all:rtra=on_2793 on theBenchmark for (2793ds/954Mi) % 213.48/30.63 % (1837778)Instruction limit reached! % 213.48/30.63 % (1837778)------------------------------ % 213.48/30.63 % (1837778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.48/30.63 % (1837778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.48/30.63 % (1837778)CaDiCaL version: 2.1.3 % 213.48/30.63 % (1837778)Termination reason: Instruction limit % 213.48/30.63 % (1837778)Termination phase: Saturation % 213.48/30.63 % (1837778)Time elapsed: 0.400 s % 213.48/30.63 % (1837778)Peak memory usage: 16 MB % 213.48/30.63 % (1837778)Instructions burned: 954 (million) % 213.48/30.63 % (1837782)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2032028030:fmbsr=1.3:i=1730:ins=25:rtra=on_2789 on theBenchmark for (2789ds/1730Mi) % 213.48/30.63 % (1837782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 213.48/30.63 % (1837782)Terminated due to inappropriate strategy. % 213.48/30.63 % (1837782)------------------------------ % 213.48/30.63 % (1837782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 213.48/30.63 % (1837782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.13 % (1837782)CaDiCaL version: 2.1.3 % 273.54/39.13 % (1837782)Termination reason: Inappropriate % 273.54/39.13 % (1837782)Time elapsed: 0.150 s % 273.54/39.13 % (1837782)Peak memory usage: 11 MB % 273.54/39.13 % (1837782)Instructions burned: 355 (million) % 273.54/39.13 % (1837782)------------------------------ % 273.54/39.13 % (1837782)------------------------------ % 273.54/39.13 % (1837784)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=695759435:i=2358:rtra=on_2787 on theBenchmark for (2787ds/2358Mi) % 273.54/39.13 % (1837784)Instruction limit reached! % 273.54/39.13 % (1837784)------------------------------ % 273.54/39.13 % (1837784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/39.13 % (1837784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.13 % (1837784)CaDiCaL version: 2.1.3 % 273.54/39.13 % (1837784)Termination reason: Instruction limit % 273.54/39.13 % (1837784)Termination phase: Saturation % 273.54/39.13 % (1837784)Time elapsed: 0.973 s % 273.54/39.13 % (1837784)Peak memory usage: 15 MB % 273.54/39.13 % (1837784)Instructions burned: 2360 (million) % 273.54/39.13 % (1837786)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1451226267:i=1778:ins=1:rtra=on_2777 on theBenchmark for (2777ds/1778Mi) % 273.54/39.13 % (1837786)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 273.54/39.13 % (1837786)Terminated due to inappropriate strategy. % 273.54/39.13 % (1837786)------------------------------ % 273.54/39.13 % (1837786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/39.13 % (1837786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.13 % (1837786)CaDiCaL version: 2.1.3 % 273.54/39.13 % (1837786)Termination reason: Inappropriate % 273.54/39.13 % (1837786)Time elapsed: 0.151 s % 273.54/39.13 % (1837786)Peak memory usage: 11 MB % 273.54/39.13 % (1837786)Instructions burned: 355 (million) % 273.54/39.13 % (1837786)------------------------------ % 273.54/39.13 % (1837786)------------------------------ % 273.54/39.13 % (1837788)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=3772818794:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2775 on theBenchmark for (2775ds/1384Mi) % 273.54/39.13 % (1837788)Instruction limit reached! % 273.54/39.13 % (1837788)------------------------------ % 273.54/39.13 % (1837788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/39.13 % (1837788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.13 % (1837788)CaDiCaL version: 2.1.3 % 273.54/39.13 % (1837788)Termination reason: Instruction limit % 273.54/39.13 % (1837788)Termination phase: Saturation % 273.54/39.13 % (1837788)Time elapsed: 0.588 s % 273.54/39.13 % (1837788)Peak memory usage: 18 MB % 273.54/39.13 % (1837788)Instructions burned: 1385 (million) % 273.54/39.13 % (1837790)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3523449855:i=1758:kws=inv_precedence:fsr=off:rtra=on_2769 on theBenchmark for (2769ds/1758Mi) % 273.54/39.13 % (1837790)Instruction limit reached! % 273.54/39.13 % (1837790)------------------------------ % 273.54/39.13 % (1837790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/39.13 % (1837790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.13 % (1837790)CaDiCaL version: 2.1.3 % 273.54/39.13 % (1837790)Termination reason: Instruction limit % 273.54/39.13 % (1837790)Termination phase: Saturation % 273.54/39.13 % (1837790)Time elapsed: 0.515 s % 273.54/39.13 % (1837790)Peak memory usage: 15 MB % 273.54/39.13 % (1837790)Instructions burned: 1763 (million) % 273.54/39.13 % (1837794)fmb+10_1_sil=64000:si=on:random_seed=1723431055:i=44122:nm=2:rtra=on:gsp=on_2764 on theBenchmark for (2764ds/44122Mi) % 273.54/39.13 % (1837794)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 273.54/39.13 % (1837794)Terminated due to inappropriate strategy. % 273.54/39.13 % (1837794)------------------------------ % 273.54/39.13 % (1837794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.54/39.13 % (1837794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.54/39.13 % (1837794)CaDiCaL version: 2.1.3 % 273.54/39.13 % (1837794)Termination reason: Inappropriate % 273.54/39.13 % (1837794)Time elapsed: 0.172 s % 273.54/39.13 % (1837794)Peak memory usage: 11 MB % 273.54/39.13 % (1837794)Instructions burned: 469 (million) % 273.54/39.13 % (1837794)------------------------------ % 273.54/39.13 % (1837794)----------------------------Terminated % 300.27/42.84 % Vampire exiting % 300.27/42.84 Terminated %------------------------------------------------------------------------------