%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX097_1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:29 PM UTC 2026 % Result : Timeout 300.56s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX097_1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.19 % Computer : n019.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 15:01:03 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 Running first-order model finding % 0.10/0.22 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.92/0.88 % (4067452)Will run a generic schedule for satisfiability detection. % 3.92/0.88 % (4067458)% WARNING: option uhcvi not known. % 3.92/0.88 % (4067458)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2944665061:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.92/0.88 % (4067457)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3201440049_2999 on theBenchmark for (2999ds/0Mi) % 3.92/0.88 % (4067459)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2262749391:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.92/0.88 % (4067460)dis+10_1_sil=32000:sp=arity:random_seed=2066933394:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.92/0.88 % (4067461)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2179667995:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.92/0.88 % (4067457)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.92/0.88 % (4067457)Terminated due to inappropriate strategy. % 3.92/0.88 % (4067457)------------------------------ % 3.92/0.88 % (4067457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.92/0.88 % (4067457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/0.88 % (4067457)CaDiCaL version: 2.1.3 % 3.92/0.88 % (4067457)Termination reason: Inappropriate % 3.92/0.88 % (4067457)Time elapsed: 0.003 s % 3.92/0.88 % (4067457)Peak memory usage: 10 MB % 3.92/0.88 % (4067457)Instructions burned: 4 (million) % 3.92/0.88 % (4067457)------------------------------ % 3.92/0.88 % (4067457)------------------------------ % 3.92/0.88 % (4067462)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=475449791:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.92/0.88 % (4067463)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2307391736:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.92/0.88 % (4067469)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=973622896:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.92/0.88 % (4067469)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.92/0.88 % (4067469)Terminated due to inappropriate strategy. % 3.92/0.89 % (4067469)------------------------------ % 3.92/0.89 % (4067469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.92/0.89 % (4067469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/0.89 % (4067469)CaDiCaL version: 2.1.3 % 3.92/0.89 % (4067469)Termination reason: Inappropriate % 3.92/0.89 % (4067469)Time elapsed: 0.002 s % 3.92/0.89 % (4067469)Peak memory usage: 11 MB % 3.92/0.89 % (4067469)Instructions burned: 3 (million) % 3.92/0.89 % (4067469)------------------------------ % 3.92/0.89 % (4067469)------------------------------ % 3.92/0.89 % (4067473)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1758303556:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.92/0.89 % (4067460)Instruction limit reached! % 3.92/0.89 % (4067460)------------------------------ % 3.92/0.89 % (4067460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.92/0.89 % (4067460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/0.89 % (4067460)CaDiCaL version: 2.1.3 % 3.92/0.89 % (4067460)Termination reason: Instruction limit % 3.92/0.89 % (4067460)Termination phase: Saturation % 3.92/0.89 % (4067460)Time elapsed: 0.069 s % 3.92/0.89 % (4067460)Peak memory usage: 13 MB % 3.92/0.89 % (4067460)Instructions burned: 103 (million) % 3.92/0.89 % (4067461)Instruction limit reached! % 3.92/0.89 % (4067461)------------------------------ % 3.92/0.89 % (4067461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.92/0.89 % (4067461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/0.89 % (4067461)CaDiCaL version: 2.1.3 % 3.92/0.89 % (4067461)Termination reason: Instruction limit % 3.92/0.89 % (4067461)Termination phase: Saturation % 3.92/0.89 % (4067461)Time elapsed: 0.079 s % 3.92/0.89 % (4067461)Peak memory usage: 13 MB % 3.92/0.89 % (4067461)Instructions burned: 117 (million) % 3.92/0.89 % (4067462)Instruction limit reached! % 3.92/0.89 % (4067462)------------------------------ % 3.92/0.89 % (4067462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.92/0.89 % (4067462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.92/0.89 % (4067462)CaDiCaL version: 2.1.3 % 3.92/0.89 % (4067462)Termination reason: Instruction limit % 5.70/1.19 % (4067462)Termination phase: Saturation % 5.70/1.19 % (4067462)Time elapsed: 0.093 s % 5.70/1.19 % (4067462)Peak memory usage: 12 MB % 5.70/1.19 % (4067462)Instructions burned: 133 (million) % 5.70/1.19 % (4067475)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=1896018222:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.70/1.19 % (4067476)ott-21_1_sil=16000:fs=off:random_seed=4031352948:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.70/1.19 % (4067463)Instruction limit reached! % 5.70/1.19 % (4067463)------------------------------ % 5.70/1.19 % (4067463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.19 % (4067463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.19 % (4067463)CaDiCaL version: 2.1.3 % 5.70/1.19 % (4067463)Termination reason: Instruction limit % 5.70/1.19 % (4067463)Termination phase: Saturation % 5.70/1.19 % (4067463)Time elapsed: 0.110 s % 5.70/1.19 % (4067463)Peak memory usage: 13 MB % 5.70/1.19 % (4067463)Instructions burned: 160 (million) % 5.70/1.19 % (4067477)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3922318464:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.70/1.19 % (4067481)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1373543556:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.70/1.19 % (4067481)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.70/1.19 % (4067481)Terminated due to inappropriate strategy. % 5.70/1.19 % (4067481)------------------------------ % 5.70/1.19 % (4067481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.19 % (4067481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.19 % (4067481)CaDiCaL version: 2.1.3 % 5.70/1.19 % (4067481)Termination reason: Inappropriate % 5.70/1.19 % (4067481)Time elapsed: 0.003 s % 5.70/1.19 % (4067481)Peak memory usage: 10 MB % 5.70/1.19 % (4067481)Instructions burned: 5 (million) % 5.70/1.19 % (4067481)------------------------------ % 5.70/1.19 % (4067481)------------------------------ % 5.70/1.19 % (4067473)Instruction limit reached! % 5.70/1.19 % (4067473)------------------------------ % 5.70/1.19 % (4067473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.19 % (4067473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.19 % (4067473)CaDiCaL version: 2.1.3 % 5.70/1.19 % (4067473)Termination reason: Instruction limit % 5.70/1.19 % (4067473)Termination phase: Saturation % 5.70/1.19 % (4067473)Time elapsed: 0.101 s % 5.70/1.19 % (4067473)Peak memory usage: 13 MB % 5.70/1.19 % (4067473)Instructions burned: 132 (million) % 5.70/1.19 % (4067483)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3405695678:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.70/1.19 % (4067484)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=712852299:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.70/1.19 % (4067484)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.70/1.19 % (4067484)Terminated due to inappropriate strategy. % 5.70/1.19 % (4067484)------------------------------ % 5.70/1.19 % (4067484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.19 % (4067484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.19 % (4067484)CaDiCaL version: 2.1.3 % 5.70/1.19 % (4067484)Termination reason: Inappropriate % 5.70/1.19 % (4067484)Time elapsed: 0.002 s % 5.70/1.19 % (4067484)Peak memory usage: 10 MB % 5.70/1.19 % (4067484)Instructions burned: 3 (million) % 5.70/1.19 % (4067484)------------------------------ % 5.70/1.19 % (4067484)------------------------------ % 5.70/1.19 % (4067487)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=387049091: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.70/1.19 % (4067476)Instruction limit reached! % 5.70/1.19 % (4067476)------------------------------ % 5.70/1.19 % (4067476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.70/1.19 % (4067476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.70/1.19 % (4067476)CaDiCaL version: 2.1.3 % 5.70/1.19 % (4067476)Termination reason: Instruction limit % 5.70/1.19 % (4067476)Termination phase: Saturation % 35.13/5.25 % (4067476)Time elapsed: 0.121 s % 35.13/5.25 % (4067476)Peak memory usage: 12 MB % 35.13/5.25 % (4067476)Instructions burned: 181 (million) % 35.13/5.25 % (4067489)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2716456864:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 35.13/5.25 % (4067477)Instruction limit reached! % 35.13/5.25 % (4067477)------------------------------ % 35.13/5.25 % (4067477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.13/5.25 % (4067477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.13/5.25 % (4067477)CaDiCaL version: 2.1.3 % 35.13/5.25 % (4067477)Termination reason: Instruction limit % 35.13/5.25 % (4067477)Termination phase: Saturation % 35.13/5.25 % (4067477)Time elapsed: 0.344 s % 35.13/5.25 % (4067477)Peak memory usage: 14 MB % 35.13/5.25 % (4067477)Instructions burned: 477 (million) % 35.13/5.25 % (4067563)fmb+10_1_sil=64000:random_seed=95066742:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 35.13/5.25 % (4067563)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.13/5.25 % (4067563)Terminated due to inappropriate strategy. % 35.13/5.25 % (4067563)------------------------------ % 35.13/5.25 % (4067563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.13/5.25 % (4067563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.13/5.25 % (4067563)CaDiCaL version: 2.1.3 % 35.13/5.25 % (4067563)Termination reason: Inappropriate % 35.13/5.25 % (4067563)Time elapsed: 0.002 s % 35.13/5.25 % (4067563)Peak memory usage: 10 MB % 35.13/5.25 % (4067563)Instructions burned: 4 (million) % 35.13/5.25 % (4067563)------------------------------ % 35.13/5.25 % (4067563)------------------------------ % 35.13/5.25 % (4067572)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1879132998:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 35.13/5.25 % (4067572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.13/5.25 % (4067572)Terminated due to inappropriate strategy. % 35.13/5.25 % (4067572)------------------------------ % 35.13/5.25 % (4067572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.13/5.25 % (4067572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.13/5.25 % (4067572)CaDiCaL version: 2.1.3 % 35.13/5.25 % (4067572)Termination reason: Inappropriate % 35.13/5.25 % (4067572)Time elapsed: 0.002 s % 35.13/5.25 % (4067572)Peak memory usage: 10 MB % 35.13/5.25 % (4067572)Instructions burned: 3 (million) % 35.13/5.25 % (4067572)------------------------------ % 35.13/5.25 % (4067572)------------------------------ % 35.13/5.25 % (4067578)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1675410298:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 35.13/5.25 % (4067578)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.13/5.25 % (4067578)Terminated due to inappropriate strategy. % 35.13/5.25 % (4067578)------------------------------ % 35.13/5.25 % (4067578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.13/5.25 % (4067578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.13/5.25 % (4067578)CaDiCaL version: 2.1.3 % 35.13/5.25 % (4067578)Termination reason: Inappropriate % 35.13/5.25 % (4067578)Time elapsed: 0.002 s % 35.13/5.25 % (4067578)Peak memory usage: 10 MB % 35.13/5.25 % (4067578)Instructions burned: 3 (million) % 35.13/5.25 % (4067578)------------------------------ % 35.13/5.25 % (4067578)------------------------------ % 35.13/5.25 % (4067475)Instruction limit reached! % 35.13/5.25 % (4067475)------------------------------ % 35.13/5.25 % (4067475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.13/5.25 % (4067475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.13/5.25 % (4067475)CaDiCaL version: 2.1.3 % 35.13/5.25 % (4067475)Termination reason: Instruction limit % 35.13/5.25 % (4067475)Termination phase: Saturation % 35.13/5.25 % (4067475)Time elapsed: 0.449 s % 35.13/5.25 % (4067475)Peak memory usage: 18 MB % 35.13/5.25 % (4067475)Instructions burned: 686 (million) % 35.13/5.25 % (4067580)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2201210346:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 35.13/5.25 % (4067585)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=917187229:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 35.13/5.25 % (4067487)Instruction limit reached! % 35.13/5.25 % (4067487)------------------------------ % 59.33/8.61 % (4067487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.33/8.61 % (4067487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.33/8.61 % (4067487)CaDiCaL version: 2.1.3 % 59.33/8.61 % (4067487)Termination reason: Instruction limit % 59.33/8.61 % (4067487)Termination phase: Saturation % 59.33/8.61 % (4067487)Time elapsed: 0.424 s % 59.33/8.61 % (4067487)Peak memory usage: 19 MB % 59.33/8.61 % (4067487)Instructions burned: 693 (million) % 59.33/8.61 % (4067604)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2385725320:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 59.33/8.61 % (4067604)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 59.33/8.61 % (4067604)Terminated due to inappropriate strategy. % 59.33/8.61 % (4067604)------------------------------ % 59.33/8.61 % (4067604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.33/8.61 % (4067604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.33/8.61 % (4067604)CaDiCaL version: 2.1.3 % 59.33/8.61 % (4067604)Termination reason: Inappropriate % 59.33/8.61 % (4067604)Time elapsed: 0.003 s % 59.33/8.61 % (4067604)Peak memory usage: 11 MB % 59.33/8.61 % (4067604)Instructions burned: 4 (million) % 59.33/8.61 % (4067604)------------------------------ % 59.33/8.61 % (4067604)------------------------------ % 59.33/8.61 % (4067612)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1166383165:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 59.33/8.61 % (4067612)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 59.33/8.61 % (4067612)Terminated due to inappropriate strategy. % 59.33/8.61 % (4067612)------------------------------ % 59.33/8.61 % (4067612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.33/8.61 % (4067612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.33/8.61 % (4067612)CaDiCaL version: 2.1.3 % 59.33/8.61 % (4067612)Termination reason: Inappropriate % 59.33/8.61 % (4067612)Time elapsed: 0.004 s % 59.33/8.61 % (4067612)Peak memory usage: 11 MB % 59.33/8.61 % (4067612)Instructions burned: 3 (million) % 59.33/8.61 % (4067612)------------------------------ % 59.33/8.61 % (4067612)------------------------------ % 59.33/8.61 % (4067623)ott-2_1_sil=16000:newcnf=on:random_seed=264083350:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 59.33/8.61 % (4067483)Instruction limit reached! % 59.33/8.61 % (4067483)------------------------------ % 59.33/8.61 % (4067483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.33/8.61 % (4067483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.33/8.61 % (4067483)CaDiCaL version: 2.1.3 % 59.33/8.61 % (4067483)Termination reason: Instruction limit % 59.33/8.61 % (4067483)Termination phase: Saturation % 59.33/8.61 % (4067483)Time elapsed: 0.673 s % 59.33/8.61 % (4067483)Peak memory usage: 17 MB % 59.33/8.61 % (4067483)Instructions burned: 1179 (million) % 59.33/8.61 % (4067654)ott+10_1_sil=32000:tgt=ground:random_seed=4193260765:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 59.33/8.61 % (4067489)Instruction limit reached! % 59.33/8.61 % (4067489)------------------------------ % 59.33/8.61 % (4067489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.33/8.61 % (4067489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.33/8.61 % (4067489)CaDiCaL version: 2.1.3 % 59.33/8.61 % (4067489)Termination reason: Instruction limit % 59.33/8.61 % (4067489)Termination phase: Saturation % 59.33/8.61 % (4067489)Time elapsed: 0.618 s % 59.33/8.61 % (4067489)Peak memory usage: 19 MB % 59.33/8.61 % (4067489)Instructions burned: 879 (million) % 59.33/8.61 % (4067659)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=638829264:i=54282_2990 on theBenchmark for (2990ds/54282Mi) % 59.33/8.61 % (4067659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 59.33/8.61 % (4067659)Terminated due to inappropriate strategy. % 59.33/8.61 % (4067659)------------------------------ % 59.33/8.61 % (4067659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.33/8.61 % (4067659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.33/8.61 % (4067659)CaDiCaL version: 2.1.3 % 59.33/8.61 % (4067659)Termination reason: Inappropriate % 59.33/8.61 % (4067659)Time elapsed: 0.005 s % 59.33/8.61 % (4067659)Peak memory usage: 11 MB % 59.33/8.61 % (4067659)Instructions burned: 4 (million) % 209.48/29.73 % (4067659)------------------------------ % 209.48/29.73 % (4067659)------------------------------ % 209.48/29.73 % (4067665)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=156618667:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 209.48/29.73 % (4067623)Instruction limit reached! % 209.48/29.73 % (4067623)------------------------------ % 209.48/29.73 % (4067623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.48/29.73 % (4067623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.48/29.73 % (4067623)CaDiCaL version: 2.1.3 % 209.48/29.73 % (4067623)Termination reason: Instruction limit % 209.48/29.73 % (4067623)Termination phase: Saturation % 209.48/29.73 % (4067623)Time elapsed: 0.831 s % 209.48/29.73 % (4067623)Peak memory usage: 16 MB % 209.48/29.73 % (4067623)Instructions burned: 869 (million) % 209.48/29.73 % (4067685)dis+21_1_sil=32000:sas=cadical:random_seed=520505409:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 209.48/29.73 % (4067585)Instruction limit reached! % 209.48/29.73 % (4067585)------------------------------ % 209.48/29.73 % (4067585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.48/29.73 % (4067585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.48/29.73 % (4067585)CaDiCaL version: 2.1.3 % 209.48/29.73 % (4067585)Termination reason: Instruction limit % 209.48/29.73 % (4067585)Termination phase: Saturation % 209.48/29.73 % (4067585)Time elapsed: 1.253 s % 209.48/29.73 % (4067585)Peak memory usage: 26 MB % 209.48/29.73 % (4067585)Instructions burned: 1473 (million) % 209.48/29.73 % (4067692)ott+11_1_sil=16000:gs=on:random_seed=2630830235:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 209.48/29.73 % (4067692)Instruction limit reached! % 209.48/29.73 % (4067692)------------------------------ % 209.48/29.73 % (4067692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.48/29.73 % (4067692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.48/29.73 % (4067692)CaDiCaL version: 2.1.3 % 209.48/29.73 % (4067692)Termination reason: Instruction limit % 209.48/29.73 % (4067692)Termination phase: Saturation % 209.48/29.73 % (4067692)Time elapsed: 2.167 s % 209.48/29.73 % (4067692)Peak memory usage: 24 MB % 209.48/29.73 % (4067692)Instructions burned: 2251 (million) % 209.48/29.73 % (4067711)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2909954177:fmbsr=1.6:i=67534_2959 on theBenchmark for (2959ds/67534Mi) % 209.48/29.73 % (4067711)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 209.48/29.73 % (4067711)Terminated due to inappropriate strategy. % 209.48/29.73 % (4067711)------------------------------ % 209.48/29.73 % (4067711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.48/29.73 % (4067711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.48/29.73 % (4067711)CaDiCaL version: 2.1.3 % 209.48/29.73 % (4067711)Termination reason: Inappropriate % 209.48/29.73 % (4067711)Time elapsed: 0.003 s % 209.48/29.73 % (4067711)Peak memory usage: 11 MB % 209.48/29.73 % (4067711)Instructions burned: 3 (million) % 209.48/29.73 % (4067711)------------------------------ % 209.48/29.73 % (4067711)------------------------------ % 209.48/29.73 % (4067713)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3632694829:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2959 on theBenchmark for (2959ds/4591Mi) % 209.48/29.73 % (4067665)Instruction limit reached! % 209.48/29.73 % (4067665)------------------------------ % 209.48/29.73 % (4067665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.48/29.73 % (4067665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.48/29.73 % (4067665)CaDiCaL version: 2.1.3 % 209.48/29.73 % (4067665)Termination reason: Instruction limit % 209.48/29.73 % (4067665)Termination phase: Saturation % 209.48/29.73 % (4067665)Time elapsed: 3.332 s % 209.48/29.73 % (4067665)Peak memory usage: 31 MB % 209.48/29.73 % (4067665)Instructions burned: 3513 (million) % 209.48/29.73 % (4067715)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2549770224:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 209.48/29.73 % (4067685)Instruction limit reached! % 209.48/29.73 % (4067685)------------------------------ % 209.48/29.73 % (4067685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 209.48/29.73 % (4067685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.48/29.73 % (4067685)CaDiCaL version: 2.1.3 % 209.48/29.73 % (4067685)Termination reason: Instruction limit % 227.28/32.22 % (4067685)Termination phase: Saturation % 227.28/32.22 % (4067685)Time elapsed: 3.422 s % 227.28/32.22 % (4067685)Peak memory usage: 34 MB % 227.28/32.22 % (4067685)Instructions burned: 3773 (million) % 227.28/32.22 % (4067717)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2195303349:i=5211_2949 on theBenchmark for (2949ds/5211Mi) % 227.28/32.22 % (4067580)Instruction limit reached! % 227.28/32.22 % (4067580)------------------------------ % 227.28/32.22 % (4067580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.28/32.22 % (4067580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.28/32.22 % (4067580)CaDiCaL version: 2.1.3 % 227.28/32.22 % (4067580)Termination reason: Instruction limit % 227.28/32.22 % (4067580)Termination phase: Saturation % 227.28/32.22 % (4067580)Time elapsed: 4.759 s % 227.28/32.22 % (4067580)Peak memory usage: 42 MB % 227.28/32.22 % (4067580)Instructions burned: 5131 (million) % 227.28/32.22 % (4067721)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2825559116:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 227.28/32.22 % (4067721)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.28/32.22 % (4067721)Terminated due to inappropriate strategy. % 227.28/32.22 % (4067721)------------------------------ % 227.28/32.22 % (4067721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.28/32.22 % (4067721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.28/32.22 % (4067721)CaDiCaL version: 2.1.3 % 227.28/32.22 % (4067721)Termination reason: Inappropriate % 227.28/32.22 % (4067721)Time elapsed: 0.004 s % 227.28/32.22 % (4067721)Peak memory usage: 11 MB % 227.28/32.22 % (4067721)Instructions burned: 4 (million) % 227.28/32.22 % (4067721)------------------------------ % 227.28/32.22 % (4067721)------------------------------ % 227.28/32.22 % (4067724)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=457710972:fmbsr=2:i=46332_2946 on theBenchmark for (2946ds/46332Mi) % 227.28/32.22 % (4067724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.28/32.22 % (4067724)Terminated due to inappropriate strategy. % 227.28/32.22 % (4067724)------------------------------ % 227.28/32.22 % (4067724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.28/32.22 % (4067724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.28/32.22 % (4067724)CaDiCaL version: 2.1.3 % 227.28/32.22 % (4067724)Termination reason: Inappropriate % 227.28/32.22 % (4067724)Time elapsed: 0.005 s % 227.28/32.22 % (4067724)Peak memory usage: 11 MB % 227.28/32.22 % (4067724)Instructions burned: 3 (million) % 227.28/32.22 % (4067724)------------------------------ % 227.28/32.22 % (4067724)------------------------------ % 227.28/32.22 % (4067727)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1338699484:i=14071_2945 on theBenchmark for (2945ds/14071Mi) % 227.28/32.22 % (4067727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 227.28/32.22 % (4067727)Terminated due to inappropriate strategy. % 227.28/32.22 % (4067727)------------------------------ % 227.28/32.22 % (4067727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.28/32.22 % (4067727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.28/32.22 % (4067727)CaDiCaL version: 2.1.3 % 227.28/32.22 % (4067727)Termination reason: Inappropriate % 227.28/32.22 % (4067727)Time elapsed: 0.005 s % 227.28/32.22 % (4067727)Peak memory usage: 10 MB % 227.28/32.22 % (4067727)Instructions burned: 3 (million) % 227.28/32.22 % (4067727)------------------------------ % 227.28/32.22 % (4067727)------------------------------ % 227.28/32.22 % (4067729)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1735831786:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 227.28/32.22 % (4067654)Instruction limit reached! % 227.28/32.22 % (4067654)------------------------------ % 227.28/32.22 % (4067654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 227.28/32.22 % (4067654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.28/32.22 % (4067654)CaDiCaL version: 2.1.3 % 227.28/32.22 % (4067654)Termination reason: Instruction limit % 227.28/32.22 % (4067654)Termination phase: Saturation % 227.28/32.22 % (4067654)Time elapsed: 5.386 s % 227.28/32.22 % (4067654)Peak memory usage: 35 MB % 227.28/32.22 % (4067654)Instructions burned: 5114 (million) % 227.28/32.22 % (4067739)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3858936785:i=8173:av=off_2936 on theBenchmark for (2936ds/8173Mi) % 227.28/32.22 % (4067713)Instruction limit reached! % 228.67/32.44 % (4067713)------------------------------ % 228.67/32.44 % (4067713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.67/32.44 % (4067713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.67/32.44 % (4067713)CaDiCaL version: 2.1.3 % 228.67/32.44 % (4067713)Termination reason: Instruction limit % 228.67/32.44 % (4067713)Termination phase: Saturation % 228.67/32.44 % (4067713)Time elapsed: 4.267 s % 228.67/32.44 % (4067713)Peak memory usage: 38 MB % 228.67/32.44 % (4067713)Instructions burned: 4592 (million) % 228.67/32.44 % (4067745)dis+10_16:1_sil=16000:random_seed=881435987:i=9155:fsr=off_2916 on theBenchmark for (2916ds/9155Mi) % 228.67/32.44 % (4067717)Instruction limit reached! % 228.67/32.44 % (4067717)------------------------------ % 228.67/32.44 % (4067717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.67/32.44 % (4067717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.67/32.44 % (4067717)CaDiCaL version: 2.1.3 % 228.67/32.44 % (4067717)Termination reason: Instruction limit % 228.67/32.44 % (4067717)Termination phase: Saturation % 228.67/32.44 % (4067717)Time elapsed: 4.257 s % 228.67/32.44 % (4067717)Peak memory usage: 41 MB % 228.67/32.44 % (4067717)Instructions burned: 5212 (million) % 228.67/32.44 % (4067747)ott-3_8_sil=64000:random_seed=3346312578:i=20139:bs=on_2906 on theBenchmark for (2906ds/20139Mi) % 228.67/32.44 % (4067739)Instruction limit reached! % 228.67/32.44 % (4067739)------------------------------ % 228.67/32.44 % (4067739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.67/32.44 % (4067739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.67/32.44 % (4067739)CaDiCaL version: 2.1.3 % 228.67/32.44 % (4067739)Termination reason: Instruction limit % 228.67/32.44 % (4067739)Termination phase: Saturation % 228.67/32.44 % (4067739)Time elapsed: 8.596 s % 228.67/32.44 % (4067739)Peak memory usage: 54 MB % 228.67/32.44 % (4067739)Instructions burned: 8173 (million) % 228.67/32.44 % (4067751)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=902058029:fmbsr=2:i=32576_2850 on theBenchmark for (2850ds/32576Mi) % 228.67/32.44 % (4067751)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 228.67/32.44 % (4067751)Terminated due to inappropriate strategy. % 228.67/32.44 % (4067751)------------------------------ % 228.67/32.44 % (4067751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.67/32.44 % (4067751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.67/32.44 % (4067751)CaDiCaL version: 2.1.3 % 228.67/32.44 % (4067751)Termination reason: Inappropriate % 228.67/32.44 % (4067751)Time elapsed: 0.005 s % 228.67/32.44 % (4067751)Peak memory usage: 11 MB % 228.67/32.44 % (4067751)Instructions burned: 4 (million) % 228.67/32.44 % (4067751)------------------------------ % 228.67/32.44 % (4067751)------------------------------ % 228.67/32.44 % (4067753)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2153130390:i=11404_2850 on theBenchmark for (2850ds/11404Mi) % 228.67/32.44 % (4067745)Instruction limit reached! % 228.67/32.44 % (4067745)------------------------------ % 228.67/32.44 % (4067745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.67/32.44 % (4067745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.67/32.44 % (4067745)CaDiCaL version: 2.1.3 % 228.67/32.44 % (4067745)Termination reason: Instruction limit % 228.67/32.44 % (4067745)Termination phase: Saturation % 228.67/32.44 % (4067745)Time elapsed: 8.344 s % 228.67/32.44 % (4067745)Peak memory usage: 52 MB % 228.67/32.44 % (4067745)Instructions burned: 9155 (million) % 228.67/32.44 % (4067761)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3779293184:i=14134_2832 on theBenchmark for (2832ds/14134Mi) % 228.67/32.44 % (4067753)Instruction limit reached! % 228.67/32.44 % (4067753)------------------------------ % 228.67/32.44 % (4067753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.67/32.44 % (4067753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.67/32.44 % (4067753)CaDiCaL version: 2.1.3 % 228.67/32.44 % (4067753)Termination reason: Instruction limit % 228.67/32.44 % (4067753)Termination phase: Saturation % 228.67/32.44 % (4067753)Time elapsed: 12.052 s % 228.67/32.44 % (4067753)Peak memory usage: 61 MB % 228.67/32.44 % (4067753)Instructions burned: 11404 (million) % 228.67/32.44 % (4067767)dis+33_16_sil=32000:sac=on:random_seed=1022198042:i=15851:nm=0_2729 on theBenchmark for (2729ds/15851Mi) % 228.67/32.44 % (4067715)Instruction limit reached! % 228.67/32.44 % (4067715)------------------------------ % 228.67/32.44 % (4067715)Version: Vampire 5.0.1 (ReleasTerminated % 300.56/42.54 % Vampire exiting % 300.56/42.54 Terminated %------------------------------------------------------------------------------