%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW660_2 : TPTP v9.3.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n016.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 296.67s 42.09s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW660_2 : TPTP v9.3.1. Released v6.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 % Computer : n016.cluster.edu % 0.10/0.22 % Model : x86_64 x86_64 % 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.22 % Memory : 8046.5625MB % 0.10/0.22 % OS : Linux 6.8.0-71-generic % 0.10/0.22 % CPULimit : 300 % 0.10/0.22 % WCLimit : 300 % 0.10/0.22 % DateTime : Mon Sep 28 14:29:03 UTC 2026 % 0.10/0.23 % CPUTime : % 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.28 Running first-order model finding % 0.24/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.05/1.17 % (3660617)Will run a generic schedule for satisfiability detection. % 6.05/1.17 % (3660627)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3869930346:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.05/1.17 % (3660623)% WARNING: option uhcvi not known. % 6.05/1.17 % (3660626)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2737295186:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.05/1.17 % (3660623)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3582254948:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.05/1.17 % (3660628)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=111431105:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.05/1.17 % (3660624)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4045224826:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.05/1.17 % (3660622)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2017245004_2999 on theBenchmark for (2999ds/0Mi) % 6.05/1.17 % (3660625)dis+10_1_sil=32000:sp=arity:random_seed=2174154859:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.05/1.17 % (3660622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.05/1.17 % (3660622)Terminated due to inappropriate strategy. % 6.05/1.17 % (3660622)------------------------------ % 6.05/1.17 % (3660622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.05/1.17 % (3660622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.05/1.17 % (3660622)CaDiCaL version: 2.1.3 % 6.05/1.17 % (3660622)Termination reason: Inappropriate % 6.05/1.17 % (3660622)Time elapsed: 0.015 s % 6.05/1.17 % (3660622)Peak memory usage: 10 MB % 6.05/1.17 % (3660622)Instructions burned: 16 (million) % 6.05/1.17 % (3660622)------------------------------ % 6.05/1.17 % (3660622)------------------------------ % 6.05/1.17 % (3660636)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2704468965:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.05/1.17 % (3660627)Instruction limit reached! % 6.05/1.17 % (3660627)------------------------------ % 6.05/1.17 % (3660627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.05/1.17 % (3660627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.05/1.17 % (3660627)CaDiCaL version: 2.1.3 % 6.05/1.17 % (3660627)Termination reason: Instruction limit % 6.05/1.17 % (3660627)Termination phase: Saturation % 6.05/1.17 % (3660627)Time elapsed: 0.071 s % 6.05/1.17 % (3660627)Peak memory usage: 13 MB % 6.05/1.17 % (3660627)Instructions burned: 131 (million) % 6.05/1.17 % (3660636)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.05/1.17 % (3660636)Terminated due to inappropriate strategy. % 6.05/1.17 % (3660636)------------------------------ % 6.05/1.17 % (3660636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.05/1.17 % (3660636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.05/1.17 % (3660636)CaDiCaL version: 2.1.3 % 6.05/1.17 % (3660636)Termination reason: Inappropriate % 6.05/1.17 % (3660636)Time elapsed: 0.013 s % 6.05/1.17 % (3660636)Peak memory usage: 11 MB % 6.05/1.17 % (3660636)Instructions burned: 13 (million) % 6.05/1.17 % (3660636)------------------------------ % 6.05/1.17 % (3660636)------------------------------ % 6.05/1.17 % (3660638)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3597789079:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.05/1.17 % (3660639)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=2443464349:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.05/1.17 % (3660625)Instruction limit reached! % 6.05/1.17 % (3660625)------------------------------ % 6.05/1.17 % (3660625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.05/1.17 % (3660625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.05/1.17 % (3660625)CaDiCaL version: 2.1.3 % 6.05/1.17 % (3660625)Termination reason: Instruction limit % 6.05/1.17 % (3660625)Termination phase: Saturation % 6.05/1.17 % (3660625)Time elapsed: 0.102 s % 6.05/1.17 % (3660625)Peak memory usage: 13 MB % 6.05/1.17 % (3660625)Instructions burned: 104 (million) % 6.05/1.17 % (3660626)Instruction limit reached! % 6.05/1.17 % (3660626)------------------------------ % 6.05/1.17 % (3660626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.55 % (3660626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.55 % (3660626)CaDiCaL version: 2.1.3 % 7.44/1.55 % (3660626)Termination reason: Instruction limit % 7.44/1.55 % (3660626)Termination phase: Saturation % 7.44/1.55 % (3660626)Time elapsed: 0.122 s % 7.44/1.55 % (3660626)Peak memory usage: 13 MB % 7.44/1.55 % (3660626)Instructions burned: 116 (million) % 7.44/1.55 % (3660642)ott-21_1_sil=16000:fs=off:random_seed=1195206017:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.44/1.55 % (3660643)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2773110960:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.44/1.55 % (3660638)Instruction limit reached! % 7.44/1.55 % (3660638)------------------------------ % 7.44/1.55 % (3660638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.55 % (3660638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.55 % (3660638)CaDiCaL version: 2.1.3 % 7.44/1.55 % (3660638)Termination reason: Instruction limit % 7.44/1.55 % (3660638)Termination phase: Saturation % 7.44/1.55 % (3660638)Time elapsed: 0.076 s % 7.44/1.55 % (3660638)Peak memory usage: 13 MB % 7.44/1.55 % (3660638)Instructions burned: 132 (million) % 7.44/1.55 % (3660628)Instruction limit reached! % 7.44/1.55 % (3660628)------------------------------ % 7.44/1.55 % (3660628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.55 % (3660628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.55 % (3660628)CaDiCaL version: 2.1.3 % 7.44/1.55 % (3660628)Termination reason: Instruction limit % 7.44/1.55 % (3660628)Termination phase: Saturation % 7.44/1.55 % (3660628)Time elapsed: 0.169 s % 7.44/1.55 % (3660628)Peak memory usage: 14 MB % 7.44/1.55 % (3660628)Instructions burned: 159 (million) % 7.44/1.55 % (3660646)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3106960888:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.44/1.55 % (3660646)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.44/1.55 % (3660646)Terminated due to inappropriate strategy. % 7.44/1.55 % (3660646)------------------------------ % 7.44/1.55 % (3660646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.55 % (3660646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.55 % (3660646)CaDiCaL version: 2.1.3 % 7.44/1.55 % (3660646)Termination reason: Inappropriate % 7.44/1.55 % (3660646)Time elapsed: 0.008 s % 7.44/1.55 % (3660646)Peak memory usage: 11 MB % 7.44/1.55 % (3660646)Instructions burned: 14 (million) % 7.44/1.55 % (3660646)------------------------------ % 7.44/1.55 % (3660646)------------------------------ % 7.44/1.55 % (3660647)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3125834750:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 7.44/1.55 % (3660649)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2987225603:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 7.44/1.55 % (3660649)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.44/1.55 % (3660649)Terminated due to inappropriate strategy. % 7.44/1.55 % (3660649)------------------------------ % 7.44/1.55 % (3660649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.55 % (3660649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.55 % (3660649)CaDiCaL version: 2.1.3 % 7.44/1.55 % (3660649)Termination reason: Inappropriate % 7.44/1.55 % (3660649)Time elapsed: 0.013 s % 7.44/1.55 % (3660649)Peak memory usage: 10 MB % 7.44/1.55 % (3660649)Instructions burned: 13 (million) % 7.44/1.55 % (3660649)------------------------------ % 7.44/1.55 % (3660649)------------------------------ % 7.44/1.55 % (3660652)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=491076204: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.44/1.55 % (3660642)Instruction limit reached! % 7.44/1.55 % (3660642)------------------------------ % 7.44/1.55 % (3660642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.55 % (3660642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.55 % (3660642)CaDiCaL version: 2.1.3 % 7.44/1.55 % (3660642)Termination reason: Instruction limit % 7.44/1.55 % (3660642)Termination phase: Saturation % 34.94/5.24 % (3660642)Time elapsed: 0.166 s % 34.94/5.24 % (3660642)Peak memory usage: 13 MB % 34.94/5.24 % (3660642)Instructions burned: 181 (million) % 34.94/5.24 % (3660654)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1583753352:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 34.94/5.24 % (3660643)Instruction limit reached! % 34.94/5.24 % (3660643)------------------------------ % 34.94/5.24 % (3660643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/5.24 % (3660643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.24 % (3660643)CaDiCaL version: 2.1.3 % 34.94/5.24 % (3660643)Termination reason: Instruction limit % 34.94/5.24 % (3660643)Termination phase: Saturation % 34.94/5.24 % (3660643)Time elapsed: 0.508 s % 34.94/5.24 % (3660643)Peak memory usage: 14 MB % 34.94/5.24 % (3660643)Instructions burned: 477 (million) % 34.94/5.24 % (3660639)Instruction limit reached! % 34.94/5.24 % (3660639)------------------------------ % 34.94/5.24 % (3660639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/5.24 % (3660639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.24 % (3660639)CaDiCaL version: 2.1.3 % 34.94/5.24 % (3660639)Termination reason: Instruction limit % 34.94/5.24 % (3660639)Termination phase: Saturation % 34.94/5.24 % (3660639)Time elapsed: 0.605 s % 34.94/5.24 % (3660639)Peak memory usage: 16 MB % 34.94/5.24 % (3660639)Instructions burned: 684 (million) % 34.94/5.24 % (3660656)fmb+10_1_sil=64000:random_seed=3874764398:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 34.94/5.24 % (3660656)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.94/5.24 % (3660656)Terminated due to inappropriate strategy. % 34.94/5.24 % (3660656)------------------------------ % 34.94/5.24 % (3660656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/5.24 % (3660656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.24 % (3660656)CaDiCaL version: 2.1.3 % 34.94/5.24 % (3660656)Termination reason: Inappropriate % 34.94/5.24 % (3660656)Time elapsed: 0.014 s % 34.94/5.24 % (3660656)Peak memory usage: 11 MB % 34.94/5.24 % (3660656)Instructions burned: 14 (million) % 34.94/5.24 % (3660656)------------------------------ % 34.94/5.24 % (3660656)------------------------------ % 34.94/5.24 % (3660658)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1990890258:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 34.94/5.24 % (3660661)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1876667888:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi) % 34.94/5.24 % (3660661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.94/5.24 % (3660661)Terminated due to inappropriate strategy. % 34.94/5.24 % (3660661)------------------------------ % 34.94/5.24 % (3660661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/5.24 % (3660661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.24 % (3660661)CaDiCaL version: 2.1.3 % 34.94/5.24 % (3660661)Termination reason: Inappropriate % 34.94/5.24 % (3660661)Time elapsed: 0.008 s % 34.94/5.24 % (3660661)Peak memory usage: 11 MB % 34.94/5.24 % (3660661)Instructions burned: 13 (million) % 34.94/5.24 % (3660661)------------------------------ % 34.94/5.24 % (3660661)------------------------------ % 34.94/5.24 % (3660658)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 34.94/5.24 % (3660658)Terminated due to inappropriate strategy. % 34.94/5.24 % (3660658)------------------------------ % 34.94/5.24 % (3660658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.94/5.24 % (3660658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.24 % (3660658)CaDiCaL version: 2.1.3 % 34.94/5.24 % (3660658)Termination reason: Inappropriate % 34.94/5.24 % (3660658)Time elapsed: 0.013 s % 34.94/5.24 % (3660658)Peak memory usage: 11 MB % 34.94/5.24 % (3660658)Instructions burned: 13 (million) % 34.94/5.24 % (3660658)------------------------------ % 34.94/5.24 % (3660658)------------------------------ % 34.94/5.24 % (3660665)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2993499817:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 34.94/5.24 % (3660664)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2605809956:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 34.94/5.24 % (3660647)Instruction limit reached! % 34.94/5.24 % (3660647)------------------------------ % 39.14/5.96 % (3660647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.14/5.96 % (3660647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/5.96 % (3660647)CaDiCaL version: 2.1.3 % 39.14/5.96 % (3660647)Termination reason: Instruction limit % 39.14/5.96 % (3660647)Termination phase: Saturation % 39.14/5.96 % (3660647)Time elapsed: 0.642 s % 39.14/5.96 % (3660647)Peak memory usage: 21 MB % 39.14/5.96 % (3660647)Instructions burned: 1181 (million) % 39.14/5.96 % (3660668)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1489280353:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 39.14/5.96 % (3660668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.14/5.96 % (3660668)Terminated due to inappropriate strategy. % 39.14/5.96 % (3660668)------------------------------ % 39.14/5.96 % (3660668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.14/5.96 % (3660668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/5.96 % (3660668)CaDiCaL version: 2.1.3 % 39.14/5.96 % (3660668)Termination reason: Inappropriate % 39.14/5.96 % (3660668)Time elapsed: 0.008 s % 39.14/5.96 % (3660668)Peak memory usage: 11 MB % 39.14/5.96 % (3660668)Instructions burned: 16 (million) % 39.14/5.96 % (3660668)------------------------------ % 39.14/5.96 % (3660668)------------------------------ % 39.14/5.96 % (3660670)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2268713822:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi) % 39.14/5.96 % (3660670)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.14/5.96 % (3660670)Terminated due to inappropriate strategy. % 39.14/5.96 % (3660670)------------------------------ % 39.14/5.96 % (3660670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.14/5.96 % (3660670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/5.96 % (3660670)CaDiCaL version: 2.1.3 % 39.14/5.96 % (3660670)Termination reason: Inappropriate % 39.14/5.96 % (3660670)Time elapsed: 0.013 s % 39.14/5.96 % (3660670)Peak memory usage: 11 MB % 39.14/5.96 % (3660670)Instructions burned: 13 (million) % 39.14/5.96 % (3660670)------------------------------ % 39.14/5.96 % (3660670)------------------------------ % 39.14/5.96 % (3660672)ott-2_1_sil=16000:newcnf=on:random_seed=1854499687:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi) % 39.14/5.96 % (3660652)Instruction limit reached! % 39.14/5.96 % (3660652)------------------------------ % 39.14/5.96 % (3660652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.14/5.96 % (3660652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/5.96 % (3660652)CaDiCaL version: 2.1.3 % 39.14/5.96 % (3660652)Termination reason: Instruction limit % 39.14/5.96 % (3660652)Termination phase: Saturation % 39.14/5.96 % (3660652)Time elapsed: 0.726 s % 39.14/5.96 % (3660652)Peak memory usage: 20 MB % 39.14/5.96 % (3660652)Instructions burned: 692 (million) % 39.14/5.96 % (3660674)ott+10_1_sil=32000:tgt=ground:random_seed=466279951:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi) % 39.14/5.96 % (3660654)Instruction limit reached! % 39.14/5.96 % (3660654)------------------------------ % 39.14/5.96 % (3660654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.14/5.96 % (3660654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/5.96 % (3660654)CaDiCaL version: 2.1.3 % 39.14/5.96 % (3660654)Termination reason: Instruction limit % 39.14/5.96 % (3660654)Termination phase: Saturation % 39.14/5.96 % (3660654)Time elapsed: 0.811 s % 39.14/5.96 % (3660654)Peak memory usage: 19 MB % 39.14/5.96 % (3660654)Instructions burned: 879 (million) % 39.14/5.96 % (3660676)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4044517553:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 39.14/5.96 % (3660676)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 39.14/5.96 % (3660676)Terminated due to inappropriate strategy. % 39.14/5.96 % (3660676)------------------------------ % 39.14/5.96 % (3660676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.14/5.96 % (3660676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/5.96 % (3660676)CaDiCaL version: 2.1.3 % 39.14/5.96 % (3660676)Termination reason: Inappropriate % 39.14/5.96 % (3660676)Time elapsed: 0.016 s % 39.14/5.96 % (3660676)Peak memory usage: 11 MB % 39.14/5.96 % (3660676)Instructions burned: 16 (million) % 155.47/22.19 % (3660676)------------------------------ % 155.47/22.19 % (3660676)------------------------------ % 155.47/22.19 % (3660678)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3075851368:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 155.47/22.19 % (3660672)Instruction limit reached! % 155.47/22.19 % (3660672)------------------------------ % 155.47/22.19 % (3660672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.47/22.19 % (3660672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.47/22.19 % (3660672)CaDiCaL version: 2.1.3 % 155.47/22.19 % (3660672)Termination reason: Instruction limit % 155.47/22.19 % (3660672)Termination phase: Saturation % 155.47/22.19 % (3660672)Time elapsed: 0.474 s % 155.47/22.19 % (3660672)Peak memory usage: 17 MB % 155.47/22.19 % (3660672)Instructions burned: 869 (million) % 155.47/22.19 % (3660680)dis+21_1_sil=32000:sas=cadical:random_seed=3262285892:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 155.47/22.19 % (3660665)Instruction limit reached! % 155.47/22.19 % (3660665)------------------------------ % 155.47/22.19 % (3660665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.47/22.19 % (3660665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.47/22.19 % (3660665)CaDiCaL version: 2.1.3 % 155.47/22.19 % (3660665)Termination reason: Instruction limit % 155.47/22.19 % (3660665)Termination phase: Saturation % 155.47/22.19 % (3660665)Time elapsed: 1.364 s % 155.47/22.19 % (3660665)Peak memory usage: 26 MB % 155.47/22.19 % (3660665)Instructions burned: 1472 (million) % 155.47/22.19 % (3660683)ott+11_1_sil=16000:gs=on:random_seed=2542170780:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2978 on theBenchmark for (2978ds/2251Mi) % 155.47/22.19 % (3660678)Instruction limit reached! % 155.47/22.19 % (3660678)------------------------------ % 155.47/22.19 % (3660678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.47/22.19 % (3660678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.47/22.19 % (3660678)CaDiCaL version: 2.1.3 % 155.47/22.19 % (3660678)Termination reason: Instruction limit % 155.47/22.19 % (3660678)Termination phase: Saturation % 155.47/22.19 % (3660678)Time elapsed: 1.807 s % 155.47/22.19 % (3660678)Peak memory usage: 31 MB % 155.47/22.19 % (3660678)Instructions burned: 3513 (million) % 155.47/22.19 % (3660687)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2036624033:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 155.47/22.19 % (3660687)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 155.47/22.19 % (3660687)Terminated due to inappropriate strategy. % 155.47/22.19 % (3660687)------------------------------ % 155.47/22.19 % (3660687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.47/22.19 % (3660687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.47/22.19 % (3660687)CaDiCaL version: 2.1.3 % 155.47/22.19 % (3660687)Termination reason: Inappropriate % 155.47/22.19 % (3660687)Time elapsed: 0.011 s % 155.47/22.19 % (3660687)Peak memory usage: 11 MB % 155.47/22.19 % (3660687)Instructions burned: 14 (million) % 155.47/22.19 % (3660687)------------------------------ % 155.47/22.19 % (3660687)------------------------------ % 155.47/22.19 % (3660689)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3658608602:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 155.47/22.19 % (3660683)Instruction limit reached! % 155.47/22.19 % (3660683)------------------------------ % 155.47/22.19 % (3660683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.47/22.19 % (3660683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.47/22.19 % (3660683)CaDiCaL version: 2.1.3 % 155.47/22.19 % (3660683)Termination reason: Instruction limit % 155.47/22.19 % (3660683)Termination phase: Saturation % 155.47/22.19 % (3660683)Time elapsed: 2.023 s % 155.47/22.19 % (3660683)Peak memory usage: 19 MB % 155.47/22.19 % (3660683)Instructions burned: 2252 (million) % 155.47/22.19 % (3660695)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=203211184:i=29340_2957 on theBenchmark for (2957ds/29340Mi) % 155.47/22.19 % (3660680)Instruction limit reached! % 155.47/22.19 % (3660680)------------------------------ % 155.47/22.19 % (3660680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 155.47/22.19 % (3660680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.47/22.19 % (3660680)CaDiCaL version: 2.1.3 % 155.47/22.19 % (3660680)Termination reason: Instruction limit % 205.58/29.22 % (3660680)Termination phase: Saturation % 205.58/29.22 % (3660680)Time elapsed: 3.450 s % 205.58/29.22 % (3660680)Peak memory usage: 35 MB % 205.58/29.22 % (3660680)Instructions burned: 3774 (million) % 205.58/29.22 % (3660697)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=595692445:i=5211_2950 on theBenchmark for (2950ds/5211Mi) % 205.58/29.22 % (3660689)Instruction limit reached! % 205.58/29.22 % (3660689)------------------------------ % 205.58/29.22 % (3660689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/29.22 % (3660689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/29.22 % (3660689)CaDiCaL version: 2.1.3 % 205.58/29.22 % (3660689)Termination reason: Instruction limit % 205.58/29.22 % (3660689)Termination phase: Saturation % 205.58/29.22 % (3660689)Time elapsed: 2.206 s % 205.58/29.22 % (3660689)Peak memory usage: 44 MB % 205.58/29.22 % (3660689)Instructions burned: 4593 (million) % 205.58/29.22 % (3660699)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1950802882:i=5497:nm=2_2946 on theBenchmark for (2946ds/5497Mi) % 205.58/29.22 % (3660699)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.58/29.22 % (3660699)Terminated due to inappropriate strategy. % 205.58/29.22 % (3660699)------------------------------ % 205.58/29.22 % (3660699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/29.22 % (3660699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/29.22 % (3660699)CaDiCaL version: 2.1.3 % 205.58/29.22 % (3660699)Termination reason: Inappropriate % 205.58/29.22 % (3660699)Time elapsed: 0.013 s % 205.58/29.22 % (3660699)Peak memory usage: 11 MB % 205.58/29.22 % (3660699)Instructions burned: 16 (million) % 205.58/29.22 % (3660699)------------------------------ % 205.58/29.22 % (3660699)------------------------------ % 205.58/29.22 % (3660701)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4209063884:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi) % 205.58/29.22 % (3660701)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.58/29.22 % (3660701)Terminated due to inappropriate strategy. % 205.58/29.22 % (3660701)------------------------------ % 205.58/29.22 % (3660701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/29.22 % (3660701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/29.22 % (3660701)CaDiCaL version: 2.1.3 % 205.58/29.22 % (3660701)Termination reason: Inappropriate % 205.58/29.22 % (3660701)Time elapsed: 0.009 s % 205.58/29.22 % (3660701)Peak memory usage: 11 MB % 205.58/29.22 % (3660701)Instructions burned: 14 (million) % 205.58/29.22 % (3660701)------------------------------ % 205.58/29.22 % (3660701)------------------------------ % 205.58/29.22 % (3660703)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4134835912:i=14071_2945 on theBenchmark for (2945ds/14071Mi) % 205.58/29.22 % (3660703)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 205.58/29.22 % (3660703)Terminated due to inappropriate strategy. % 205.58/29.22 % (3660703)------------------------------ % 205.58/29.22 % (3660703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/29.22 % (3660703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/29.22 % (3660703)CaDiCaL version: 2.1.3 % 205.58/29.22 % (3660703)Termination reason: Inappropriate % 205.58/29.22 % (3660703)Time elapsed: 0.007 s % 205.58/29.22 % (3660703)Peak memory usage: 11 MB % 205.58/29.22 % (3660703)Instructions burned: 14 (million) % 205.58/29.22 % (3660703)------------------------------ % 205.58/29.22 % (3660703)------------------------------ % 205.58/29.22 % (3660705)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=848250821:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 205.58/29.22 % (3660664)Instruction limit reached! % 205.58/29.22 % (3660664)------------------------------ % 205.58/29.22 % (3660664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.58/29.22 % (3660664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.58/29.22 % (3660664)CaDiCaL version: 2.1.3 % 205.58/29.22 % (3660664)Termination reason: Instruction limit % 205.58/29.22 % (3660664)Termination phase: Saturation % 205.58/29.22 % (3660664)Time elapsed: 4.792 s % 205.58/29.22 % (3660664)Peak memory usage: 38 MB % 205.58/29.22 % (3660664)Instructions burned: 5131 (million) % 205.58/29.22 % (3660721)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3119844721:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 206.27/29.37 % (3660674)Instruction limit reached! % 206.27/29.37 % (3660674)------------------------------ % 206.27/29.37 % (3660674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.27/29.37 % (3660674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.27/29.37 % (3660674)CaDiCaL version: 2.1.3 % 206.27/29.37 % (3660674)Termination reason: Instruction limit % 206.27/29.37 % (3660674)Termination phase: Saturation % 206.27/29.37 % (3660674)Time elapsed: 4.821 s % 206.27/29.37 % (3660674)Peak memory usage: 47 MB % 206.27/29.37 % (3660674)Instructions burned: 5115 (million) % 206.27/29.37 % (3660723)dis+10_16:1_sil=16000:random_seed=1415529:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi) % 206.27/29.37 % (3660697)Instruction limit reached! % 206.27/29.37 % (3660697)------------------------------ % 206.27/29.37 % (3660697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.27/29.37 % (3660697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.27/29.37 % (3660697)CaDiCaL version: 2.1.3 % 206.27/29.37 % (3660697)Termination reason: Instruction limit % 206.27/29.37 % (3660697)Termination phase: Saturation % 206.27/29.37 % (3660697)Time elapsed: 4.429 s % 206.27/29.37 % (3660697)Peak memory usage: 41 MB % 206.27/29.37 % (3660697)Instructions burned: 5211 (million) % 206.27/29.37 % (3660727)ott-3_8_sil=64000:random_seed=330112977:i=20139:bs=on_2905 on theBenchmark for (2905ds/20139Mi) % 206.27/29.37 % (3660721)Instruction limit reached! % 206.27/29.37 % (3660721)------------------------------ % 206.27/29.37 % (3660721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.27/29.37 % (3660721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.27/29.37 % (3660721)CaDiCaL version: 2.1.3 % 206.27/29.37 % (3660721)Termination reason: Instruction limit % 206.27/29.37 % (3660721)Termination phase: Saturation % 206.27/29.37 % (3660721)Time elapsed: 8.197 s % 206.27/29.37 % (3660721)Peak memory usage: 72 MB % 206.27/29.37 % (3660721)Instructions burned: 8174 (million) % 206.27/29.37 % (3660745)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1140670728:fmbsr=2:i=32576_2861 on theBenchmark for (2861ds/32576Mi) % 206.27/29.37 % (3660745)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 206.27/29.37 % (3660745)Terminated due to inappropriate strategy. % 206.27/29.37 % (3660745)------------------------------ % 206.27/29.37 % (3660745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.27/29.37 % (3660745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.27/29.37 % (3660745)CaDiCaL version: 2.1.3 % 206.27/29.37 % (3660745)Termination reason: Inappropriate % 206.27/29.37 % (3660745)Time elapsed: 0.012 s % 206.27/29.37 % (3660745)Peak memory usage: 11 MB % 206.27/29.37 % (3660745)Instructions burned: 17 (million) % 206.27/29.37 % (3660745)------------------------------ % 206.27/29.37 % (3660745)------------------------------ % 206.27/29.37 % (3660747)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=178200422:i=11404_2860 on theBenchmark for (2860ds/11404Mi) % 206.27/29.37 % (3660723)Instruction limit reached! % 206.27/29.37 % (3660723)------------------------------ % 206.27/29.37 % (3660723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.27/29.37 % (3660723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.27/29.37 % (3660723)CaDiCaL version: 2.1.3 % 206.27/29.37 % (3660723)Termination reason: Instruction limit % 206.27/29.37 % (3660723)Termination phase: Saturation % 206.27/29.37 % (3660723)Time elapsed: 8.199 s % 206.27/29.37 % (3660723)Peak memory usage: 54 MB % 206.27/29.37 % (3660723)Instructions burned: 9156 (million) % 206.27/29.37 % (3660751)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2686258028:i=14134_2858 on theBenchmark for (2858ds/14134Mi) % 206.27/29.37 % (3660705)Instruction limit reached! % 206.27/29.37 % (3660705)------------------------------ % 206.27/29.37 % (3660705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.27/29.37 % (3660705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.27/29.37 % (3660705)CaDiCaL version: 2.1.3 % 206.27/29.37 % (3660705)Termination reason: Instruction limit % 206.27/29.37 % (3660705)Termination phase: Saturation % 206.27/29.37 % (3660705)Time elapsed: 8.715 s % 206.27/29.37 % (3660705)Peak memory usage: 22 MB % 206.27/29.37 % (3660705)Instructions burned: 22566 (million) % 206.27/29.37 % (3660753)dis+33_16_sil=32000:sac=on:random_seed=3640797595:i=15851:nm=0_2857 on theBenchmark for (2857ds/15851Mi) % 206.27/29.37 % (3660753)Instruction limit reached! % 206.27/29.37 % (3660753)------------------------------ % 206.27/29.37 % (3660753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.15/30.77 % (3660753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.15/30.77 % (3660753)CaDiCaL version: 2.1.3 % 216.15/30.77 % (3660753)Termination reason: Instruction limit % 216.15/30.77 % (3660753)Termination phase: Saturation % 216.15/30.77 % (3660753)Time elapsed: 7.649 s % 216.15/30.77 % (3660753)Peak memory usage: 118 MB % 216.15/30.77 % (3660753)Instructions burned: 15853 (million) % 216.15/30.77 % (3660773)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1371578415:avsq=on:i=17627:add=on:amm=off_2780 on theBenchmark for (2780ds/17627Mi) % 216.15/30.77 % (3660747)Instruction limit reached! % 216.15/30.77 % (3660747)------------------------------ % 216.15/30.77 % (3660747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.15/30.77 % (3660747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.15/30.77 % (3660747)CaDiCaL version: 2.1.3 % 216.15/30.77 % (3660747)Termination reason: Instruction limit % 216.15/30.77 % (3660747)Termination phase: Saturation % 216.15/30.77 % (3660747)Time elapsed: 12.231 s % 216.15/30.77 % (3660747)Peak memory usage: 90 MB % 216.15/30.77 % (3660747)Instructions burned: 11404 (million) % 216.15/30.77 % (3660775)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=350058809:s2a=on:i=53295_2738 on theBenchmark for (2738ds/53295Mi) % 216.15/30.77 % (3660751)Instruction limit reached! % 216.15/30.77 % (3660751)------------------------------ % 216.15/30.77 % (3660751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.15/30.77 % (3660751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.15/30.77 % (3660751)CaDiCaL version: 2.1.3 % 216.15/30.77 % (3660751)Termination reason: Instruction limit % 216.15/30.77 % (3660751)Termination phase: Saturation % 216.15/30.77 % (3660751)Time elapsed: 13.745 s % 216.15/30.77 % (3660751)Peak memory usage: 85 MB % 216.15/30.77 % (3660751)Instructions burned: 14135 (million) % 216.15/30.77 % (3660779)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3668814304:i=26857:ins=20_2720 on theBenchmark for (2720ds/26857Mi) % 216.15/30.77 % (3660779)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.15/30.77 % (3660779)Terminated due to inappropriate strategy. % 216.15/30.77 % (3660779)------------------------------ % 216.15/30.77 % (3660779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.15/30.77 % (3660779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.15/30.77 % (3660779)CaDiCaL version: 2.1.3 % 216.15/30.77 % (3660779)Termination reason: Inappropriate % 216.15/30.77 % (3660779)Time elapsed: 0.007 s % 216.15/30.77 % (3660779)Peak memory usage: 11 MB % 216.15/30.77 % (3660779)Instructions burned: 13 (million) % 216.15/30.77 % (3660779)------------------------------ % 216.15/30.77 % (3660779)------------------------------ % 216.15/30.77 % (3660781)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2339989797:i=28120:bs=on:fsr=off_2720 on theBenchmark for (2720ds/28120Mi) % 216.15/30.77 % (3660695)Instruction limit reached! % 216.15/30.77 % (3660695)------------------------------ % 216.15/30.77 % (3660695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.15/30.77 % (3660695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.15/30.77 % (3660695)CaDiCaL version: 2.1.3 % 216.15/30.77 % (3660695)Termination reason: Instruction limit % 216.15/30.77 % (3660695)Termination phase: Saturation % 216.15/30.77 % (3660695)Time elapsed: 24.571 s % 216.15/30.77 % (3660695)Peak memory usage: 363 MB % 216.15/30.77 % (3660695)Instructions burned: 29340 (million) % 216.15/30.77 % (3660936)fmb+10_1_sil=256000:fmbss=7:random_seed=472402144:fmbsr=1.6:i=182295_2711 on theBenchmark for (2711ds/182295Mi) % 216.15/30.77 % (3660936)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 216.15/30.77 % (3660936)Terminated due to inappropriate strategy. % 216.15/30.77 % (3660936)------------------------------ % 216.15/30.77 % (3660936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.15/30.77 % (3660936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.15/30.77 % (3660936)CaDiCaL version: 2.1.3 % 216.15/30.77 % (3660936)Termination reason: Inappropriate % 216.15/30.77 % (3660936)Time elapsed: 0.007 s % 216.15/30.77 % (3660936)Peak memory usage: 11 MB % 216.15/30.77 % (3660936)Instructions burned: 13 (million) % 216.15/30.77 % (3660936)------------------------------ % 216.15/30.77 % (3660936)------------------------------ % 216.15/30.77 % (3660938)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1229882480:i=44625:gsp=on_2710 on theBenchmark for (2710ds/44625Mi) % 223.01/31.74 % (3660938)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.01/31.74 % (3660938)Terminated due to inappropriate strategy. % 223.01/31.74 % (3660938)------------------------------ % 223.01/31.74 % (3660938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.01/31.74 % (3660938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.01/31.74 % (3660938)CaDiCaL version: 2.1.3 % 223.01/31.74 % (3660938)Termination reason: Inappropriate % 223.01/31.74 % (3660938)Time elapsed: 0.007 s % 223.01/31.74 % (3660938)Peak memory usage: 11 MB % 223.01/31.74 % (3660938)Instructions burned: 14 (million) % 223.01/31.74 % (3660938)------------------------------ % 223.01/31.74 % (3660938)------------------------------ % 223.01/31.74 % (3660940)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1458027457:i=160505_2710 on theBenchmark for (2710ds/160505Mi) % 223.01/31.74 % (3660940)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.01/31.74 % (3660940)Terminated due to inappropriate strategy. % 223.01/31.74 % (3660940)------------------------------ % 223.01/31.74 % (3660940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.01/31.74 % (3660940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.01/31.74 % (3660940)CaDiCaL version: 2.1.3 % 223.01/31.74 % (3660940)Termination reason: Inappropriate % 223.01/31.74 % (3660940)Time elapsed: 0.007 s % 223.01/31.74 % (3660940)Peak memory usage: 11 MB % 223.01/31.74 % (3660940)Instructions burned: 13 (million) % 223.01/31.74 % (3660940)------------------------------ % 223.01/31.74 % (3660940)------------------------------ % 223.01/31.74 % (3660942)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1464855422:fmbsr=1.3:i=225729_2710 on theBenchmark for (2710ds/225729Mi) % 223.01/31.74 % (3660942)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.01/31.74 % (3660942)Terminated due to inappropriate strategy. % 223.01/31.74 % (3660942)------------------------------ % 223.01/31.74 % (3660942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.01/31.74 % (3660942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.01/31.74 % (3660942)CaDiCaL version: 2.1.3 % 223.01/31.74 % (3660942)Termination reason: Inappropriate % 223.01/31.74 % (3660942)Time elapsed: 0.007 s % 223.01/31.74 % (3660942)Peak memory usage: 11 MB % 223.01/31.74 % (3660942)Instructions burned: 14 (million) % 223.01/31.74 % (3660942)------------------------------ % 223.01/31.74 % (3660942)------------------------------ % 223.01/31.74 % (3660944)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3351349116:fmbsr=2:i=185024:ins=7_2710 on theBenchmark for (2710ds/185024Mi) % 223.01/31.74 % (3660944)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.01/31.74 % (3660944)Terminated due to inappropriate strategy. % 223.01/31.74 % (3660944)------------------------------ % 223.01/31.74 % (3660944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.01/31.74 % (3660944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.01/31.74 % (3660944)CaDiCaL version: 2.1.3 % 223.01/31.74 % (3660944)Termination reason: Inappropriate % 223.01/31.74 % (3660944)Time elapsed: 0.007 s % 223.01/31.74 % (3660944)Peak memory usage: 11 MB % 223.01/31.74 % (3660944)Instructions burned: 14 (million) % 223.01/31.74 % (3660944)------------------------------ % 223.01/31.74 % (3660944)------------------------------ % 223.01/31.74 % (3660946)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3257877872:rtra=on_2709 on theBenchmark for (2709ds/0Mi) % 223.01/31.74 % (3660946)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 223.01/31.74 % (3660946)Terminated due to inappropriate strategy. % 223.01/31.74 % (3660946)------------------------------ % 223.01/31.74 % (3660946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 223.01/31.74 % (3660946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.01/31.74 % (3660946)CaDiCaL version: 2.1.3 % 223.01/31.74 % (3660946)Termination reason: Inappropriate % 223.01/31.74 % (3660946)Time elapsed: 0.010 s % 223.01/31.74 % (3660946)Peak memory usage: 11 MB % 223.01/31.74 % (3660946)Instructions burned: 17 (million) % 223.01/31.74 % (3660946)------------------------------ % 223.01/31.74 % (3660946)------------------------------ % 223.01/31.74 % (3660948)% WARNING: option uhcvi not known. % 223.01/31.74 % (3660948)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3717588186:i=271062:add=off:rtra=on:rawr=on_2709 on theBenchmark for (2709ds/271062Mi) % 236.31/33.68 % (3660727)Instruction limit reached! % 236.31/33.68 % (3660727)------------------------------ % 236.31/33.68 % (3660727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.31/33.68 % (3660727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.31/33.68 % (3660727)CaDiCaL version: 2.1.3 % 236.31/33.68 % (3660727)Termination reason: Instruction limit % 236.31/33.68 % (3660727)Termination phase: Saturation % 236.31/33.68 % (3660727)Time elapsed: 19.874 s % 236.31/33.68 % (3660727)Peak memory usage: 119 MB % 236.31/33.68 % (3660727)Instructions burned: 20140 (million) % 236.31/33.68 % (3660950)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2018448386:i=176048:add=on:rtra=on:rawr=on_2706 on theBenchmark for (2706ds/176048Mi) % 236.31/33.68 % (3660773)Instruction limit reached! % 236.31/33.68 % (3660773)------------------------------ % 236.31/33.68 % (3660773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.31/33.68 % (3660773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.31/33.68 % (3660773)CaDiCaL version: 2.1.3 % 236.31/33.68 % (3660773)Termination reason: Instruction limit % 236.31/33.68 % (3660773)Termination phase: Saturation % 236.31/33.68 % (3660773)Time elapsed: 8.122 s % 236.31/33.68 % (3660773)Peak memory usage: 93 MB % 236.31/33.68 % (3660773)Instructions burned: 17629 (million) % 236.31/33.68 % (3660952)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1515805187:i=206:fgj=on:rtra=on_2699 on theBenchmark for (2699ds/206Mi) % 236.31/33.68 % (3660952)Instruction limit reached! % 236.31/33.68 % (3660952)------------------------------ % 236.31/33.68 % (3660952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.31/33.68 % (3660952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.31/33.68 % (3660952)CaDiCaL version: 2.1.3 % 236.31/33.68 % (3660952)Termination reason: Instruction limit % 236.31/33.68 % (3660952)Termination phase: Saturation % 236.31/33.68 % (3660952)Time elapsed: 0.069 s % 236.31/33.68 % (3660952)Peak memory usage: 14 MB % 236.31/33.68 % (3660952)Instructions burned: 208 (million) % 236.31/33.68 % (3660954)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2356251424:i=232:rtra=on_2698 on theBenchmark for (2698ds/232Mi) % 236.31/33.68 % (3660954)Instruction limit reached! % 236.31/33.68 % (3660954)------------------------------ % 236.31/33.68 % (3660954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.31/33.68 % (3660954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.31/33.68 % (3660954)CaDiCaL version: 2.1.3 % 236.31/33.68 % (3660954)Termination reason: Instruction limit % 236.31/33.68 % (3660954)Termination phase: Saturation % 236.31/33.68 % (3660954)Time elapsed: 0.081 s % 236.31/33.68 % (3660954)Peak memory usage: 14 MB % 236.31/33.68 % (3660954)Instructions burned: 234 (million) % 236.31/33.68 % (3660956)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3254149587:i=262:rtra=on_2697 on theBenchmark for (2697ds/262Mi) % 236.31/33.68 % (3660956)Instruction limit reached! % 236.31/33.68 % (3660956)------------------------------ % 236.31/33.68 % (3660956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.31/33.68 % (3660956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.31/33.68 % (3660956)CaDiCaL version: 2.1.3 % 236.31/33.68 % (3660956)Termination reason: Instruction limit % 236.31/33.68 % (3660956)Termination phase: Saturation % 236.31/33.68 % (3660956)Time elapsed: 0.085 s % 236.31/33.68 % (3660956)Peak memory usage: 14 MB % 236.31/33.68 % (3660956)Instructions burned: 264 (million) % 236.31/33.68 % (3660958)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=272487413:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2696 on theBenchmark for (2696ds/318Mi) % 236.31/33.68 % (3660958)Instruction limit reached! % 236.31/33.68 % (3660958)------------------------------ % 236.31/33.68 % (3660958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.31/33.68 % (3660958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.31/33.68 % (3660958)CaDiCaL version: 2.1.3 % 236.31/33.68 % (3660958)Termination reason: Instruction limit % 236.31/33.68 % (3660958)Termination phase: Saturation % 236.31/33.68 % (3660958)Time elapsed: 0.119 s % 236.31/33.68 % (3660958)Peak memory usage: 15 MB % 236.31/33.68 % (3660958)Instructions burned: 319 (million) % 236.31/33.68 % (3660960)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=514769363:i=1428:nm=2:rtra=on_2695 on theBenchmark for (2695ds/1428Mi) % 260.21/37.00 % (3660960)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.21/37.00 % (3660960)Terminated due to inappropriate strategy. % 260.21/37.00 % (3660960)------------------------------ % 260.21/37.00 % (3660960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.21/37.00 % (3660960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.21/37.00 % (3660960)CaDiCaL version: 2.1.3 % 260.21/37.00 % (3660960)Termination reason: Inappropriate % 260.21/37.00 % (3660960)Time elapsed: 0.004 s % 260.21/37.00 % (3660960)Peak memory usage: 11 MB % 260.21/37.00 % (3660960)Instructions burned: 14 (million) % 260.21/37.00 % (3660960)------------------------------ % 260.21/37.00 % (3660960)------------------------------ % 260.21/37.00 % (3660962)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3654509275:i=262:bd=preordered:rtra=on:fsd=on_2695 on theBenchmark for (2695ds/262Mi) % 260.21/37.00 % (3660962)Instruction limit reached! % 260.21/37.00 % (3660962)------------------------------ % 260.21/37.00 % (3660962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.21/37.00 % (3660962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.21/37.00 % (3660962)CaDiCaL version: 2.1.3 % 260.21/37.00 % (3660962)Termination reason: Instruction limit % 260.21/37.00 % (3660962)Termination phase: Saturation % 260.21/37.00 % (3660962)Time elapsed: 0.095 s % 260.21/37.00 % (3660962)Peak memory usage: 14 MB % 260.21/37.00 % (3660962)Instructions burned: 263 (million) % 260.21/37.00 % (3660964)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=3999256045:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2694 on theBenchmark for (2694ds/1368Mi) % 260.21/37.00 % (3660964)Instruction limit reached! % 260.21/37.00 % (3660964)------------------------------ % 260.21/37.00 % (3660964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.21/37.00 % (3660964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.21/37.00 % (3660964)CaDiCaL version: 2.1.3 % 260.21/37.00 % (3660964)Termination reason: Instruction limit % 260.21/37.00 % (3660964)Termination phase: Saturation % 260.21/37.00 % (3660964)Time elapsed: 0.377 s % 260.21/37.00 % (3660964)Peak memory usage: 20 MB % 260.21/37.00 % (3660964)Instructions burned: 1372 (million) % 260.21/37.00 % (3660966)ott-21_1_sil=16000:si=on:fs=off:random_seed=3852365102:i=360:av=off:fsr=off:rtra=on_2690 on theBenchmark for (2690ds/360Mi) % 260.21/37.00 % (3660966)Instruction limit reached! % 260.21/37.00 % (3660966)------------------------------ % 260.21/37.00 % (3660966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.21/37.00 % (3660966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.21/37.00 % (3660966)CaDiCaL version: 2.1.3 % 260.21/37.00 % (3660966)Termination reason: Instruction limit % 260.21/37.00 % (3660966)Termination phase: Saturation % 260.21/37.00 % (3660966)Time elapsed: 0.100 s % 260.21/37.00 % (3660966)Peak memory usage: 14 MB % 260.21/37.00 % (3660966)Instructions burned: 360 (million) % 260.21/37.00 % (3660968)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3570764309:i=954:bd=all:rtra=on_2689 on theBenchmark for (2689ds/954Mi) % 260.21/37.00 % (3660968)Instruction limit reached! % 260.21/37.00 % (3660968)------------------------------ % 260.21/37.00 % (3660968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.21/37.00 % (3660968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.21/37.00 % (3660968)CaDiCaL version: 2.1.3 % 260.21/37.00 % (3660968)Termination reason: Instruction limit % 260.21/37.00 % (3660968)Termination phase: Saturation % 260.21/37.00 % (3660968)Time elapsed: 0.326 s % 260.21/37.00 % (3660968)Peak memory usage: 17 MB % 260.21/37.00 % (3660968)Instructions burned: 956 (million) % 260.21/37.00 % (3660970)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3509501276:fmbsr=1.3:i=1730:ins=25:rtra=on_2685 on theBenchmark for (2685ds/1730Mi) % 260.21/37.00 % (3660970)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 260.21/37.00 % (3660970)Terminated due to inappropriate strategy. % 260.21/37.00 % (3660970)------------------------------ % 260.21/37.00 % (3660970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.21/37.00 % (3660970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.21/37.00 % (3660970)CaDiCaL version: 2.1.3 % 260.21/37.00 % (3660970)Termination reason: Inappropriate % 296.67/42.09 % (3660970)Time elapsed: 0.004 s % 296.67/42.09 % (3660970)Peak memory usage: 11 MB % 296.67/42.09 % (3660970)Instructions burned: 15 (million) % 296.67/42.09 % (3660970)------------------------------ % 296.67/42.09 % (3660970)------------------------------ % 296.67/42.09 % (3660972)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2512082218:i=2358:rtra=on_2685 on theBenchmark for (2685ds/2358Mi) % 296.67/42.09 % (3660972)Instruction limit reached! % 296.67/42.09 % (3660972)------------------------------ % 296.67/42.09 % (3660972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.67/42.09 % (3660972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.67/42.09 % (3660972)CaDiCaL version: 2.1.3 % 296.67/42.09 % (3660972)Termination reason: Instruction limit % 296.67/42.09 % (3660972)Termination phase: Saturation % 296.67/42.09 % (3660972)Time elapsed: 0.845 s % 296.67/42.09 % (3660972)Peak memory usage: 30 MB % 296.67/42.09 % (3660972)Instructions burned: 2359 (million) % 296.67/42.09 % (3660974)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=755529934:i=1778:ins=1:rtra=on_2676 on theBenchmark for (2676ds/1778Mi) % 296.67/42.09 % (3660974)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 296.67/42.09 % (3660974)Terminated due to inappropriate strategy. % 296.67/42.09 % (3660974)------------------------------ % 296.67/42.09 % (3660974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.67/42.09 % (3660974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.67/42.09 % (3660974)CaDiCaL version: 2.1.3 % 296.67/42.09 % (3660974)Termination reason: Inappropriate % 296.67/42.09 % (3660974)Time elapsed: 0.004 s % 296.67/42.09 % (3660974)Peak memory usage: 11 MB % 296.67/42.09 % (3660974)Instructions burned: 14 (million) % 296.67/42.09 % (3660974)------------------------------ % 296.67/42.09 % (3660974)------------------------------ % 296.67/42.09 % (3660976)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=2702232427:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2676 on theBenchmark for (2676ds/1384Mi) % 296.67/42.09 % (3660976)Instruction limit reached! % 296.67/42.09 % (3660976)------------------------------ % 296.67/42.09 % (3660976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.67/42.09 % (3660976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.67/42.09 % (3660976)CaDiCaL version: 2.1.3 % 296.67/42.09 % (3660976)Termination reason: Instruction limit % 296.67/42.09 % (3660976)Termination phase: Saturation % 296.67/42.09 % (3660976)Time elapsed: 0.482 s % 296.67/42.09 % (3660976)Peak memory usage: 26 MB % 296.67/42.09 % (3660976)Instructions burned: 1386 (million) % 296.67/42.09 % (3660978)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1090828497:i=1758:kws=inv_precedence:fsr=off:rtra=on_2671 on theBenchmark for (2671ds/1758Mi) % 296.67/42.09 % (3660978)Instruction limit reached! % 296.67/42.09 % (3660978)------------------------------ % 296.67/42.09 % (3660978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.67/42.09 % (3660978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.67/42.09 % (3660978)CaDiCaL version: 2.1.3 % 296.67/42.09 % (3660978)Termination reason: Instruction limit % 296.67/42.09 % (3660978)Termination phase: Saturation % 296.67/42.09 % (3660978)Time elapsed: 0.524 s % 296.67/42.09 % (3660978)Peak memory usage: 23 MB % 296.67/42.09 % (3660978)Instructions burned: 1761 (million) % 296.67/42.09 % (3660980)fmb+10_1_sil=64000:si=on:random_seed=3278114673:i=44122:nm=2:rtra=on:gsp=on_2666 on theBenchmark for (2666ds/44122Mi) % 296.67/42.09 % (3660980)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 296.67/42.09 % (3660980)Terminated due to inappropriate strategy. % 296.67/42.09 % (3660980)------------------------------ % 296.67/42.09 % (3660980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 296.67/42.09 % (3660980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.67/42.09 % (3660980)CaDiCaL version: 2.1.3 % 296.67/42.09 % (3660980)Termination reason: Inappropriate % 296.67/42.09 % (3660980)Time elapsed: 0.004 s % 296.67/42.09 % (3660980)Peak memory usage: 11 MB % 296.67/42.09 % (3660980)Instructions burned: 16 (million) % 296.67/42.09 % (3660980)------------------------------ % 296.67/42.09 % (3660980)------------------------------ % 296.67/42.09 % (3660982)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3340021974:i=19030:nm=5:rtTerminated % 300.15/42.64 % Vampire exiting % 300.15/42.64 Terminated %------------------------------------------------------------------------------