%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW633_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:34 PM UTC 2026 % Result : Timeout 300.58s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW633_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n026.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 14:25:42 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/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.28/0.79 % (3882630)Will run a generic schedule for satisfiability detection. % 3.28/0.79 % (3882635)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4162156951_2999 on theBenchmark for (2999ds/0Mi) % 3.28/0.79 % (3882635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.79 % (3882635)Terminated due to inappropriate strategy. % 3.28/0.79 % (3882635)------------------------------ % 3.28/0.79 % (3882635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.79 % (3882635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.79 % (3882635)CaDiCaL version: 2.1.3 % 3.28/0.79 % (3882635)Termination reason: Inappropriate % 3.28/0.79 % (3882635)Time elapsed: 0.001 s % 3.28/0.79 % (3882635)Peak memory usage: 11 MB % 3.28/0.79 % (3882635)Instructions burned: 3 (million) % 3.28/0.79 % (3882635)------------------------------ % 3.28/0.79 % (3882635)------------------------------ % 3.28/0.79 % (3882636)% WARNING: option uhcvi not known. % 3.28/0.79 % (3882638)dis+10_1_sil=32000:sp=arity:random_seed=3486089936:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.28/0.79 % (3882636)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4254105016:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.28/0.79 % (3882637)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4247837067:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.28/0.79 % (3882639)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3560418101:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.28/0.79 % (3882643)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1752538791:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.28/0.79 % (3882641)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3384817389:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.28/0.79 % (3882643)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.28/0.79 % (3882643)Terminated due to inappropriate strategy. % 3.28/0.79 % (3882643)------------------------------ % 3.28/0.79 % (3882643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.79 % (3882643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.79 % (3882643)CaDiCaL version: 2.1.3 % 3.28/0.79 % (3882643)Termination reason: Inappropriate % 3.28/0.79 % (3882643)Time elapsed: 0.001 s % 3.28/0.79 % (3882643)Peak memory usage: 11 MB % 3.28/0.79 % (3882643)Instructions burned: 2 (million) % 3.28/0.79 % (3882640)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3462652681:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.28/0.79 % (3882643)------------------------------ % 3.28/0.79 % (3882643)------------------------------ % 3.28/0.79 % (3882651)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2902616211:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.28/0.79 % (3882651)Instruction limit reached! % 3.28/0.79 % (3882651)------------------------------ % 3.28/0.79 % (3882651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.79 % (3882651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.79 % (3882651)CaDiCaL version: 2.1.3 % 3.28/0.79 % (3882651)Termination reason: Instruction limit % 3.28/0.79 % (3882651)Termination phase: Saturation % 3.28/0.79 % (3882651)Time elapsed: 0.045 s % 3.28/0.79 % (3882651)Peak memory usage: 13 MB % 3.28/0.79 % (3882651)Instructions burned: 133 (million) % 3.28/0.79 % (3882638)Instruction limit reached! % 3.28/0.79 % (3882638)------------------------------ % 3.28/0.79 % (3882638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.28/0.79 % (3882638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.28/0.79 % (3882638)CaDiCaL version: 2.1.3 % 3.28/0.79 % (3882638)Termination reason: Instruction limit % 3.28/0.79 % (3882638)Termination phase: Saturation % 3.28/0.79 % (3882638)Time elapsed: 0.072 s % 3.28/0.79 % (3882638)Peak memory usage: 13 MB % 3.28/0.79 % (3882638)Instructions burned: 103 (million) % 3.28/0.79 % (3882653)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=2276050880:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 3.28/0.79 % (3882639)Instruction limit reached! % 3.28/0.79 % (3882639)------------------------------ % 3.28/0.79 % (3882639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (3882639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (3882639)CaDiCaL version: 2.1.3 % 5.60/1.05 % (3882639)Termination reason: Instruction limit % 5.60/1.05 % (3882639)Termination phase: Saturation % 5.60/1.05 % (3882639)Time elapsed: 0.080 s % 5.60/1.05 % (3882639)Peak memory usage: 13 MB % 5.60/1.05 % (3882639)Instructions burned: 120 (million) % 5.60/1.05 % (3882654)ott-21_1_sil=16000:fs=off:random_seed=3348396487:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.60/1.05 % (3882656)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1477391362:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 5.60/1.05 % (3882640)Instruction limit reached! % 5.60/1.05 % (3882640)------------------------------ % 5.60/1.05 % (3882640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (3882640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (3882640)CaDiCaL version: 2.1.3 % 5.60/1.05 % (3882640)Termination reason: Instruction limit % 5.60/1.05 % (3882640)Termination phase: Saturation % 5.60/1.05 % (3882640)Time elapsed: 0.097 s % 5.60/1.05 % (3882640)Peak memory usage: 12 MB % 5.60/1.05 % (3882640)Instructions burned: 134 (million) % 5.60/1.05 % (3882659)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2035903196:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 5.60/1.05 % (3882659)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.05 % (3882659)Terminated due to inappropriate strategy. % 5.60/1.05 % (3882659)------------------------------ % 5.60/1.05 % (3882659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (3882659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (3882659)CaDiCaL version: 2.1.3 % 5.60/1.05 % (3882659)Termination reason: Inappropriate % 5.60/1.05 % (3882659)Time elapsed: 0.0000 s % 5.60/1.05 % (3882659)Peak memory usage: 10 MB % 5.60/1.05 % (3882659)Instructions burned: 2 (million) % 5.60/1.05 % (3882659)------------------------------ % 5.60/1.05 % (3882659)------------------------------ % 5.60/1.05 % (3882641)Instruction limit reached! % 5.60/1.05 % (3882641)------------------------------ % 5.60/1.05 % (3882641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (3882641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (3882641)CaDiCaL version: 2.1.3 % 5.60/1.05 % (3882641)Termination reason: Instruction limit % 5.60/1.05 % (3882641)Termination phase: Saturation % 5.60/1.05 % (3882641)Time elapsed: 0.114 s % 5.60/1.05 % (3882641)Peak memory usage: 14 MB % 5.60/1.05 % (3882641)Instructions burned: 160 (million) % 5.60/1.05 % (3882666)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2024219937:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 5.60/1.05 % (3882668)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1126489708:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 5.60/1.05 % (3882668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 5.60/1.05 % (3882668)Terminated due to inappropriate strategy. % 5.60/1.05 % (3882668)------------------------------ % 5.60/1.05 % (3882668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (3882668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (3882668)CaDiCaL version: 2.1.3 % 5.60/1.05 % (3882668)Termination reason: Inappropriate % 5.60/1.05 % (3882668)Time elapsed: 0.002 s % 5.60/1.05 % (3882668)Peak memory usage: 10 MB % 5.60/1.05 % (3882668)Instructions burned: 3 (million) % 5.60/1.05 % (3882668)------------------------------ % 5.60/1.05 % (3882668)------------------------------ % 5.60/1.05 % (3882674)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=3237342830: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) % 5.60/1.05 % (3882654)Instruction limit reached! % 5.60/1.05 % (3882654)------------------------------ % 5.60/1.05 % (3882654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.60/1.05 % (3882654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.60/1.05 % (3882654)CaDiCaL version: 2.1.3 % 5.60/1.05 % (3882654)Termination reason: Instruction limit % 5.60/1.05 % (3882654)Termination phase: Saturation % 27.06/4.07 % (3882654)Time elapsed: 0.092 s % 27.06/4.07 % (3882654)Peak memory usage: 12 MB % 27.06/4.07 % (3882654)Instructions burned: 181 (million) % 27.06/4.07 % (3882688)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2330193512:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 27.06/4.07 % (3882656)Instruction limit reached! % 27.06/4.07 % (3882656)------------------------------ % 27.06/4.07 % (3882656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.06/4.07 % (3882656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.06/4.07 % (3882656)CaDiCaL version: 2.1.3 % 27.06/4.07 % (3882656)Termination reason: Instruction limit % 27.06/4.07 % (3882656)Termination phase: Saturation % 27.06/4.07 % (3882656)Time elapsed: 0.321 s % 27.06/4.07 % (3882656)Peak memory usage: 14 MB % 27.06/4.07 % (3882656)Instructions burned: 478 (million) % 27.06/4.07 % (3882753)fmb+10_1_sil=64000:random_seed=1204816487:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 27.06/4.07 % (3882753)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.06/4.07 % (3882753)Terminated due to inappropriate strategy. % 27.06/4.07 % (3882753)------------------------------ % 27.06/4.07 % (3882753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.06/4.07 % (3882753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.06/4.07 % (3882753)CaDiCaL version: 2.1.3 % 27.06/4.07 % (3882753)Termination reason: Inappropriate % 27.06/4.07 % (3882753)Time elapsed: 0.002 s % 27.06/4.07 % (3882753)Peak memory usage: 10 MB % 27.06/4.07 % (3882753)Instructions burned: 3 (million) % 27.06/4.07 % (3882753)------------------------------ % 27.06/4.07 % (3882753)------------------------------ % 27.06/4.07 % (3882767)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1647371130:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 27.06/4.07 % (3882767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.06/4.07 % (3882767)Terminated due to inappropriate strategy. % 27.06/4.07 % (3882767)------------------------------ % 27.06/4.07 % (3882767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.06/4.07 % (3882767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.06/4.07 % (3882767)CaDiCaL version: 2.1.3 % 27.06/4.07 % (3882767)Termination reason: Inappropriate % 27.06/4.07 % (3882767)Time elapsed: 0.002 s % 27.06/4.07 % (3882767)Peak memory usage: 10 MB % 27.06/4.07 % (3882767)Instructions burned: 3 (million) % 27.06/4.07 % (3882767)------------------------------ % 27.06/4.07 % (3882767)------------------------------ % 27.06/4.07 % (3882772)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2607253930:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 27.06/4.07 % (3882772)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 27.06/4.07 % (3882772)Terminated due to inappropriate strategy. % 27.06/4.07 % (3882772)------------------------------ % 27.06/4.07 % (3882772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.06/4.07 % (3882772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.06/4.07 % (3882772)CaDiCaL version: 2.1.3 % 27.06/4.07 % (3882772)Termination reason: Inappropriate % 27.06/4.07 % (3882772)Time elapsed: 0.002 s % 27.06/4.07 % (3882772)Peak memory usage: 10 MB % 27.06/4.07 % (3882772)Instructions burned: 3 (million) % 27.06/4.07 % (3882772)------------------------------ % 27.06/4.07 % (3882772)------------------------------ % 27.06/4.07 % (3882666)Instruction limit reached! % 27.06/4.07 % (3882666)------------------------------ % 27.06/4.07 % (3882666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.06/4.07 % (3882666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.06/4.07 % (3882666)CaDiCaL version: 2.1.3 % 27.06/4.07 % (3882666)Termination reason: Instruction limit % 27.06/4.07 % (3882666)Termination phase: Saturation % 27.06/4.07 % (3882666)Time elapsed: 0.377 s % 27.06/4.07 % (3882666)Peak memory usage: 19 MB % 27.06/4.07 % (3882666)Instructions burned: 1180 (million) % 27.06/4.07 % (3882778)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1858998834:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 27.06/4.07 % (3882781)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1661318553:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 27.06/4.07 % (3882653)Instruction limit reached! % 27.06/4.07 % (3882653)------------------------------ % 37.31/5.51 % (3882653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.31/5.51 % (3882653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/5.51 % (3882653)CaDiCaL version: 2.1.3 % 37.31/5.51 % (3882653)Termination reason: Instruction limit % 37.31/5.51 % (3882653)Termination phase: Saturation % 37.31/5.51 % (3882653)Time elapsed: 0.444 s % 37.31/5.51 % (3882653)Peak memory usage: 18 MB % 37.31/5.51 % (3882653)Instructions burned: 685 (million) % 37.31/5.51 % (3882788)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1223542304:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 37.31/5.51 % (3882788)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.31/5.51 % (3882788)Terminated due to inappropriate strategy. % 37.31/5.51 % (3882788)------------------------------ % 37.31/5.51 % (3882788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.31/5.51 % (3882788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/5.51 % (3882788)CaDiCaL version: 2.1.3 % 37.31/5.51 % (3882788)Termination reason: Inappropriate % 37.31/5.51 % (3882788)Time elapsed: 0.002 s % 37.31/5.51 % (3882788)Peak memory usage: 11 MB % 37.31/5.51 % (3882788)Instructions burned: 3 (million) % 37.31/5.51 % (3882788)------------------------------ % 37.31/5.51 % (3882788)------------------------------ % 37.31/5.51 % (3882795)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1684702429:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 37.31/5.51 % (3882795)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.31/5.51 % (3882795)Terminated due to inappropriate strategy. % 37.31/5.51 % (3882795)------------------------------ % 37.31/5.51 % (3882795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.31/5.51 % (3882795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/5.51 % (3882795)CaDiCaL version: 2.1.3 % 37.31/5.51 % (3882795)Termination reason: Inappropriate % 37.31/5.51 % (3882795)Time elapsed: 0.002 s % 37.31/5.51 % (3882795)Peak memory usage: 11 MB % 37.31/5.51 % (3882795)Instructions burned: 3 (million) % 37.31/5.51 % (3882795)------------------------------ % 37.31/5.51 % (3882795)------------------------------ % 37.31/5.51 % (3882804)ott-2_1_sil=16000:newcnf=on:random_seed=4063328710:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 37.31/5.51 % (3882674)Instruction limit reached! % 37.31/5.51 % (3882674)------------------------------ % 37.31/5.51 % (3882674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.31/5.51 % (3882674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/5.51 % (3882674)CaDiCaL version: 2.1.3 % 37.31/5.51 % (3882674)Termination reason: Instruction limit % 37.31/5.51 % (3882674)Termination phase: Saturation % 37.31/5.51 % (3882674)Time elapsed: 0.483 s % 37.31/5.51 % (3882674)Peak memory usage: 20 MB % 37.31/5.51 % (3882674)Instructions burned: 693 (million) % 37.31/5.51 % (3882815)ott+10_1_sil=32000:tgt=ground:random_seed=3771989744:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 37.31/5.51 % (3882688)Instruction limit reached! % 37.31/5.51 % (3882688)------------------------------ % 37.31/5.51 % (3882688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.31/5.51 % (3882688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/5.51 % (3882688)CaDiCaL version: 2.1.3 % 37.31/5.51 % (3882688)Termination reason: Instruction limit % 37.31/5.51 % (3882688)Termination phase: Saturation % 37.31/5.51 % (3882688)Time elapsed: 0.547 s % 37.31/5.51 % (3882688)Peak memory usage: 21 MB % 37.31/5.51 % (3882688)Instructions burned: 879 (million) % 37.31/5.51 % (3882817)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2502959008:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 37.31/5.51 % (3882817)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 37.31/5.51 % (3882817)Terminated due to inappropriate strategy. % 37.31/5.51 % (3882817)------------------------------ % 37.31/5.51 % (3882817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.31/5.51 % (3882817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.31/5.51 % (3882817)CaDiCaL version: 2.1.3 % 37.31/5.51 % (3882817)Termination reason: Inappropriate % 37.31/5.51 % (3882817)Time elapsed: 0.002 s % 37.31/5.51 % (3882817)Peak memory usage: 11 MB % 37.31/5.51 % (3882817)Instructions burned: 3 (million) % 152.58/21.74 % (3882817)------------------------------ % 152.58/21.74 % (3882817)------------------------------ % 152.58/21.74 % (3882819)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1216565291:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 152.58/21.74 % (3882804)Instruction limit reached! % 152.58/21.74 % (3882804)------------------------------ % 152.58/21.74 % (3882804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.74 % (3882804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.74 % (3882804)CaDiCaL version: 2.1.3 % 152.58/21.74 % (3882804)Termination reason: Instruction limit % 152.58/21.74 % (3882804)Termination phase: Saturation % 152.58/21.74 % (3882804)Time elapsed: 0.289 s % 152.58/21.74 % (3882804)Peak memory usage: 16 MB % 152.58/21.74 % (3882804)Instructions burned: 872 (million) % 152.58/21.74 % (3882821)dis+21_1_sil=32000:sas=cadical:random_seed=842790247:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi) % 152.58/21.74 % (3882781)Instruction limit reached! % 152.58/21.74 % (3882781)------------------------------ % 152.58/21.74 % (3882781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.74 % (3882781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.74 % (3882781)CaDiCaL version: 2.1.3 % 152.58/21.74 % (3882781)Termination reason: Instruction limit % 152.58/21.74 % (3882781)Termination phase: Saturation % 152.58/21.74 % (3882781)Time elapsed: 1.089 s % 152.58/21.74 % (3882781)Peak memory usage: 23 MB % 152.58/21.74 % (3882781)Instructions burned: 1473 (million) % 152.58/21.74 % (3882845)ott+11_1_sil=16000:gs=on:random_seed=3954226141:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi) % 152.58/21.74 % (3882821)Instruction limit reached! % 152.58/21.74 % (3882821)------------------------------ % 152.58/21.74 % (3882821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.74 % (3882821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.74 % (3882821)CaDiCaL version: 2.1.3 % 152.58/21.74 % (3882821)Termination reason: Instruction limit % 152.58/21.74 % (3882821)Termination phase: Saturation % 152.58/21.74 % (3882821)Time elapsed: 1.446 s % 152.58/21.74 % (3882821)Peak memory usage: 32 MB % 152.58/21.74 % (3882821)Instructions burned: 3775 (million) % 152.58/21.74 % (3882888)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4028273234:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi) % 152.58/21.74 % (3882888)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 152.58/21.74 % (3882888)Terminated due to inappropriate strategy. % 152.58/21.74 % (3882888)------------------------------ % 152.58/21.74 % (3882888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.74 % (3882888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.74 % (3882888)CaDiCaL version: 2.1.3 % 152.58/21.74 % (3882888)Termination reason: Inappropriate % 152.58/21.74 % (3882888)Time elapsed: 0.001 s % 152.58/21.74 % (3882888)Peak memory usage: 10 MB % 152.58/21.74 % (3882888)Instructions burned: 3 (million) % 152.58/21.74 % (3882888)------------------------------ % 152.58/21.74 % (3882888)------------------------------ % 152.58/21.74 % (3882891)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3505512628:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi) % 152.58/21.74 % (3882845)Instruction limit reached! % 152.58/21.74 % (3882845)------------------------------ % 152.58/21.74 % (3882845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.74 % (3882845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.74 % (3882845)CaDiCaL version: 2.1.3 % 152.58/21.74 % (3882845)Termination reason: Instruction limit % 152.58/21.74 % (3882845)Termination phase: Saturation % 152.58/21.74 % (3882845)Time elapsed: 1.778 s % 152.58/21.74 % (3882845)Peak memory usage: 16 MB % 152.58/21.74 % (3882845)Instructions burned: 2251 (million) % 152.58/21.74 % (3882929)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3593072935:i=29340_2965 on theBenchmark for (2965ds/29340Mi) % 152.58/21.74 % (3882819)Instruction limit reached! % 152.58/21.74 % (3882819)------------------------------ % 152.58/21.74 % (3882819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.58/21.74 % (3882819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.58/21.74 % (3882819)CaDiCaL version: 2.1.3 % 152.58/21.74 % (3882819)Termination reason: Instruction limit % 197.74/28.06 % (3882819)Termination phase: Saturation % 197.74/28.06 % (3882819)Time elapsed: 2.996 s % 197.74/28.06 % (3882819)Peak memory usage: 32 MB % 197.74/28.06 % (3882819)Instructions burned: 3512 (million) % 197.74/28.06 % (3882942)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2063021318:i=5211_2961 on theBenchmark for (2961ds/5211Mi) % 197.74/28.06 % (3882778)Instruction limit reached! % 197.74/28.06 % (3882778)------------------------------ % 197.74/28.06 % (3882778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.74/28.06 % (3882778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.74/28.06 % (3882778)CaDiCaL version: 2.1.3 % 197.74/28.06 % (3882778)Termination reason: Instruction limit % 197.74/28.06 % (3882778)Termination phase: Saturation % 197.74/28.06 % (3882778)Time elapsed: 3.837 s % 197.74/28.06 % (3882778)Peak memory usage: 36 MB % 197.74/28.06 % (3882778)Instructions burned: 5131 (million) % 197.74/28.06 % (3882959)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3388076551:i=5497:nm=2_2956 on theBenchmark for (2956ds/5497Mi) % 197.74/28.06 % (3882959)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.74/28.06 % (3882959)Terminated due to inappropriate strategy. % 197.74/28.06 % (3882959)------------------------------ % 197.74/28.06 % (3882959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.74/28.06 % (3882959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.74/28.06 % (3882959)CaDiCaL version: 2.1.3 % 197.74/28.06 % (3882959)Termination reason: Inappropriate % 197.74/28.06 % (3882959)Time elapsed: 0.003 s % 197.74/28.06 % (3882959)Peak memory usage: 11 MB % 197.74/28.06 % (3882959)Instructions burned: 3 (million) % 197.74/28.06 % (3882959)------------------------------ % 197.74/28.06 % (3882959)------------------------------ % 197.74/28.06 % (3882961)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=272384152:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 197.74/28.06 % (3882961)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.74/28.06 % (3882961)Terminated due to inappropriate strategy. % 197.74/28.06 % (3882961)------------------------------ % 197.74/28.06 % (3882961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.74/28.06 % (3882961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.74/28.06 % (3882961)CaDiCaL version: 2.1.3 % 197.74/28.06 % (3882961)Termination reason: Inappropriate % 197.74/28.06 % (3882961)Time elapsed: 0.002 s % 197.74/28.06 % (3882961)Peak memory usage: 11 MB % 197.74/28.06 % (3882961)Instructions burned: 3 (million) % 197.74/28.06 % (3882961)------------------------------ % 197.74/28.06 % (3882961)------------------------------ % 197.74/28.06 % (3882966)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=241937907:i=14071_2955 on theBenchmark for (2955ds/14071Mi) % 197.74/28.06 % (3882966)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 197.74/28.06 % (3882966)Terminated due to inappropriate strategy. % 197.74/28.06 % (3882966)------------------------------ % 197.74/28.06 % (3882966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.74/28.06 % (3882966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.74/28.06 % (3882966)CaDiCaL version: 2.1.3 % 197.74/28.06 % (3882966)Termination reason: Inappropriate % 197.74/28.06 % (3882966)Time elapsed: 0.003 s % 197.74/28.06 % (3882966)Peak memory usage: 10 MB % 197.74/28.06 % (3882966)Instructions burned: 3 (million) % 197.74/28.06 % (3882966)------------------------------ % 197.74/28.06 % (3882966)------------------------------ % 197.74/28.06 % (3882968)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1959873337:i=22565:add=on:rawr=on_2955 on theBenchmark for (2955ds/22565Mi) % 197.74/28.06 % (3882891)Instruction limit reached! % 197.74/28.06 % (3882891)------------------------------ % 197.74/28.06 % (3882891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 197.74/28.06 % (3882891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.74/28.06 % (3882891)CaDiCaL version: 2.1.3 % 197.74/28.06 % (3882891)Termination reason: Instruction limit % 197.74/28.06 % (3882891)Termination phase: Saturation % 197.74/28.06 % (3882891)Time elapsed: 2.198 s % 197.74/28.06 % (3882891)Peak memory usage: 62 MB % 197.74/28.06 % (3882891)Instructions burned: 4592 (million) % 197.74/28.06 % (3882973)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=509089243:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi) % 197.74/28.06 % (3882815)Instruction limit reached! % 198.88/28.20 % (3882815)------------------------------ % 198.88/28.20 % (3882815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.88/28.20 % (3882815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.88/28.20 % (3882815)CaDiCaL version: 2.1.3 % 198.88/28.20 % (3882815)Termination reason: Instruction limit % 198.88/28.20 % (3882815)Termination phase: Saturation % 198.88/28.20 % (3882815)Time elapsed: 4.575 s % 198.88/28.20 % (3882815)Peak memory usage: 38 MB % 198.88/28.20 % (3882815)Instructions burned: 5114 (million) % 198.88/28.20 % (3882992)dis+10_16:1_sil=16000:random_seed=2911071146:i=9155:fsr=off_2947 on theBenchmark for (2947ds/9155Mi) % 198.88/28.20 % (3882942)Instruction limit reached! % 198.88/28.20 % (3882942)------------------------------ % 198.88/28.20 % (3882942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.88/28.20 % (3882942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.88/28.20 % (3882942)CaDiCaL version: 2.1.3 % 198.88/28.20 % (3882942)Termination reason: Instruction limit % 198.88/28.20 % (3882942)Termination phase: Saturation % 198.88/28.20 % (3882942)Time elapsed: 2.656 s % 198.88/28.20 % (3882942)Peak memory usage: 44 MB % 198.88/28.20 % (3882942)Instructions burned: 5212 (million) % 198.88/28.20 % (3883017)ott-3_8_sil=64000:random_seed=2982074355:i=20139:bs=on_2934 on theBenchmark for (2934ds/20139Mi) % 198.88/28.20 % (3882973)Instruction limit reached! % 198.88/28.20 % (3882973)------------------------------ % 198.88/28.20 % (3882973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.88/28.20 % (3882973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.88/28.20 % (3882973)CaDiCaL version: 2.1.3 % 198.88/28.20 % (3882973)Termination reason: Instruction limit % 198.88/28.20 % (3882973)Termination phase: Saturation % 198.88/28.20 % (3882973)Time elapsed: 7.963 s % 198.88/28.20 % (3882973)Peak memory usage: 64 MB % 198.88/28.20 % (3882973)Instructions burned: 8173 (million) % 198.88/28.20 % (3883065)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4186514203:fmbsr=2:i=32576_2873 on theBenchmark for (2873ds/32576Mi) % 198.88/28.20 % (3883065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.88/28.20 % (3883065)Terminated due to inappropriate strategy. % 198.88/28.20 % (3883065)------------------------------ % 198.88/28.20 % (3883065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.88/28.20 % (3883065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.88/28.20 % (3883065)CaDiCaL version: 2.1.3 % 198.88/28.20 % (3883065)Termination reason: Inappropriate % 198.88/28.20 % (3883065)Time elapsed: 0.003 s % 198.88/28.20 % (3883065)Peak memory usage: 10 MB % 198.88/28.20 % (3883065)Instructions burned: 3 (million) % 198.88/28.20 % (3883065)------------------------------ % 198.88/28.20 % (3883065)------------------------------ % 198.88/28.20 % (3883067)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2305262944:i=11404_2873 on theBenchmark for (2873ds/11404Mi) % 198.88/28.20 % (3882992)Instruction limit reached! % 198.88/28.20 % (3882992)------------------------------ % 198.88/28.20 % (3882992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.88/28.20 % (3882992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.88/28.20 % (3882992)CaDiCaL version: 2.1.3 % 198.88/28.20 % (3882992)Termination reason: Instruction limit % 198.88/28.20 % (3882992)Termination phase: Saturation % 198.88/28.20 % (3882992)Time elapsed: 8.354 s % 198.88/28.20 % (3882992)Peak memory usage: 52 MB % 198.88/28.20 % (3882992)Instructions burned: 9155 (million) % 198.88/28.20 % (3883074)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3826646268:i=14134_2863 on theBenchmark for (2863ds/14134Mi) % 198.88/28.20 % (3883017)Instruction limit reached! % 198.88/28.20 % (3883017)------------------------------ % 198.88/28.20 % (3883017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.88/28.20 % (3883017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.88/28.20 % (3883017)CaDiCaL version: 2.1.3 % 198.88/28.20 % (3883017)Termination reason: Instruction limit % 198.88/28.20 % (3883017)Termination phase: Saturation % 198.88/28.20 % (3883017)Time elapsed: 11.757 s % 198.88/28.20 % (3883017)Peak memory usage: 103 MB % 198.88/28.20 % (3883017)Instructions burned: 20139 (million) % 198.88/28.20 % (3883092)dis+33_16_sil=32000:sac=on:random_seed=1296605816:i=15851:nm=0_2816 on theBenchmark for (2816ds/15851Mi) % 198.88/28.20 % (3882968)Instruction limit reached! % 198.88/28.20 % (3882968)------------------------------ % 198.88/28.20 % (3882968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.10 % (3882968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.10 % (3882968)CaDiCaL version: 2.1.3 % 261.78/37.10 % (3882968)Termination reason: Instruction limit % 261.78/37.10 % (3882968)Termination phase: Saturation % 261.78/37.10 % (3882968)Time elapsed: 16.976 s % 261.78/37.10 % (3882968)Peak memory usage: 85 MB % 261.78/37.10 % (3882968)Instructions burned: 22567 (million) % 261.78/37.10 % (3883094)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=537417136:avsq=on:i=17627:add=on:amm=off_2784 on theBenchmark for (2784ds/17627Mi) % 261.78/37.10 % (3883067)Instruction limit reached! % 261.78/37.10 % (3883067)------------------------------ % 261.78/37.10 % (3883067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.10 % (3883067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.10 % (3883067)CaDiCaL version: 2.1.3 % 261.78/37.10 % (3883067)Termination reason: Instruction limit % 261.78/37.10 % (3883067)Termination phase: Saturation % 261.78/37.10 % (3883067)Time elapsed: 11.508 s % 261.78/37.10 % (3883067)Peak memory usage: 74 MB % 261.78/37.10 % (3883067)Instructions burned: 11404 (million) % 261.78/37.10 % (3883102)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=707757912:s2a=on:i=53295_2757 on theBenchmark for (2757ds/53295Mi) % 261.78/37.10 % (3883092)Instruction limit reached! % 261.78/37.10 % (3883092)------------------------------ % 261.78/37.10 % (3883092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.10 % (3883092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.10 % (3883092)CaDiCaL version: 2.1.3 % 261.78/37.10 % (3883092)Termination reason: Instruction limit % 261.78/37.10 % (3883092)Termination phase: Saturation % 261.78/37.10 % (3883092)Time elapsed: 8.593 s % 261.78/37.10 % (3883092)Peak memory usage: 144 MB % 261.78/37.10 % (3883092)Instructions burned: 15852 (million) % 261.78/37.10 % (3883108)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2265599392:i=26857:ins=20_2730 on theBenchmark for (2730ds/26857Mi) % 261.78/37.10 % (3883108)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.78/37.10 % (3883108)Terminated due to inappropriate strategy. % 261.78/37.10 % (3883108)------------------------------ % 261.78/37.10 % (3883108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.10 % (3883108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.10 % (3883108)CaDiCaL version: 2.1.3 % 261.78/37.10 % (3883108)Termination reason: Inappropriate % 261.78/37.10 % (3883108)Time elapsed: 0.002 s % 261.78/37.10 % (3883108)Peak memory usage: 10 MB % 261.78/37.10 % (3883108)Instructions burned: 3 (million) % 261.78/37.10 % (3883108)------------------------------ % 261.78/37.10 % (3883108)------------------------------ % 261.78/37.10 % (3883110)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2265513119:i=28120:bs=on:fsr=off_2730 on theBenchmark for (2730ds/28120Mi) % 261.78/37.10 % (3882929)Instruction limit reached! % 261.78/37.10 % (3882929)------------------------------ % 261.78/37.10 % (3882929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.10 % (3882929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.10 % (3882929)CaDiCaL version: 2.1.3 % 261.78/37.10 % (3882929)Termination reason: Instruction limit % 261.78/37.10 % (3882929)Termination phase: Saturation % 261.78/37.10 % (3882929)Time elapsed: 24.198 s % 261.78/37.10 % (3882929)Peak memory usage: 256 MB % 261.78/37.10 % (3882929)Instructions burned: 29340 (million) % 261.78/37.10 % (3883115)fmb+10_1_sil=256000:fmbss=7:random_seed=2686146249:fmbsr=1.6:i=182295_2722 on theBenchmark for (2722ds/182295Mi) % 261.78/37.10 % (3883115)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 261.78/37.10 % (3883115)Terminated due to inappropriate strategy. % 261.78/37.10 % (3883115)------------------------------ % 261.78/37.10 % (3883115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.78/37.10 % (3883115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.78/37.10 % (3883115)CaDiCaL version: 2.1.3 % 261.78/37.10 % (3883115)Termination reason: Inappropriate % 261.78/37.10 % (3883115)Time elapsed: 0.003 s % 261.78/37.10 % (3883115)Peak memory usage: 10 MB % 261.78/37.10 % (3883115)Instructions burned: 3 (million) % 261.78/37.10 % (3883115)------------------------------ % 261.78/37.10 % (3883115)------------------------------ % 261.78/37.10 % (3883117)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1970670971:i=44625:gsp=on_2722 on theBenchmark for (2722ds/44625Mi) % 284.26/40.29 % (3883117)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.26/40.29 % (3883117)Terminated due to inappropriate strategy. % 284.26/40.29 % (3883117)------------------------------ % 284.26/40.29 % (3883117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.29 % (3883117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.29 % (3883117)CaDiCaL version: 2.1.3 % 284.26/40.29 % (3883117)Termination reason: Inappropriate % 284.26/40.29 % (3883117)Time elapsed: 0.004 s % 284.26/40.29 % (3883117)Peak memory usage: 10 MB % 284.26/40.29 % (3883117)Instructions burned: 3 (million) % 284.26/40.29 % (3883117)------------------------------ % 284.26/40.29 % (3883117)------------------------------ % 284.26/40.29 % (3883119)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3034101037:i=160505_2721 on theBenchmark for (2721ds/160505Mi) % 284.26/40.29 % (3883119)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.26/40.29 % (3883119)Terminated due to inappropriate strategy. % 284.26/40.29 % (3883119)------------------------------ % 284.26/40.29 % (3883119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.29 % (3883119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.29 % (3883119)CaDiCaL version: 2.1.3 % 284.26/40.29 % (3883119)Termination reason: Inappropriate % 284.26/40.29 % (3883119)Time elapsed: 0.002 s % 284.26/40.29 % (3883119)Peak memory usage: 11 MB % 284.26/40.29 % (3883119)Instructions burned: 3 (million) % 284.26/40.29 % (3883119)------------------------------ % 284.26/40.29 % (3883119)------------------------------ % 284.26/40.29 % (3883122)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=687814325:fmbsr=1.3:i=225729_2721 on theBenchmark for (2721ds/225729Mi) % 284.26/40.29 % (3883122)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.26/40.29 % (3883122)Terminated due to inappropriate strategy. % 284.26/40.29 % (3883122)------------------------------ % 284.26/40.29 % (3883122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.29 % (3883122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.29 % (3883122)CaDiCaL version: 2.1.3 % 284.26/40.29 % (3883122)Termination reason: Inappropriate % 284.26/40.29 % (3883122)Time elapsed: 0.002 s % 284.26/40.29 % (3883122)Peak memory usage: 11 MB % 284.26/40.29 % (3883122)Instructions burned: 3 (million) % 284.26/40.29 % (3883122)------------------------------ % 284.26/40.29 % (3883122)------------------------------ % 284.26/40.29 % (3883124)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2354759921:fmbsr=2:i=185024:ins=7_2721 on theBenchmark for (2721ds/185024Mi) % 284.26/40.29 % (3883124)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.26/40.29 % (3883124)Terminated due to inappropriate strategy. % 284.26/40.29 % (3883124)------------------------------ % 284.26/40.29 % (3883124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.29 % (3883124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.29 % (3883124)CaDiCaL version: 2.1.3 % 284.26/40.29 % (3883124)Termination reason: Inappropriate % 284.26/40.29 % (3883124)Time elapsed: 0.002 s % 284.26/40.29 % (3883124)Peak memory usage: 11 MB % 284.26/40.29 % (3883124)Instructions burned: 3 (million) % 284.26/40.29 % (3883124)------------------------------ % 284.26/40.29 % (3883124)------------------------------ % 284.26/40.29 % (3883126)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2886307727:rtra=on_2720 on theBenchmark for (2720ds/0Mi) % 284.26/40.29 % (3883126)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 284.26/40.29 % (3883126)Terminated due to inappropriate strategy. % 284.26/40.29 % (3883126)------------------------------ % 284.26/40.29 % (3883126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.26/40.29 % (3883126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.26/40.29 % (3883126)CaDiCaL version: 2.1.3 % 284.26/40.29 % (3883126)Termination reason: Inappropriate % 284.26/40.29 % (3883126)Time elapsed: 0.005 s % 284.26/40.29 % (3883126)Peak memory usage: 11 MB % 284.26/40.29 % (3883126)Instructions burned: 3 (million) % 284.26/40.29 % (3883126)------------------------------ % 284.26/40.29 % (3883126)------------------------------ % 284.26/40.29 % (3883128)% WARNING: option uhcvi not known. % 284.26/40.29 % (3883128)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=22434420Terminated % 300.58/42.54 % Vampire exiting % 300.58/42.54 Terminated %------------------------------------------------------------------------------