%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW828_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 : n014.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:45:02 PM UTC 2026 % Result : Timeout 300.53s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW828_1 : TPTP v9.3.1. Released v7.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n014.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:30:45 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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.18/0.79 % (1818568)Will run a generic schedule for satisfiability detection. % 3.18/0.79 % (1818576)dis+10_1_sil=32000:sp=arity:random_seed=3268748206:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.18/0.79 % (1818574)% WARNING: option uhcvi not known. % 3.18/0.79 % (1818573)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1501390405_2999 on theBenchmark for (2999ds/0Mi) % 3.18/0.79 % (1818574)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=879058183:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.18/0.79 % (1818575)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2987774937:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.18/0.79 % (1818577)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1391453799:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.18/0.79 % (1818579)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1528935916:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.18/0.79 % (1818578)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=543225265:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.18/0.79 % (1818576)Instruction limit reached! % 3.18/0.79 % (1818576)------------------------------ % 3.18/0.79 % (1818576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.18/0.79 % (1818576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.18/0.79 % (1818576)CaDiCaL version: 2.1.3 % 3.18/0.79 % (1818576)Termination reason: Instruction limit % 3.18/0.79 % (1818576)Termination phase: Saturation % 3.18/0.79 % (1818576)Time elapsed: 0.027 s % 3.18/0.79 % (1818576)Peak memory usage: 13 MB % 3.18/0.79 % (1818576)Instructions burned: 104 (million) % 3.18/0.79 % (1818587)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3851329012:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.18/0.79 % (1818573)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.18/0.79 % (1818573)Terminated due to inappropriate strategy. % 3.18/0.79 % (1818573)------------------------------ % 3.18/0.79 % (1818573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.18/0.79 % (1818573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.18/0.79 % (1818573)CaDiCaL version: 2.1.3 % 3.18/0.79 % (1818573)Termination reason: Inappropriate % 3.18/0.79 % (1818573)Time elapsed: 0.039 s % 3.18/0.79 % (1818573)Peak memory usage: 12 MB % 3.18/0.79 % (1818573)Instructions burned: 82 (million) % 3.18/0.79 % (1818573)------------------------------ % 3.18/0.79 % (1818573)------------------------------ % 3.18/0.79 % (1818587)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 3.18/0.79 % (1818587)Terminated due to inappropriate strategy. % 3.18/0.79 % (1818587)------------------------------ % 3.18/0.79 % (1818587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.18/0.79 % (1818587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.18/0.79 % (1818587)CaDiCaL version: 2.1.3 % 3.18/0.79 % (1818587)Termination reason: Inappropriate % 3.18/0.79 % (1818587)Time elapsed: 0.020 s % 3.18/0.79 % (1818587)Peak memory usage: 12 MB % 3.18/0.79 % (1818587)Instructions burned: 81 (million) % 3.18/0.79 % (1818587)------------------------------ % 3.18/0.79 % (1818587)------------------------------ % 3.18/0.79 % (1818577)Instruction limit reached! % 3.18/0.79 % (1818577)------------------------------ % 3.18/0.79 % (1818577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.18/0.79 % (1818577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.18/0.79 % (1818577)CaDiCaL version: 2.1.3 % 3.18/0.79 % (1818577)Termination reason: Instruction limit % 3.18/0.79 % (1818577)Termination phase: Saturation % 3.18/0.79 % (1818577)Time elapsed: 0.058 s % 3.18/0.79 % (1818577)Peak memory usage: 13 MB % 3.18/0.79 % (1818577)Instructions burned: 117 (million) % 3.18/0.79 % (1818589)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1263227537:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 3.18/0.79 % (1818578)Instruction limit reached! % 3.18/0.79 % (1818578)------------------------------ % 3.18/0.79 % (1818578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.18/0.79 % (1818578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.18/0.79 % (1818578)CaDiCaL version: 2.1.3 % 3.18/0.79 % (1818578)Termination reason: Instruction limit % 6.65/1.22 % (1818578)Termination phase: Saturation % 6.65/1.22 % (1818578)Time elapsed: 0.069 s % 6.65/1.22 % (1818578)Peak memory usage: 14 MB % 6.65/1.22 % (1818578)Instructions burned: 132 (million) % 6.65/1.22 % (1818591)ott-21_1_sil=16000:fs=off:random_seed=3772481176:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.65/1.22 % (1818579)Instruction limit reached! % 6.65/1.22 % (1818579)------------------------------ % 6.65/1.22 % (1818579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.22 % (1818579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.22 % (1818579)CaDiCaL version: 2.1.3 % 6.65/1.22 % (1818579)Termination reason: Instruction limit % 6.65/1.22 % (1818579)Termination phase: Saturation % 6.65/1.22 % (1818579)Time elapsed: 0.088 s % 6.65/1.22 % (1818579)Peak memory usage: 14 MB % 6.65/1.22 % (1818579)Instructions burned: 160 (million) % 6.65/1.22 % (1818594)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3682777465:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.65/1.22 % (1818590)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=4102814715:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.65/1.22 % (1818596)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2922728290:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 6.65/1.22 % (1818591)Instruction limit reached! % 6.65/1.22 % (1818591)------------------------------ % 6.65/1.22 % (1818591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.22 % (1818591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.22 % (1818591)CaDiCaL version: 2.1.3 % 6.65/1.22 % (1818591)Termination reason: Instruction limit % 6.65/1.22 % (1818591)Termination phase: Saturation % 6.65/1.22 % (1818591)Time elapsed: 0.046 s % 6.65/1.22 % (1818591)Peak memory usage: 14 MB % 6.65/1.22 % (1818591)Instructions burned: 182 (million) % 6.65/1.22 % (1818608)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2542559980:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 6.65/1.22 % (1818589)Instruction limit reached! % 6.65/1.22 % (1818589)------------------------------ % 6.65/1.22 % (1818589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.22 % (1818589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.22 % (1818589)CaDiCaL version: 2.1.3 % 6.65/1.22 % (1818589)Termination reason: Instruction limit % 6.65/1.22 % (1818589)Termination phase: Saturation % 6.65/1.22 % (1818589)Time elapsed: 0.071 s % 6.65/1.22 % (1818589)Peak memory usage: 14 MB % 6.65/1.22 % (1818589)Instructions burned: 132 (million) % 6.65/1.22 % (1818596)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.65/1.22 % (1818596)Terminated due to inappropriate strategy. % 6.65/1.22 % (1818596)------------------------------ % 6.65/1.22 % (1818596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.22 % (1818596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.22 % (1818596)CaDiCaL version: 2.1.3 % 6.65/1.22 % (1818596)Termination reason: Inappropriate % 6.65/1.22 % (1818596)Time elapsed: 0.037 s % 6.65/1.22 % (1818596)Peak memory usage: 12 MB % 6.65/1.22 % (1818596)Instructions burned: 81 (million) % 6.65/1.22 % (1818596)------------------------------ % 6.65/1.22 % (1818596)------------------------------ % 6.65/1.22 % (1818612)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1273329328:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 6.65/1.22 % (1818617)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=3891218173: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) % 6.65/1.22 % (1818612)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 6.65/1.22 % (1818612)Terminated due to inappropriate strategy. % 6.65/1.22 % (1818612)------------------------------ % 6.65/1.22 % (1818612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.65/1.22 % (1818612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.65/1.22 % (1818612)CaDiCaL version: 2.1.3 % 6.65/1.22 % (1818612)Termination reason: Inappropriate % 6.65/1.22 % (1818612)Time elapsed: 0.038 s % 6.65/1.22 % (1818612)Peak memory usage: 12 MB % 28.73/4.39 % (1818612)Instructions burned: 82 (million) % 28.73/4.39 % (1818612)------------------------------ % 28.73/4.39 % (1818612)------------------------------ % 28.73/4.39 % (1818635)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=222077929:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 28.73/4.39 % (1818594)Instruction limit reached! % 28.73/4.39 % (1818594)------------------------------ % 28.73/4.39 % (1818594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.73/4.39 % (1818594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.73/4.39 % (1818594)CaDiCaL version: 2.1.3 % 28.73/4.39 % (1818594)Termination reason: Instruction limit % 28.73/4.39 % (1818594)Termination phase: Saturation % 28.73/4.39 % (1818594)Time elapsed: 0.296 s % 28.73/4.39 % (1818594)Peak memory usage: 16 MB % 28.73/4.39 % (1818594)Instructions burned: 478 (million) % 28.73/4.39 % (1818690)fmb+10_1_sil=64000:random_seed=4032795078:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 28.73/4.39 % (1818590)Instruction limit reached! % 28.73/4.39 % (1818590)------------------------------ % 28.73/4.39 % (1818590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.73/4.39 % (1818590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.73/4.39 % (1818590)CaDiCaL version: 2.1.3 % 28.73/4.39 % (1818590)Termination reason: Instruction limit % 28.73/4.39 % (1818590)Termination phase: Saturation % 28.73/4.39 % (1818590)Time elapsed: 0.345 s % 28.73/4.39 % (1818590)Peak memory usage: 15 MB % 28.73/4.39 % (1818590)Instructions burned: 685 (million) % 28.73/4.39 % (1818690)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.73/4.39 % (1818690)Terminated due to inappropriate strategy. % 28.73/4.39 % (1818690)------------------------------ % 28.73/4.39 % (1818690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.73/4.39 % (1818690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.73/4.39 % (1818690)CaDiCaL version: 2.1.3 % 28.73/4.39 % (1818690)Termination reason: Inappropriate % 28.73/4.39 % (1818690)Time elapsed: 0.040 s % 28.73/4.39 % (1818690)Peak memory usage: 12 MB % 28.73/4.39 % (1818690)Instructions burned: 82 (million) % 28.73/4.39 % (1818690)------------------------------ % 28.73/4.39 % (1818690)------------------------------ % 28.73/4.39 % (1818708)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=657205639:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 28.73/4.39 % (1818710)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3024598307:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 28.73/4.39 % (1818608)Instruction limit reached! % 28.73/4.39 % (1818608)------------------------------ % 28.73/4.39 % (1818608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.73/4.39 % (1818608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.73/4.39 % (1818608)CaDiCaL version: 2.1.3 % 28.73/4.39 % (1818608)Termination reason: Instruction limit % 28.73/4.39 % (1818608)Termination phase: Saturation % 28.73/4.39 % (1818608)Time elapsed: 0.365 s % 28.73/4.39 % (1818608)Peak memory usage: 23 MB % 28.73/4.39 % (1818608)Instructions burned: 1181 (million) % 28.73/4.39 % (1818708)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.73/4.39 % (1818708)Terminated due to inappropriate strategy. % 28.73/4.39 % (1818708)------------------------------ % 28.73/4.39 % (1818708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.73/4.39 % (1818708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.73/4.39 % (1818708)CaDiCaL version: 2.1.3 % 28.73/4.39 % (1818708)Termination reason: Inappropriate % 28.73/4.39 % (1818708)Time elapsed: 0.041 s % 28.73/4.39 % (1818708)Peak memory usage: 12 MB % 28.73/4.39 % (1818708)Instructions burned: 81 (million) % 28.73/4.39 % (1818708)------------------------------ % 28.73/4.39 % (1818708)------------------------------ % 28.73/4.39 % (1818722)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1278235518:i=5131_2994 on theBenchmark for (2994ds/5131Mi) % 28.73/4.39 % (1818710)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 28.73/4.39 % (1818710)Terminated due to inappropriate strategy. % 28.73/4.39 % (1818710)------------------------------ % 28.73/4.39 % (1818710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 28.73/4.39 % (1818710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.08/6.05 % (1818710)CaDiCaL version: 2.1.3 % 41.08/6.05 % (1818710)Termination reason: Inappropriate % 41.08/6.05 % (1818710)Time elapsed: 0.037 s % 41.08/6.05 % (1818710)Peak memory usage: 12 MB % 41.08/6.05 % (1818710)Instructions burned: 81 (million) % 41.08/6.05 % (1818710)------------------------------ % 41.08/6.05 % (1818710)------------------------------ % 41.08/6.05 % (1818724)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3948729588:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi) % 41.08/6.05 % (1818727)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1065860839:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 41.08/6.05 % (1818617)Instruction limit reached! % 41.08/6.05 % (1818617)------------------------------ % 41.08/6.05 % (1818617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.08/6.05 % (1818617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.08/6.05 % (1818617)CaDiCaL version: 2.1.3 % 41.08/6.05 % (1818617)Termination reason: Instruction limit % 41.08/6.05 % (1818617)Termination phase: Saturation % 41.08/6.05 % (1818617)Time elapsed: 0.412 s % 41.08/6.05 % (1818617)Peak memory usage: 19 MB % 41.08/6.05 % (1818617)Instructions burned: 693 (million) % 41.08/6.05 % (1818727)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.08/6.05 % (1818727)Terminated due to inappropriate strategy. % 41.08/6.05 % (1818727)------------------------------ % 41.08/6.05 % (1818727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.08/6.05 % (1818727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.08/6.05 % (1818727)CaDiCaL version: 2.1.3 % 41.08/6.05 % (1818727)Termination reason: Inappropriate % 41.08/6.05 % (1818727)Time elapsed: 0.056 s % 41.08/6.05 % (1818727)Peak memory usage: 12 MB % 41.08/6.05 % (1818727)Instructions burned: 82 (million) % 41.08/6.05 % (1818727)------------------------------ % 41.08/6.05 % (1818727)------------------------------ % 41.08/6.05 % (1818742)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2614600925:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 41.08/6.05 % (1818745)ott-2_1_sil=16000:newcnf=on:random_seed=617346386:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 41.08/6.05 % (1818742)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.08/6.05 % (1818742)Terminated due to inappropriate strategy. % 41.08/6.05 % (1818742)------------------------------ % 41.08/6.05 % (1818742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.08/6.05 % (1818742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.08/6.05 % (1818742)CaDiCaL version: 2.1.3 % 41.08/6.05 % (1818742)Termination reason: Inappropriate % 41.08/6.05 % (1818742)Time elapsed: 0.046 s % 41.08/6.05 % (1818742)Peak memory usage: 12 MB % 41.08/6.05 % (1818742)Instructions burned: 81 (million) % 41.08/6.05 % (1818742)------------------------------ % 41.08/6.05 % (1818742)------------------------------ % 41.08/6.05 % (1818761)ott+10_1_sil=32000:tgt=ground:random_seed=2779822101:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 41.08/6.05 % (1818635)Instruction limit reached! % 41.08/6.05 % (1818635)------------------------------ % 41.08/6.05 % (1818635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.08/6.05 % (1818635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.08/6.05 % (1818635)CaDiCaL version: 2.1.3 % 41.08/6.05 % (1818635)Termination reason: Instruction limit % 41.08/6.05 % (1818635)Termination phase: Saturation % 41.08/6.05 % (1818635)Time elapsed: 0.616 s % 41.08/6.05 % (1818635)Peak memory usage: 19 MB % 41.08/6.05 % (1818635)Instructions burned: 879 (million) % 41.08/6.05 % (1818781)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=636408197:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 41.08/6.05 % (1818781)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 41.08/6.05 % (1818781)Terminated due to inappropriate strategy. % 41.08/6.05 % (1818781)------------------------------ % 41.08/6.05 % (1818781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.08/6.05 % (1818781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.08/6.05 % (1818781)CaDiCaL version: 2.1.3 % 41.08/6.05 % (1818781)Termination reason: Inappropriate % 41.08/6.05 % (1818781)Time elapsed: 0.072 s % 41.08/6.05 % (1818781)Peak memory usage: 12 MB % 41.08/6.05 % (1818781)Instructions burned: 82 (million) % 158.98/22.62 % (1818781)------------------------------ % 158.98/22.62 % (1818781)------------------------------ % 158.98/22.62 % (1818786)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=555152453:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi) % 158.98/22.62 % (1818745)Instruction limit reached! % 158.98/22.62 % (1818745)------------------------------ % 158.98/22.62 % (1818745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/22.62 % (1818745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/22.62 % (1818745)CaDiCaL version: 2.1.3 % 158.98/22.62 % (1818745)Termination reason: Instruction limit % 158.98/22.62 % (1818745)Termination phase: Saturation % 158.98/22.62 % (1818745)Time elapsed: 0.786 s % 158.98/22.62 % (1818745)Peak memory usage: 18 MB % 158.98/22.62 % (1818745)Instructions burned: 869 (million) % 158.98/22.62 % (1818796)dis+21_1_sil=32000:sas=cadical:random_seed=44416364:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 158.98/22.62 % (1818724)Instruction limit reached! % 158.98/22.62 % (1818724)------------------------------ % 158.98/22.62 % (1818724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/22.62 % (1818724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/22.62 % (1818724)CaDiCaL version: 2.1.3 % 158.98/22.62 % (1818724)Termination reason: Instruction limit % 158.98/22.62 % (1818724)Termination phase: Saturation % 158.98/22.62 % (1818724)Time elapsed: 1.143 s % 158.98/22.62 % (1818724)Peak memory usage: 27 MB % 158.98/22.62 % (1818724)Instructions burned: 1474 (million) % 158.98/22.62 % (1818809)ott+11_1_sil=16000:gs=on:random_seed=2834002172:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi) % 158.98/22.62 % (1818722)Instruction limit reached! % 158.98/22.62 % (1818722)------------------------------ % 158.98/22.62 % (1818722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/22.62 % (1818722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/22.62 % (1818722)CaDiCaL version: 2.1.3 % 158.98/22.62 % (1818722)Termination reason: Instruction limit % 158.98/22.62 % (1818722)Termination phase: Saturation % 158.98/22.62 % (1818722)Time elapsed: 2.439 s % 158.98/22.62 % (1818722)Peak memory usage: 47 MB % 158.98/22.62 % (1818722)Instructions burned: 5132 (million) % 158.98/22.62 % (1818821)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2311789225:fmbsr=1.6:i=67534_2969 on theBenchmark for (2969ds/67534Mi) % 158.98/22.62 % (1818821)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 158.98/22.62 % (1818821)Terminated due to inappropriate strategy. % 158.98/22.62 % (1818821)------------------------------ % 158.98/22.62 % (1818821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/22.62 % (1818821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/22.62 % (1818821)CaDiCaL version: 2.1.3 % 158.98/22.62 % (1818821)Termination reason: Inappropriate % 158.98/22.62 % (1818821)Time elapsed: 0.072 s % 158.98/22.62 % (1818821)Peak memory usage: 12 MB % 158.98/22.62 % (1818821)Instructions burned: 81 (million) % 158.98/22.62 % (1818821)------------------------------ % 158.98/22.62 % (1818821)------------------------------ % 158.98/22.62 % (1818825)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3256842872:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2968 on theBenchmark for (2968ds/4591Mi) % 158.98/22.62 % (1818809)Instruction limit reached! % 158.98/22.62 % (1818809)------------------------------ % 158.98/22.62 % (1818809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/22.62 % (1818809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/22.62 % (1818809)CaDiCaL version: 2.1.3 % 158.98/22.62 % (1818809)Termination reason: Instruction limit % 158.98/22.62 % (1818809)Termination phase: Saturation % 158.98/22.62 % (1818809)Time elapsed: 2.298 s % 158.98/22.62 % (1818809)Peak memory usage: 34 MB % 158.98/22.62 % (1818809)Instructions burned: 2251 (million) % 158.98/22.62 % (1818827)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=412617171:i=29340_2959 on theBenchmark for (2959ds/29340Mi) % 158.98/22.62 % (1818786)Instruction limit reached! % 158.98/22.62 % (1818786)------------------------------ % 158.98/22.62 % (1818786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.98/22.62 % (1818786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.98/22.62 % (1818786)CaDiCaL version: 2.1.3 % 158.98/22.62 % (1818786)Termination reason: Instruction limit % 198.38/28.19 % (1818786)Termination phase: Saturation % 198.38/28.19 % (1818786)Time elapsed: 3.131 s % 198.38/28.19 % (1818786)Peak memory usage: 35 MB % 198.38/28.19 % (1818786)Instructions burned: 3512 (million) % 198.38/28.19 % (1818829)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4235711926:i=5211_2958 on theBenchmark for (2958ds/5211Mi) % 198.38/28.19 % (1818796)Instruction limit reached! % 198.38/28.19 % (1818796)------------------------------ % 198.38/28.19 % (1818796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.38/28.19 % (1818796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.38/28.19 % (1818796)CaDiCaL version: 2.1.3 % 198.38/28.19 % (1818796)Termination reason: Instruction limit % 198.38/28.19 % (1818796)Termination phase: Saturation % 198.38/28.19 % (1818796)Time elapsed: 3.601 s % 198.38/28.19 % (1818796)Peak memory usage: 36 MB % 198.38/28.19 % (1818796)Instructions burned: 3773 (million) % 198.38/28.19 % (1818833)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3189807611:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 198.38/28.19 % (1818833)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.38/28.19 % (1818833)Terminated due to inappropriate strategy. % 198.38/28.19 % (1818833)------------------------------ % 198.38/28.19 % (1818833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.38/28.19 % (1818833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.38/28.19 % (1818833)CaDiCaL version: 2.1.3 % 198.38/28.19 % (1818833)Termination reason: Inappropriate % 198.38/28.19 % (1818833)Time elapsed: 0.044 s % 198.38/28.19 % (1818833)Peak memory usage: 13 MB % 198.38/28.19 % (1818833)Instructions burned: 82 (million) % 198.38/28.19 % (1818833)------------------------------ % 198.38/28.19 % (1818833)------------------------------ % 198.38/28.19 % (1818836)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2188651425:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 198.38/28.19 % (1818836)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.38/28.19 % (1818836)Terminated due to inappropriate strategy. % 198.38/28.19 % (1818836)------------------------------ % 198.38/28.19 % (1818836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.38/28.19 % (1818836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.38/28.19 % (1818836)CaDiCaL version: 2.1.3 % 198.38/28.19 % (1818836)Termination reason: Inappropriate % 198.38/28.19 % (1818836)Time elapsed: 0.085 s % 198.38/28.19 % (1818836)Peak memory usage: 12 MB % 198.38/28.19 % (1818836)Instructions burned: 81 (million) % 198.38/28.19 % (1818836)------------------------------ % 198.38/28.19 % (1818836)------------------------------ % 198.38/28.19 % (1818841)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2026609038:i=14071_2946 on theBenchmark for (2946ds/14071Mi) % 198.38/28.19 % (1818841)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 198.38/28.19 % (1818841)Terminated due to inappropriate strategy. % 198.38/28.19 % (1818841)------------------------------ % 198.38/28.19 % (1818841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.38/28.19 % (1818841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.38/28.19 % (1818841)CaDiCaL version: 2.1.3 % 198.38/28.19 % (1818841)Termination reason: Inappropriate % 198.38/28.19 % (1818841)Time elapsed: 0.085 s % 198.38/28.19 % (1818841)Peak memory usage: 12 MB % 198.38/28.19 % (1818841)Instructions burned: 81 (million) % 198.38/28.19 % (1818841)------------------------------ % 198.38/28.19 % (1818841)------------------------------ % 198.38/28.19 % (1818843)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1697395408:i=22565:add=on:rawr=on_2945 on theBenchmark for (2945ds/22565Mi) % 198.38/28.19 % (1818825)Instruction limit reached! % 198.38/28.19 % (1818825)------------------------------ % 198.38/28.19 % (1818825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.38/28.19 % (1818825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.38/28.19 % (1818825)CaDiCaL version: 2.1.3 % 198.38/28.19 % (1818825)Termination reason: Instruction limit % 198.38/28.19 % (1818825)Termination phase: Saturation % 198.38/28.19 % (1818825)Time elapsed: 2.354 s % 198.38/28.19 % (1818825)Peak memory usage: 52 MB % 198.38/28.19 % (1818825)Instructions burned: 4592 (million) % 198.38/28.19 % (1818845)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3244034758:i=8173:av=off_2945 on theBenchmark for (2945ds/8173Mi) % 200.93/28.59 % (1818761)Instruction limit reached! % 200.93/28.59 % (1818761)------------------------------ % 200.93/28.59 % (1818761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.93/28.59 % (1818761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.93/28.59 % (1818761)CaDiCaL version: 2.1.3 % 200.93/28.59 % (1818761)Termination reason: Instruction limit % 200.93/28.59 % (1818761)Termination phase: Saturation % 200.93/28.59 % (1818761)Time elapsed: 5.098 s % 200.93/28.59 % (1818761)Peak memory usage: 53 MB % 200.93/28.59 % (1818761)Instructions burned: 5115 (million) % 200.93/28.59 % (1818847)dis+10_16:1_sil=16000:random_seed=653620290:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi) % 200.93/28.59 % (1818829)Instruction limit reached! % 200.93/28.59 % (1818829)------------------------------ % 200.93/28.59 % (1818829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.93/28.59 % (1818829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.93/28.59 % (1818829)CaDiCaL version: 2.1.3 % 200.93/28.59 % (1818829)Termination reason: Instruction limit % 200.93/28.59 % (1818829)Termination phase: Saturation % 200.93/28.59 % (1818829)Time elapsed: 4.711 s % 200.93/28.59 % (1818829)Peak memory usage: 45 MB % 200.93/28.59 % (1818829)Instructions burned: 5211 (million) % 200.93/28.59 % (1818861)ott-3_8_sil=64000:random_seed=4069169117:i=20139:bs=on_2910 on theBenchmark for (2910ds/20139Mi) % 200.93/28.59 % (1818845)Instruction limit reached! % 200.93/28.59 % (1818845)------------------------------ % 200.93/28.59 % (1818845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.93/28.59 % (1818845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.93/28.59 % (1818845)CaDiCaL version: 2.1.3 % 200.93/28.59 % (1818845)Termination reason: Instruction limit % 200.93/28.59 % (1818845)Termination phase: Saturation % 200.93/28.59 % (1818845)Time elapsed: 5.140 s % 200.93/28.59 % (1818845)Peak memory usage: 83 MB % 200.93/28.59 % (1818845)Instructions burned: 8173 (million) % 200.93/28.59 % (1818865)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2295952690:fmbsr=2:i=32576_2893 on theBenchmark for (2893ds/32576Mi) % 200.93/28.59 % (1818865)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 200.93/28.59 % (1818865)Terminated due to inappropriate strategy. % 200.93/28.59 % (1818865)------------------------------ % 200.93/28.59 % (1818865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.93/28.59 % (1818865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.93/28.59 % (1818865)CaDiCaL version: 2.1.3 % 200.93/28.59 % (1818865)Termination reason: Inappropriate % 200.93/28.59 % (1818865)Time elapsed: 0.074 s % 200.93/28.59 % (1818865)Peak memory usage: 12 MB % 200.93/28.59 % (1818865)Instructions burned: 82 (million) % 200.93/28.59 % (1818865)------------------------------ % 200.93/28.59 % (1818865)------------------------------ % 200.93/28.59 % (1818869)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3057088704:i=11404_2892 on theBenchmark for (2892ds/11404Mi) % 200.93/28.59 % (1818847)Instruction limit reached! % 200.93/28.59 % (1818847)------------------------------ % 200.93/28.59 % (1818847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.93/28.59 % (1818847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.93/28.59 % (1818847)CaDiCaL version: 2.1.3 % 200.93/28.59 % (1818847)Termination reason: Instruction limit % 200.93/28.59 % (1818847)Termination phase: Saturation % 200.93/28.59 % (1818847)Time elapsed: 8.379 s % 200.93/28.59 % (1818847)Peak memory usage: 59 MB % 200.93/28.59 % (1818847)Instructions burned: 9155 (million) % 200.93/28.59 % (1818871)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2358269661:i=14134_2857 on theBenchmark for (2857ds/14134Mi) % 200.93/28.59 % (1818861)Instruction limit reached! % 200.93/28.59 % (1818861)------------------------------ % 200.93/28.59 % (1818861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.93/28.59 % (1818861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.93/28.59 % (1818861)CaDiCaL version: 2.1.3 % 200.93/28.59 % (1818861)Termination reason: Instruction limit % 200.93/28.59 % (1818861)Termination phase: Saturation % 200.93/28.59 % (1818861)Time elapsed: 9.441 s % 200.93/28.59 % (1818861)Peak memory usage: 79 MB % 200.93/28.59 % (1818861)Instructions burned: 20139 (million) % 200.93/28.59 % (1818879)dis+33_16_sil=32000:sac=on:random_seed=978756236:i=15851:nm=0_2816 on theBenchmark for (2816ds/15851Mi) % 200.93/28.59 % (1818869)Instruction limit reached! % 200.93/28.59 % (1818869)------------------------------ % 200.93/28.59 % (1818869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.00/40.04 % (1818869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.00/40.04 % (1818869)CaDiCaL version: 2.1.3 % 283.00/40.04 % (1818869)Termination reason: Instruction limit % 283.00/40.04 % (1818869)Termination phase: Saturation % 283.00/40.04 % (1818869)Time elapsed: 11.561 s % 283.00/40.04 % (1818869)Peak memory usage: 96 MB % 283.00/40.04 % (1818869)Instructions burned: 11405 (million) % 283.00/40.04 % (1818881)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=10709803:avsq=on:i=17627:add=on:amm=off_2775 on theBenchmark for (2775ds/17627Mi) % 283.00/40.04 % (1818879)Instruction limit reached! % 283.00/40.04 % (1818879)------------------------------ % 283.00/40.04 % (1818879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.00/40.04 % (1818879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.00/40.04 % (1818879)CaDiCaL version: 2.1.3 % 283.00/40.04 % (1818879)Termination reason: Instruction limit % 283.00/40.04 % (1818879)Termination phase: Saturation % 283.00/40.04 % (1818879)Time elapsed: 6.769 s % 283.00/40.04 % (1818879)Peak memory usage: 21 MB % 283.00/40.05 % (1818879)Instructions burned: 15853 (million) % 283.00/40.05 % (1818885)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1890097104:s2a=on:i=53295_2748 on theBenchmark for (2748ds/53295Mi) % 283.00/40.05 % (1818843)Instruction limit reached! % 283.00/40.05 % (1818843)------------------------------ % 283.00/40.05 % (1818843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.00/40.05 % (1818843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.00/40.05 % (1818843)CaDiCaL version: 2.1.3 % 283.00/40.05 % (1818843)Termination reason: Instruction limit % 283.00/40.05 % (1818843)Termination phase: Saturation % 283.00/40.05 % (1818843)Time elapsed: 20.484 s % 283.00/40.05 % (1818843)Peak memory usage: 595 MB % 283.00/40.05 % (1818843)Instructions burned: 22566 (million) % 283.00/40.05 % (1818889)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=967882553:i=26857:ins=20_2739 on theBenchmark for (2739ds/26857Mi) % 283.00/40.05 % (1818889)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.00/40.05 % (1818889)Terminated due to inappropriate strategy. % 283.00/40.05 % (1818889)------------------------------ % 283.00/40.05 % (1818889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.00/40.05 % (1818889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.00/40.05 % (1818889)CaDiCaL version: 2.1.3 % 283.00/40.05 % (1818889)Termination reason: Inappropriate % 283.00/40.05 % (1818889)Time elapsed: 0.070 s % 283.00/40.05 % (1818889)Peak memory usage: 12 MB % 283.00/40.05 % (1818889)Instructions burned: 81 (million) % 283.00/40.05 % (1818889)------------------------------ % 283.00/40.05 % (1818889)------------------------------ % 283.00/40.05 % (1818891)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1310538059:i=28120:bs=on:fsr=off_2738 on theBenchmark for (2738ds/28120Mi) % 283.00/40.05 % (1818827)Instruction limit reached! % 283.00/40.05 % (1818827)------------------------------ % 283.00/40.05 % (1818827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.00/40.05 % (1818827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.00/40.05 % (1818827)CaDiCaL version: 2.1.3 % 283.00/40.05 % (1818827)Termination reason: Instruction limit % 283.00/40.05 % (1818827)Termination phase: Saturation % 283.00/40.05 % (1818827)Time elapsed: 23.716 s % 283.00/40.05 % (1818827)Peak memory usage: 150 MB % 283.00/40.05 % (1818827)Instructions burned: 29340 (million) % 283.00/40.05 % (1818895)fmb+10_1_sil=256000:fmbss=7:random_seed=2592046563:fmbsr=1.6:i=182295_2721 on theBenchmark for (2721ds/182295Mi) % 283.00/40.05 % (1818895)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem! % 283.00/40.05 % (1818895)Terminated due to inappropriate strategy. % 283.00/40.05 % (1818895)------------------------------ % 283.00/40.05 % (1818895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.00/40.05 % (1818895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.00/40.05 % (1818895)CaDiCaL version: 2.1.3 % 283.00/40.05 % (1818895)Termination reason: Inappropriate % 283.00/40.05 % (1818895)Time elapsed: 0.042 s % 283.00/40.05 % (1818895)Peak memory usage: 12 MB % 283.00/40.05 % (1818895)Instructions burned: 81 (million) % 283.00/40.05 % (1818895)------------------------------ % 283.00/40.05 % (1818895)------------------------------ % 283.00/40.05 % (1818897)fmb+10_1_sil=128000:fmbss=21:newcnf=onTerminated % 300.53/42.54 % Vampire exiting %------------------------------------------------------------------------------