%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW745_1 : TPTP v9.3.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n005.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:42 PM UTC 2026 % Result : Timeout 300.48s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW745_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 % Computer : n005.cluster.edu % 0.07/0.21 % Model : x86_64 x86_64 % 0.07/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.21 % Memory : 8046.5625MB % 0.07/0.21 % OS : Linux 6.8.0-71-generic % 0.07/0.21 % CPULimit : 300 % 0.07/0.21 % WCLimit : 300 % 0.07/0.21 % DateTime : Mon Sep 28 14:29:02 UTC 2026 % 0.07/0.22 % CPUTime : % 0.07/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.25 Running first-order model finding % 0.07/0.25 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.06/0.75 % (824484)Will run a generic schedule for satisfiability detection. % 3.06/0.75 % (824515)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1234820226:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.06/0.75 % (824509)% WARNING: option uhcvi not known. % 3.06/0.75 % (824508)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2222505859_2999 on theBenchmark for (2999ds/0Mi) % 3.06/0.75 % (824511)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2879226363:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.06/0.75 % (824509)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2489949754:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.06/0.75 % (824512)dis+10_1_sil=32000:sp=arity:random_seed=3236721561:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.06/0.75 % (824514)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3385540850:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.06/0.75 % (824513)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4290426204:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.06/0.75 % (824515)Instruction limit reached! % 3.06/0.75 % (824515)------------------------------ % 3.06/0.75 % (824515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.06/0.75 % (824515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.06/0.75 % (824515)CaDiCaL version: 2.1.3 % 3.06/0.75 % (824515)Termination reason: Instruction limit % 3.06/0.75 % (824515)Termination phase: Saturation % 3.06/0.75 % (824515)Time elapsed: 0.042 s % 3.06/0.75 % (824515)Peak memory usage: 17 MB % 3.06/0.75 % (824515)Instructions burned: 163 (million) % 3.06/0.75 % (824539)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2813968701:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.06/0.75 % (824512)Instruction limit reached! % 3.06/0.75 % (824512)------------------------------ % 3.06/0.75 % (824512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.06/0.75 % (824512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.06/0.75 % (824512)CaDiCaL version: 2.1.3 % 3.06/0.75 % (824512)Termination reason: Instruction limit % 3.06/0.75 % (824512)Termination phase: Saturation % 3.06/0.75 % (824512)Time elapsed: 0.048 s % 3.06/0.75 % (824512)Peak memory usage: 15 MB % 3.06/0.75 % (824512)Instructions burned: 104 (million) % 3.06/0.75 % (824513)Instruction limit reached! % 3.06/0.75 % (824513)------------------------------ % 3.06/0.75 % (824513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.06/0.75 % (824513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.06/0.75 % (824513)CaDiCaL version: 2.1.3 % 3.06/0.75 % (824513)Termination reason: Instruction limit % 3.06/0.75 % (824513)Termination phase: Blocked clause elimination % 3.06/0.75 % (824513)Time elapsed: 0.052 s % 3.06/0.75 % (824513)Peak memory usage: 13 MB % 3.06/0.75 % (824513)Instructions burned: 117 (million) % 3.06/0.75 % (824539)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.06/0.75 % (824539)Terminated due to inappropriate strategy. % 3.06/0.75 % (824539)------------------------------ % 3.06/0.75 % (824539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.06/0.75 % (824539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.06/0.75 % (824539)CaDiCaL version: 2.1.3 % 3.06/0.75 % (824539)Termination reason: Inappropriate % 3.06/0.75 % (824539)Time elapsed: 0.015 s % 3.06/0.75 % (824539)Peak memory usage: 12 MB % 3.06/0.75 % (824539)Instructions burned: 63 (million) % 3.06/0.75 % (824539)------------------------------ % 3.06/0.75 % (824539)------------------------------ % 3.06/0.75 % (824514)Instruction limit reached! % 3.06/0.75 % (824514)------------------------------ % 3.06/0.75 % (824514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.06/0.75 % (824514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.06/0.75 % (824514)CaDiCaL version: 2.1.3 % 3.06/0.75 % (824514)Termination reason: Instruction limit % 3.06/0.75 % (824514)Termination phase: Saturation % 3.06/0.75 % (824514)Time elapsed: 0.064 s % 3.06/0.75 % (824514)Peak memory usage: 16 MB % 3.06/0.75 % (824514)Instructions burned: 132 (million) % 3.06/0.75 % (824547)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=175584810:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.06/0.75 % (824550)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=1824316391:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.30/1.31 % (824555)ott-21_1_sil=16000:fs=off:random_seed=2614217619:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.30/1.31 % (824556)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2259410892:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.30/1.31 % (824508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.30/1.31 % (824508)Terminated due to inappropriate strategy. % 7.30/1.31 % (824508)------------------------------ % 7.30/1.31 % (824508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.30/1.31 % (824508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.31 % (824508)CaDiCaL version: 2.1.3 % 7.30/1.31 % (824508)Termination reason: Inappropriate % 7.30/1.31 % (824508)Time elapsed: 0.120 s % 7.30/1.31 % (824508)Peak memory usage: 13 MB % 7.30/1.31 % (824508)Instructions burned: 249 (million) % 7.30/1.31 % (824555)Instruction limit reached! % 7.30/1.31 % (824555)------------------------------ % 7.30/1.31 % (824555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.30/1.31 % (824555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.31 % (824555)CaDiCaL version: 2.1.3 % 7.30/1.31 % (824555)Termination reason: Instruction limit % 7.30/1.31 % (824555)Termination phase: Saturation % 7.30/1.31 % (824555)Time elapsed: 0.045 s % 7.30/1.31 % (824555)Peak memory usage: 14 MB % 7.30/1.31 % (824555)Instructions burned: 180 (million) % 7.30/1.31 % (824508)------------------------------ % 7.30/1.31 % (824508)------------------------------ % 7.30/1.31 % (824547)Instruction limit reached! % 7.30/1.31 % (824547)------------------------------ % 7.30/1.31 % (824547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.30/1.31 % (824547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.31 % (824547)CaDiCaL version: 2.1.3 % 7.30/1.31 % (824547)Termination reason: Instruction limit % 7.30/1.31 % (824547)Termination phase: Blocked clause elimination % 7.30/1.31 % (824547)Time elapsed: 0.061 s % 7.30/1.31 % (824547)Peak memory usage: 13 MB % 7.30/1.31 % (824547)Instructions burned: 133 (million) % 7.30/1.31 % (824578)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2396788797:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 7.30/1.31 % (824581)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1613150730:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 7.30/1.31 % (824582)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2026343049:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 7.30/1.31 % (824578)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.30/1.31 % (824578)Terminated due to inappropriate strategy. % 7.30/1.31 % (824578)------------------------------ % 7.30/1.31 % (824578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.30/1.31 % (824578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.31 % (824578)CaDiCaL version: 2.1.3 % 7.30/1.31 % (824578)Termination reason: Inappropriate % 7.30/1.31 % (824578)Time elapsed: 0.021 s % 7.30/1.31 % (824578)Peak memory usage: 14 MB % 7.30/1.31 % (824578)Instructions burned: 81 (million) % 7.30/1.31 % (824578)------------------------------ % 7.30/1.31 % (824578)------------------------------ % 7.30/1.31 % (824591)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=4085968118: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.30/1.31 % (824582)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 7.30/1.31 % (824582)Terminated due to inappropriate strategy. % 7.30/1.31 % (824582)------------------------------ % 7.30/1.31 % (824582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.30/1.31 % (824582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.30/1.31 % (824582)CaDiCaL version: 2.1.3 % 7.30/1.31 % (824582)Termination reason: Inappropriate % 7.30/1.31 % (824582)Time elapsed: 0.031 s % 7.30/1.31 % (824582)Peak memory usage: 12 MB % 7.30/1.31 % (824582)Instructions burned: 71 (million) % 7.30/1.31 % (824582)------------------------------ % 19.61/3.10 % (824582)------------------------------ % 19.61/3.10 % (824611)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=748146892:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.61/3.10 % (824556)Instruction limit reached! % 19.61/3.10 % (824556)------------------------------ % 19.61/3.10 % (824556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.61/3.10 % (824556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.10 % (824556)CaDiCaL version: 2.1.3 % 19.61/3.10 % (824556)Termination reason: Instruction limit % 19.61/3.10 % (824556)Termination phase: Saturation % 19.61/3.10 % (824556)Time elapsed: 0.251 s % 19.61/3.10 % (824556)Peak memory usage: 17 MB % 19.61/3.10 % (824556)Instructions burned: 478 (million) % 19.61/3.10 % (824632)fmb+10_1_sil=64000:random_seed=1629714342:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.61/3.10 % (824591)Instruction limit reached! % 19.61/3.10 % (824591)------------------------------ % 19.61/3.10 % (824591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.61/3.10 % (824591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.10 % (824591)CaDiCaL version: 2.1.3 % 19.61/3.10 % (824591)Termination reason: Instruction limit % 19.61/3.10 % (824591)Termination phase: Saturation % 19.61/3.10 % (824591)Time elapsed: 0.218 s % 19.61/3.10 % (824591)Peak memory usage: 22 MB % 19.61/3.10 % (824591)Instructions burned: 694 (million) % 19.61/3.10 % (824632)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.61/3.10 % (824632)Terminated due to inappropriate strategy. % 19.61/3.10 % (824632)------------------------------ % 19.61/3.10 % (824632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.61/3.10 % (824632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.10 % (824632)CaDiCaL version: 2.1.3 % 19.61/3.10 % (824632)Termination reason: Inappropriate % 19.61/3.10 % (824632)Time elapsed: 0.029 s % 19.61/3.10 % (824632)Peak memory usage: 12 MB % 19.61/3.10 % (824632)Instructions burned: 68 (million) % 19.61/3.10 % (824632)------------------------------ % 19.61/3.10 % (824632)------------------------------ % 19.61/3.10 % (824634)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3767990509:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 19.61/3.10 % (824635)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3318192639:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 19.61/3.10 % (824634)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.61/3.10 % (824634)Terminated due to inappropriate strategy. % 19.61/3.10 % (824634)------------------------------ % 19.61/3.10 % (824634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.61/3.10 % (824634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.10 % (824634)CaDiCaL version: 2.1.3 % 19.61/3.10 % (824634)Termination reason: Inappropriate % 19.61/3.10 % (824634)Time elapsed: 0.015 s % 19.61/3.10 % (824634)Peak memory usage: 12 MB % 19.61/3.10 % (824634)Instructions burned: 65 (million) % 19.61/3.10 % (824634)------------------------------ % 19.61/3.10 % (824634)------------------------------ % 19.61/3.10 % (824638)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2093878279:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 19.61/3.10 % (824635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 19.61/3.10 % (824635)Terminated due to inappropriate strategy. % 19.61/3.10 % (824635)------------------------------ % 19.61/3.10 % (824635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.61/3.10 % (824635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.10 % (824635)CaDiCaL version: 2.1.3 % 19.61/3.10 % (824635)Termination reason: Inappropriate % 19.61/3.10 % (824635)Time elapsed: 0.030 s % 19.61/3.10 % (824635)Peak memory usage: 12 MB % 19.61/3.10 % (824635)Instructions burned: 70 (million) % 19.61/3.10 % (824635)------------------------------ % 19.61/3.10 % (824635)------------------------------ % 19.61/3.10 % (824550)Instruction limit reached! % 19.61/3.10 % (824550)------------------------------ % 19.61/3.10 % (824550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.61/3.10 % (824550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.61/3.10 % (824550)CaDiCaL version: 2.1.3 % 19.61/3.10 % (824550)Termination reason: Instruction limit % 19.61/3.10 % (824550)Termination phase: Saturation % 26.70/4.04 % (824550)Time elapsed: 0.375 s % 26.70/4.04 % (824550)Peak memory usage: 21 MB % 26.70/4.04 % (824550)Instructions burned: 685 (million) % 26.70/4.04 % (824640)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1786260892:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 26.70/4.04 % (824641)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=162346816:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 26.70/4.04 % (824611)Instruction limit reached! % 26.70/4.04 % (824611)------------------------------ % 26.70/4.04 % (824611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.70/4.04 % (824611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.70/4.04 % (824611)CaDiCaL version: 2.1.3 % 26.70/4.04 % (824611)Termination reason: Instruction limit % 26.70/4.04 % (824611)Termination phase: Saturation % 26.70/4.04 % (824611)Time elapsed: 0.358 s % 26.70/4.04 % (824611)Peak memory usage: 19 MB % 26.70/4.04 % (824611)Instructions burned: 881 (million) % 26.70/4.04 % (824644)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1667135598:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 26.70/4.04 % (824641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.70/4.04 % (824641)Terminated due to inappropriate strategy. % 26.70/4.04 % (824641)------------------------------ % 26.70/4.04 % (824641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.70/4.04 % (824641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.70/4.04 % (824641)CaDiCaL version: 2.1.3 % 26.70/4.04 % (824641)Termination reason: Inappropriate % 26.70/4.04 % (824641)Time elapsed: 0.117 s % 26.70/4.04 % (824641)Peak memory usage: 13 MB % 26.70/4.04 % (824641)Instructions burned: 247 (million) % 26.70/4.04 % (824641)------------------------------ % 26.70/4.04 % (824641)------------------------------ % 26.70/4.04 % (824646)ott-2_1_sil=16000:newcnf=on:random_seed=2964307228:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 26.70/4.04 % (824644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.70/4.04 % (824644)Terminated due to inappropriate strategy. % 26.70/4.04 % (824644)------------------------------ % 26.70/4.04 % (824644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.70/4.04 % (824644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.70/4.04 % (824644)CaDiCaL version: 2.1.3 % 26.70/4.04 % (824644)Termination reason: Inappropriate % 26.70/4.04 % (824644)Time elapsed: 0.030 s % 26.70/4.04 % (824644)Peak memory usage: 12 MB % 26.70/4.04 % (824644)Instructions burned: 70 (million) % 26.70/4.04 % (824644)------------------------------ % 26.70/4.04 % (824644)------------------------------ % 26.70/4.04 % (824648)ott+10_1_sil=32000:tgt=ground:random_seed=1264015782:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 26.70/4.04 % (824581)Instruction limit reached! % 26.70/4.04 % (824581)------------------------------ % 26.70/4.04 % (824581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.70/4.04 % (824581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.70/4.04 % (824581)CaDiCaL version: 2.1.3 % 26.70/4.04 % (824581)Termination reason: Instruction limit % 26.70/4.04 % (824581)Termination phase: Saturation % 26.70/4.04 % (824581)Time elapsed: 0.697 s % 26.70/4.04 % (824581)Peak memory usage: 24 MB % 26.70/4.04 % (824581)Instructions burned: 1181 (million) % 26.70/4.04 % (824650)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1512184437:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 26.70/4.04 % (824650)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 26.70/4.04 % (824650)Terminated due to inappropriate strategy. % 26.70/4.04 % (824650)------------------------------ % 26.70/4.04 % (824650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 26.70/4.04 % (824650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.70/4.04 % (824650)CaDiCaL version: 2.1.3 % 26.70/4.04 % (824650)Termination reason: Inappropriate % 26.70/4.04 % (824650)Time elapsed: 0.118 s % 26.70/4.04 % (824650)Peak memory usage: 13 MB % 26.70/4.04 % (824650)Instructions burned: 249 (million) % 26.70/4.04 % (824650)------------------------------ % 26.70/4.04 % (824650)------------------------------ % 26.70/4.04 % (824652)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2083105219:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 83.47/12.11 % (824646)Instruction limit reached! % 83.47/12.11 % (824646)------------------------------ % 83.47/12.11 % (824646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.47/12.11 % (824646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.11 % (824646)CaDiCaL version: 2.1.3 % 83.47/12.11 % (824646)Termination reason: Instruction limit % 83.47/12.11 % (824646)Termination phase: Saturation % 83.47/12.11 % (824646)Time elapsed: 0.468 s % 83.47/12.11 % (824646)Peak memory usage: 23 MB % 83.47/12.11 % (824646)Instructions burned: 870 (million) % 83.47/12.11 % (824654)dis+21_1_sil=32000:sas=cadical:random_seed=595919585:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 83.47/12.11 % (824640)Instruction limit reached! % 83.47/12.11 % (824640)------------------------------ % 83.47/12.11 % (824640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.47/12.11 % (824640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.11 % (824640)CaDiCaL version: 2.1.3 % 83.47/12.11 % (824640)Termination reason: Instruction limit % 83.47/12.11 % (824640)Termination phase: Saturation % 83.47/12.11 % (824640)Time elapsed: 0.738 s % 83.47/12.11 % (824640)Peak memory usage: 26 MB % 83.47/12.11 % (824640)Instructions burned: 1472 (million) % 83.47/12.11 % (824656)ott+11_1_sil=16000:gs=on:random_seed=85801384:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 83.47/12.11 % (824638)Instruction limit reached! % 83.47/12.11 % (824638)------------------------------ % 83.47/12.11 % (824638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.47/12.11 % (824638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.11 % (824638)CaDiCaL version: 2.1.3 % 83.47/12.11 % (824638)Termination reason: Instruction limit % 83.47/12.11 % (824638)Termination phase: Saturation % 83.47/12.11 % (824638)Time elapsed: 1.431 s % 83.47/12.11 % (824638)Peak memory usage: 47 MB % 83.47/12.11 % (824638)Instructions burned: 5132 (million) % 83.47/12.11 % (824658)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=836540293:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi) % 83.47/12.11 % (824658)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 83.47/12.11 % (824658)Terminated due to inappropriate strategy. % 83.47/12.11 % (824658)------------------------------ % 83.47/12.11 % (824658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.47/12.11 % (824658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.11 % (824658)CaDiCaL version: 2.1.3 % 83.47/12.11 % (824658)Termination reason: Inappropriate % 83.47/12.11 % (824658)Time elapsed: 0.016 s % 83.47/12.11 % (824658)Peak memory usage: 12 MB % 83.47/12.11 % (824658)Instructions burned: 70 (million) % 83.47/12.11 % (824658)------------------------------ % 83.47/12.11 % (824658)------------------------------ % 83.47/12.11 % (824660)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1073643490:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi) % 83.47/12.11 % (824656)Instruction limit reached! % 83.47/12.11 % (824656)------------------------------ % 83.47/12.11 % (824656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.47/12.11 % (824656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.11 % (824656)CaDiCaL version: 2.1.3 % 83.47/12.11 % (824656)Termination reason: Instruction limit % 83.47/12.11 % (824656)Termination phase: Saturation % 83.47/12.11 % (824656)Time elapsed: 1.237 s % 83.47/12.11 % (824656)Peak memory usage: 30 MB % 83.47/12.11 % (824656)Instructions burned: 2252 (million) % 83.47/12.11 % (824662)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3588725405:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 83.47/12.11 % (824652)Instruction limit reached! % 83.47/12.11 % (824652)------------------------------ % 83.47/12.11 % (824652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 83.47/12.11 % (824652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.47/12.11 % (824652)CaDiCaL version: 2.1.3 % 83.47/12.11 % (824652)Termination reason: Instruction limit % 83.47/12.11 % (824652)Termination phase: Saturation % 83.47/12.11 % (824652)Time elapsed: 1.765 s % 83.47/12.11 % (824652)Peak memory usage: 34 MB % 83.47/12.11 % (824652)Instructions burned: 3513 (million) % 83.47/12.11 % (824664)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3588776085:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 126.08/18.08 % (824654)Instruction limit reached! % 126.08/18.08 % (824654)------------------------------ % 126.08/18.08 % (824654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (824654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (824654)CaDiCaL version: 2.1.3 % 126.08/18.08 % (824654)Termination reason: Instruction limit % 126.08/18.08 % (824654)Termination phase: Saturation % 126.08/18.08 % (824654)Time elapsed: 2.001 s % 126.08/18.08 % (824654)Peak memory usage: 38 MB % 126.08/18.08 % (824654)Instructions burned: 3774 (million) % 126.08/18.08 % (824666)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2050899117:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 126.08/18.08 % (824666)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.08/18.08 % (824666)Terminated due to inappropriate strategy. % 126.08/18.08 % (824666)------------------------------ % 126.08/18.08 % (824666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (824666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (824666)CaDiCaL version: 2.1.3 % 126.08/18.08 % (824666)Termination reason: Inappropriate % 126.08/18.08 % (824666)Time elapsed: 0.071 s % 126.08/18.08 % (824666)Peak memory usage: 13 MB % 126.08/18.08 % (824666)Instructions burned: 150 (million) % 126.08/18.08 % (824666)------------------------------ % 126.08/18.08 % (824666)------------------------------ % 126.08/18.08 % (824668)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3021104681:fmbsr=2:i=46332_2967 on theBenchmark for (2967ds/46332Mi) % 126.08/18.08 % (824668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.08/18.08 % (824668)Terminated due to inappropriate strategy. % 126.08/18.08 % (824668)------------------------------ % 126.08/18.08 % (824668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (824668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (824668)CaDiCaL version: 2.1.3 % 126.08/18.08 % (824668)Termination reason: Inappropriate % 126.08/18.08 % (824668)Time elapsed: 0.030 s % 126.08/18.08 % (824668)Peak memory usage: 12 MB % 126.08/18.08 % (824668)Instructions burned: 70 (million) % 126.08/18.08 % (824660)Instruction limit reached! % 126.08/18.08 % (824660)------------------------------ % 126.08/18.08 % (824660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (824660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (824660)CaDiCaL version: 2.1.3 % 126.08/18.08 % (824668)------------------------------ % 126.08/18.08 % (824668)------------------------------ % 126.08/18.08 % (824660)Termination reason: Instruction limit % 126.08/18.08 % (824660)Termination phase: Saturation % 126.08/18.08 % (824660)Time elapsed: 1.351 s % 126.08/18.08 % (824660)Peak memory usage: 47 MB % 126.08/18.08 % (824660)Instructions burned: 4592 (million) % 126.08/18.08 % (824671)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=422278563:i=22565:add=on:rawr=on_2966 on theBenchmark for (2966ds/22565Mi) % 126.08/18.08 % (824670)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2624005323:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 126.08/18.08 % (824670)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 126.08/18.08 % (824670)Terminated due to inappropriate strategy. % 126.08/18.08 % (824670)------------------------------ % 126.08/18.08 % (824670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (824670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (824670)CaDiCaL version: 2.1.3 % 126.08/18.08 % (824670)Termination reason: Inappropriate % 126.08/18.08 % (824670)Time elapsed: 0.030 s % 126.08/18.08 % (824670)Peak memory usage: 12 MB % 126.08/18.08 % (824670)Instructions burned: 70 (million) % 126.08/18.08 % (824670)------------------------------ % 126.08/18.08 % (824670)------------------------------ % 126.08/18.08 % (824674)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4181575935:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 126.08/18.08 % (824648)Instruction limit reached! % 126.08/18.08 % (824648)------------------------------ % 126.08/18.08 % (824648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 126.08/18.08 % (824648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.08/18.08 % (824648)CaDiCaL version: 2.1.3 % 126.08/18.08 % (824648)Termination reason: Instruction limit % 135.10/19.37 % (824648)Termination phase: Saturation % 135.10/19.37 % (824648)Time elapsed: 3.098 s % 135.10/19.37 % (824648)Peak memory usage: 34 MB % 135.10/19.37 % (824648)Instructions burned: 5114 (million) % 135.10/19.37 % (824676)dis+10_16:1_sil=16000:random_seed=473484202:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 135.10/19.37 % (824664)Instruction limit reached! % 135.10/19.37 % (824664)------------------------------ % 135.10/19.37 % (824664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.37 % (824664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.37 % (824664)CaDiCaL version: 2.1.3 % 135.10/19.37 % (824664)Termination reason: Instruction limit % 135.10/19.37 % (824664)Termination phase: Saturation % 135.10/19.37 % (824664)Time elapsed: 2.256 s % 135.10/19.37 % (824664)Peak memory usage: 69 MB % 135.10/19.37 % (824664)Instructions burned: 5213 (million) % 135.10/19.37 % (824678)ott-3_8_sil=64000:random_seed=416049470:i=20139:bs=on_2948 on theBenchmark for (2948ds/20139Mi) % 135.10/19.37 % (824671)Instruction limit reached! % 135.10/19.37 % (824671)------------------------------ % 135.10/19.37 % (824671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.37 % (824671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.37 % (824671)CaDiCaL version: 2.1.3 % 135.10/19.37 % (824671)Termination reason: Instruction limit % 135.10/19.37 % (824671)Termination phase: Saturation % 135.10/19.37 % (824671)Time elapsed: 4.850 s % 135.10/19.37 % (824671)Peak memory usage: 29 MB % 135.10/19.37 % (824671)Instructions burned: 22570 (million) % 135.10/19.37 % (824680)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1293060739:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 135.10/19.37 % (824680)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 135.10/19.37 % (824680)Terminated due to inappropriate strategy. % 135.10/19.37 % (824680)------------------------------ % 135.10/19.37 % (824680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.37 % (824680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.37 % (824680)CaDiCaL version: 2.1.3 % 135.10/19.37 % (824680)Termination reason: Inappropriate % 135.10/19.37 % (824680)Time elapsed: 0.063 s % 135.10/19.37 % (824680)Peak memory usage: 13 MB % 135.10/19.37 % (824680)Instructions burned: 247 (million) % 135.10/19.37 % (824680)------------------------------ % 135.10/19.37 % (824680)------------------------------ % 135.10/19.37 % (824682)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=361671015:i=11404_2917 on theBenchmark for (2917ds/11404Mi) % 135.10/19.37 % (824674)Instruction limit reached! % 135.10/19.37 % (824674)------------------------------ % 135.10/19.37 % (824674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.37 % (824674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.37 % (824674)CaDiCaL version: 2.1.3 % 135.10/19.37 % (824674)Termination reason: Instruction limit % 135.10/19.37 % (824674)Termination phase: Saturation % 135.10/19.37 % (824674)Time elapsed: 5.077 s % 135.10/19.37 % (824674)Peak memory usage: 50 MB % 135.10/19.37 % (824674)Instructions burned: 8175 (million) % 135.10/19.37 % (824684)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=51198055:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 135.10/19.37 % (824676)Instruction limit reached! % 135.10/19.37 % (824676)------------------------------ % 135.10/19.37 % (824676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.37 % (824676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.37 % (824676)CaDiCaL version: 2.1.3 % 135.10/19.37 % (824676)Termination reason: Instruction limit % 135.10/19.37 % (824676)Termination phase: Saturation % 135.10/19.37 % (824676)Time elapsed: 4.811 s % 135.10/19.37 % (824676)Peak memory usage: 58 MB % 135.10/19.37 % (824676)Instructions burned: 9157 (million) % 135.10/19.37 % (824686)dis+33_16_sil=32000:sac=on:random_seed=2363199554:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 135.10/19.37 % (824682)Instruction limit reached! % 135.10/19.37 % (824682)------------------------------ % 135.10/19.37 % (824682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.10/19.37 % (824682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.10/19.37 % (824682)CaDiCaL version: 2.1.3 % 135.10/19.37 % (824682)Termination reason: Instruction limit % 135.10/19.37 % (824682)Termination phase: Saturation % 135.10/19.37 % (824682)Time elapsed: 3.587 s % 135.10/19.37 % (824682)Peak memory usage: 87 MB % 135.10/19.37 % (824682)Instructions burned: 11407 (million) % 135.10/19.37 % (824688)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4088276846:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 174.07/24.86 % (824678)Instruction limit reached! % 174.07/24.86 % (824678)------------------------------ % 174.07/24.86 % (824678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.07/24.86 % (824678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.07/24.86 % (824678)CaDiCaL version: 2.1.3 % 174.07/24.86 % (824678)Termination reason: Instruction limit % 174.07/24.86 % (824678)Termination phase: Saturation % 174.07/24.86 % (824678)Time elapsed: 10.875 s % 174.07/24.86 % (824678)Peak memory usage: 56 MB % 174.07/24.86 % (824678)Instructions burned: 20140 (million) % 174.07/24.86 % (825043)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1435611804:s2a=on:i=53295_2839 on theBenchmark for (2839ds/53295Mi) % 174.07/24.86 % (824688)Instruction limit reached! % 174.07/24.86 % (824688)------------------------------ % 174.07/24.86 % (824688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.07/24.86 % (824688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.07/24.86 % (824688)CaDiCaL version: 2.1.3 % 174.07/24.86 % (824688)Termination reason: Instruction limit % 174.07/24.86 % (824688)Termination phase: Saturation % 174.07/24.86 % (824688)Time elapsed: 5.453 s % 174.07/24.86 % (824688)Peak memory usage: 261 MB % 174.07/24.86 % (824688)Instructions burned: 17628 (million) % 174.07/24.86 % (825051)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2118985024:i=26857:ins=20_2826 on theBenchmark for (2826ds/26857Mi) % 174.07/24.86 % (825051)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.07/24.86 % (825051)Terminated due to inappropriate strategy. % 174.07/24.86 % (825051)------------------------------ % 174.07/24.86 % (825051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.07/24.86 % (825051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.07/24.86 % (825051)CaDiCaL version: 2.1.3 % 174.07/24.86 % (825051)Termination reason: Inappropriate % 174.07/24.86 % (825051)Time elapsed: 0.016 s % 174.07/24.86 % (825051)Peak memory usage: 12 MB % 174.07/24.86 % (825051)Instructions burned: 70 (million) % 174.07/24.86 % (825051)------------------------------ % 174.07/24.86 % (825051)------------------------------ % 174.07/24.86 % (825053)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1607523891:i=28120:bs=on:fsr=off_2826 on theBenchmark for (2826ds/28120Mi) % 174.07/24.86 % (824684)Instruction limit reached! % 174.07/24.86 % (824684)------------------------------ % 174.07/24.86 % (824684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.07/24.86 % (824684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.07/24.86 % (824684)CaDiCaL version: 2.1.3 % 174.07/24.86 % (824684)Termination reason: Instruction limit % 174.07/24.86 % (824684)Termination phase: Saturation % 174.07/24.86 % (824684)Time elapsed: 9.228 s % 174.07/24.86 % (824684)Peak memory usage: 60 MB % 174.07/24.86 % (824684)Instructions burned: 14134 (million) % 174.07/24.86 % (825055)fmb+10_1_sil=256000:fmbss=7:random_seed=40015851:fmbsr=1.6:i=182295_2822 on theBenchmark for (2822ds/182295Mi) % 174.07/24.86 % (825055)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.07/24.86 % (825055)Terminated due to inappropriate strategy. % 174.07/24.86 % (825055)------------------------------ % 174.07/24.86 % (825055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.07/24.86 % (825055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.07/24.86 % (825055)CaDiCaL version: 2.1.3 % 174.07/24.86 % (825055)Termination reason: Inappropriate % 174.07/24.86 % (825055)Time elapsed: 0.030 s % 174.07/24.86 % (825055)Peak memory usage: 12 MB % 174.07/24.86 % (825055)Instructions burned: 70 (million) % 174.07/24.86 % (825055)------------------------------ % 174.07/24.86 % (825055)------------------------------ % 174.07/24.86 % (825057)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2948441442:i=44625:gsp=on_2822 on theBenchmark for (2822ds/44625Mi) % 174.07/24.86 % (825057)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 174.07/24.86 % (825057)Terminated due to inappropriate strategy. % 174.07/24.86 % (825057)------------------------------ % 174.07/24.86 % (825057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.07/24.86 % (825057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.07/24.86 % (825057)CaDiCaL version: 2.1.3 % 164.09/25.82 % (825057)Termination reason: Inappropriate % 164.09/25.82 % (825057)Time elapsed: 0.044 s % 164.09/25.82 % (825057)Peak memory usage: 12 MB % 164.09/25.82 % (825057)Instructions burned: 105 (million) % 164.09/25.82 % (825057)------------------------------ % 164.09/25.82 % (825057)------------------------------ % 164.09/25.82 % (825059)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=778186200:i=160505_2821 on theBenchmark for (2821ds/160505Mi) % 164.09/25.82 % (825059)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.09/25.82 % (825059)Terminated due to inappropriate strategy. % 164.09/25.82 % (825059)------------------------------ % 164.09/25.82 % (825059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.09/25.82 % (825059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.09/25.82 % (825059)CaDiCaL version: 2.1.3 % 164.09/25.82 % (825059)Termination reason: Inappropriate % 164.09/25.82 % (825059)Time elapsed: 0.030 s % 164.09/25.82 % (825059)Peak memory usage: 12 MB % 164.09/25.82 % (825059)Instructions burned: 70 (million) % 164.09/25.82 % (825059)------------------------------ % 164.09/25.82 % (825059)------------------------------ % 164.09/25.82 % (825061)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3915417729:fmbsr=1.3:i=225729_2821 on theBenchmark for (2821ds/225729Mi) % 164.09/25.82 % (825061)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.09/25.82 % (825061)Terminated due to inappropriate strategy. % 164.09/25.82 % (825061)------------------------------ % 164.09/25.82 % (825061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.09/25.82 % (825061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.09/25.82 % (825061)CaDiCaL version: 2.1.3 % 164.09/25.82 % (825061)Termination reason: Inappropriate % 164.09/25.82 % (825061)Time elapsed: 0.030 s % 164.09/25.82 % (825061)Peak memory usage: 12 MB % 164.09/25.82 % (825061)Instructions burned: 70 (million) % 164.09/25.82 % (825061)------------------------------ % 164.09/25.82 % (825061)------------------------------ % 164.09/25.82 % (825063)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2162652199:fmbsr=2:i=185024:ins=7_2820 on theBenchmark for (2820ds/185024Mi) % 164.09/25.82 % (825063)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.09/25.82 % (825063)Terminated due to inappropriate strategy. % 164.09/25.82 % (825063)------------------------------ % 164.09/25.82 % (825063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.09/25.82 % (825063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.09/25.82 % (825063)CaDiCaL version: 2.1.3 % 164.09/25.82 % (825063)Termination reason: Inappropriate % 164.09/25.82 % (825063)Time elapsed: 0.030 s % 164.09/25.82 % (825063)Peak memory usage: 12 MB % 164.09/25.82 % (825063)Instructions burned: 70 (million) % 164.09/25.82 % (825063)------------------------------ % 164.09/25.82 % (825063)------------------------------ % 164.09/25.82 % (825065)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1666532790:rtra=on_2820 on theBenchmark for (2820ds/0Mi) % 164.09/25.82 % (825065)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 164.09/25.82 % (825065)Terminated due to inappropriate strategy. % 164.09/25.82 % (825065)------------------------------ % 164.09/25.82 % (825065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.09/25.82 % (825065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.09/25.82 % (825065)CaDiCaL version: 2.1.3 % 164.09/25.82 % (825065)Termination reason: Inappropriate % 164.09/25.82 % (825065)Time elapsed: 0.103 s % 164.09/25.82 % (825065)Peak memory usage: 13 MB % 164.09/25.82 % (825065)Instructions burned: 210 (million) % 164.09/25.82 % (825065)------------------------------ % 164.09/25.82 % (825065)------------------------------ % 164.09/25.82 % (825067)% WARNING: option uhcvi not known. % 164.09/25.82 % (825067)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2222139559:i=271062:add=off:rtra=on:rawr=on_2818 on theBenchmark for (2818ds/271062Mi) % 164.09/25.82 % (824662)Instruction limit reached! % 164.09/25.82 % (824662)------------------------------ % 164.09/25.82 % (824662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.09/25.82 % (824662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.09/25.82 % (824662)CaDiCaL version: 2.1.3 % 164.09/25.82 % (824662)Termination reason: Instruction limit % 164.09/25.82 % (824662)Termination phase: Saturation % 164.09/25.82 % (824662)Time elapsed: 16.587 s % 164.09/25.82 % (824662)Peak memory usage: 82 MB % 164.09/25.82 % (824662)Instructions burned: 29342 (million) % 190.67/27.19 % (825069)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2292992353:i=176048:add=on:rtra=on:rawr=on_2808 on theBenchmark for (2808ds/176048Mi) % 190.67/27.19 % (825053)Instruction limit reached! % 190.67/27.19 % (825053)------------------------------ % 190.67/27.19 % (825053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.67/27.19 % (825053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.67/27.19 % (825053)CaDiCaL version: 2.1.3 % 190.67/27.19 % (825053)Termination reason: Instruction limit % 190.67/27.19 % (825053)Termination phase: Saturation % 190.67/27.19 % (825053)Time elapsed: 6.864 s % 190.67/27.19 % (825053)Peak memory usage: 43 MB % 190.67/27.19 % (825053)Instructions burned: 28125 (million) % 190.67/27.19 % (825071)dis+10_1_sil=32000:si=on:sp=arity:random_seed=4056715637:i=206:fgj=on:rtra=on_2757 on theBenchmark for (2757ds/206Mi) % 190.67/27.19 % (825071)Instruction limit reached! % 190.67/27.19 % (825071)------------------------------ % 190.67/27.19 % (825071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.67/27.19 % (825071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.67/27.19 % (825071)CaDiCaL version: 2.1.3 % 190.67/27.19 % (825071)Termination reason: Instruction limit % 190.67/27.19 % (825071)Termination phase: Saturation % 190.67/27.19 % (825071)Time elapsed: 0.058 s % 190.67/27.19 % (825071)Peak memory usage: 17 MB % 190.67/27.19 % (825071)Instructions burned: 208 (million) % 190.67/27.19 % (825073)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=18587901:i=232:rtra=on_2756 on theBenchmark for (2756ds/232Mi) % 190.67/27.19 % (825073)Instruction limit reached! % 190.67/27.19 % (825073)------------------------------ % 190.67/27.19 % (825073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.67/27.19 % (825073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.67/27.19 % (825073)CaDiCaL version: 2.1.3 % 190.67/27.19 % (825073)Termination reason: Instruction limit % 190.67/27.19 % (825073)Termination phase: Blocked clause elimination % 190.67/27.19 % (825073)Time elapsed: 0.058 s % 190.67/27.19 % (825073)Peak memory usage: 13 MB % 190.67/27.19 % (825073)Instructions burned: 236 (million) % 190.67/27.19 % (825075)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2484612973:i=262:rtra=on_2756 on theBenchmark for (2756ds/262Mi) % 190.67/27.19 % (825075)Instruction limit reached! % 190.67/27.19 % (825075)------------------------------ % 190.67/27.19 % (825075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.67/27.19 % (825075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.67/27.19 % (825075)CaDiCaL version: 2.1.3 % 190.67/27.19 % (825075)Termination reason: Instruction limit % 190.67/27.19 % (825075)Termination phase: Saturation % 190.67/27.19 % (825075)Time elapsed: 0.077 s % 190.67/27.19 % (825075)Peak memory usage: 18 MB % 190.67/27.19 % (825075)Instructions burned: 263 (million) % 190.67/27.19 % (825077)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1568623021:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2755 on theBenchmark for (2755ds/318Mi) % 190.67/27.19 % (825077)Instruction limit reached! % 190.67/27.19 % (825077)------------------------------ % 190.67/27.19 % (825077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.67/27.19 % (825077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.67/27.19 % (825077)CaDiCaL version: 2.1.3 % 190.67/27.19 % (825077)Termination reason: Instruction limit % 190.67/27.19 % (825077)Termination phase: Saturation % 190.67/27.19 % (825077)Time elapsed: 0.096 s % 190.67/27.19 % (825077)Peak memory usage: 18 MB % 190.67/27.19 % (825077)Instructions burned: 320 (million) % 190.67/27.19 % (825079)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4287133773:i=1428:nm=2:rtra=on_2754 on theBenchmark for (2754ds/1428Mi) % 190.67/27.19 % (825079)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 190.67/27.19 % (825079)Terminated due to inappropriate strategy. % 190.67/27.19 % (825079)------------------------------ % 190.67/27.19 % (825079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 190.67/27.19 % (825079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.67/27.19 % (825079)CaDiCaL version: 2.1.3 % 190.67/27.19 % (825079)Termination reason: Inappropriate % 190.67/27.19 % (825079)Time elapsed: 0.016 s % 190.67/27.19 % (825079)Peak memory usage: 12 MB % 190.67/27.19 % (825079)Instructions burned: 66 (million) % 210.35/29.91 % (825079)------------------------------ % 210.35/29.91 % (825079)------------------------------ % 210.35/29.91 % (825081)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=193095395:i=262:bd=preordered:rtra=on:fsd=on_2753 on theBenchmark for (2753ds/262Mi) % 210.35/29.91 % (825081)Instruction limit reached! % 210.35/29.91 % (825081)------------------------------ % 210.35/29.91 % (825081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.35/29.91 % (825081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.35/29.91 % (825081)CaDiCaL version: 2.1.3 % 210.35/29.91 % (825081)Termination reason: Instruction limit % 210.35/29.91 % (825081)Termination phase: Saturation % 210.35/29.91 % (825081)Time elapsed: 0.070 s % 210.35/29.91 % (825081)Peak memory usage: 16 MB % 210.35/29.91 % (825081)Instructions burned: 263 (million) % 210.35/29.91 % (825083)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=416626371:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2753 on theBenchmark for (2753ds/1368Mi) % 210.35/29.91 % (824686)Instruction limit reached! % 210.35/29.91 % (824686)------------------------------ % 210.35/29.91 % (824686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.35/29.91 % (824686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.35/29.91 % (824686)CaDiCaL version: 2.1.3 % 210.35/29.91 % (824686)Termination reason: Instruction limit % 210.35/29.91 % (824686)Termination phase: Clausification % 210.35/29.91 % (824686)Time elapsed: 16.201 s % 210.35/29.91 % (824686)Peak memory usage: 8624 MB % 210.35/29.91 % (824686)Instructions burned: 15852 (million) % 210.35/29.91 % (825083)Instruction limit reached! % 210.35/29.91 % (825083)------------------------------ % 210.35/29.91 % (825083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.35/29.91 % (825083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.35/29.91 % (825083)CaDiCaL version: 2.1.3 % 210.35/29.91 % (825083)Termination reason: Instruction limit % 210.35/29.91 % (825083)Termination phase: Saturation % 210.35/29.91 % (825083)Time elapsed: 0.400 s % 210.35/29.91 % (825083)Peak memory usage: 28 MB % 210.35/29.91 % (825083)Instructions burned: 1369 (million) % 210.35/29.91 % (825085)ott-21_1_sil=16000:si=on:fs=off:random_seed=481915551:i=360:av=off:fsr=off:rtra=on_2748 on theBenchmark for (2748ds/360Mi) % 210.35/29.91 % (825085)Instruction limit reached! % 210.35/29.91 % (825085)------------------------------ % 210.35/29.91 % (825085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.35/29.91 % (825085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.35/29.91 % (825085)CaDiCaL version: 2.1.3 % 210.35/29.91 % (825085)Termination reason: Instruction limit % 210.35/29.91 % (825085)Termination phase: Saturation % 210.35/29.91 % (825085)Time elapsed: 0.093 s % 210.35/29.91 % (825085)Peak memory usage: 16 MB % 210.35/29.91 % (825085)Instructions burned: 365 (million) % 210.35/29.91 % (825087)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1793913698:i=954:bd=all:rtra=on_2747 on theBenchmark for (2747ds/954Mi) % 210.35/29.91 % (825087)Instruction limit reached! % 210.35/29.91 % (825087)------------------------------ % 210.35/29.91 % (825087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.35/29.91 % (825087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.35/29.91 % (825087)CaDiCaL version: 2.1.3 % 210.35/29.91 % (825087)Termination reason: Instruction limit % 210.35/29.91 % (825087)Termination phase: Saturation % 210.35/29.91 % (825087)Time elapsed: 0.298 s % 210.35/29.91 % (825087)Peak memory usage: 20 MB % 210.35/29.91 % (825087)Instructions burned: 955 (million) % 210.35/29.91 % (825089)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3156996432:fmbsr=1.3:i=1730:ins=25:rtra=on_2744 on theBenchmark for (2744ds/1730Mi) % 210.35/29.91 % (825089)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 210.35/29.91 % (825089)Terminated due to inappropriate strategy. % 210.35/29.91 % (825089)------------------------------ % 210.35/29.91 % (825089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 210.35/29.91 % (825089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.35/29.91 % (825089)CaDiCaL version: 2.1.3 % 210.35/29.91 % (825089)Termination reason: Inappropriate % 210.35/29.91 % (825089)Time elapsed: 0.022 s % 210.35/29.91 % (825089)Peak memory usage: 14 MB % 210.35/29.91 % (825089)Instructions burned: 86 (million) % 210.35/29.91 % (825089)------------------------------ % 255.73/36.32 % (825089)------------------------------ % 255.73/36.32 % (825091)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4288542192:i=2358:rtra=on_2744 on theBenchmark for (2744ds/2358Mi) % 255.73/36.32 % (825093)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=817186130:i=1778:ins=1:rtra=on_2740 on theBenchmark for (2740ds/1778Mi) % 255.73/36.32 % (825093)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.73/36.32 % (825093)Terminated due to inappropriate strategy. % 255.73/36.32 % (825093)------------------------------ % 255.73/36.32 % (825093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.73/36.32 % (825093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.73/36.32 % (825093)CaDiCaL version: 2.1.3 % 255.73/36.32 % (825093)Termination reason: Inappropriate % 255.73/36.32 % (825093)Time elapsed: 0.033 s % 255.73/36.32 % (825093)Peak memory usage: 12 MB % 255.73/36.32 % (825093)Instructions burned: 74 (million) % 255.73/36.32 % (825093)------------------------------ % 255.73/36.32 % (825093)------------------------------ % 255.73/36.32 % (825095)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=1427876836:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/1384Mi) % 255.73/36.32 % (825091)Instruction limit reached! % 255.73/36.32 % (825091)------------------------------ % 255.73/36.32 % (825091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.73/36.32 % (825091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.73/36.32 % (825091)CaDiCaL version: 2.1.3 % 255.73/36.32 % (825091)Termination reason: Instruction limit % 255.73/36.32 % (825091)Termination phase: Saturation % 255.73/36.32 % (825091)Time elapsed: 0.851 s % 255.73/36.32 % (825091)Peak memory usage: 29 MB % 255.73/36.32 % (825091)Instructions burned: 2360 (million) % 255.73/36.32 % (825097)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2702165312:i=1758:kws=inv_precedence:fsr=off:rtra=on_2735 on theBenchmark for (2735ds/1758Mi) % 255.73/36.32 % (825095)Instruction limit reached! % 255.73/36.32 % (825095)------------------------------ % 255.73/36.33 % (825095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.73/36.33 % (825095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.73/36.33 % (825095)CaDiCaL version: 2.1.3 % 255.73/36.33 % (825095)Termination reason: Instruction limit % 255.73/36.33 % (825095)Termination phase: Saturation % 255.73/36.33 % (825095)Time elapsed: 0.860 s % 255.73/36.33 % (825095)Peak memory usage: 27 MB % 255.73/36.33 % (825095)Instructions burned: 1384 (million) % 255.73/36.33 % (825099)fmb+10_1_sil=64000:si=on:random_seed=2694254483:i=44122:nm=2:rtra=on:gsp=on_2731 on theBenchmark for (2731ds/44122Mi) % 255.73/36.33 % (825097)Instruction limit reached! % 255.73/36.33 % (825097)------------------------------ % 255.73/36.33 % (825097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.73/36.33 % (825097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.73/36.33 % (825097)CaDiCaL version: 2.1.3 % 255.73/36.33 % (825097)Termination reason: Instruction limit % 255.73/36.33 % (825097)Termination phase: Saturation % 255.73/36.33 % (825097)Time elapsed: 0.455 s % 255.73/36.33 % (825097)Peak memory usage: 24 MB % 255.73/36.33 % (825097)Instructions burned: 1760 (million) % 255.73/36.33 % (825099)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.73/36.33 % (825099)Terminated due to inappropriate strategy. % 255.73/36.33 % (825099)------------------------------ % 255.73/36.33 % (825099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.73/36.33 % (825099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.73/36.33 % (825099)CaDiCaL version: 2.1.3 % 255.73/36.33 % (825099)Termination reason: Inappropriate % 255.73/36.33 % (825099)Time elapsed: 0.032 s % 255.73/36.33 % (825099)Peak memory usage: 12 MB % 255.73/36.33 % (825099)Instructions burned: 72 (million) % 255.73/36.33 % (825099)------------------------------ % 255.73/36.33 % (825099)------------------------------ % 255.73/36.33 % (825101)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3740949513:i=19030:nm=5:rtra=on_2730 on theBenchmark for (2730ds/19030Mi) % 255.73/36.33 % (825101)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 255.73/36.33 % (825101)Terminated due to inappropriate strategy. % 255.73/36.33 % (825101)------------------------------ % 283.38/40.26 % (825101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.38/40.26 % (825101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.38/40.26 % (825101)CaDiCaL version: 2.1.3 % 283.38/40.26 % (825101)Termination reason: Inappropriate % 283.38/40.26 % (825101)Time elapsed: 0.016 s % 283.38/40.26 % (825101)Peak memory usage: 12 MB % 283.38/40.26 % (825101)Instructions burned: 69 (million) % 283.38/40.26 % (825101)------------------------------ % 283.38/40.26 % (825101)------------------------------ % 283.38/40.26 % (825103)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3327554081:fmbsr=1.7:i=1840:rtra=on_2730 on theBenchmark for (2730ds/1840Mi) % 283.38/40.26 % (825104)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2843497922:i=10262:rtra=on_2730 on theBenchmark for (2730ds/10262Mi) % 283.38/40.26 % (825103)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.38/40.26 % (825103)Terminated due to inappropriate strategy. % 283.38/40.26 % (825103)------------------------------ % 283.38/40.26 % (825103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.38/40.26 % (825103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.38/40.26 % (825103)CaDiCaL version: 2.1.3 % 283.38/40.26 % (825103)Termination reason: Inappropriate % 283.38/40.26 % (825103)Time elapsed: 0.033 s % 283.38/40.26 % (825103)Peak memory usage: 12 MB % 283.38/40.26 % (825103)Instructions burned: 73 (million) % 283.38/40.26 % (825103)------------------------------ % 283.38/40.26 % (825103)------------------------------ % 283.38/40.26 % (825107)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=382980678:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2730 on theBenchmark for (2730ds/2944Mi) % 283.38/40.26 % (825107)Instruction limit reached! % 283.38/40.26 % (825107)------------------------------ % 283.38/40.26 % (825107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.38/40.26 % (825107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.38/40.26 % (825107)CaDiCaL version: 2.1.3 % 283.38/40.26 % (825107)Termination reason: Instruction limit % 283.38/40.26 % (825107)Termination phase: Saturation % 283.38/40.26 % (825107)Time elapsed: 1.484 s % 283.38/40.26 % (825107)Peak memory usage: 46 MB % 283.38/40.26 % (825107)Instructions burned: 2945 (million) % 283.38/40.26 % (825241)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2180492014:i=12648:rtra=on_2715 on theBenchmark for (2715ds/12648Mi) % 283.38/40.26 % (825241)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.38/40.26 % (825241)Terminated due to inappropriate strategy. % 283.38/40.26 % (825241)------------------------------ % 283.38/40.26 % (825241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.38/40.26 % (825241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.38/40.26 % (825241)CaDiCaL version: 2.1.3 % 283.38/40.26 % (825241)Termination reason: Inappropriate % 283.38/40.26 % (825241)Time elapsed: 0.101 s % 283.38/40.26 % (825241)Peak memory usage: 13 MB % 283.38/40.26 % (825241)Instructions burned: 207 (million) % 283.38/40.26 % (825241)------------------------------ % 283.38/40.26 % (825241)------------------------------ % 283.38/40.26 % (825243)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3191723901:fmbsr=2.30978:i=4348:rtra=on_2713 on theBenchmark for (2713ds/4348Mi) % 283.38/40.26 % (825243)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.38/40.26 % (825243)Terminated due to inappropriate strategy. % 283.38/40.26 % (825243)------------------------------ % 283.38/40.26 % (825243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.38/40.26 % (825243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.38/40.26 % (825243)CaDiCaL version: 2.1.3 % 283.38/40.26 % (825243)Termination reason: Inappropriate % 283.38/40.26 % (825243)Time elapsed: 0.032 s % 283.38/40.26 % (825243)Peak memory usage: 12 MB % 283.38/40.26 % (825243)Instructions burned: 73 (million) % 283.38/40.26 % (825243)------------------------------ % 283.38/40.26 % (825243)------------------------------ % 283.38/40.26 % (825245)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4097459656:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2713 on theBenchmark for (2713ds/1738Mi) % 283.38/40.26 % (825245)Instruction limit reached! % 283.38/40.26 % (825245)------------------------------ % 283.38/40.26 % (825245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (825245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (825245)CaDiCaL version: 2.1.3 % 300.48/42.64 % (825245)Termination reason: Instruction limit % 300.48/42.64 % (825245)Termination phase: Saturation % 300.48/42.64 % (825245)Time elapsed: 0.975 s % 300.48/42.64 % (825245)Peak memory usage: 34 MB % 300.48/42.64 % (825245)Instructions burned: 1738 (million) % 300.48/42.64 % (825377)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1194304748:i=10228:av=off:rtra=on_2703 on theBenchmark for (2703ds/10228Mi) % 300.48/42.64 % (825104)Instruction limit reached! % 300.48/42.64 % (825104)------------------------------ % 300.48/42.64 % (825104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (825104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (825104)CaDiCaL version: 2.1.3 % 300.48/42.64 % (825104)Termination reason: Instruction limit % 300.48/42.64 % (825104)Termination phase: Saturation % 300.48/42.64 % (825104)Time elapsed: 3.164 s % 300.48/42.64 % (825104)Peak memory usage: 69 MB % 300.48/42.64 % (825104)Instructions burned: 10264 (million) % 300.48/42.64 % (825379)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2505291189:i=108564:rtra=on_2698 on theBenchmark for (2698ds/108564Mi) % 300.48/42.64 % (825379)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.64 % (825379)Terminated due to inappropriate strategy. % 300.48/42.64 % (825379)------------------------------ % 300.48/42.64 % (825379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (825379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (825379)CaDiCaL version: 2.1.3 % 300.48/42.64 % (825379)Termination reason: Inappropriate % 300.48/42.64 % (825379)Time elapsed: 0.054 s % 300.48/42.64 % (825379)Peak memory usage: 13 MB % 300.48/42.64 % (825379)Instructions burned: 210 (million) % 300.48/42.64 % (825379)------------------------------ % 300.48/42.64 % (825379)------------------------------ % 300.48/42.64 % (825381)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1267086397:i=7024:aac=none:rtra=on_2698 on theBenchmark for (2698ds/7024Mi) % 300.48/42.64 % (825381)Instruction limit reached! % 300.48/42.64 % (825381)------------------------------ % 300.48/42.64 % (825381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (825381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (825381)CaDiCaL version: 2.1.3 % 300.48/42.64 % (825381)Termination reason: Instruction limit % 300.48/42.64 % (825381)Termination phase: Saturation % 300.48/42.64 % (825381)Time elapsed: 2.039 s % 300.48/42.64 % (825381)Peak memory usage: 49 MB % 300.48/42.64 % (825381)Instructions burned: 7025 (million) % 300.48/42.64 % (825384)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=631616646:i=7546:rtra=on:amm=off_2677 on theBenchmark for (2677ds/7546Mi) % 300.48/42.64 % (825384)Instruction limit reached! % 300.48/42.64 % (825384)------------------------------ % 300.48/42.64 % (825384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (825384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (825384)CaDiCaL version: 2.1.3 % 300.48/42.64 % (825384)Termination reason: Instruction limit % 300.48/42.64 % (825384)Termination phase: Saturation % 300.48/42.64 % (825384)Time elapsed: 2.313 s % 300.48/42.64 % (825384)Peak memory usage: 55 MB % 300.48/42.64 % (825384)Instructions burned: 7547 (million) % 300.48/42.64 % (825388)ott+11_1_sil=16000:si=on:gs=on:random_seed=279374088:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2654 on theBenchmark for (2654ds/4502Mi) % 300.48/42.64 % (825388)Instruction limit reached! % 300.48/42.64 % (825388)------------------------------ % 300.48/42.64 % (825388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.48/42.64 % (825388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.48/42.64 % (825388)CaDiCaL version: 2.1.3 % 300.48/42.64 % (825388)Termination reason: Instruction limit % 300.48/42.64 % (825388)Termination phase: Saturation % 300.48/42.64 % (825388)Time elapsed: 1.464 s % 300.48/42.64 % (825388)Peak memory usage: 39 MB % 300.48/42.64 % (825388)Instructions burned: 4503 (million) % 300.48/42.64 % (825390)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=1981172815:fmbsr=1.6:i=135068:rtra=on_2639 on theBenchmark for (2639ds/135068Mi) % 300.48/42.64 % (825390)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 300.48/42.64 % (825390)Terminated due to inappropriate strat % 300.48/42.64 Terminated % 300.48/42.64 % Vampire exiting % 300.48/42.64 Terminated %------------------------------------------------------------------------------