%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW654_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 : n003.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:36 PM UTC 2026 % Result : Timeout 292.69s 41.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW654_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.13/0.25 % Computer : n003.cluster.edu % 0.13/0.25 % Model : x86_64 x86_64 % 0.13/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.25 % Memory : 8046.5625MB % 0.13/0.25 % OS : Linux 6.8.0-71-generic % 0.13/0.25 % CPULimit : 300 % 0.13/0.25 % WCLimit : 300 % 0.13/0.25 % DateTime : Mon Sep 28 14:25:42 UTC 2026 % 0.13/0.25 % CPUTime : % 0.13/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.30/0.30 Running first-order model finding % 0.30/0.30 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 % 6.07/1.17 % (1623659)Will run a generic schedule for satisfiability detection. % 6.07/1.17 % (1623668)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=94707464:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.07/1.17 % (1623665)% WARNING: option uhcvi not known. % 6.07/1.17 % (1623667)dis+10_1_sil=32000:sp=arity:random_seed=1047291973:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.07/1.17 % (1623665)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2873743174:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.07/1.17 % (1623664)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=358926834_2999 on theBenchmark for (2999ds/0Mi) % 6.07/1.17 % (1623666)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3148460958:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.07/1.17 % (1623669)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1343898338:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.07/1.17 % (1623670)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3130561797:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.07/1.17 % (1623664)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.07/1.17 % (1623664)Terminated due to inappropriate strategy. % 6.07/1.17 % (1623664)------------------------------ % 6.07/1.17 % (1623664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.07/1.17 % (1623664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.07/1.17 % (1623664)CaDiCaL version: 2.1.3 % 6.07/1.17 % (1623664)Termination reason: Inappropriate % 6.07/1.17 % (1623664)Time elapsed: 0.008 s % 6.07/1.17 % (1623664)Peak memory usage: 10 MB % 6.07/1.17 % (1623664)Instructions burned: 8 (million) % 6.07/1.17 % (1623664)------------------------------ % 6.07/1.17 % (1623664)------------------------------ % 6.07/1.17 % (1623678)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3052563707:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.07/1.17 % (1623668)Instruction limit reached! % 6.07/1.17 % (1623668)------------------------------ % 6.07/1.17 % (1623668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.07/1.17 % (1623668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.07/1.17 % (1623668)CaDiCaL version: 2.1.3 % 6.07/1.17 % (1623668)Termination reason: Instruction limit % 6.07/1.17 % (1623668)Termination phase: Saturation % 6.07/1.17 % (1623668)Time elapsed: 0.063 s % 6.07/1.17 % (1623668)Peak memory usage: 13 MB % 6.07/1.17 % (1623668)Instructions burned: 118 (million) % 6.07/1.17 % (1623678)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.07/1.17 % (1623678)Terminated due to inappropriate strategy. % 6.07/1.17 % (1623678)------------------------------ % 6.07/1.17 % (1623678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.07/1.17 % (1623678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.07/1.17 % (1623678)CaDiCaL version: 2.1.3 % 6.07/1.17 % (1623678)Termination reason: Inappropriate % 6.07/1.17 % (1623678)Time elapsed: 0.007 s % 6.07/1.17 % (1623678)Peak memory usage: 11 MB % 6.07/1.17 % (1623678)Instructions burned: 7 (million) % 6.07/1.17 % (1623678)------------------------------ % 6.07/1.17 % (1623678)------------------------------ % 6.07/1.17 % (1623680)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2767071582:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.07/1.17 % (1623681)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=1797173243:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.07/1.17 % (1623667)Instruction limit reached! % 6.07/1.17 % (1623667)------------------------------ % 6.07/1.17 % (1623667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.07/1.17 % (1623667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.07/1.17 % (1623667)CaDiCaL version: 2.1.3 % 6.07/1.17 % (1623667)Termination reason: Instruction limit % 6.07/1.17 % (1623667)Termination phase: Saturation % 6.07/1.17 % (1623667)Time elapsed: 0.105 s % 6.07/1.17 % (1623667)Peak memory usage: 13 MB % 6.07/1.17 % (1623667)Instructions burned: 104 (million) % 6.07/1.17 % (1623669)Instruction limit reached! % 6.07/1.17 % (1623669)------------------------------ % 6.07/1.17 % (1623669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.40/1.53 % (1623669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.40/1.53 % (1623669)CaDiCaL version: 2.1.3 % 7.40/1.53 % (1623669)Termination reason: Instruction limit % 7.40/1.53 % (1623669)Termination phase: Saturation % 7.40/1.53 % (1623669)Time elapsed: 0.135 s % 7.40/1.53 % (1623669)Peak memory usage: 13 MB % 7.40/1.53 % (1623669)Instructions burned: 131 (million) % 7.40/1.53 % (1623684)ott-21_1_sil=16000:fs=off:random_seed=2288142907:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.40/1.53 % (1623680)Instruction limit reached! % 7.40/1.53 % (1623680)------------------------------ % 7.40/1.53 % (1623680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.40/1.53 % (1623680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.40/1.53 % (1623680)CaDiCaL version: 2.1.3 % 7.40/1.53 % (1623680)Termination reason: Instruction limit % 7.40/1.53 % (1623680)Termination phase: Saturation % 7.40/1.53 % (1623680)Time elapsed: 0.081 s % 7.40/1.53 % (1623680)Peak memory usage: 13 MB % 7.40/1.53 % (1623680)Instructions burned: 131 (million) % 7.40/1.53 % (1623685)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2616717962:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.40/1.53 % (1623687)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2544116246:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.40/1.53 % (1623687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.40/1.53 % (1623687)Terminated due to inappropriate strategy. % 7.40/1.53 % (1623687)------------------------------ % 7.40/1.53 % (1623687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.40/1.53 % (1623687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.40/1.53 % (1623687)CaDiCaL version: 2.1.3 % 7.40/1.53 % (1623687)Termination reason: Inappropriate % 7.40/1.53 % (1623687)Time elapsed: 0.003 s % 7.40/1.53 % (1623687)Peak memory usage: 10 MB % 7.40/1.53 % (1623687)Instructions burned: 5 (million) % 7.40/1.53 % (1623687)------------------------------ % 7.40/1.53 % (1623687)------------------------------ % 7.40/1.53 % (1623670)Instruction limit reached! % 7.40/1.53 % (1623670)------------------------------ % 7.40/1.53 % (1623670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.40/1.53 % (1623670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.40/1.53 % (1623670)CaDiCaL version: 2.1.3 % 7.40/1.53 % (1623670)Termination reason: Instruction limit % 7.40/1.53 % (1623670)Termination phase: Saturation % 7.40/1.53 % (1623670)Time elapsed: 0.182 s % 7.40/1.53 % (1623670)Peak memory usage: 13 MB % 7.40/1.53 % (1623670)Instructions burned: 160 (million) % 7.40/1.53 % (1623690)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2698543527:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.40/1.53 % (1623691)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4135740001:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.40/1.53 % (1623691)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.40/1.53 % (1623691)Terminated due to inappropriate strategy. % 7.40/1.53 % (1623691)------------------------------ % 7.40/1.53 % (1623691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.40/1.53 % (1623691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.40/1.53 % (1623691)CaDiCaL version: 2.1.3 % 7.40/1.53 % (1623691)Termination reason: Inappropriate % 7.40/1.53 % (1623691)Time elapsed: 0.007 s % 7.40/1.53 % (1623691)Peak memory usage: 10 MB % 7.40/1.53 % (1623691)Instructions burned: 7 (million) % 7.40/1.53 % (1623691)------------------------------ % 7.40/1.53 % (1623691)------------------------------ % 7.40/1.53 % (1623694)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=1009856393: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) % 7.40/1.53 % (1623684)Instruction limit reached! % 7.40/1.53 % (1623684)------------------------------ % 7.40/1.53 % (1623684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.40/1.53 % (1623684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.40/1.53 % (1623684)CaDiCaL version: 2.1.3 % 7.40/1.53 % (1623684)Termination reason: Instruction limit % 7.40/1.53 % (1623684)Termination phase: Saturation % 31.34/4.78 % (1623684)Time elapsed: 0.161 s % 31.34/4.78 % (1623684)Peak memory usage: 12 MB % 31.34/4.78 % (1623684)Instructions burned: 180 (million) % 31.34/4.78 % (1623696)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1941289346:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 31.34/4.78 % (1623685)Instruction limit reached! % 31.34/4.78 % (1623685)------------------------------ % 31.34/4.78 % (1623685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.34/4.78 % (1623685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.34/4.78 % (1623685)CaDiCaL version: 2.1.3 % 31.34/4.78 % (1623685)Termination reason: Instruction limit % 31.34/4.78 % (1623685)Termination phase: Saturation % 31.34/4.78 % (1623685)Time elapsed: 0.535 s % 31.34/4.78 % (1623685)Peak memory usage: 14 MB % 31.34/4.78 % (1623685)Instructions burned: 478 (million) % 31.34/4.78 % (1623698)fmb+10_1_sil=64000:random_seed=1261326929:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 31.34/4.78 % (1623698)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.34/4.79 % (1623698)Terminated due to inappropriate strategy. % 31.34/4.79 % (1623698)------------------------------ % 31.34/4.79 % (1623698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.34/4.79 % (1623698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.34/4.79 % (1623698)CaDiCaL version: 2.1.3 % 31.34/4.79 % (1623698)Termination reason: Inappropriate % 31.34/4.79 % (1623698)Time elapsed: 0.006 s % 31.34/4.79 % (1623698)Peak memory usage: 11 MB % 31.34/4.79 % (1623698)Instructions burned: 9 (million) % 31.34/4.79 % (1623698)------------------------------ % 31.34/4.79 % (1623698)------------------------------ % 31.34/4.79 % (1623681)Instruction limit reached! % 31.34/4.79 % (1623681)------------------------------ % 31.34/4.79 % (1623681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.34/4.79 % (1623681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.34/4.79 % (1623681)CaDiCaL version: 2.1.3 % 31.34/4.79 % (1623681)Termination reason: Instruction limit % 31.34/4.79 % (1623681)Termination phase: Saturation % 31.34/4.79 % (1623681)Time elapsed: 0.652 s % 31.34/4.79 % (1623681)Peak memory usage: 19 MB % 31.34/4.79 % (1623681)Instructions burned: 684 (million) % 31.34/4.79 % (1623700)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1337665769:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 31.34/4.79 % (1623700)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.34/4.79 % (1623700)Terminated due to inappropriate strategy. % 31.34/4.79 % (1623700)------------------------------ % 31.34/4.79 % (1623700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.34/4.79 % (1623700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.34/4.79 % (1623700)CaDiCaL version: 2.1.3 % 31.34/4.79 % (1623700)Termination reason: Inappropriate % 31.34/4.79 % (1623700)Time elapsed: 0.007 s % 31.34/4.79 % (1623700)Peak memory usage: 10 MB % 31.34/4.79 % (1623700)Instructions burned: 7 (million) % 31.34/4.79 % (1623700)------------------------------ % 31.34/4.79 % (1623700)------------------------------ % 31.34/4.79 % (1623701)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=6264853:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 31.34/4.79 % (1623701)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 31.34/4.79 % (1623701)Terminated due to inappropriate strategy. % 31.34/4.79 % (1623701)------------------------------ % 31.34/4.79 % (1623701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.34/4.79 % (1623701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.34/4.79 % (1623701)CaDiCaL version: 2.1.3 % 31.34/4.79 % (1623701)Termination reason: Inappropriate % 31.34/4.79 % (1623701)Time elapsed: 0.007 s % 31.34/4.79 % (1623701)Peak memory usage: 10 MB % 31.34/4.79 % (1623701)Instructions burned: 7 (million) % 31.34/4.79 % (1623701)------------------------------ % 31.34/4.79 % (1623701)------------------------------ % 31.34/4.79 % (1623704)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1054049301:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 31.34/4.79 % (1623705)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=206705763:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 31.34/4.79 % (1623690)Instruction limit reached! % 31.34/4.79 % (1623690)------------------------------ % 43.85/6.62 % (1623690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.85/6.62 % (1623690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.85/6.62 % (1623690)CaDiCaL version: 2.1.3 % 43.85/6.62 % (1623690)Termination reason: Instruction limit % 43.85/6.62 % (1623690)Termination phase: Saturation % 43.85/6.62 % (1623690)Time elapsed: 0.625 s % 43.85/6.62 % (1623690)Peak memory usage: 21 MB % 43.85/6.62 % (1623690)Instructions burned: 1179 (million) % 43.85/6.62 % (1623708)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=137898956:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 43.85/6.62 % (1623708)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.85/6.62 % (1623708)Terminated due to inappropriate strategy. % 43.85/6.62 % (1623708)------------------------------ % 43.85/6.62 % (1623708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.85/6.62 % (1623708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.85/6.62 % (1623708)CaDiCaL version: 2.1.3 % 43.85/6.62 % (1623708)Termination reason: Inappropriate % 43.85/6.62 % (1623708)Time elapsed: 0.005 s % 43.85/6.62 % (1623708)Peak memory usage: 11 MB % 43.85/6.62 % (1623708)Instructions burned: 8 (million) % 43.85/6.62 % (1623708)------------------------------ % 43.85/6.62 % (1623708)------------------------------ % 43.85/6.62 % (1623710)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3308027011:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 43.85/6.62 % (1623710)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.85/6.62 % (1623710)Terminated due to inappropriate strategy. % 43.85/6.62 % (1623710)------------------------------ % 43.85/6.62 % (1623710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.85/6.62 % (1623710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.85/6.62 % (1623710)CaDiCaL version: 2.1.3 % 43.85/6.62 % (1623710)Termination reason: Inappropriate % 43.85/6.62 % (1623710)Time elapsed: 0.004 s % 43.85/6.62 % (1623710)Peak memory usage: 11 MB % 43.85/6.62 % (1623710)Instructions burned: 7 (million) % 43.85/6.62 % (1623710)------------------------------ % 43.85/6.62 % (1623710)------------------------------ % 43.85/6.62 % (1623712)ott-2_1_sil=16000:newcnf=on:random_seed=2467477209:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 43.85/6.62 % (1623694)Instruction limit reached! % 43.85/6.62 % (1623694)------------------------------ % 43.85/6.62 % (1623694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.85/6.62 % (1623694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.85/6.62 % (1623694)CaDiCaL version: 2.1.3 % 43.85/6.62 % (1623694)Termination reason: Instruction limit % 43.85/6.62 % (1623694)Termination phase: Saturation % 43.85/6.62 % (1623694)Time elapsed: 0.668 s % 43.85/6.62 % (1623694)Peak memory usage: 17 MB % 43.85/6.62 % (1623694)Instructions burned: 692 (million) % 43.85/6.62 % (1623714)ott+10_1_sil=32000:tgt=ground:random_seed=4251134010:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 43.85/6.62 % (1623696)Instruction limit reached! % 43.85/6.62 % (1623696)------------------------------ % 43.85/6.62 % (1623696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.85/6.62 % (1623696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.85/6.62 % (1623696)CaDiCaL version: 2.1.3 % 43.85/6.62 % (1623696)Termination reason: Instruction limit % 43.85/6.62 % (1623696)Termination phase: Saturation % 43.85/6.62 % (1623696)Time elapsed: 0.808 s % 43.85/6.62 % (1623696)Peak memory usage: 18 MB % 43.85/6.62 % (1623696)Instructions burned: 879 (million) % 43.85/6.62 % (1623716)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4095404658:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 43.85/6.62 % (1623716)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 43.85/6.62 % (1623716)Terminated due to inappropriate strategy. % 43.85/6.62 % (1623716)------------------------------ % 43.85/6.62 % (1623716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.85/6.62 % (1623716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.85/6.62 % (1623716)CaDiCaL version: 2.1.3 % 43.85/6.62 % (1623716)Termination reason: Inappropriate % 43.85/6.62 % (1623716)Time elapsed: 0.009 s % 43.85/6.62 % (1623716)Peak memory usage: 11 MB % 43.85/6.62 % (1623716)Instructions burned: 8 (million) % 121.61/17.47 % (1623716)------------------------------ % 121.61/17.47 % (1623716)------------------------------ % 121.61/17.47 % (1623718)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3643745795:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 121.61/17.47 % (1623712)Instruction limit reached! % 121.61/17.47 % (1623712)------------------------------ % 121.61/17.47 % (1623712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.61/17.47 % (1623712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.61/17.47 % (1623712)CaDiCaL version: 2.1.3 % 121.61/17.47 % (1623712)Termination reason: Instruction limit % 121.61/17.47 % (1623712)Termination phase: Saturation % 121.61/17.47 % (1623712)Time elapsed: 0.488 s % 121.61/17.47 % (1623712)Peak memory usage: 18 MB % 121.61/17.47 % (1623712)Instructions burned: 870 (million) % 121.61/17.47 % (1623720)dis+21_1_sil=32000:sas=cadical:random_seed=700345554:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 121.61/17.47 % (1623705)Instruction limit reached! % 121.61/17.47 % (1623705)------------------------------ % 121.61/17.47 % (1623705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.61/17.47 % (1623705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.61/17.47 % (1623705)CaDiCaL version: 2.1.3 % 121.61/17.47 % (1623705)Termination reason: Instruction limit % 121.61/17.47 % (1623705)Termination phase: Saturation % 121.61/17.47 % (1623705)Time elapsed: 1.319 s % 121.61/17.47 % (1623705)Peak memory usage: 24 MB % 121.61/17.47 % (1623705)Instructions burned: 1472 (million) % 121.61/17.47 % (1623722)ott+11_1_sil=16000:gs=on:random_seed=4170666462:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 121.61/17.47 % (1623720)Instruction limit reached! % 121.61/17.47 % (1623720)------------------------------ % 121.61/17.47 % (1623720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.61/17.47 % (1623720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.61/17.47 % (1623720)CaDiCaL version: 2.1.3 % 121.61/17.47 % (1623720)Termination reason: Instruction limit % 121.61/17.47 % (1623720)Termination phase: Saturation % 121.61/17.47 % (1623720)Time elapsed: 1.953 s % 121.61/17.47 % (1623720)Peak memory usage: 33 MB % 121.61/17.47 % (1623720)Instructions burned: 3775 (million) % 121.61/17.47 % (1623724)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2758649015:fmbsr=1.6:i=67534_2965 on theBenchmark for (2965ds/67534Mi) % 121.61/17.47 % (1623724)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 121.61/17.47 % (1623724)Terminated due to inappropriate strategy. % 121.61/17.47 % (1623724)------------------------------ % 121.61/17.47 % (1623724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.61/17.47 % (1623724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.61/17.47 % (1623724)CaDiCaL version: 2.1.3 % 121.61/17.47 % (1623724)Termination reason: Inappropriate % 121.61/17.47 % (1623724)Time elapsed: 0.004 s % 121.61/17.47 % (1623724)Peak memory usage: 10 MB % 121.61/17.47 % (1623724)Instructions burned: 7 (million) % 121.61/17.47 % (1623724)------------------------------ % 121.61/17.47 % (1623724)------------------------------ % 121.61/17.47 % (1623726)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=277186900:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2965 on theBenchmark for (2965ds/4591Mi) % 121.61/17.47 % (1623718)Instruction limit reached! % 121.61/17.47 % (1623718)------------------------------ % 121.61/17.47 % (1623718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.61/17.47 % (1623718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.61/17.47 % (1623718)CaDiCaL version: 2.1.3 % 121.61/17.47 % (1623718)Termination reason: Instruction limit % 121.61/17.47 % (1623718)Termination phase: Saturation % 121.61/17.47 % (1623718)Time elapsed: 3.192 s % 121.61/17.47 % (1623718)Peak memory usage: 32 MB % 121.61/17.47 % (1623718)Instructions burned: 3513 (million) % 121.61/17.47 % (1623722)Instruction limit reached! % 121.61/17.47 % (1623722)------------------------------ % 121.61/17.47 % (1623722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.61/17.47 % (1623722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.61/17.47 % (1623722)CaDiCaL version: 2.1.3 % 121.61/17.47 % (1623722)Termination reason: Instruction limit % 121.61/17.47 % (1623722)Termination phase: Saturation % 121.61/17.47 % (1623722)Time elapsed: 2.263 s % 121.61/17.47 % (1623722)Peak memory usage: 28 MB % 157.00/22.49 % (1623722)Instructions burned: 2251 (million) % 157.00/22.49 % (1623728)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4204534665:i=29340_2955 on theBenchmark for (2955ds/29340Mi) % 157.00/22.49 % (1623729)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=975020979:i=5211_2955 on theBenchmark for (2955ds/5211Mi) % 157.00/22.49 % (1623726)Instruction limit reached! % 157.00/22.49 % (1623726)------------------------------ % 157.00/22.49 % (1623726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.00/22.49 % (1623726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/22.49 % (1623726)CaDiCaL version: 2.1.3 % 157.00/22.49 % (1623726)Termination reason: Instruction limit % 157.00/22.49 % (1623726)Termination phase: Saturation % 157.00/22.49 % (1623726)Time elapsed: 2.244 s % 157.00/22.49 % (1623726)Peak memory usage: 40 MB % 157.00/22.49 % (1623726)Instructions burned: 4592 (million) % 157.00/22.49 % (1623704)Instruction limit reached! % 157.00/22.49 % (1623704)------------------------------ % 157.00/22.49 % (1623704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.00/22.49 % (1623704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/22.49 % (1623704)CaDiCaL version: 2.1.3 % 157.00/22.49 % (1623704)Termination reason: Instruction limit % 157.00/22.49 % (1623704)Termination phase: Saturation % 157.00/22.49 % (1623704)Time elapsed: 4.884 s % 157.00/22.49 % (1623704)Peak memory usage: 41 MB % 157.00/22.49 % (1623704)Instructions burned: 5131 (million) % 157.00/22.49 % (1623732)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1432809427:i=5497:nm=2_2942 on theBenchmark for (2942ds/5497Mi) % 157.00/22.49 % (1623732)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.00/22.49 % (1623732)Terminated due to inappropriate strategy. % 157.00/22.49 % (1623732)------------------------------ % 157.00/22.49 % (1623732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.00/22.49 % (1623732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/22.49 % (1623732)CaDiCaL version: 2.1.3 % 157.00/22.49 % (1623732)Termination reason: Inappropriate % 157.00/22.49 % (1623732)Time elapsed: 0.005 s % 157.00/22.49 % (1623732)Peak memory usage: 11 MB % 157.00/22.49 % (1623732)Instructions burned: 9 (million) % 157.00/22.49 % (1623732)------------------------------ % 157.00/22.49 % (1623732)------------------------------ % 157.00/22.49 % (1623733)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2367313495:fmbsr=2:i=46332_2942 on theBenchmark for (2942ds/46332Mi) % 157.00/22.49 % (1623733)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.00/22.49 % (1623733)Terminated due to inappropriate strategy. % 157.00/22.49 % (1623733)------------------------------ % 157.00/22.49 % (1623733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.00/22.49 % (1623733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/22.49 % (1623733)CaDiCaL version: 2.1.3 % 157.00/22.49 % (1623733)Termination reason: Inappropriate % 157.00/22.49 % (1623733)Time elapsed: 0.004 s % 157.00/22.49 % (1623733)Peak memory usage: 10 MB % 157.00/22.49 % (1623733)Instructions burned: 7 (million) % 157.00/22.49 % (1623733)------------------------------ % 157.00/22.49 % (1623733)------------------------------ % 157.00/22.49 % (1623735)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3176078707:i=14071_2942 on theBenchmark for (2942ds/14071Mi) % 157.00/22.49 % (1623737)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2600789995:i=22565:add=on:rawr=on_2942 on theBenchmark for (2942ds/22565Mi) % 157.00/22.49 % (1623735)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.00/22.49 % (1623735)Terminated due to inappropriate strategy. % 157.00/22.49 % (1623735)------------------------------ % 157.00/22.49 % (1623735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.00/22.49 % (1623735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.00/22.49 % (1623735)CaDiCaL version: 2.1.3 % 157.00/22.49 % (1623735)Termination reason: Inappropriate % 157.00/22.49 % (1623735)Time elapsed: 0.007 s % 157.00/22.49 % (1623735)Peak memory usage: 11 MB % 157.00/22.49 % (1623735)Instructions burned: 7 (million) % 157.00/22.49 % (1623735)------------------------------ % 157.00/22.49 % (1623735)------------------------------ % 157.00/22.49 % (1623740)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1074624869:i=8173:av=off_2942 on theBenchmark for (2942ds/8173Mi) % 157.00/22.49 % (1623714)Instruction limit reached! % 157.61/22.58 % (1623714)------------------------------ % 157.61/22.58 % (1623714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.61/22.58 % (1623714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.61/22.58 % (1623714)CaDiCaL version: 2.1.3 % 157.61/22.58 % (1623714)Termination reason: Instruction limit % 157.61/22.58 % (1623714)Termination phase: Saturation % 157.61/22.58 % (1623714)Time elapsed: 5.310 s % 157.61/22.58 % (1623714)Peak memory usage: 37 MB % 157.61/22.58 % (1623714)Instructions burned: 5114 (million) % 157.61/22.58 % (1623742)dis+10_16:1_sil=16000:random_seed=1417819743:i=9155:fsr=off_2936 on theBenchmark for (2936ds/9155Mi) % 157.61/22.58 % (1623729)Instruction limit reached! % 157.61/22.58 % (1623729)------------------------------ % 157.61/22.58 % (1623729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.61/22.58 % (1623729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.61/22.58 % (1623729)CaDiCaL version: 2.1.3 % 157.61/22.58 % (1623729)Termination reason: Instruction limit % 157.61/22.58 % (1623729)Termination phase: Saturation % 157.61/22.58 % (1623729)Time elapsed: 4.211 s % 157.61/22.58 % (1623729)Peak memory usage: 37 MB % 157.61/22.58 % (1623729)Instructions burned: 5211 (million) % 157.61/22.58 % (1623744)ott-3_8_sil=64000:random_seed=4164563314:i=20139:bs=on_2912 on theBenchmark for (2912ds/20139Mi) % 157.61/22.58 % (1623737)Instruction limit reached! % 157.61/22.58 % (1623737)------------------------------ % 157.61/22.58 % (1623737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.61/22.58 % (1623737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.61/22.58 % (1623737)CaDiCaL version: 2.1.3 % 157.61/22.58 % (1623737)Termination reason: Instruction limit % 157.61/22.58 % (1623737)Termination phase: Saturation % 157.61/22.58 % (1623737)Time elapsed: 7.526 s % 157.61/22.58 % (1623737)Peak memory usage: 28 MB % 157.61/22.58 % (1623737)Instructions burned: 22568 (million) % 157.61/22.58 % (1623918)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2132461851:fmbsr=2:i=32576_2866 on theBenchmark for (2866ds/32576Mi) % 157.61/22.58 % (1623918)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 157.61/22.58 % (1623918)Terminated due to inappropriate strategy. % 157.61/22.58 % (1623918)------------------------------ % 157.61/22.58 % (1623918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.61/22.58 % (1623918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.61/22.58 % (1623918)CaDiCaL version: 2.1.3 % 157.61/22.58 % (1623918)Termination reason: Inappropriate % 157.61/22.58 % (1623918)Time elapsed: 0.002 s % 157.61/22.58 % (1623918)Peak memory usage: 11 MB % 157.61/22.58 % (1623918)Instructions burned: 8 (million) % 157.61/22.58 % (1623918)------------------------------ % 157.61/22.58 % (1623918)------------------------------ % 157.61/22.58 % (1623920)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2607042434:i=11404_2866 on theBenchmark for (2866ds/11404Mi) % 157.61/22.58 % (1623742)Instruction limit reached! % 157.61/22.58 % (1623742)------------------------------ % 157.61/22.58 % (1623742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.61/22.58 % (1623742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.61/22.58 % (1623742)CaDiCaL version: 2.1.3 % 157.61/22.58 % (1623742)Termination reason: Instruction limit % 157.61/22.58 % (1623742)Termination phase: Saturation % 157.61/22.58 % (1623742)Time elapsed: 7.178 s % 157.61/22.58 % (1623742)Peak memory usage: 55 MB % 157.61/22.58 % (1623742)Instructions burned: 9156 (million) % 157.61/22.58 % (1623922)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2971615204:i=14134_2864 on theBenchmark for (2864ds/14134Mi) % 157.61/22.58 % (1623740)Instruction limit reached! % 157.61/22.58 % (1623740)------------------------------ % 157.61/22.58 % (1623740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.61/22.58 % (1623740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.61/22.58 % (1623740)CaDiCaL version: 2.1.3 % 157.61/22.58 % (1623740)Termination reason: Instruction limit % 157.61/22.58 % (1623740)Termination phase: Saturation % 157.61/22.58 % (1623740)Time elapsed: 7.706 s % 157.61/22.58 % (1623740)Peak memory usage: 54 MB % 157.61/22.58 % (1623740)Instructions burned: 8174 (million) % 157.61/22.58 % (1623924)dis+33_16_sil=32000:sac=on:random_seed=611917837:i=15851:nm=0_2864 on theBenchmark for (2864ds/15851Mi) % 157.61/22.58 % (1623920)Instruction limit reached! % 157.61/22.58 % (1623920)------------------------------ % 157.61/22.58 % (1623920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.03/23.45 % (1623920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.03/23.45 % (1623920)CaDiCaL version: 2.1.3 % 164.03/23.45 % (1623920)Termination reason: Instruction limit % 164.03/23.45 % (1623920)Termination phase: Saturation % 164.03/23.45 % (1623920)Time elapsed: 3.807 s % 164.03/23.45 % (1623920)Peak memory usage: 66 MB % 164.03/23.45 % (1623920)Instructions burned: 11404 (million) % 164.03/23.45 % (1623926)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3843281980:avsq=on:i=17627:add=on:amm=off_2828 on theBenchmark for (2828ds/17627Mi) % 164.03/23.45 % (1623926)Instruction limit reached! % 164.03/23.45 % (1623926)------------------------------ % 164.03/23.45 % (1623926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.03/23.45 % (1623926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.03/23.45 % (1623926)CaDiCaL version: 2.1.3 % 164.03/23.45 % (1623926)Termination reason: Instruction limit % 164.03/23.45 % (1623926)Termination phase: Saturation % 164.03/23.45 % (1623926)Time elapsed: 2.809 s % 164.03/23.45 % (1623926)Peak memory usage: 13 MB % 164.03/23.45 % (1623926)Instructions burned: 17628 (million) % 164.03/23.45 % (1623928)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=316105968:s2a=on:i=53295_2800 on theBenchmark for (2800ds/53295Mi) % 164.03/23.45 % (1623744)Instruction limit reached! % 164.03/23.45 % (1623744)------------------------------ % 164.03/23.45 % (1623744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.03/23.45 % (1623744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.03/23.45 % (1623744)CaDiCaL version: 2.1.3 % 164.03/23.45 % (1623744)Termination reason: Instruction limit % 164.03/23.45 % (1623744)Termination phase: Saturation % 164.03/23.45 % (1623744)Time elapsed: 13.153 s % 164.03/23.45 % (1623744)Peak memory usage: 129 MB % 164.03/23.45 % (1623744)Instructions burned: 20140 (million) % 164.03/23.45 % (1623930)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=739531631:i=26857:ins=20_2780 on theBenchmark for (2780ds/26857Mi) % 164.03/23.45 % (1623930)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.03/23.45 % (1623930)Terminated due to inappropriate strategy. % 164.03/23.45 % (1623930)------------------------------ % 164.03/23.45 % (1623930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.03/23.45 % (1623930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.03/23.45 % (1623930)CaDiCaL version: 2.1.3 % 164.03/23.45 % (1623930)Termination reason: Inappropriate % 164.03/23.45 % (1623930)Time elapsed: 0.004 s % 164.03/23.45 % (1623930)Peak memory usage: 10 MB % 164.03/23.45 % (1623930)Instructions burned: 7 (million) % 164.03/23.45 % (1623930)------------------------------ % 164.03/23.45 % (1623930)------------------------------ % 164.03/23.45 % (1623932)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3898853922:i=28120:bs=on:fsr=off_2780 on theBenchmark for (2780ds/28120Mi) % 164.03/23.45 % (1623924)Instruction limit reached! % 164.03/23.45 % (1623924)------------------------------ % 164.03/23.45 % (1623924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.03/23.45 % (1623924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.03/23.45 % (1623924)CaDiCaL version: 2.1.3 % 164.03/23.45 % (1623924)Termination reason: Instruction limit % 164.03/23.45 % (1623924)Termination phase: Saturation % 164.03/23.45 % (1623924)Time elapsed: 8.545 s % 164.03/23.45 % (1623924)Peak memory usage: 127 MB % 164.03/23.45 % (1623924)Instructions burned: 15851 (million) % 164.03/23.45 % (1623934)fmb+10_1_sil=256000:fmbss=7:random_seed=3333796977:fmbsr=1.6:i=182295_2778 on theBenchmark for (2778ds/182295Mi) % 164.03/23.45 % (1623934)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.03/23.45 % (1623934)Terminated due to inappropriate strategy. % 164.03/23.45 % (1623934)------------------------------ % 164.03/23.45 % (1623934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.03/23.45 % (1623934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.03/23.45 % (1623934)CaDiCaL version: 2.1.3 % 164.03/23.45 % (1623934)Termination reason: Inappropriate % 164.03/23.45 % (1623934)Time elapsed: 0.004 s % 164.03/23.45 % (1623934)Peak memory usage: 10 MB % 164.03/23.45 % (1623934)Instructions burned: 7 (million) % 164.03/23.45 % (1623934)------------------------------ % 164.03/23.45 % (1623934)------------------------------ % 164.03/23.45 % (1623936)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=328908412:i=44625:gsp=on_2778 on theBenchmark for (2778ds/44625Mi) % 178.42/25.41 % (1623936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.42/25.41 % (1623936)Terminated due to inappropriate strategy. % 178.42/25.41 % (1623936)------------------------------ % 178.42/25.41 % (1623936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.42/25.41 % (1623936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.42/25.41 % (1623936)CaDiCaL version: 2.1.3 % 178.42/25.41 % (1623936)Termination reason: Inappropriate % 178.42/25.41 % (1623936)Time elapsed: 0.005 s % 178.42/25.41 % (1623936)Peak memory usage: 11 MB % 178.42/25.41 % (1623936)Instructions burned: 10 (million) % 178.42/25.41 % (1623936)------------------------------ % 178.42/25.41 % (1623936)------------------------------ % 178.42/25.41 % (1623938)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2450357258:i=160505_2778 on theBenchmark for (2778ds/160505Mi) % 178.42/25.41 % (1623938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.42/25.41 % (1623938)Terminated due to inappropriate strategy. % 178.42/25.41 % (1623938)------------------------------ % 178.42/25.41 % (1623938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.42/25.41 % (1623938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.42/25.41 % (1623938)CaDiCaL version: 2.1.3 % 178.42/25.41 % (1623938)Termination reason: Inappropriate % 178.42/25.41 % (1623938)Time elapsed: 0.004 s % 178.42/25.41 % (1623938)Peak memory usage: 10 MB % 178.42/25.41 % (1623938)Instructions burned: 7 (million) % 178.42/25.41 % (1623938)------------------------------ % 178.42/25.41 % (1623938)------------------------------ % 178.42/25.41 % (1623940)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2038101071:fmbsr=1.3:i=225729_2777 on theBenchmark for (2777ds/225729Mi) % 178.42/25.41 % (1623940)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.42/25.41 % (1623940)Terminated due to inappropriate strategy. % 178.42/25.41 % (1623940)------------------------------ % 178.42/25.41 % (1623940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.42/25.41 % (1623940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.42/25.41 % (1623940)CaDiCaL version: 2.1.3 % 178.42/25.41 % (1623940)Termination reason: Inappropriate % 178.42/25.41 % (1623940)Time elapsed: 0.004 s % 178.42/25.41 % (1623940)Peak memory usage: 10 MB % 178.42/25.41 % (1623940)Instructions burned: 7 (million) % 178.42/25.41 % (1623940)------------------------------ % 178.42/25.41 % (1623940)------------------------------ % 178.42/25.41 % (1623922)Instruction limit reached! % 178.42/25.41 % (1623922)------------------------------ % 178.42/25.41 % (1623922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.42/25.41 % (1623922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.42/25.41 % (1623922)CaDiCaL version: 2.1.3 % 178.42/25.41 % (1623922)Termination reason: Instruction limit % 178.42/25.41 % (1623922)Termination phase: Saturation % 178.42/25.41 % (1623922)Time elapsed: 8.694 s % 178.42/25.41 % (1623922)Peak memory usage: 74 MB % 178.42/25.41 % (1623922)Instructions burned: 14136 (million) % 178.42/25.41 % (1623942)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3457103030:fmbsr=2:i=185024:ins=7_2777 on theBenchmark for (2777ds/185024Mi) % 178.42/25.41 % (1623942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.42/25.41 % (1623942)Terminated due to inappropriate strategy. % 178.42/25.41 % (1623942)------------------------------ % 178.42/25.41 % (1623942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.42/25.41 % (1623942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.42/25.41 % (1623942)CaDiCaL version: 2.1.3 % 178.42/25.41 % (1623942)Termination reason: Inappropriate % 178.42/25.41 % (1623942)Time elapsed: 0.004 s % 178.42/25.41 % (1623942)Peak memory usage: 10 MB % 178.42/25.41 % (1623942)Instructions burned: 7 (million) % 178.42/25.41 % (1623942)------------------------------ % 178.42/25.41 % (1623942)------------------------------ % 178.42/25.41 % (1623943)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2851010839:rtra=on_2777 on theBenchmark for (2777ds/0Mi) % 178.42/25.41 % (1623943)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 178.42/25.41 % (1623943)Terminated due to inappropriate strategy. % 178.42/25.41 % (1623943)------------------------------ % 178.42/25.41 % (1623943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 178.42/25.41 % (1623943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.26/28.91 % (1623943)CaDiCaL version: 2.1.3 % 203.26/28.91 % (1623943)Termination reason: Inappropriate % 203.26/28.91 % (1623943)Time elapsed: 0.005 s % 203.26/28.91 % (1623943)Peak memory usage: 11 MB % 203.26/28.91 % (1623943)Instructions burned: 9 (million) % 203.26/28.91 % (1623945)% WARNING: option uhcvi not known. % 203.26/28.91 % (1623943)------------------------------ % 203.26/28.91 % (1623943)------------------------------ % 203.26/28.91 % (1623945)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=994785629:i=271062:add=off:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/271062Mi) % 203.26/28.91 % (1623947)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=162281912:i=176048:add=on:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/176048Mi) % 203.26/28.91 % (1623728)Instruction limit reached! % 203.26/28.91 % (1623728)------------------------------ % 203.26/28.91 % (1623728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.26/28.91 % (1623728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.26/28.91 % (1623728)CaDiCaL version: 2.1.3 % 203.26/28.91 % (1623728)Termination reason: Instruction limit % 203.26/28.91 % (1623728)Termination phase: Saturation % 203.26/28.91 % (1623728)Time elapsed: 17.859 s % 203.26/28.91 % (1623728)Peak memory usage: 209 MB % 203.26/28.91 % (1623728)Instructions burned: 29341 (million) % 203.26/28.91 % (1623950)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3240838056:i=206:fgj=on:rtra=on_2776 on theBenchmark for (2776ds/206Mi) % 203.26/28.91 % (1623950)Instruction limit reached! % 203.26/28.91 % (1623950)------------------------------ % 203.26/28.91 % (1623950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.26/28.91 % (1623950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.26/28.91 % (1623950)CaDiCaL version: 2.1.3 % 203.26/28.91 % (1623950)Termination reason: Instruction limit % 203.26/28.91 % (1623950)Termination phase: Saturation % 203.26/28.91 % (1623950)Time elapsed: 0.135 s % 203.26/28.91 % (1623950)Peak memory usage: 14 MB % 203.26/28.91 % (1623950)Instructions burned: 207 (million) % 203.26/28.91 % (1623952)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3660596619:i=232:rtra=on_2774 on theBenchmark for (2774ds/232Mi) % 203.26/28.91 % (1623952)Instruction limit reached! % 203.26/28.91 % (1623952)------------------------------ % 203.26/28.91 % (1623952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.26/28.91 % (1623952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.26/28.91 % (1623952)CaDiCaL version: 2.1.3 % 203.26/28.91 % (1623952)Termination reason: Instruction limit % 203.26/28.91 % (1623952)Termination phase: Saturation % 203.26/28.91 % (1623952)Time elapsed: 0.149 s % 203.26/28.91 % (1623952)Peak memory usage: 14 MB % 203.26/28.91 % (1623952)Instructions burned: 232 (million) % 203.26/28.91 % (1623954)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1133242198:i=262:rtra=on_2773 on theBenchmark for (2773ds/262Mi) % 203.26/28.91 % (1623954)Instruction limit reached! % 203.26/28.91 % (1623954)------------------------------ % 203.26/28.91 % (1623954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.26/28.91 % (1623954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.26/28.91 % (1623954)CaDiCaL version: 2.1.3 % 203.26/28.91 % (1623954)Termination reason: Instruction limit % 203.26/28.91 % (1623954)Termination phase: Saturation % 203.26/28.91 % (1623954)Time elapsed: 0.165 s % 203.26/28.91 % (1623954)Peak memory usage: 15 MB % 203.26/28.91 % (1623954)Instructions burned: 262 (million) % 203.26/28.91 % (1623956)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2480087595:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2771 on theBenchmark for (2771ds/318Mi) % 203.26/28.91 % (1623956)Instruction limit reached! % 203.26/28.91 % (1623956)------------------------------ % 203.26/28.91 % (1623956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 203.26/28.91 % (1623956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.26/28.91 % (1623956)CaDiCaL version: 2.1.3 % 203.26/28.91 % (1623956)Termination reason: Instruction limit % 203.26/28.91 % (1623956)Termination phase: Saturation % 203.26/28.91 % (1623956)Time elapsed: 0.224 s % 203.26/28.91 % (1623956)Peak memory usage: 16 MB % 203.26/28.91 % (1623956)Instructions burned: 318 (million) % 203.26/28.91 % (1623958)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=478436008:i=1428:nm=2:rtra=on_2768 on theBenchmark for (2768ds/1428Mi) % 235.20/33.46 % (1623958)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.20/33.46 % (1623958)Terminated due to inappropriate strategy. % 235.20/33.46 % (1623958)------------------------------ % 235.20/33.46 % (1623958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.20/33.46 % (1623958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.20/33.46 % (1623958)CaDiCaL version: 2.1.3 % 235.20/33.46 % (1623958)Termination reason: Inappropriate % 235.20/33.46 % (1623958)Time elapsed: 0.005 s % 235.20/33.46 % (1623958)Peak memory usage: 10 MB % 235.20/33.46 % (1623958)Instructions burned: 8 (million) % 235.20/33.46 % (1623958)------------------------------ % 235.20/33.46 % (1623958)------------------------------ % 235.20/33.46 % (1623960)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4002824913:i=262:bd=preordered:rtra=on:fsd=on_2768 on theBenchmark for (2768ds/262Mi) % 235.20/33.46 % (1623960)Instruction limit reached! % 235.20/33.46 % (1623960)------------------------------ % 235.20/33.46 % (1623960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.20/33.46 % (1623960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.20/33.46 % (1623960)CaDiCaL version: 2.1.3 % 235.20/33.46 % (1623960)Termination reason: Instruction limit % 235.20/33.46 % (1623960)Termination phase: Saturation % 235.20/33.46 % (1623960)Time elapsed: 0.177 s % 235.20/33.46 % (1623960)Peak memory usage: 14 MB % 235.20/33.46 % (1623960)Instructions burned: 262 (million) % 235.20/33.46 % (1623962)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1063871254:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2766 on theBenchmark for (2766ds/1368Mi) % 235.20/33.46 % (1623962)Instruction limit reached! % 235.20/33.46 % (1623962)------------------------------ % 235.20/33.46 % (1623962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.20/33.46 % (1623962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.20/33.46 % (1623962)CaDiCaL version: 2.1.3 % 235.20/33.46 % (1623962)Termination reason: Instruction limit % 235.20/33.46 % (1623962)Termination phase: Saturation % 235.20/33.46 % (1623962)Time elapsed: 0.848 s % 235.20/33.46 % (1623962)Peak memory usage: 27 MB % 235.20/33.46 % (1623962)Instructions burned: 1369 (million) % 235.20/33.46 % (1623964)ott-21_1_sil=16000:si=on:fs=off:random_seed=1163170824:i=360:av=off:fsr=off:rtra=on_2757 on theBenchmark for (2757ds/360Mi) % 235.20/33.46 % (1623964)Instruction limit reached! % 235.20/33.46 % (1623964)------------------------------ % 235.20/33.46 % (1623964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.20/33.46 % (1623964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.20/33.46 % (1623964)CaDiCaL version: 2.1.3 % 235.20/33.46 % (1623964)Termination reason: Instruction limit % 235.20/33.46 % (1623964)Termination phase: Saturation % 235.20/33.46 % (1623964)Time elapsed: 0.166 s % 235.20/33.46 % (1623964)Peak memory usage: 13 MB % 235.20/33.46 % (1623964)Instructions burned: 361 (million) % 235.20/33.46 % (1623966)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4276146105:i=954:bd=all:rtra=on_2756 on theBenchmark for (2756ds/954Mi) % 235.20/33.46 % (1623966)Instruction limit reached! % 235.20/33.46 % (1623966)------------------------------ % 235.20/33.46 % (1623966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.20/33.46 % (1623966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.20/33.46 % (1623966)CaDiCaL version: 2.1.3 % 235.20/33.46 % (1623966)Termination reason: Instruction limit % 235.20/33.46 % (1623966)Termination phase: Saturation % 235.20/33.46 % (1623966)Time elapsed: 0.653 s % 235.20/33.46 % (1623966)Peak memory usage: 16 MB % 235.20/33.46 % (1623966)Instructions burned: 954 (million) % 235.20/33.46 % (1623968)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2059871231:fmbsr=1.3:i=1730:ins=25:rtra=on_2749 on theBenchmark for (2749ds/1730Mi) % 235.20/33.46 % (1623968)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 235.20/33.46 % (1623968)Terminated due to inappropriate strategy. % 235.20/33.46 % (1623968)------------------------------ % 235.20/33.46 % (1623968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.20/33.46 % (1623968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.20/33.46 % (1623968)CaDiCaL version: 2.1.3 % 235.20/33.46 % (1623968)Termination reason: Inappropriate % 235.20/33.46 % (1623968)Time elapsed: 0.004 s % 266.41/37.82 % (1623968)Peak memory usage: 10 MB % 266.41/37.82 % (1623968)Instructions burned: 6 (million) % 266.41/37.82 % (1623968)------------------------------ % 266.41/37.82 % (1623968)------------------------------ % 266.41/37.82 % (1623970)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2329079085:i=2358:rtra=on_2749 on theBenchmark for (2749ds/2358Mi) % 266.41/37.82 % (1623970)Instruction limit reached! % 266.41/37.82 % (1623970)------------------------------ % 266.41/37.82 % (1623970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.82 % (1623970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.82 % (1623970)CaDiCaL version: 2.1.3 % 266.41/37.82 % (1623970)Termination reason: Instruction limit % 266.41/37.82 % (1623970)Termination phase: Saturation % 266.41/37.82 % (1623970)Time elapsed: 1.494 s % 266.41/37.82 % (1623970)Peak memory usage: 27 MB % 266.41/37.82 % (1623970)Instructions burned: 2359 (million) % 266.41/37.82 % (1623973)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3994642506:i=1778:ins=1:rtra=on_2733 on theBenchmark for (2733ds/1778Mi) % 266.41/37.82 % (1623973)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.41/37.82 % (1623973)Terminated due to inappropriate strategy. % 266.41/37.82 % (1623973)------------------------------ % 266.41/37.82 % (1623973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.82 % (1623973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.82 % (1623973)CaDiCaL version: 2.1.3 % 266.41/37.82 % (1623973)Termination reason: Inappropriate % 266.41/37.82 % (1623973)Time elapsed: 0.004 s % 266.41/37.82 % (1623973)Peak memory usage: 10 MB % 266.41/37.82 % (1623973)Instructions burned: 7 (million) % 266.41/37.82 % (1623973)------------------------------ % 266.41/37.82 % (1623973)------------------------------ % 266.41/37.82 % (1623975)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=412996574:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/1384Mi) % 266.41/37.82 % (1623975)Instruction limit reached! % 266.41/37.82 % (1623975)------------------------------ % 266.41/37.82 % (1623975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.82 % (1623975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.82 % (1623975)CaDiCaL version: 2.1.3 % 266.41/37.82 % (1623975)Termination reason: Instruction limit % 266.41/37.82 % (1623975)Termination phase: Saturation % 266.41/37.82 % (1623975)Time elapsed: 0.869 s % 266.41/37.82 % (1623975)Peak memory usage: 27 MB % 266.41/37.82 % (1623975)Instructions burned: 1385 (million) % 266.41/37.82 % (1623977)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3838527752:i=1758:kws=inv_precedence:fsr=off:rtra=on_2724 on theBenchmark for (2724ds/1758Mi) % 266.41/37.82 % (1623977)Instruction limit reached! % 266.41/37.82 % (1623977)------------------------------ % 266.41/37.82 % (1623977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.82 % (1623977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.82 % (1623977)CaDiCaL version: 2.1.3 % 266.41/37.82 % (1623977)Termination reason: Instruction limit % 266.41/37.82 % (1623977)Termination phase: Saturation % 266.41/37.82 % (1623977)Time elapsed: 0.989 s % 266.41/37.82 % (1623977)Peak memory usage: 23 MB % 266.41/37.82 % (1623977)Instructions burned: 1759 (million) % 266.41/37.82 % (1623979)fmb+10_1_sil=64000:si=on:random_seed=53853972:i=44122:nm=2:rtra=on:gsp=on_2714 on theBenchmark for (2714ds/44122Mi) % 266.41/37.82 % (1623979)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 266.41/37.82 % (1623979)Terminated due to inappropriate strategy. % 266.41/37.82 % (1623979)------------------------------ % 266.41/37.82 % (1623979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 266.41/37.82 % (1623979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.41/37.82 % (1623979)CaDiCaL version: 2.1.3 % 266.41/37.82 % (1623979)Termination reason: Inappropriate % 266.41/37.82 % (1623979)Time elapsed: 0.006 s % 266.41/37.82 % (1623979)Peak memory usage: 10 MB % 266.41/37.82 % (1623979)Instructions burned: 10 (million) % 266.41/37.82 % (1623979)------------------------------ % 266.41/37.82 % (1623979)------------------------------ % 266.41/37.82 % (1623981)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=754049325:i=19030:nm=5:rtra=on_2714 on theBenchmark for (2714ds/19030Mi) % 292.69/41.54 % (1623981)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.69/41.54 % (1623981)Terminated due to inappropriate strategy. % 292.69/41.54 % (1623981)------------------------------ % 292.69/41.54 % (1623981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.69/41.54 % (1623981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.69/41.54 % (1623981)CaDiCaL version: 2.1.3 % 292.69/41.54 % (1623981)Termination reason: Inappropriate % 292.69/41.54 % (1623981)Time elapsed: 0.004 s % 292.69/41.54 % (1623981)Peak memory usage: 10 MB % 292.69/41.54 % (1623981)Instructions burned: 7 (million) % 292.69/41.54 % (1623981)------------------------------ % 292.69/41.54 % (1623981)------------------------------ % 292.69/41.54 % (1623983)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2228676465:fmbsr=1.7:i=1840:rtra=on_2713 on theBenchmark for (2713ds/1840Mi) % 292.69/41.54 % (1623983)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.69/41.54 % (1623983)Terminated due to inappropriate strategy. % 292.69/41.54 % (1623983)------------------------------ % 292.69/41.54 % (1623983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.69/41.54 % (1623983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.69/41.54 % (1623983)CaDiCaL version: 2.1.3 % 292.69/41.54 % (1623983)Termination reason: Inappropriate % 292.69/41.54 % (1623983)Time elapsed: 0.004 s % 292.69/41.54 % (1623983)Peak memory usage: 10 MB % 292.69/41.54 % (1623983)Instructions burned: 7 (million) % 292.69/41.54 % (1623983)------------------------------ % 292.69/41.54 % (1623983)------------------------------ % 292.69/41.54 % (1623985)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3670341356:i=10262:rtra=on_2713 on theBenchmark for (2713ds/10262Mi) % 292.69/41.54 % (1623928)Instruction limit reached! % 292.69/41.54 % (1623928)------------------------------ % 292.69/41.54 % (1623928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.69/41.54 % (1623928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.69/41.54 % (1623928)CaDiCaL version: 2.1.3 % 292.69/41.54 % (1623928)Termination reason: Instruction limit % 292.69/41.54 % (1623928)Termination phase: Saturation % 292.69/41.54 % (1623928)Time elapsed: 12.164 s % 292.69/41.54 % (1623928)Peak memory usage: 189 MB % 292.69/41.54 % (1623928)Instructions burned: 53299 (million) % 292.69/41.54 % (1624346)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2085464294:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2678 on theBenchmark for (2678ds/2944Mi) % 292.69/41.54 % (1624346)Instruction limit reached! % 292.69/41.54 % (1624346)------------------------------ % 292.69/41.54 % (1624346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.69/41.54 % (1624346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.69/41.54 % (1624346)CaDiCaL version: 2.1.3 % 292.69/41.54 % (1624346)Termination reason: Instruction limit % 292.69/41.54 % (1624346)Termination phase: Saturation % 292.69/41.54 % (1624346)Time elapsed: 0.934 s % 292.69/41.54 % (1624346)Peak memory usage: 32 MB % 292.69/41.54 % (1624346)Instructions burned: 2945 (million) % 292.69/41.54 % (1624348)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3872933533:i=12648:rtra=on_2668 on theBenchmark for (2668ds/12648Mi) % 292.69/41.54 % (1624348)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.69/41.54 % (1624348)Terminated due to inappropriate strategy. % 292.69/41.54 % (1624348)------------------------------ % 292.69/41.54 % (1624348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 292.69/41.54 % (1624348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 292.69/41.54 % (1624348)CaDiCaL version: 2.1.3 % 292.69/41.54 % (1624348)Termination reason: Inappropriate % 292.69/41.54 % (1624348)Time elapsed: 0.003 s % 292.69/41.54 % (1624348)Peak memory usage: 11 MB % 292.69/41.54 % (1624348)Instructions burned: 9 (million) % 292.69/41.54 % (1624348)------------------------------ % 292.69/41.54 % (1624348)------------------------------ % 292.69/41.54 % (1624350)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3411962273:fmbsr=2.30978:i=4348:rtra=on_2668 on theBenchmark for (2668ds/4348Mi) % 292.69/41.54 % (1624350)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 292.69/41.54 % (1624350)Terminated due to inappropriate strategy. % 292.69/41.54 % (1624350)------------------------------ % 292.69/41.54 % (1624350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (1624350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (1624350)CaDiCaL version: 2.1.3 % 300.48/42.64 % (1624350)Termination reason: Inappropriate % 300.48/42.64 % (1624350)Time elapsed: 0.002 s % 300.48/42.64 % (1624350)Peak memory usage: 10 MB % 300.48/42.64 % (1624350)Instructions burned: 7 (million) % 300.48/42.64 % (1624350)------------------------------ % 300.48/42.64 % (1624350)------------------------------ % 300.48/42.64 % (1624352)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1314498551:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2668 on theBenchmark for (2668ds/1738Mi) % 300.48/42.64 % (1624352)Instruction limit reached! % 300.48/42.64 % (1624352)------------------------------ % 300.48/42.64 % (1624352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (1624352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (1624352)CaDiCaL version: 2.1.3 % 300.48/42.64 % (1624352)Termination reason: Instruction limit % 300.48/42.64 % (1624352)Termination phase: Saturation % 300.48/42.64 % (1624352)Time elapsed: 0.593 s % 300.48/42.64 % (1624352)Peak memory usage: 20 MB % 300.48/42.64 % (1624352)Instructions burned: 1741 (million) % 300.48/42.64 % (1624354)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2368390054:i=10228:av=off:rtra=on_2662 on theBenchmark for (2662ds/10228Mi) % 300.48/42.64 % (1623985)Instruction limit reached! % 300.48/42.64 % (1623985)------------------------------ % 300.48/42.64 % (1623985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (1623985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (1623985)CaDiCaL version: 2.1.3 % 300.48/42.64 % (1623985)Termination reason: Instruction limit % 300.48/42.64 % (1623985)Termination phase: Saturation % 300.48/42.64 % (1623985)Time elapsed: 5.991 s % 300.48/42.64 % (1623985)Peak memory usage: 69 MB % 300.48/42.64 % (1623985)Instructions burned: 10263 (million) % 300.48/42.64 % (1624356)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2115253486:i=108564:rtra=on_2653 on theBenchmark for (2653ds/108564Mi) % 300.48/42.64 % (1624356)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.64 % (1624356)Terminated due to inappropriate strategy. % 300.48/42.64 % (1624356)------------------------------ % 300.48/42.64 % (1624356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (1624356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (1624356)CaDiCaL version: 2.1.3 % 300.48/42.64 % (1624356)Termination reason: Inappropriate % 300.48/42.64 % (1624356)Time elapsed: 0.005 s % 300.48/42.64 % (1624356)Peak memory usage: 11 MB % 300.48/42.64 % (1624356)Instructions burned: 9 (million) % 300.48/42.64 % (1624356)------------------------------ % 300.48/42.64 % (1624356)------------------------------ % 300.48/42.64 % (1624358)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1131667666:i=7024:aac=none:rtra=on_2653 on theBenchmark for (2653ds/7024Mi) % 300.48/42.64 % (1623932)Instruction limit reached! % 300.48/42.64 % (1623932)------------------------------ % 300.48/42.64 % (1623932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (1623932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (1623932)CaDiCaL version: 2.1.3 % 300.48/42.64 % (1623932)Termination reason: Instruction limit % 300.48/42.64 % (1623932)Termination phase: Saturation % 300.48/42.64 % (1623932)Time elapsed: 13.836 s % 300.48/42.64 % (1623932)Peak memory usage: 69 MB % 300.48/42.64 % (1623932)Instructions burned: 28123 (million) % 300.48/42.64 % (1624360)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2397839082:i=7546:rtra=on:amm=off_2641 on theBenchmark for (2641ds/7546Mi) % 300.48/42.64 % (1624354)Instruction limit reached! % 300.48/42.64 % (1624354)------------------------------ % 300.48/42.64 % (1624354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (1624354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (1624354)CaDiCaL version: 2.1.3 % 300.48/42.64 % (1624354)Termination reason: Instruction limit % 300.48/42.64 % (1624354)Termination phase: Saturation % 300.48/42.64 % (1624354)Time elapsed: 3.705 s % 300.48/42.64 % (1624354)Peak memory usage: 57 MB % 300.48/42.64 % (1624354)Instructions burned: 10230 (million) % 300.48/42.64 % (1624362)ott+11_1_sil=16000:si=on:gs=on:random_seed=1480657869:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2625 on theBenchmark fo % 300.48/42.64 Terminated % 300.48/42.64 % Vampire exiting %------------------------------------------------------------------------------