%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW672_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 : n012.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:37 PM UTC 2026 % Result : Timeout 300.60s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW672_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 14:24:04 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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.33/0.65 % (3411457)Will run a generic schedule for satisfiability detection. % 3.33/0.65 % (3411483)% WARNING: option uhcvi not known. % 3.33/0.65 % (3411483)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2023648299:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.33/0.65 % (3411484)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3568338822:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.33/0.65 % (3411482)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3386212239_2999 on theBenchmark for (2999ds/0Mi) % 3.33/0.65 % (3411485)dis+10_1_sil=32000:sp=arity:random_seed=523734361:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.33/0.65 % (3411487)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=750801757:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.33/0.65 % (3411486)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=869098360:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.33/0.65 % (3411488)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3448069171:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.33/0.65 % (3411482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.33/0.65 % (3411482)Terminated due to inappropriate strategy. % 3.33/0.65 % (3411482)------------------------------ % 3.33/0.65 % (3411482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.65 % (3411482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.65 % (3411482)CaDiCaL version: 2.1.3 % 3.33/0.65 % (3411482)Termination reason: Inappropriate % 3.33/0.65 % (3411482)Time elapsed: 0.002 s % 3.33/0.65 % (3411482)Peak memory usage: 11 MB % 3.33/0.65 % (3411482)Instructions burned: 8 (million) % 3.33/0.65 % (3411482)------------------------------ % 3.33/0.65 % (3411482)------------------------------ % 3.33/0.65 % (3411498)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1770857064:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.33/0.65 % (3411498)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.33/0.65 % (3411498)Terminated due to inappropriate strategy. % 3.33/0.65 % (3411498)------------------------------ % 3.33/0.65 % (3411498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.65 % (3411498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.65 % (3411498)CaDiCaL version: 2.1.3 % 3.33/0.65 % (3411498)Termination reason: Inappropriate % 3.33/0.65 % (3411498)Time elapsed: 0.002 s % 3.33/0.65 % (3411498)Peak memory usage: 11 MB % 3.33/0.65 % (3411498)Instructions burned: 7 (million) % 3.33/0.65 % (3411498)------------------------------ % 3.33/0.65 % (3411498)------------------------------ % 3.33/0.65 % (3411486)Instruction limit reached! % 3.33/0.65 % (3411486)------------------------------ % 3.33/0.65 % (3411486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.65 % (3411486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.65 % (3411486)CaDiCaL version: 2.1.3 % 3.33/0.65 % (3411486)Termination reason: Instruction limit % 3.33/0.65 % (3411486)Termination phase: Saturation % 3.33/0.65 % (3411486)Time elapsed: 0.027 s % 3.33/0.65 % (3411486)Peak memory usage: 12 MB % 3.33/0.65 % (3411486)Instructions burned: 116 (million) % 3.33/0.65 % (3411505)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=695741145:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.33/0.65 % (3411487)Instruction limit reached! % 3.33/0.65 % (3411487)------------------------------ % 3.33/0.65 % (3411487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.65 % (3411487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.65 % (3411487)CaDiCaL version: 2.1.3 % 3.33/0.65 % (3411487)Termination reason: Instruction limit % 3.33/0.65 % (3411487)Termination phase: Saturation % 3.33/0.65 % (3411487)Time elapsed: 0.033 s % 3.33/0.65 % (3411487)Peak memory usage: 12 MB % 3.33/0.65 % (3411487)Instructions burned: 132 (million) % 3.33/0.65 % (3411485)Instruction limit reached! % 3.33/0.65 % (3411485)------------------------------ % 3.33/0.65 % (3411485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.33/0.65 % (3411485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.33/0.65 % (3411485)CaDiCaL version: 2.1.3 % 3.33/0.65 % (3411485)Termination reason: Instruction limit % 4.35/0.84 % (3411485)Termination phase: Saturation % 4.35/0.84 % (3411485)Time elapsed: 0.033 s % 4.35/0.84 % (3411485)Peak memory usage: 12 MB % 4.35/0.84 % (3411485)Instructions burned: 103 (million) % 4.35/0.84 % (3411488)Instruction limit reached! % 4.35/0.84 % (3411488)------------------------------ % 4.35/0.84 % (3411488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.35/0.84 % (3411488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.35/0.84 % (3411488)CaDiCaL version: 2.1.3 % 4.35/0.84 % (3411488)Termination reason: Instruction limit % 4.35/0.84 % (3411488)Termination phase: Saturation % 4.35/0.84 % (3411488)Time elapsed: 0.037 s % 4.35/0.84 % (3411488)Peak memory usage: 12 MB % 4.35/0.84 % (3411488)Instructions burned: 160 (million) % 4.35/0.84 % (3411513)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=243507054:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.35/0.84 % (3411518)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=709448101:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 4.35/0.84 % (3411521)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3570343725:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 4.35/0.84 % (3411517)ott-21_1_sil=16000:fs=off:random_seed=998524378:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.35/0.84 % (3411521)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.35/0.84 % (3411521)Terminated due to inappropriate strategy. % 4.35/0.84 % (3411521)------------------------------ % 4.35/0.84 % (3411521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.35/0.84 % (3411521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.35/0.84 % (3411521)CaDiCaL version: 2.1.3 % 4.35/0.84 % (3411521)Termination reason: Inappropriate % 4.35/0.84 % (3411521)Time elapsed: 0.002 s % 4.35/0.84 % (3411521)Peak memory usage: 10 MB % 4.35/0.84 % (3411521)Instructions burned: 7 (million) % 4.35/0.84 % (3411521)------------------------------ % 4.35/0.84 % (3411521)------------------------------ % 4.35/0.84 % (3411527)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1521074218:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 4.35/0.84 % (3411505)Instruction limit reached! % 4.35/0.84 % (3411505)------------------------------ % 4.35/0.84 % (3411505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.35/0.84 % (3411505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.35/0.84 % (3411505)CaDiCaL version: 2.1.3 % 4.35/0.84 % (3411505)Termination reason: Instruction limit % 4.35/0.84 % (3411505)Termination phase: Saturation % 4.35/0.84 % (3411505)Time elapsed: 0.037 s % 4.35/0.84 % (3411505)Peak memory usage: 12 MB % 4.35/0.84 % (3411505)Instructions burned: 133 (million) % 4.35/0.84 % (3411544)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=249200099:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 4.35/0.84 % (3411544)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 4.35/0.84 % (3411544)Terminated due to inappropriate strategy. % 4.35/0.84 % (3411544)------------------------------ % 4.35/0.84 % (3411544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.35/0.84 % (3411544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.35/0.84 % (3411544)CaDiCaL version: 2.1.3 % 4.35/0.84 % (3411544)Termination reason: Inappropriate % 4.35/0.84 % (3411544)Time elapsed: 0.003 s % 4.35/0.84 % (3411544)Peak memory usage: 10 MB % 4.35/0.84 % (3411544)Instructions burned: 6 (million) % 4.35/0.84 % (3411544)------------------------------ % 4.35/0.84 % (3411544)------------------------------ % 4.35/0.84 % (3411555)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=3939155779: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) % 4.35/0.84 % (3411517)Instruction limit reached! % 4.35/0.84 % (3411517)------------------------------ % 4.35/0.84 % (3411517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.35/0.84 % (3411517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.35/0.84 % (3411517)CaDiCaL version: 2.1.3 % 4.35/0.84 % (3411517)Termination reason: Instruction limit % 4.35/0.84 % (3411517)Termination phase: Saturation % 18.31/2.86 % (3411517)Time elapsed: 0.081 s % 18.31/2.86 % (3411517)Peak memory usage: 13 MB % 18.31/2.86 % (3411517)Instructions burned: 182 (million) % 18.31/2.86 % (3411559)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=980579110:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 18.31/2.86 % (3411518)Instruction limit reached! % 18.31/2.86 % (3411518)------------------------------ % 18.31/2.86 % (3411518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.86 % (3411518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.86 % (3411518)CaDiCaL version: 2.1.3 % 18.31/2.86 % (3411518)Termination reason: Instruction limit % 18.31/2.86 % (3411518)Termination phase: Saturation % 18.31/2.86 % (3411518)Time elapsed: 0.162 s % 18.31/2.86 % (3411518)Peak memory usage: 12 MB % 18.31/2.86 % (3411518)Instructions burned: 477 (million) % 18.31/2.86 % (3411572)fmb+10_1_sil=64000:random_seed=2368260855:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 18.31/2.86 % (3411572)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.31/2.86 % (3411572)Terminated due to inappropriate strategy. % 18.31/2.86 % (3411572)------------------------------ % 18.31/2.86 % (3411572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.86 % (3411572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.86 % (3411572)CaDiCaL version: 2.1.3 % 18.31/2.86 % (3411572)Termination reason: Inappropriate % 18.31/2.86 % (3411572)Time elapsed: 0.002 s % 18.31/2.86 % (3411572)Peak memory usage: 10 MB % 18.31/2.86 % (3411572)Instructions burned: 8 (million) % 18.31/2.86 % (3411572)------------------------------ % 18.31/2.86 % (3411572)------------------------------ % 18.31/2.86 % (3411576)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3006356599:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 18.31/2.86 % (3411576)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.31/2.86 % (3411576)Terminated due to inappropriate strategy. % 18.31/2.86 % (3411576)------------------------------ % 18.31/2.86 % (3411576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.86 % (3411576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.86 % (3411576)CaDiCaL version: 2.1.3 % 18.31/2.86 % (3411576)Termination reason: Inappropriate % 18.31/2.86 % (3411576)Time elapsed: 0.002 s % 18.31/2.86 % (3411576)Peak memory usage: 10 MB % 18.31/2.86 % (3411576)Instructions burned: 6 (million) % 18.31/2.86 % (3411576)------------------------------ % 18.31/2.86 % (3411576)------------------------------ % 18.31/2.86 % (3411579)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4218491629:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 18.31/2.86 % (3411579)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 18.31/2.86 % (3411579)Terminated due to inappropriate strategy. % 18.31/2.86 % (3411579)------------------------------ % 18.31/2.86 % (3411579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.86 % (3411579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.86 % (3411579)CaDiCaL version: 2.1.3 % 18.31/2.86 % (3411579)Termination reason: Inappropriate % 18.31/2.86 % (3411579)Time elapsed: 0.004 s % 18.31/2.86 % (3411579)Peak memory usage: 10 MB % 18.31/2.86 % (3411579)Instructions burned: 6 (million) % 18.31/2.86 % (3411579)------------------------------ % 18.31/2.86 % (3411579)------------------------------ % 18.31/2.86 % (3411582)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=640852806:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 18.31/2.86 % (3411513)Instruction limit reached! % 18.31/2.86 % (3411513)------------------------------ % 18.31/2.86 % (3411513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.31/2.86 % (3411513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.31/2.86 % (3411513)CaDiCaL version: 2.1.3 % 18.31/2.86 % (3411513)Termination reason: Instruction limit % 18.31/2.86 % (3411513)Termination phase: Saturation % 18.31/2.86 % (3411513)Time elapsed: 0.281 s % 18.31/2.86 % (3411513)Peak memory usage: 14 MB % 18.31/2.86 % (3411513)Instructions burned: 686 (million) % 18.31/2.86 % (3411585)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2521911687:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 18.31/2.86 % (3411555)Instruction limit reached! % 18.31/2.86 % (3411555)------------------------------ % 21.87/3.35 % (3411555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.87/3.35 % (3411555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.35 % (3411555)CaDiCaL version: 2.1.3 % 21.87/3.35 % (3411555)Termination reason: Instruction limit % 21.87/3.35 % (3411555)Termination phase: Saturation % 21.87/3.35 % (3411555)Time elapsed: 0.375 s % 21.87/3.35 % (3411555)Peak memory usage: 18 MB % 21.87/3.35 % (3411555)Instructions burned: 693 (million) % 21.87/3.35 % (3411597)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1009814942:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 21.87/3.35 % (3411597)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.87/3.35 % (3411597)Terminated due to inappropriate strategy. % 21.87/3.35 % (3411597)------------------------------ % 21.87/3.35 % (3411597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.87/3.35 % (3411597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.35 % (3411597)CaDiCaL version: 2.1.3 % 21.87/3.35 % (3411597)Termination reason: Inappropriate % 21.87/3.35 % (3411597)Time elapsed: 0.004 s % 21.87/3.35 % (3411597)Peak memory usage: 11 MB % 21.87/3.35 % (3411597)Instructions burned: 8 (million) % 21.87/3.35 % (3411597)------------------------------ % 21.87/3.35 % (3411597)------------------------------ % 21.87/3.35 % (3411599)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=373805863:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 21.87/3.35 % (3411599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.87/3.35 % (3411599)Terminated due to inappropriate strategy. % 21.87/3.35 % (3411599)------------------------------ % 21.87/3.35 % (3411599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.87/3.35 % (3411599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.35 % (3411599)CaDiCaL version: 2.1.3 % 21.87/3.35 % (3411599)Termination reason: Inappropriate % 21.87/3.35 % (3411599)Time elapsed: 0.004 s % 21.87/3.35 % (3411599)Peak memory usage: 11 MB % 21.87/3.35 % (3411599)Instructions burned: 6 (million) % 21.87/3.35 % (3411599)------------------------------ % 21.87/3.35 % (3411599)------------------------------ % 21.87/3.35 % (3411601)ott-2_1_sil=16000:newcnf=on:random_seed=2692191250:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 21.87/3.35 % (3411559)Instruction limit reached! % 21.87/3.35 % (3411559)------------------------------ % 21.87/3.35 % (3411559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.87/3.35 % (3411559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.35 % (3411559)CaDiCaL version: 2.1.3 % 21.87/3.35 % (3411559)Termination reason: Instruction limit % 21.87/3.35 % (3411559)Termination phase: Saturation % 21.87/3.35 % (3411559)Time elapsed: 0.422 s % 21.87/3.35 % (3411559)Peak memory usage: 17 MB % 21.87/3.35 % (3411559)Instructions burned: 880 (million) % 21.87/3.35 % (3411603)ott+10_1_sil=32000:tgt=ground:random_seed=1012372900:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 21.87/3.35 % (3411527)Instruction limit reached! % 21.87/3.35 % (3411527)------------------------------ % 21.87/3.35 % (3411527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.87/3.35 % (3411527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.35 % (3411527)CaDiCaL version: 2.1.3 % 21.87/3.35 % (3411527)Termination reason: Instruction limit % 21.87/3.35 % (3411527)Termination phase: Saturation % 21.87/3.35 % (3411527)Time elapsed: 0.590 s % 21.87/3.35 % (3411527)Peak memory usage: 21 MB % 21.87/3.35 % (3411527)Instructions burned: 1179 (million) % 21.87/3.35 % (3411608)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2006453418:i=54282_2993 on theBenchmark for (2993ds/54282Mi) % 21.87/3.35 % (3411608)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 21.87/3.35 % (3411608)Terminated due to inappropriate strategy. % 21.87/3.35 % (3411608)------------------------------ % 21.87/3.35 % (3411608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.87/3.35 % (3411608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.87/3.35 % (3411608)CaDiCaL version: 2.1.3 % 21.87/3.35 % (3411608)Termination reason: Inappropriate % 21.87/3.35 % (3411608)Time elapsed: 0.003 s % 21.87/3.35 % (3411608)Peak memory usage: 11 MB % 21.87/3.35 % (3411608)Instructions burned: 8 (million) % 77.84/11.23 % (3411608)------------------------------ % 77.84/11.23 % (3411608)------------------------------ % 77.84/11.23 % (3411612)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4013505506:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi) % 77.84/11.23 % (3411601)Instruction limit reached! % 77.84/11.23 % (3411601)------------------------------ % 77.84/11.23 % (3411601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.84/11.23 % (3411601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.84/11.23 % (3411601)CaDiCaL version: 2.1.3 % 77.84/11.23 % (3411601)Termination reason: Instruction limit % 77.84/11.23 % (3411601)Termination phase: Saturation % 77.84/11.23 % (3411601)Time elapsed: 0.296 s % 77.84/11.23 % (3411601)Peak memory usage: 12 MB % 77.84/11.23 % (3411601)Instructions burned: 872 (million) % 77.84/11.23 % (3411621)dis+21_1_sil=32000:sas=cadical:random_seed=2632634681:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi) % 77.84/11.23 % (3411585)Instruction limit reached! % 77.84/11.23 % (3411585)------------------------------ % 77.84/11.23 % (3411585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.84/11.23 % (3411585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.84/11.23 % (3411585)CaDiCaL version: 2.1.3 % 77.84/11.23 % (3411585)Termination reason: Instruction limit % 77.84/11.23 % (3411585)Termination phase: Saturation % 77.84/11.23 % (3411585)Time elapsed: 0.803 s % 77.84/11.23 % (3411585)Peak memory usage: 22 MB % 77.84/11.23 % (3411585)Instructions burned: 1474 (million) % 77.84/11.23 % (3411623)ott+11_1_sil=16000:gs=on:random_seed=2630758580:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 77.84/11.23 % (3411623)Instruction limit reached! % 77.84/11.23 % (3411623)------------------------------ % 77.84/11.23 % (3411623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.84/11.23 % (3411623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.84/11.23 % (3411623)CaDiCaL version: 2.1.3 % 77.84/11.23 % (3411623)Termination reason: Instruction limit % 77.84/11.23 % (3411623)Termination phase: Saturation % 77.84/11.23 % (3411623)Time elapsed: 0.642 s % 77.84/11.23 % (3411623)Peak memory usage: 16 MB % 77.84/11.23 % (3411623)Instructions burned: 2253 (million) % 77.84/11.23 % (3411629)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3311748665:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 77.84/11.23 % (3411629)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 77.84/11.23 % (3411629)Terminated due to inappropriate strategy. % 77.84/11.23 % (3411629)------------------------------ % 77.84/11.23 % (3411629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.84/11.23 % (3411629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.84/11.23 % (3411629)CaDiCaL version: 2.1.3 % 77.84/11.23 % (3411629)Termination reason: Inappropriate % 77.84/11.23 % (3411629)Time elapsed: 0.002 s % 77.84/11.23 % (3411629)Peak memory usage: 11 MB % 77.84/11.23 % (3411629)Instructions burned: 6 (million) % 77.84/11.23 % (3411629)------------------------------ % 77.84/11.23 % (3411629)------------------------------ % 77.84/11.23 % (3411631)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3177505902:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 77.84/11.23 % (3411612)Instruction limit reached! % 77.84/11.23 % (3411612)------------------------------ % 77.84/11.23 % (3411612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.84/11.23 % (3411612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.84/11.23 % (3411612)CaDiCaL version: 2.1.3 % 77.84/11.23 % (3411612)Termination reason: Instruction limit % 77.84/11.23 % (3411612)Termination phase: Saturation % 77.84/11.23 % (3411612)Time elapsed: 1.674 s % 77.84/11.23 % (3411612)Peak memory usage: 32 MB % 77.84/11.23 % (3411612)Instructions burned: 3512 (million) % 77.84/11.23 % (3411637)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3798614014:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 77.84/11.23 % (3411621)Instruction limit reached! % 77.84/11.23 % (3411621)------------------------------ % 77.84/11.23 % (3411621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 77.84/11.23 % (3411621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.84/11.23 % (3411621)CaDiCaL version: 2.1.3 % 77.84/11.23 % (3411621)Termination reason: Instruction limit % 108.64/15.65 % (3411621)Termination phase: Saturation % 108.64/15.65 % (3411621)Time elapsed: 1.832 s % 108.64/15.65 % (3411621)Peak memory usage: 35 MB % 108.64/15.65 % (3411621)Instructions burned: 3775 (million) % 108.64/15.65 % (3411641)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1273506776:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 108.64/15.65 % (3411582)Instruction limit reached! % 108.64/15.65 % (3411582)------------------------------ % 108.64/15.65 % (3411582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.64/15.65 % (3411582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.64/15.65 % (3411582)CaDiCaL version: 2.1.3 % 108.64/15.65 % (3411582)Termination reason: Instruction limit % 108.64/15.65 % (3411582)Termination phase: Saturation % 108.64/15.65 % (3411582)Time elapsed: 2.562 s % 108.64/15.65 % (3411582)Peak memory usage: 35 MB % 108.64/15.65 % (3411582)Instructions burned: 5132 (million) % 108.64/15.65 % (3411643)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=418221631:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 108.64/15.65 % (3411643)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.64/15.65 % (3411643)Terminated due to inappropriate strategy. % 108.64/15.65 % (3411643)------------------------------ % 108.64/15.65 % (3411643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.64/15.65 % (3411643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.64/15.65 % (3411643)CaDiCaL version: 2.1.3 % 108.64/15.65 % (3411643)Termination reason: Inappropriate % 108.64/15.65 % (3411643)Time elapsed: 0.005 s % 108.64/15.65 % (3411643)Peak memory usage: 11 MB % 108.64/15.65 % (3411643)Instructions burned: 9 (million) % 108.64/15.65 % (3411643)------------------------------ % 108.64/15.65 % (3411643)------------------------------ % 108.64/15.65 % (3411645)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=387848877:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi) % 108.64/15.65 % (3411645)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.64/15.65 % (3411645)Terminated due to inappropriate strategy. % 108.64/15.65 % (3411645)------------------------------ % 108.64/15.65 % (3411645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.64/15.65 % (3411645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.64/15.65 % (3411645)CaDiCaL version: 2.1.3 % 108.64/15.65 % (3411645)Termination reason: Inappropriate % 108.64/15.65 % (3411645)Time elapsed: 0.002 s % 108.64/15.65 % (3411645)Peak memory usage: 11 MB % 108.64/15.65 % (3411645)Instructions burned: 6 (million) % 108.64/15.65 % (3411645)------------------------------ % 108.64/15.65 % (3411645)------------------------------ % 108.64/15.65 % (3411647)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=912540087:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 108.64/15.65 % (3411647)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 108.64/15.65 % (3411647)Terminated due to inappropriate strategy. % 108.64/15.65 % (3411647)------------------------------ % 108.64/15.65 % (3411647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.64/15.65 % (3411647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.64/15.65 % (3411647)CaDiCaL version: 2.1.3 % 108.64/15.65 % (3411647)Termination reason: Inappropriate % 108.64/15.65 % (3411647)Time elapsed: 0.002 s % 108.64/15.65 % (3411647)Peak memory usage: 11 MB % 108.64/15.65 % (3411647)Instructions burned: 6 (million) % 108.64/15.65 % (3411647)------------------------------ % 108.64/15.65 % (3411647)------------------------------ % 108.64/15.65 % (3411650)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2858428554:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 108.64/15.65 % (3411603)Instruction limit reached! % 108.64/15.65 % (3411603)------------------------------ % 108.64/15.65 % (3411603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.64/15.65 % (3411603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.64/15.65 % (3411603)CaDiCaL version: 2.1.3 % 108.64/15.65 % (3411603)Termination reason: Instruction limit % 108.64/15.65 % (3411603)Termination phase: Saturation % 108.64/15.65 % (3411603)Time elapsed: 2.580 s % 108.64/15.65 % (3411603)Peak memory usage: 42 MB % 108.64/15.65 % (3411603)Instructions burned: 5115 (million) % 108.64/15.65 % (3411660)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=313593847:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 108.64/15.65 % (3411631)Instruction limit reached! % 109.37/15.73 % (3411631)------------------------------ % 109.37/15.73 % (3411631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.37/15.73 % (3411631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.37/15.73 % (3411631)CaDiCaL version: 2.1.3 % 109.37/15.73 % (3411631)Termination reason: Instruction limit % 109.37/15.73 % (3411631)Termination phase: Saturation % 109.37/15.73 % (3411631)Time elapsed: 1.362 s % 109.37/15.73 % (3411631)Peak memory usage: 13 MB % 109.37/15.73 % (3411631)Instructions burned: 4591 (million) % 109.37/15.73 % (3411664)dis+10_16:1_sil=16000:random_seed=4245753926:i=9155:fsr=off_2967 on theBenchmark for (2967ds/9155Mi) % 109.37/15.73 % (3411641)Instruction limit reached! % 109.37/15.73 % (3411641)------------------------------ % 109.37/15.73 % (3411641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.37/15.73 % (3411641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.37/15.73 % (3411641)CaDiCaL version: 2.1.3 % 109.37/15.73 % (3411641)Termination reason: Instruction limit % 109.37/15.73 % (3411641)Termination phase: Saturation % 109.37/15.73 % (3411641)Time elapsed: 2.366 s % 109.37/15.73 % (3411641)Peak memory usage: 44 MB % 109.37/15.73 % (3411641)Instructions burned: 5211 (million) % 109.37/15.73 % (3411671)ott-3_8_sil=64000:random_seed=947484147:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 109.37/15.73 % (3411664)Instruction limit reached! % 109.37/15.73 % (3411664)------------------------------ % 109.37/15.73 % (3411664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.37/15.73 % (3411664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.37/15.73 % (3411664)CaDiCaL version: 2.1.3 % 109.37/15.73 % (3411664)Termination reason: Instruction limit % 109.37/15.73 % (3411664)Termination phase: Saturation % 109.37/15.73 % (3411664)Time elapsed: 4.309 s % 109.37/15.73 % (3411664)Peak memory usage: 57 MB % 109.37/15.73 % (3411664)Instructions burned: 9155 (million) % 109.37/15.73 % (3411675)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3748642185:fmbsr=2:i=32576_2924 on theBenchmark for (2924ds/32576Mi) % 109.37/15.73 % (3411675)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 109.37/15.73 % (3411675)Terminated due to inappropriate strategy. % 109.37/15.73 % (3411675)------------------------------ % 109.37/15.73 % (3411675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.37/15.73 % (3411675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.37/15.73 % (3411675)CaDiCaL version: 2.1.3 % 109.37/15.73 % (3411675)Termination reason: Inappropriate % 109.37/15.73 % (3411675)Time elapsed: 0.003 s % 109.37/15.73 % (3411675)Peak memory usage: 11 MB % 109.37/15.73 % (3411675)Instructions burned: 8 (million) % 109.37/15.73 % (3411675)------------------------------ % 109.37/15.73 % (3411675)------------------------------ % 109.37/15.73 % (3411677)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3164329181:i=11404_2924 on theBenchmark for (2924ds/11404Mi) % 109.37/15.73 % (3411660)Instruction limit reached! % 109.37/15.73 % (3411660)------------------------------ % 109.37/15.73 % (3411660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.37/15.73 % (3411660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.37/15.73 % (3411660)CaDiCaL version: 2.1.3 % 109.37/15.73 % (3411660)Termination reason: Instruction limit % 109.37/15.73 % (3411660)Termination phase: Saturation % 109.37/15.73 % (3411660)Time elapsed: 4.575 s % 109.37/15.73 % (3411660)Peak memory usage: 79 MB % 109.37/15.73 % (3411660)Instructions burned: 8174 (million) % 109.37/15.73 % (3411679)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2486758602:i=14134_2922 on theBenchmark for (2922ds/14134Mi) % 109.37/15.73 % (3411650)Instruction limit reached! % 109.37/15.73 % (3411650)------------------------------ % 109.37/15.73 % (3411650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.37/15.73 % (3411650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.37/15.73 % (3411650)CaDiCaL version: 2.1.3 % 109.37/15.73 % (3411650)Termination reason: Instruction limit % 109.37/15.73 % (3411650)Termination phase: Saturation % 109.37/15.73 % (3411650)Time elapsed: 6.882 s % 109.37/15.73 % (3411650)Peak memory usage: 17 MB % 109.37/15.73 % (3411650)Instructions burned: 22567 (million) % 109.37/15.73 % (3411687)dis+33_16_sil=32000:sac=on:random_seed=189462345:i=15851:nm=0_2901 on theBenchmark for (2901ds/15851Mi) % 109.37/15.73 % (3411671)Instruction limit reached! % 109.37/15.73 % (3411671)------------------------------ % 109.37/15.73 % (3411671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.03/17.58 % (3411671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/17.58 % (3411671)CaDiCaL version: 2.1.3 % 122.03/17.58 % (3411671)Termination reason: Instruction limit % 122.03/17.58 % (3411671)Termination phase: Saturation % 122.03/17.58 % (3411671)Time elapsed: 5.961 s % 122.03/17.58 % (3411671)Peak memory usage: 17 MB % 122.03/17.58 % (3411671)Instructions burned: 20141 (million) % 122.03/17.58 % (3411689)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=850293264:avsq=on:i=17627:add=on:amm=off_2889 on theBenchmark for (2889ds/17627Mi) % 122.03/17.58 % (3411637)Instruction limit reached! % 122.03/17.58 % (3411637)------------------------------ % 122.03/17.58 % (3411637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.03/17.58 % (3411637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/17.58 % (3411637)CaDiCaL version: 2.1.3 % 122.03/17.58 % (3411637)Termination reason: Instruction limit % 122.03/17.58 % (3411637)Termination phase: Saturation % 122.03/17.58 % (3411637)Time elapsed: 9.865 s % 122.03/17.58 % (3411637)Peak memory usage: 16 MB % 122.03/17.58 % (3411637)Instructions burned: 29343 (million) % 122.03/17.58 % (3411693)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1922922938:s2a=on:i=53295_2877 on theBenchmark for (2877ds/53295Mi) % 122.03/17.58 % (3411677)Instruction limit reached! % 122.03/17.58 % (3411677)------------------------------ % 122.03/17.58 % (3411677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.03/17.58 % (3411677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/17.58 % (3411677)CaDiCaL version: 2.1.3 % 122.03/17.58 % (3411677)Termination reason: Instruction limit % 122.03/17.58 % (3411677)Termination phase: Saturation % 122.03/17.58 % (3411677)Time elapsed: 6.415 s % 122.03/17.58 % (3411677)Peak memory usage: 75 MB % 122.03/17.58 % (3411677)Instructions burned: 11404 (million) % 122.03/17.58 % (3411695)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3871243560:i=26857:ins=20_2859 on theBenchmark for (2859ds/26857Mi) % 122.03/17.58 % (3411695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.03/17.58 % (3411695)Terminated due to inappropriate strategy. % 122.03/17.58 % (3411695)------------------------------ % 122.03/17.59 % (3411695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.03/17.59 % (3411695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/17.59 % (3411695)CaDiCaL version: 2.1.3 % 122.03/17.59 % (3411695)Termination reason: Inappropriate % 122.03/17.59 % (3411695)Time elapsed: 0.002 s % 122.03/17.59 % (3411695)Peak memory usage: 11 MB % 122.03/17.59 % (3411695)Instructions burned: 6 (million) % 122.03/17.59 % (3411695)------------------------------ % 122.03/17.59 % (3411695)------------------------------ % 122.03/17.59 % (3411697)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=604041581:i=28120:bs=on:fsr=off_2859 on theBenchmark for (2859ds/28120Mi) % 122.03/17.59 % (3411679)Instruction limit reached! % 122.03/17.59 % (3411679)------------------------------ % 122.03/17.59 % (3411679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.03/17.59 % (3411679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/17.59 % (3411679)CaDiCaL version: 2.1.3 % 122.03/17.59 % (3411679)Termination reason: Instruction limit % 122.03/17.59 % (3411679)Termination phase: Saturation % 122.03/17.59 % (3411679)Time elapsed: 7.673 s % 122.03/17.59 % (3411679)Peak memory usage: 101 MB % 122.03/17.59 % (3411679)Instructions burned: 14134 (million) % 122.03/17.59 % (3411703)fmb+10_1_sil=256000:fmbss=7:random_seed=155978922:fmbsr=1.6:i=182295_2845 on theBenchmark for (2845ds/182295Mi) % 122.03/17.59 % (3411703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 122.03/17.59 % (3411703)Terminated due to inappropriate strategy. % 122.03/17.59 % (3411703)------------------------------ % 122.03/17.59 % (3411703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.03/17.59 % (3411703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.03/17.59 % (3411703)CaDiCaL version: 2.1.3 % 122.03/17.59 % (3411703)Termination reason: Inappropriate % 122.03/17.59 % (3411703)Time elapsed: 0.002 s % 122.03/17.59 % (3411703)Peak memory usage: 11 MB % 122.03/17.59 % (3411703)Instructions burned: 6 (million) % 122.03/17.59 % (3411703)------------------------------ % 122.03/17.59 % (3411703)------------------------------ % 122.03/17.59 % (3411705)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1249827550:i=44625:gsp=on_2844 on theBenchmark for (2844ds/44625Mi) % 130.18/18.80 % (3411705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.18/18.80 % (3411705)Terminated due to inappropriate strategy. % 130.18/18.80 % (3411705)------------------------------ % 130.18/18.80 % (3411705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.18/18.80 % (3411705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/18.80 % (3411705)CaDiCaL version: 2.1.3 % 130.18/18.80 % (3411705)Termination reason: Inappropriate % 130.18/18.80 % (3411705)Time elapsed: 0.002 s % 130.18/18.80 % (3411705)Peak memory usage: 11 MB % 130.18/18.80 % (3411705)Instructions burned: 7 (million) % 130.18/18.80 % (3411705)------------------------------ % 130.18/18.80 % (3411705)------------------------------ % 130.18/18.80 % (3411707)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3267168261:i=160505_2844 on theBenchmark for (2844ds/160505Mi) % 130.18/18.80 % (3411707)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.18/18.80 % (3411707)Terminated due to inappropriate strategy. % 130.18/18.80 % (3411707)------------------------------ % 130.18/18.80 % (3411707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.18/18.80 % (3411707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/18.80 % (3411707)CaDiCaL version: 2.1.3 % 130.18/18.80 % (3411707)Termination reason: Inappropriate % 130.18/18.80 % (3411707)Time elapsed: 0.002 s % 130.18/18.80 % (3411707)Peak memory usage: 11 MB % 130.18/18.80 % (3411707)Instructions burned: 6 (million) % 130.18/18.80 % (3411707)------------------------------ % 130.18/18.80 % (3411707)------------------------------ % 130.18/18.80 % (3411709)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2330380839:fmbsr=1.3:i=225729_2844 on theBenchmark for (2844ds/225729Mi) % 130.18/18.80 % (3411709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.18/18.80 % (3411709)Terminated due to inappropriate strategy. % 130.18/18.80 % (3411709)------------------------------ % 130.18/18.80 % (3411709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.18/18.80 % (3411709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/18.80 % (3411709)CaDiCaL version: 2.1.3 % 130.18/18.80 % (3411709)Termination reason: Inappropriate % 130.18/18.80 % (3411709)Time elapsed: 0.002 s % 130.18/18.80 % (3411709)Peak memory usage: 11 MB % 130.18/18.80 % (3411709)Instructions burned: 6 (million) % 130.18/18.80 % (3411709)------------------------------ % 130.18/18.80 % (3411709)------------------------------ % 130.18/18.80 % (3411711)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2085893631:fmbsr=2:i=185024:ins=7_2844 on theBenchmark for (2844ds/185024Mi) % 130.18/18.80 % (3411711)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.18/18.80 % (3411711)Terminated due to inappropriate strategy. % 130.18/18.80 % (3411711)------------------------------ % 130.18/18.80 % (3411711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.18/18.80 % (3411711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/18.80 % (3411711)CaDiCaL version: 2.1.3 % 130.18/18.80 % (3411711)Termination reason: Inappropriate % 130.18/18.80 % (3411711)Time elapsed: 0.003 s % 130.18/18.80 % (3411711)Peak memory usage: 11 MB % 130.18/18.80 % (3411711)Instructions burned: 6 (million) % 130.18/18.80 % (3411711)------------------------------ % 130.18/18.80 % (3411711)------------------------------ % 130.18/18.80 % (3411713)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3997898073:rtra=on_2844 on theBenchmark for (2844ds/0Mi) % 130.18/18.80 % (3411713)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 130.18/18.80 % (3411713)Terminated due to inappropriate strategy. % 130.18/18.80 % (3411713)------------------------------ % 130.18/18.80 % (3411713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 130.18/18.80 % (3411713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.18/18.80 % (3411713)CaDiCaL version: 2.1.3 % 130.18/18.80 % (3411713)Termination reason: Inappropriate % 130.18/18.80 % (3411713)Time elapsed: 0.003 s % 130.18/18.80 % (3411713)Peak memory usage: 11 MB % 130.18/18.80 % (3411713)Instructions burned: 9 (million) % 130.18/18.80 % (3411713)------------------------------ % 130.18/18.80 % (3411713)------------------------------ % 130.18/18.80 % (3411715)% WARNING: option uhcvi not known. % 130.18/18.80 % (3411715)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3185084452:i=271062:add=off:rtra=on:rawr=on_2844 on theBenchmark for (2844ds/271062Mi) % 152.36/21.80 % (3411689)Instruction limit reached! % 152.36/21.80 % (3411689)------------------------------ % 152.36/21.80 % (3411689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.36/21.80 % (3411689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.36/21.80 % (3411689)CaDiCaL version: 2.1.3 % 152.36/21.80 % (3411689)Termination reason: Instruction limit % 152.36/21.80 % (3411689)Termination phase: Saturation % 152.36/21.80 % (3411689)Time elapsed: 5.176 s % 152.36/21.80 % (3411689)Peak memory usage: 16 MB % 152.36/21.80 % (3411689)Instructions burned: 17628 (million) % 152.36/21.80 % (3411721)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=261284152:i=176048:add=on:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/176048Mi) % 152.36/21.80 % (3411687)Instruction limit reached! % 152.36/21.80 % (3411687)------------------------------ % 152.36/21.80 % (3411687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.36/21.80 % (3411687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.36/21.80 % (3411687)CaDiCaL version: 2.1.3 % 152.36/21.80 % (3411687)Termination reason: Instruction limit % 152.36/21.80 % (3411687)Termination phase: Saturation % 152.36/21.80 % (3411687)Time elapsed: 7.170 s % 152.36/21.80 % (3411687)Peak memory usage: 131 MB % 152.36/21.80 % (3411687)Instructions burned: 15852 (million) % 152.36/21.80 % (3411737)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2734366818:i=206:fgj=on:rtra=on_2829 on theBenchmark for (2829ds/206Mi) % 152.36/21.80 % (3411737)Instruction limit reached! % 152.36/21.80 % (3411737)------------------------------ % 152.36/21.80 % (3411737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.36/21.80 % (3411737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.36/21.80 % (3411737)CaDiCaL version: 2.1.3 % 152.36/21.80 % (3411737)Termination reason: Instruction limit % 152.36/21.80 % (3411737)Termination phase: Saturation % 152.36/21.80 % (3411737)Time elapsed: 0.113 s % 152.36/21.80 % (3411737)Peak memory usage: 14 MB % 152.36/21.80 % (3411737)Instructions burned: 206 (million) % 152.36/21.80 % (3411739)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=950322723:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi) % 152.36/21.80 % (3411739)Instruction limit reached! % 152.36/21.80 % (3411739)------------------------------ % 152.36/21.80 % (3411739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.36/21.80 % (3411739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.36/21.80 % (3411739)CaDiCaL version: 2.1.3 % 152.36/21.80 % (3411739)Termination reason: Instruction limit % 152.36/21.80 % (3411739)Termination phase: Saturation % 152.36/21.80 % (3411739)Time elapsed: 0.059 s % 152.36/21.80 % (3411739)Peak memory usage: 12 MB % 152.36/21.80 % (3411739)Instructions burned: 235 (million) % 152.36/21.80 % (3411741)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3038790172:i=262:rtra=on_2827 on theBenchmark for (2827ds/262Mi) % 152.36/21.80 % (3411741)Instruction limit reached! % 152.36/21.80 % (3411741)------------------------------ % 152.36/21.80 % (3411741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.36/21.80 % (3411741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.36/21.80 % (3411741)CaDiCaL version: 2.1.3 % 152.36/21.80 % (3411741)Termination reason: Instruction limit % 152.36/21.80 % (3411741)Termination phase: Saturation % 152.36/21.80 % (3411741)Time elapsed: 0.068 s % 152.36/21.80 % (3411741)Peak memory usage: 12 MB % 152.36/21.80 % (3411741)Instructions burned: 262 (million) % 152.36/21.80 % (3411743)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2450631557:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2826 on theBenchmark for (2826ds/318Mi) % 152.36/21.80 % (3411743)Instruction limit reached! % 152.36/21.80 % (3411743)------------------------------ % 152.36/21.80 % (3411743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 152.36/21.80 % (3411743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.36/21.80 % (3411743)CaDiCaL version: 2.1.3 % 152.36/21.80 % (3411743)Termination reason: Instruction limit % 152.36/21.80 % (3411743)Termination phase: Saturation % 152.36/21.80 % (3411743)Time elapsed: 0.103 s % 152.36/21.80 % (3411743)Peak memory usage: 12 MB % 152.36/21.80 % (3411743)Instructions burned: 318 (million) % 152.36/21.80 % (3411745)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1579024494:i=1428:nm=2:rtra=on_2825 on theBenchmark for (2825ds/1428Mi) % 165.80/23.73 % (3411745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.80/23.73 % (3411745)Terminated due to inappropriate strategy. % 165.80/23.73 % (3411745)------------------------------ % 165.80/23.73 % (3411745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.80/23.73 % (3411745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.80/23.73 % (3411745)CaDiCaL version: 2.1.3 % 165.80/23.73 % (3411745)Termination reason: Inappropriate % 165.80/23.73 % (3411745)Time elapsed: 0.003 s % 165.80/23.73 % (3411745)Peak memory usage: 11 MB % 165.80/23.73 % (3411745)Instructions burned: 7 (million) % 165.80/23.73 % (3411745)------------------------------ % 165.80/23.73 % (3411745)------------------------------ % 165.80/23.73 % (3411747)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1037224344:i=262:bd=preordered:rtra=on:fsd=on_2825 on theBenchmark for (2825ds/262Mi) % 165.80/23.73 % (3411747)Instruction limit reached! % 165.80/23.73 % (3411747)------------------------------ % 165.80/23.73 % (3411747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.80/23.73 % (3411747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.80/23.73 % (3411747)CaDiCaL version: 2.1.3 % 165.80/23.73 % (3411747)Termination reason: Instruction limit % 165.80/23.73 % (3411747)Termination phase: Saturation % 165.80/23.73 % (3411747)Time elapsed: 0.133 s % 165.80/23.73 % (3411747)Peak memory usage: 13 MB % 165.80/23.73 % (3411747)Instructions burned: 262 (million) % 165.80/23.73 % (3411749)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=1723954062:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/1368Mi) % 165.80/23.73 % (3411749)Instruction limit reached! % 165.80/23.73 % (3411749)------------------------------ % 165.80/23.73 % (3411749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.80/23.73 % (3411749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.80/23.73 % (3411749)CaDiCaL version: 2.1.3 % 165.80/23.73 % (3411749)Termination reason: Instruction limit % 165.80/23.73 % (3411749)Termination phase: Saturation % 165.80/23.73 % (3411749)Time elapsed: 0.506 s % 165.80/23.73 % (3411749)Peak memory usage: 19 MB % 165.80/23.73 % (3411749)Instructions burned: 1369 (million) % 165.80/23.73 % (3411751)ott-21_1_sil=16000:si=on:fs=off:random_seed=1820079118:i=360:av=off:fsr=off:rtra=on_2818 on theBenchmark for (2818ds/360Mi) % 165.80/23.73 % (3411751)Instruction limit reached! % 165.80/23.73 % (3411751)------------------------------ % 165.80/23.73 % (3411751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.80/23.73 % (3411751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.80/23.73 % (3411751)CaDiCaL version: 2.1.3 % 165.80/23.73 % (3411751)Termination reason: Instruction limit % 165.80/23.73 % (3411751)Termination phase: Saturation % 165.80/23.73 % (3411751)Time elapsed: 0.111 s % 165.80/23.73 % (3411751)Peak memory usage: 14 MB % 165.80/23.73 % (3411751)Instructions burned: 363 (million) % 165.80/23.73 % (3411753)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=590557760:i=954:bd=all:rtra=on_2817 on theBenchmark for (2817ds/954Mi) % 165.80/23.73 % (3411753)Instruction limit reached! % 165.80/23.73 % (3411753)------------------------------ % 165.80/23.73 % (3411753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.80/23.73 % (3411753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.80/23.73 % (3411753)CaDiCaL version: 2.1.3 % 165.80/23.73 % (3411753)Termination reason: Instruction limit % 165.80/23.73 % (3411753)Termination phase: Saturation % 165.80/23.73 % (3411753)Time elapsed: 0.357 s % 165.80/23.73 % (3411753)Peak memory usage: 13 MB % 165.80/23.73 % (3411753)Instructions burned: 954 (million) % 165.80/23.73 % (3411755)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1775253767:fmbsr=1.3:i=1730:ins=25:rtra=on_2813 on theBenchmark for (2813ds/1730Mi) % 165.80/23.73 % (3411755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 165.80/23.73 % (3411755)Terminated due to inappropriate strategy. % 165.80/23.73 % (3411755)------------------------------ % 165.80/23.73 % (3411755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.80/23.73 % (3411755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.80/23.73 % (3411755)CaDiCaL version: 2.1.3 % 165.80/23.73 % (3411755)Termination reason: Inappropriate % 165.80/23.73 % (3411755)Time elapsed: 0.005 s % 204.02/29.17 % (3411755)Peak memory usage: 10 MB % 204.02/29.17 % (3411755)Instructions burned: 8 (million) % 204.02/29.17 % (3411755)------------------------------ % 204.02/29.17 % (3411755)------------------------------ % 204.02/29.17 % (3411757)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3107007496:i=2358:rtra=on_2813 on theBenchmark for (2813ds/2358Mi) % 204.02/29.17 % (3411757)Instruction limit reached! % 204.02/29.17 % (3411757)------------------------------ % 204.02/29.17 % (3411757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.02/29.17 % (3411757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.02/29.17 % (3411757)CaDiCaL version: 2.1.3 % 204.02/29.17 % (3411757)Termination reason: Instruction limit % 204.02/29.17 % (3411757)Termination phase: Saturation % 204.02/29.17 % (3411757)Time elapsed: 1.133 s % 204.02/29.17 % (3411757)Peak memory usage: 26 MB % 204.02/29.17 % (3411757)Instructions burned: 2361 (million) % 204.02/29.17 % (3411761)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=900339305:i=1778:ins=1:rtra=on_2801 on theBenchmark for (2801ds/1778Mi) % 204.02/29.17 % (3411761)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.02/29.17 % (3411761)Terminated due to inappropriate strategy. % 204.02/29.17 % (3411761)------------------------------ % 204.02/29.17 % (3411761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.02/29.17 % (3411761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.02/29.17 % (3411761)CaDiCaL version: 2.1.3 % 204.02/29.17 % (3411761)Termination reason: Inappropriate % 204.02/29.17 % (3411761)Time elapsed: 0.002 s % 204.02/29.17 % (3411761)Peak memory usage: 10 MB % 204.02/29.17 % (3411761)Instructions burned: 7 (million) % 204.02/29.17 % (3411761)------------------------------ % 204.02/29.17 % (3411761)------------------------------ % 204.02/29.17 % (3411763)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=1059947212:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2801 on theBenchmark for (2801ds/1384Mi) % 204.02/29.17 % (3411763)Instruction limit reached! % 204.02/29.17 % (3411763)------------------------------ % 204.02/29.17 % (3411763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.02/29.17 % (3411763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.02/29.17 % (3411763)CaDiCaL version: 2.1.3 % 204.02/29.17 % (3411763)Termination reason: Instruction limit % 204.02/29.17 % (3411763)Termination phase: Saturation % 204.02/29.17 % (3411763)Time elapsed: 0.874 s % 204.02/29.17 % (3411763)Peak memory usage: 27 MB % 204.02/29.17 % (3411763)Instructions burned: 1386 (million) % 204.02/29.17 % (3411765)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2969195179:i=1758:kws=inv_precedence:fsr=off:rtra=on_2792 on theBenchmark for (2792ds/1758Mi) % 204.02/29.17 % (3411765)Instruction limit reached! % 204.02/29.17 % (3411765)------------------------------ % 204.02/29.17 % (3411765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.02/29.17 % (3411765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.02/29.17 % (3411765)CaDiCaL version: 2.1.3 % 204.02/29.17 % (3411765)Termination reason: Instruction limit % 204.02/29.17 % (3411765)Termination phase: Saturation % 204.02/29.17 % (3411765)Time elapsed: 0.870 s % 204.02/29.17 % (3411765)Peak memory usage: 23 MB % 204.02/29.17 % (3411765)Instructions burned: 1759 (million) % 204.02/29.17 % (3411767)fmb+10_1_sil=64000:si=on:random_seed=3995759409:i=44122:nm=2:rtra=on:gsp=on_2783 on theBenchmark for (2783ds/44122Mi) % 204.02/29.17 % (3411767)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 204.02/29.17 % (3411767)Terminated due to inappropriate strategy. % 204.02/29.17 % (3411767)------------------------------ % 204.02/29.17 % (3411767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.02/29.17 % (3411767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.02/29.17 % (3411767)CaDiCaL version: 2.1.3 % 204.02/29.17 % (3411767)Termination reason: Inappropriate % 204.02/29.17 % (3411767)Time elapsed: 0.004 s % 204.02/29.17 % (3411767)Peak memory usage: 10 MB % 204.02/29.17 % (3411767)Instructions burned: 8 (million) % 204.02/29.17 % (3411767)------------------------------ % 204.02/29.17 % (3411767)------------------------------ % 204.02/29.17 % (3411769)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2517876669:i=19030:nm=5:rtra=on_2783 on theBenchmark for (2783ds/19030Mi) % 230.03/32.81 % (3411769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.03/32.81 % (3411769)Terminated due to inappropriate strategy. % 230.03/32.81 % (3411769)------------------------------ % 230.03/32.81 % (3411769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.03/32.81 % (3411769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/32.81 % (3411769)CaDiCaL version: 2.1.3 % 230.03/32.81 % (3411769)Termination reason: Inappropriate % 230.03/32.81 % (3411769)Time elapsed: 0.004 s % 230.03/32.81 % (3411769)Peak memory usage: 11 MB % 230.03/32.81 % (3411769)Instructions burned: 7 (million) % 230.03/32.81 % (3411769)------------------------------ % 230.03/32.81 % (3411769)------------------------------ % 230.03/32.81 % (3411771)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=655702659:fmbsr=1.7:i=1840:rtra=on_2783 on theBenchmark for (2783ds/1840Mi) % 230.03/32.81 % (3411771)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.03/32.81 % (3411771)Terminated due to inappropriate strategy. % 230.03/32.81 % (3411771)------------------------------ % 230.03/32.81 % (3411771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.03/32.81 % (3411771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/32.81 % (3411771)CaDiCaL version: 2.1.3 % 230.03/32.81 % (3411771)Termination reason: Inappropriate % 230.03/32.81 % (3411771)Time elapsed: 0.004 s % 230.03/32.81 % (3411771)Peak memory usage: 10 MB % 230.03/32.81 % (3411771)Instructions burned: 7 (million) % 230.03/32.81 % (3411771)------------------------------ % 230.03/32.81 % (3411771)------------------------------ % 230.03/32.81 % (3411773)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4240526876:i=10262:rtra=on_2783 on theBenchmark for (2783ds/10262Mi) % 230.03/32.81 % (3411697)Instruction limit reached! % 230.03/32.81 % (3411697)------------------------------ % 230.03/32.81 % (3411697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.03/32.81 % (3411697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/32.81 % (3411697)CaDiCaL version: 2.1.3 % 230.03/32.81 % (3411697)Termination reason: Instruction limit % 230.03/32.81 % (3411697)Termination phase: Saturation % 230.03/32.81 % (3411697)Time elapsed: 7.805 s % 230.03/32.81 % (3411697)Peak memory usage: 15 MB % 230.03/32.81 % (3411697)Instructions burned: 28123 (million) % 230.03/32.81 % (3411775)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2954539505:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2781 on theBenchmark for (2781ds/2944Mi) % 230.03/32.81 % (3411775)Instruction limit reached! % 230.03/32.81 % (3411775)------------------------------ % 230.03/32.81 % (3411775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.03/32.81 % (3411775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/32.81 % (3411775)CaDiCaL version: 2.1.3 % 230.03/32.81 % (3411775)Termination reason: Instruction limit % 230.03/32.81 % (3411775)Termination phase: Saturation % 230.03/32.81 % (3411775)Time elapsed: 1.700 s % 230.03/32.81 % (3411775)Peak memory usage: 89 MB % 230.03/32.81 % (3411775)Instructions burned: 2944 (million) % 230.03/32.81 % (3411791)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3256149969:i=12648:rtra=on_2764 on theBenchmark for (2764ds/12648Mi) % 230.03/32.81 % (3411791)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.03/32.81 % (3411791)Terminated due to inappropriate strategy. % 230.03/32.81 % (3411791)------------------------------ % 230.03/32.81 % (3411791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 230.03/32.81 % (3411791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.03/32.81 % (3411791)CaDiCaL version: 2.1.3 % 230.03/32.81 % (3411791)Termination reason: Inappropriate % 230.03/32.81 % (3411791)Time elapsed: 0.003 s % 230.03/32.81 % (3411791)Peak memory usage: 11 MB % 230.03/32.81 % (3411791)Instructions burned: 9 (million) % 230.03/32.81 % (3411791)------------------------------ % 230.03/32.81 % (3411791)------------------------------ % 230.03/32.81 % (3411793)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=567760453:fmbsr=2.30978:i=4348:rtra=on_2764 on theBenchmark for (2764ds/4348Mi) % 230.03/32.81 % (3411793)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 230.03/32.81 % (3411793)Terminated due to inappropriate strategy. % 230.03/32.81 % (3411793)------------------------------ % 230.03/32.81 % (3411793)Version: Vampire 5.0Terminated % 300.60/42.84 % Vampire exiting %------------------------------------------------------------------------------