%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC443_1 : TPTP v9.3.1. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n010.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:06:01 PM UTC 2026 % Result : Timeout 300.69s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC443_1 : TPTP v9.3.1. Released v9.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.18 % Computer : n010.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Mon Sep 28 09:38:32 UTC 2026 % 0.10/0.18 % CPUTime : % 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 Running first-order model finding % 0.10/0.21 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.96/0.86 % (1802863)Will run a generic schedule for satisfiability detection. % 3.96/0.86 % (1802869)% WARNING: option uhcvi not known. % 3.96/0.86 % (1802869)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3096664179:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.96/0.86 % (1802868)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=758395514_2999 on theBenchmark for (2999ds/0Mi) % 3.96/0.86 % (1802870)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3965196556:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.96/0.86 % (1802872)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1297245190:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.96/0.86 % (1802871)dis+10_1_sil=32000:sp=arity:random_seed=1359364181:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.96/0.86 % (1802868)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.96/0.86 % (1802868)Terminated due to inappropriate strategy. % 3.96/0.86 % (1802868)------------------------------ % 3.96/0.86 % (1802868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.86 % (1802868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.86 % (1802868)CaDiCaL version: 2.1.3 % 3.96/0.86 % (1802868)Termination reason: Inappropriate % 3.96/0.86 % (1802868)Time elapsed: 0.001 s % 3.96/0.86 % (1802868)Peak memory usage: 10 MB % 3.96/0.86 % (1802868)Instructions burned: 2 (million) % 3.96/0.86 % (1802868)------------------------------ % 3.96/0.86 % (1802868)------------------------------ % 3.96/0.86 % (1802873)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=498446167:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.96/0.86 % (1802874)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1933399815:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.96/0.86 % (1802880)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1345333439:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.96/0.86 % (1802880)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.96/0.86 % (1802880)Terminated due to inappropriate strategy. % 3.96/0.86 % (1802880)------------------------------ % 3.96/0.86 % (1802880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.86 % (1802880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.86 % (1802880)CaDiCaL version: 2.1.3 % 3.96/0.86 % (1802880)Termination reason: Inappropriate % 3.96/0.86 % (1802880)Time elapsed: 0.002 s % 3.96/0.86 % (1802880)Peak memory usage: 10 MB % 3.96/0.86 % (1802880)Instructions burned: 2 (million) % 3.96/0.86 % (1802880)------------------------------ % 3.96/0.86 % (1802880)------------------------------ % 3.96/0.86 % (1802884)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=970373884:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.96/0.86 % (1802871)Instruction limit reached! % 3.96/0.86 % (1802871)------------------------------ % 3.96/0.86 % (1802871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.86 % (1802871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.86 % (1802871)CaDiCaL version: 2.1.3 % 3.96/0.86 % (1802871)Termination reason: Instruction limit % 3.96/0.86 % (1802871)Termination phase: Saturation % 3.96/0.86 % (1802871)Time elapsed: 0.063 s % 3.96/0.86 % (1802871)Peak memory usage: 12 MB % 3.96/0.86 % (1802871)Instructions burned: 103 (million) % 3.96/0.86 % (1802872)Instruction limit reached! % 3.96/0.86 % (1802872)------------------------------ % 3.96/0.86 % (1802872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.96/0.86 % (1802872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.96/0.86 % (1802872)CaDiCaL version: 2.1.3 % 3.96/0.86 % (1802872)Termination reason: Instruction limit % 3.96/0.86 % (1802872)Termination phase: Saturation % 3.96/0.86 % (1802872)Time elapsed: 0.069 s % 3.96/0.86 % (1802872)Peak memory usage: 12 MB % 3.96/0.86 % (1802872)Instructions burned: 119 (million) % 3.96/0.86 % (1802896)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=2348491794:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.96/0.86 % (1802873)Instruction limit reached! % 3.96/0.86 % (1802873)------------------------------ % 3.96/0.86 % (1802873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.29 % (1802873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.29 % (1802873)CaDiCaL version: 2.1.3 % 6.73/1.29 % (1802873)Termination reason: Instruction limit % 6.73/1.29 % (1802873)Termination phase: Saturation % 6.73/1.29 % (1802873)Time elapsed: 0.080 s % 6.73/1.29 % (1802873)Peak memory usage: 13 MB % 6.73/1.29 % (1802873)Instructions burned: 131 (million) % 6.73/1.29 % (1802899)ott-21_1_sil=16000:fs=off:random_seed=3823586068:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.73/1.29 % (1802907)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3601548627:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.73/1.29 % (1802874)Instruction limit reached! % 6.73/1.29 % (1802874)------------------------------ % 6.73/1.29 % (1802874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.29 % (1802874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.29 % (1802874)CaDiCaL version: 2.1.3 % 6.73/1.29 % (1802874)Termination reason: Instruction limit % 6.73/1.29 % (1802874)Termination phase: Saturation % 6.73/1.29 % (1802874)Time elapsed: 0.105 s % 6.73/1.29 % (1802874)Peak memory usage: 13 MB % 6.73/1.29 % (1802874)Instructions burned: 160 (million) % 6.73/1.29 % (1802884)Instruction limit reached! % 6.73/1.29 % (1802884)------------------------------ % 6.73/1.29 % (1802884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.29 % (1802884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.29 % (1802884)CaDiCaL version: 2.1.3 % 6.73/1.29 % (1802884)Termination reason: Instruction limit % 6.73/1.29 % (1802884)Termination phase: Saturation % 6.73/1.29 % (1802884)Time elapsed: 0.078 s % 6.73/1.29 % (1802884)Peak memory usage: 13 MB % 6.73/1.29 % (1802884)Instructions burned: 132 (million) % 6.73/1.29 % (1802917)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3343073849:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.73/1.29 % (1802917)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.73/1.29 % (1802917)Terminated due to inappropriate strategy. % 6.73/1.29 % (1802917)------------------------------ % 6.73/1.29 % (1802917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.29 % (1802917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.29 % (1802917)CaDiCaL version: 2.1.3 % 6.73/1.29 % (1802917)Termination reason: Inappropriate % 6.73/1.29 % (1802917)Time elapsed: 0.001 s % 6.73/1.29 % (1802917)Peak memory usage: 10 MB % 6.73/1.29 % (1802917)Instructions burned: 2 (million) % 6.73/1.29 % (1802917)------------------------------ % 6.73/1.29 % (1802917)------------------------------ % 6.73/1.29 % (1802923)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=695003351:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.73/1.29 % (1802928)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=300614676:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.73/1.29 % (1802928)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.73/1.29 % (1802928)Terminated due to inappropriate strategy. % 6.73/1.29 % (1802928)------------------------------ % 6.73/1.29 % (1802928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.29 % (1802928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.29 % (1802928)CaDiCaL version: 2.1.3 % 6.73/1.29 % (1802928)Termination reason: Inappropriate % 6.73/1.29 % (1802928)Time elapsed: 0.001 s % 6.73/1.29 % (1802928)Peak memory usage: 10 MB % 6.73/1.29 % (1802928)Instructions burned: 2 (million) % 6.73/1.29 % (1802928)------------------------------ % 6.73/1.29 % (1802928)------------------------------ % 6.73/1.29 % (1802899)Instruction limit reached! % 6.73/1.29 % (1802899)------------------------------ % 6.73/1.29 % (1802899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.73/1.29 % (1802899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.73/1.29 % (1802899)CaDiCaL version: 2.1.3 % 6.73/1.29 % (1802899)Termination reason: Instruction limit % 6.73/1.29 % (1802899)Termination phase: Saturation % 6.73/1.29 % (1802899)Time elapsed: 0.083 s % 6.73/1.29 % (1802899)Peak memory usage: 12 MB % 6.73/1.29 % (1802899)Instructions burned: 180 (million) % 6.73/1.29 % (1802940)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=2751651590:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 35.31/5.29 % (1802947)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1417909473:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 35.31/5.29 % (1802907)Instruction limit reached! % 35.31/5.29 % (1802907)------------------------------ % 35.31/5.29 % (1802907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.31/5.29 % (1802907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.31/5.29 % (1802907)CaDiCaL version: 2.1.3 % 35.31/5.29 % (1802907)Termination reason: Instruction limit % 35.31/5.29 % (1802907)Termination phase: Saturation % 35.31/5.29 % (1802907)Time elapsed: 0.319 s % 35.31/5.29 % (1802907)Peak memory usage: 14 MB % 35.31/5.29 % (1802907)Instructions burned: 477 (million) % 35.31/5.29 % (1803009)fmb+10_1_sil=64000:random_seed=2760681844:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 35.31/5.29 % (1803009)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.31/5.29 % (1803009)Terminated due to inappropriate strategy. % 35.31/5.29 % (1803009)------------------------------ % 35.31/5.29 % (1803009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.31/5.29 % (1803009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.31/5.29 % (1803009)CaDiCaL version: 2.1.3 % 35.31/5.29 % (1803009)Termination reason: Inappropriate % 35.31/5.29 % (1803009)Time elapsed: 0.001 s % 35.31/5.29 % (1803009)Peak memory usage: 10 MB % 35.31/5.29 % (1803009)Instructions burned: 2 (million) % 35.31/5.29 % (1803009)------------------------------ % 35.31/5.29 % (1803009)------------------------------ % 35.31/5.29 % (1802896)Instruction limit reached! % 35.31/5.29 % (1802896)------------------------------ % 35.31/5.29 % (1802896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.31/5.29 % (1802896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.31/5.29 % (1802896)CaDiCaL version: 2.1.3 % 35.31/5.29 % (1802896)Termination reason: Instruction limit % 35.31/5.29 % (1802896)Termination phase: Saturation % 35.31/5.29 % (1802896)Time elapsed: 0.380 s % 35.31/5.29 % (1802896)Peak memory usage: 17 MB % 35.31/5.29 % (1802896)Instructions burned: 685 (million) % 35.31/5.29 % (1803015)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1882499241:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 35.31/5.29 % (1803015)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.31/5.29 % (1803015)Terminated due to inappropriate strategy. % 35.31/5.29 % (1803015)------------------------------ % 35.31/5.29 % (1803015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.31/5.29 % (1803015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.31/5.29 % (1803015)CaDiCaL version: 2.1.3 % 35.31/5.29 % (1803015)Termination reason: Inappropriate % 35.31/5.29 % (1803015)Time elapsed: 0.001 s % 35.31/5.29 % (1803015)Peak memory usage: 10 MB % 35.31/5.29 % (1803015)Instructions burned: 2 (million) % 35.31/5.29 % (1803015)------------------------------ % 35.31/5.29 % (1803015)------------------------------ % 35.31/5.29 % (1803017)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1619270722:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 35.31/5.29 % (1803017)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 35.31/5.29 % (1803017)Terminated due to inappropriate strategy. % 35.31/5.29 % (1803017)------------------------------ % 35.31/5.29 % (1803017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.31/5.29 % (1803017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.31/5.29 % (1803017)CaDiCaL version: 2.1.3 % 35.31/5.29 % (1803017)Termination reason: Inappropriate % 35.31/5.29 % (1803017)Time elapsed: 0.001 s % 35.31/5.29 % (1803017)Peak memory usage: 10 MB % 35.31/5.29 % (1803017)Instructions burned: 2 (million) % 35.31/5.29 % (1803017)------------------------------ % 35.31/5.29 % (1803017)------------------------------ % 35.31/5.29 % (1803022)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3707053926:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 35.31/5.29 % (1803026)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2702666468:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 35.31/5.29 % (1802940)Instruction limit reached! % 35.31/5.29 % (1802940)------------------------------ % 58.04/8.44 % (1802940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.04/8.44 % (1802940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.04/8.44 % (1802940)CaDiCaL version: 2.1.3 % 58.04/8.44 % (1802940)Termination reason: Instruction limit % 58.04/8.44 % (1802940)Termination phase: Saturation % 58.04/8.44 % (1802940)Time elapsed: 0.422 s % 58.04/8.44 % (1802940)Peak memory usage: 19 MB % 58.04/8.44 % (1802940)Instructions burned: 693 (million) % 58.04/8.44 % (1803057)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2993775387:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 58.04/8.44 % (1803057)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.04/8.44 % (1803057)Terminated due to inappropriate strategy. % 58.04/8.44 % (1803057)------------------------------ % 58.04/8.44 % (1803057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.04/8.44 % (1803057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.04/8.44 % (1803057)CaDiCaL version: 2.1.3 % 58.04/8.44 % (1803057)Termination reason: Inappropriate % 58.04/8.44 % (1803057)Time elapsed: 0.002 s % 58.04/8.44 % (1803057)Peak memory usage: 11 MB % 58.04/8.44 % (1803057)Instructions burned: 2 (million) % 58.04/8.44 % (1803057)------------------------------ % 58.04/8.44 % (1803057)------------------------------ % 58.04/8.44 % (1803061)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=208015038:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 58.04/8.44 % (1803061)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.04/8.44 % (1803061)Terminated due to inappropriate strategy. % 58.04/8.44 % (1803061)------------------------------ % 58.04/8.44 % (1803061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.04/8.44 % (1803061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.04/8.44 % (1803061)CaDiCaL version: 2.1.3 % 58.04/8.44 % (1803061)Termination reason: Inappropriate % 58.04/8.44 % (1803061)Time elapsed: 0.003 s % 58.04/8.44 % (1803061)Peak memory usage: 10 MB % 58.04/8.44 % (1803061)Instructions burned: 2 (million) % 58.04/8.44 % (1803061)------------------------------ % 58.04/8.44 % (1803061)------------------------------ % 58.04/8.44 % (1803064)ott-2_1_sil=16000:newcnf=on:random_seed=1343438066:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi) % 58.04/8.44 % (1802947)Instruction limit reached! % 58.04/8.44 % (1802947)------------------------------ % 58.04/8.44 % (1802947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.04/8.44 % (1802947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.04/8.44 % (1802947)CaDiCaL version: 2.1.3 % 58.04/8.44 % (1802947)Termination reason: Instruction limit % 58.04/8.44 % (1802947)Termination phase: Saturation % 58.04/8.44 % (1802947)Time elapsed: 0.604 s % 58.04/8.44 % (1802947)Peak memory usage: 19 MB % 58.04/8.44 % (1802947)Instructions burned: 879 (million) % 58.04/8.44 % (1803075)ott+10_1_sil=32000:tgt=ground:random_seed=2031551825:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi) % 58.04/8.44 % (1802923)Instruction limit reached! % 58.04/8.44 % (1802923)------------------------------ % 58.04/8.44 % (1802923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.04/8.44 % (1802923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.04/8.44 % (1802923)CaDiCaL version: 2.1.3 % 58.04/8.44 % (1802923)Termination reason: Instruction limit % 58.04/8.44 % (1802923)Termination phase: Saturation % 58.04/8.44 % (1802923)Time elapsed: 0.836 s % 58.04/8.44 % (1802923)Peak memory usage: 18 MB % 58.04/8.44 % (1802923)Instructions burned: 1179 (million) % 58.04/8.44 % (1803084)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1694445652:i=54282_2989 on theBenchmark for (2989ds/54282Mi) % 58.04/8.44 % (1803084)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 58.04/8.44 % (1803084)Terminated due to inappropriate strategy. % 58.04/8.44 % (1803084)------------------------------ % 58.04/8.44 % (1803084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 58.04/8.44 % (1803084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.04/8.44 % (1803084)CaDiCaL version: 2.1.3 % 58.04/8.44 % (1803084)Termination reason: Inappropriate % 58.04/8.44 % (1803084)Time elapsed: 0.003 s % 58.04/8.44 % (1803084)Peak memory usage: 10 MB % 58.04/8.44 % (1803084)Instructions burned: 2 (million) % 181.87/25.83 % (1803084)------------------------------ % 181.87/25.83 % (1803084)------------------------------ % 181.87/25.83 % (1803086)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3146651563:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 181.87/25.83 % (1803064)Instruction limit reached! % 181.87/25.83 % (1803064)------------------------------ % 181.87/25.83 % (1803064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.87/25.83 % (1803064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.87/25.83 % (1803064)CaDiCaL version: 2.1.3 % 181.87/25.83 % (1803064)Termination reason: Instruction limit % 181.87/25.83 % (1803064)Termination phase: Saturation % 181.87/25.83 % (1803064)Time elapsed: 0.818 s % 181.87/25.83 % (1803064)Peak memory usage: 18 MB % 181.87/25.83 % (1803064)Instructions burned: 869 (million) % 181.87/25.83 % (1803098)dis+21_1_sil=32000:sas=cadical:random_seed=2691927480:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi) % 181.87/25.83 % (1803026)Instruction limit reached! % 181.87/25.83 % (1803026)------------------------------ % 181.87/25.83 % (1803026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.87/25.83 % (1803026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.87/25.83 % (1803026)CaDiCaL version: 2.1.3 % 181.87/25.83 % (1803026)Termination reason: Instruction limit % 181.87/25.83 % (1803026)Termination phase: Saturation % 181.87/25.83 % (1803026)Time elapsed: 1.321 s % 181.87/25.83 % (1803026)Peak memory usage: 24 MB % 181.87/25.83 % (1803026)Instructions burned: 1473 (million) % 181.87/25.83 % (1803108)ott+11_1_sil=16000:gs=on:random_seed=1671241054:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 181.87/25.83 % (1803108)Instruction limit reached! % 181.87/25.83 % (1803108)------------------------------ % 181.87/25.83 % (1803108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.87/25.83 % (1803108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.87/25.83 % (1803108)CaDiCaL version: 2.1.3 % 181.87/25.83 % (1803108)Termination reason: Instruction limit % 181.87/25.83 % (1803108)Termination phase: Saturation % 181.87/25.83 % (1803108)Time elapsed: 2.124 s % 181.87/25.83 % (1803108)Peak memory usage: 23 MB % 181.87/25.83 % (1803108)Instructions burned: 2251 (million) % 181.87/25.83 % (1803119)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=294666858:fmbsr=1.6:i=67534_2959 on theBenchmark for (2959ds/67534Mi) % 181.87/25.83 % (1803119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 181.87/25.83 % (1803119)Terminated due to inappropriate strategy. % 181.87/25.83 % (1803119)------------------------------ % 181.87/25.83 % (1803119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.87/25.83 % (1803119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.87/25.83 % (1803119)CaDiCaL version: 2.1.3 % 181.87/25.83 % (1803119)Termination reason: Inappropriate % 181.87/25.83 % (1803119)Time elapsed: 0.003 s % 181.87/25.83 % (1803119)Peak memory usage: 10 MB % 181.87/25.83 % (1803119)Instructions burned: 2 (million) % 181.87/25.83 % (1803119)------------------------------ % 181.87/25.83 % (1803119)------------------------------ % 181.87/25.83 % (1803121)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=881657511:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2959 on theBenchmark for (2959ds/4591Mi) % 181.87/25.83 % (1803086)Instruction limit reached! % 181.87/25.83 % (1803086)------------------------------ % 181.87/25.83 % (1803086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.87/25.83 % (1803086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.87/25.83 % (1803086)CaDiCaL version: 2.1.3 % 181.87/25.83 % (1803086)Termination reason: Instruction limit % 181.87/25.83 % (1803086)Termination phase: Saturation % 181.87/25.83 % (1803086)Time elapsed: 3.273 s % 181.87/25.83 % (1803086)Peak memory usage: 32 MB % 181.87/25.83 % (1803086)Instructions burned: 3512 (million) % 181.87/25.83 % (1803123)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=584757398:i=29340_2956 on theBenchmark for (2956ds/29340Mi) % 181.87/25.83 % (1803022)Instruction limit reached! % 181.87/25.83 % (1803022)------------------------------ % 181.87/25.83 % (1803022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.87/25.83 % (1803022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.87/25.83 % (1803022)CaDiCaL version: 2.1.3 % 181.87/25.83 % (1803022)Termination reason: Instruction limit % 222.43/31.52 % (1803022)Termination phase: Saturation % 222.43/31.52 % (1803022)Time elapsed: 4.527 s % 222.43/31.52 % (1803022)Peak memory usage: 41 MB % 222.43/31.52 % (1803022)Instructions burned: 5131 (million) % 222.43/31.52 % (1803125)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2754066697:i=5211_2949 on theBenchmark for (2949ds/5211Mi) % 222.43/31.52 % (1803098)Instruction limit reached! % 222.43/31.52 % (1803098)------------------------------ % 222.43/31.52 % (1803098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.43/31.52 % (1803098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.43/31.52 % (1803098)CaDiCaL version: 2.1.3 % 222.43/31.52 % (1803098)Termination reason: Instruction limit % 222.43/31.52 % (1803098)Termination phase: Saturation % 222.43/31.52 % (1803098)Time elapsed: 3.567 s % 222.43/31.52 % (1803098)Peak memory usage: 32 MB % 222.43/31.52 % (1803098)Instructions burned: 3774 (million) % 222.43/31.52 % (1803127)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1040381776:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 222.43/31.52 % (1803127)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.43/31.52 % (1803127)Terminated due to inappropriate strategy. % 222.43/31.52 % (1803127)------------------------------ % 222.43/31.52 % (1803127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.43/31.52 % (1803127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.43/31.52 % (1803127)CaDiCaL version: 2.1.3 % 222.43/31.52 % (1803127)Termination reason: Inappropriate % 222.43/31.52 % (1803127)Time elapsed: 0.003 s % 222.43/31.52 % (1803127)Peak memory usage: 10 MB % 222.43/31.52 % (1803127)Instructions burned: 2 (million) % 222.43/31.52 % (1803127)------------------------------ % 222.43/31.52 % (1803127)------------------------------ % 222.43/31.52 % (1803130)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=599302748:fmbsr=2:i=46332_2947 on theBenchmark for (2947ds/46332Mi) % 222.43/31.52 % (1803130)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.43/31.52 % (1803130)Terminated due to inappropriate strategy. % 222.43/31.52 % (1803130)------------------------------ % 222.43/31.52 % (1803130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.43/31.52 % (1803130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.43/31.52 % (1803130)CaDiCaL version: 2.1.3 % 222.43/31.52 % (1803130)Termination reason: Inappropriate % 222.43/31.52 % (1803130)Time elapsed: 0.002 s % 222.43/31.52 % (1803130)Peak memory usage: 11 MB % 222.43/31.52 % (1803130)Instructions burned: 2 (million) % 222.43/31.52 % (1803130)------------------------------ % 222.43/31.52 % (1803130)------------------------------ % 222.43/31.52 % (1803135)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=366128830:i=14071_2947 on theBenchmark for (2947ds/14071Mi) % 222.43/31.52 % (1803135)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 222.43/31.52 % (1803135)Terminated due to inappropriate strategy. % 222.43/31.52 % (1803135)------------------------------ % 222.43/31.52 % (1803135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.43/31.52 % (1803135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.43/31.52 % (1803135)CaDiCaL version: 2.1.3 % 222.43/31.52 % (1803135)Termination reason: Inappropriate % 222.43/31.52 % (1803135)Time elapsed: 0.003 s % 222.43/31.52 % (1803135)Peak memory usage: 11 MB % 222.43/31.52 % (1803135)Instructions burned: 2 (million) % 222.43/31.52 % (1803135)------------------------------ % 222.43/31.52 % (1803135)------------------------------ % 222.43/31.52 % (1803139)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2733557281:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi) % 222.43/31.52 % (1803075)Instruction limit reached! % 222.43/31.52 % (1803075)------------------------------ % 222.43/31.52 % (1803075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 222.43/31.52 % (1803075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.43/31.52 % (1803075)CaDiCaL version: 2.1.3 % 222.43/31.52 % (1803075)Termination reason: Instruction limit % 222.43/31.52 % (1803075)Termination phase: Saturation % 222.43/31.52 % (1803075)Time elapsed: 5.261 s % 222.43/31.52 % (1803075)Peak memory usage: 34 MB % 222.43/31.52 % (1803075)Instructions burned: 5115 (million) % 222.43/31.52 % (1803146)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3383421297:i=8173:av=off_2938 on theBenchmark for (2938ds/8173Mi) % 222.43/31.52 % (1803121)Instruction limit reached! % 223.15/31.70 % (1803121)------------------------------ % 223.15/31.70 % (1803121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.15/31.70 % (1803121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.15/31.70 % (1803121)CaDiCaL version: 2.1.3 % 223.15/31.70 % (1803121)Termination reason: Instruction limit % 223.15/31.70 % (1803121)Termination phase: Saturation % 223.15/31.70 % (1803121)Time elapsed: 4.117 s % 223.15/31.70 % (1803121)Peak memory usage: 56 MB % 223.15/31.70 % (1803121)Instructions burned: 4592 (million) % 223.15/31.70 % (1803155)dis+10_16:1_sil=16000:random_seed=3866824560:i=9155:fsr=off_2917 on theBenchmark for (2917ds/9155Mi) % 223.15/31.70 % (1803125)Instruction limit reached! % 223.15/31.70 % (1803125)------------------------------ % 223.15/31.70 % (1803125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.15/31.70 % (1803125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.15/31.70 % (1803125)CaDiCaL version: 2.1.3 % 223.15/31.70 % (1803125)Termination reason: Instruction limit % 223.15/31.70 % (1803125)Termination phase: Saturation % 223.15/31.70 % (1803125)Time elapsed: 4.744 s % 223.15/31.70 % (1803125)Peak memory usage: 52 MB % 223.15/31.70 % (1803125)Instructions burned: 5212 (million) % 223.15/31.70 % (1803159)ott-3_8_sil=64000:random_seed=637990817:i=20139:bs=on_2901 on theBenchmark for (2901ds/20139Mi) % 223.15/31.70 % (1803146)Instruction limit reached! % 223.15/31.70 % (1803146)------------------------------ % 223.15/31.70 % (1803146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.15/31.70 % (1803146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.15/31.70 % (1803146)CaDiCaL version: 2.1.3 % 223.15/31.70 % (1803146)Termination reason: Instruction limit % 223.15/31.70 % (1803146)Termination phase: Saturation % 223.15/31.70 % (1803146)Time elapsed: 8.065 s % 223.15/31.70 % (1803146)Peak memory usage: 58 MB % 223.15/31.70 % (1803146)Instructions burned: 8173 (million) % 223.15/31.70 % (1803163)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=976568129:fmbsr=2:i=32576_2857 on theBenchmark for (2857ds/32576Mi) % 223.15/31.70 % (1803163)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.15/31.70 % (1803163)Terminated due to inappropriate strategy. % 223.15/31.70 % (1803163)------------------------------ % 223.15/31.70 % (1803163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.15/31.70 % (1803163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.15/31.70 % (1803163)CaDiCaL version: 2.1.3 % 223.15/31.70 % (1803163)Termination reason: Inappropriate % 223.15/31.70 % (1803163)Time elapsed: 0.003 s % 223.15/31.70 % (1803163)Peak memory usage: 11 MB % 223.15/31.70 % (1803163)Instructions burned: 2 (million) % 223.15/31.70 % (1803163)------------------------------ % 223.15/31.70 % (1803163)------------------------------ % 223.15/31.70 % (1803165)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2762556720:i=11404_2857 on theBenchmark for (2857ds/11404Mi) % 223.15/31.70 % (1803155)Instruction limit reached! % 223.15/31.70 % (1803155)------------------------------ % 223.15/31.70 % (1803155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.15/31.70 % (1803155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.15/31.70 % (1803155)CaDiCaL version: 2.1.3 % 223.15/31.70 % (1803155)Termination reason: Instruction limit % 223.15/31.70 % (1803155)Termination phase: Saturation % 223.15/31.70 % (1803155)Time elapsed: 8.245 s % 223.15/31.70 % (1803155)Peak memory usage: 53 MB % 223.15/31.70 % (1803155)Instructions burned: 9155 (million) % 223.15/31.70 % (1803171)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3909011383:i=14134_2834 on theBenchmark for (2834ds/14134Mi) % 223.15/31.70 % (1803139)Instruction limit reached! % 223.15/31.70 % (1803139)------------------------------ % 223.15/31.70 % (1803139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.15/31.70 % (1803139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.15/31.70 % (1803139)CaDiCaL version: 2.1.3 % 223.15/31.70 % (1803139)Termination reason: Instruction limit % 223.15/31.70 % (1803139)Termination phase: Saturation % 223.15/31.70 % (1803139)Time elapsed: 16.288 s % 223.15/31.70 % (1803139)Peak memory usage: 164 MB % 223.15/31.70 % (1803139)Instructions burned: 22565 (million) % 223.15/31.70 % (1803175)dis+33_16_sil=32000:sac=on:random_seed=4267787170:i=15851:nm=0_2783 on theBenchmark for (2783ds/15851Mi) % 223.15/31.70 % (1803165)Instruction limit reached! % 223.15/31.70 % (1803165)------------------------------ % 223.15/31.70 % (1803165)Version: Vampire 5.0.1 (ReleTerminated % 300.69/42.54 % Vampire exiting % 300.69/42.54 Terminated %------------------------------------------------------------------------------