%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX068+1 : TPTP v9.3.1. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:46:25 PM UTC 2026 % Result : Timeout 300.35s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX068+1 : TPTP v9.3.1. Released v9.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 % Computer : n006.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:57:40 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.24 Running first-order model finding % 0.09/0.24 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 % 15.23/2.44 % (4027031)Will run a generic schedule for satisfiability detection. % 15.23/2.44 % (4027042)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3962055745:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 15.23/2.44 % (4027037)% WARNING: option uhcvi not known. % 15.23/2.44 % (4027036)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3568704949_2999 on theBenchmark for (2999ds/0Mi) % 15.23/2.44 % (4027040)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2933416464:i=116_2999 on theBenchmark for (2999ds/116Mi) % 15.23/2.44 % (4027037)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2429000686:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 15.23/2.44 % (4027038)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3901044920:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 15.23/2.44 % (4027039)dis+10_1_sil=32000:sp=arity:random_seed=1401262999:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 15.23/2.44 % (4027041)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1716619803:i=131_2999 on theBenchmark for (2999ds/131Mi) % 15.23/2.44 % (4027042)Instruction limit reached! % 15.23/2.44 % (4027042)------------------------------ % 15.23/2.44 % (4027042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.23/2.44 % (4027042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.44 % (4027042)CaDiCaL version: 2.1.3 % 15.23/2.44 % (4027042)Termination reason: Instruction limit % 15.23/2.44 % (4027042)Termination phase: Saturation % 15.23/2.44 % (4027042)Time elapsed: 0.048 s % 15.23/2.44 % (4027042)Peak memory usage: 14 MB % 15.23/2.44 % (4027042)Instructions burned: 160 (million) % 15.23/2.44 % (4027050)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3352203255:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 15.23/2.44 % (4027040)Instruction limit reached! % 15.23/2.44 % (4027040)------------------------------ % 15.23/2.44 % (4027040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.23/2.44 % (4027040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.44 % (4027040)CaDiCaL version: 2.1.3 % 15.23/2.44 % (4027040)Termination reason: Instruction limit % 15.23/2.44 % (4027040)Termination phase: Saturation % 15.23/2.44 % (4027040)Time elapsed: 0.054 s % 15.23/2.44 % (4027040)Peak memory usage: 12 MB % 15.23/2.44 % (4027040)Instructions burned: 118 (million) % 15.23/2.44 % Detected minimum model sizes of [3] % 15.23/2.44 % Detected maximum model sizes of [max] % 15.23/2.44 % TRYING [3] % 15.23/2.44 % (4027039)Instruction limit reached! % 15.23/2.44 % (4027039)------------------------------ % 15.23/2.44 % (4027039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.23/2.44 % (4027039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.44 % (4027039)CaDiCaL version: 2.1.3 % 15.23/2.44 % (4027039)Termination reason: Instruction limit % 15.23/2.44 % (4027039)Termination phase: Saturation % 15.23/2.44 % (4027039)Time elapsed: 0.065 s % 15.23/2.44 % (4027039)Peak memory usage: 13 MB % 15.23/2.44 % (4027039)Instructions burned: 104 (million) % 15.23/2.44 % Detected minimum model sizes of [3] % 15.23/2.44 % Detected maximum model sizes of [max] % 15.23/2.44 % TRYING [3] % 15.23/2.44 % (4027052)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3380801123:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 15.23/2.44 % (4027041)Instruction limit reached! % 15.23/2.44 % (4027041)------------------------------ % 15.23/2.44 % (4027041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.23/2.44 % (4027041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.44 % (4027041)CaDiCaL version: 2.1.3 % 15.23/2.44 % (4027041)Termination reason: Instruction limit % 15.23/2.44 % (4027041)Termination phase: Saturation % 15.23/2.44 % (4027041)Time elapsed: 0.075 s % 15.23/2.44 % (4027041)Peak memory usage: 14 MB % 15.23/2.44 % (4027041)Instructions burned: 131 (million) % 15.23/2.44 % (4027053)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=1603010615:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 15.23/2.44 % (4027055)ott-21_1_sil=16000:fs=off:random_seed=2585244348:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 15.23/2.44 % TRYING [4] % 15.23/2.44 % (4027052)Instruction limit reached! % 15.23/2.44 % (4027052)------------------------------ % 15.23/2.44 % (4027052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.46/4.73 % (4027052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.46/4.73 % (4027052)CaDiCaL version: 2.1.3 % 27.46/4.73 % (4027052)Termination reason: Instruction limit % 27.46/4.73 % (4027052)Termination phase: Saturation % 27.46/4.73 % (4027052)Time elapsed: 0.076 s % 27.46/4.73 % (4027052)Peak memory usage: 14 MB % 27.46/4.73 % (4027052)Instructions burned: 132 (million) % 27.46/4.73 % (4027058)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1365217548:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 27.46/4.73 % TRYING [4] % 27.46/4.73 % (4027055)Instruction limit reached! % 27.46/4.73 % (4027055)------------------------------ % 27.46/4.73 % (4027055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.46/4.73 % (4027055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.46/4.73 % (4027055)CaDiCaL version: 2.1.3 % 27.46/4.73 % (4027055)Termination reason: Instruction limit % 27.46/4.73 % (4027055)Termination phase: Saturation % 27.46/4.73 % (4027055)Time elapsed: 0.095 s % 27.46/4.73 % (4027055)Peak memory usage: 13 MB % 27.46/4.73 % (4027055)Instructions burned: 180 (million) % 27.46/4.73 % (4027050)Instruction limit reached! % 27.46/4.73 % (4027050)------------------------------ % 27.46/4.73 % (4027050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.46/4.73 % (4027050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.46/4.73 % (4027050)CaDiCaL version: 2.1.3 % 27.46/4.73 % (4027050)Termination reason: Instruction limit % 27.46/4.73 % (4027050)Termination phase: Finite model building constraint generation % 27.46/4.73 % (4027050)Time elapsed: 0.149 s % 27.46/4.73 % (4027050)Peak memory usage: 41 MB % 27.46/4.73 % (4027050)Instructions burned: 715 (million) % 27.46/4.73 % (4027060)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1947438122:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 27.46/4.73 % (4027061)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1472897491:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 27.46/4.73 % Detected minimum model sizes of [3] % 27.46/4.73 % Detected maximum model sizes of [max] % 27.46/4.73 % TRYING [3] % 27.46/4.73 % (4027053)Instruction limit reached! % 27.46/4.73 % (4027053)------------------------------ % 27.46/4.73 % (4027053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.46/4.73 % (4027053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.46/4.73 % (4027053)CaDiCaL version: 2.1.3 % 27.46/4.73 % (4027053)Termination reason: Instruction limit % 27.46/4.73 % (4027053)Termination phase: Saturation % 27.46/4.73 % (4027053)Time elapsed: 0.399 s % 27.46/4.73 % (4027053)Peak memory usage: 18 MB % 27.46/4.73 % (4027053)Instructions burned: 685 (million) % 27.46/4.73 % (4027058)Instruction limit reached! % 27.46/4.73 % (4027058)------------------------------ % 27.46/4.73 % (4027058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.46/4.73 % (4027058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.46/4.73 % (4027058)CaDiCaL version: 2.1.3 % 27.46/4.73 % (4027058)Termination reason: Instruction limit % 27.46/4.73 % (4027058)Termination phase: Saturation % 27.46/4.73 % (4027058)Time elapsed: 0.320 s % 27.46/4.73 % (4027058)Peak memory usage: 15 MB % 27.46/4.73 % (4027058)Instructions burned: 478 (million) % 27.46/4.73 % (4027064)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2378800517:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 27.46/4.73 % (4027065)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=1354765794:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 27.46/4.73 % TRYING [5] % 27.46/4.73 % (4027060)Instruction limit reached! % 27.46/4.73 % (4027060)------------------------------ % 27.46/4.73 % (4027060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 27.46/4.73 % (4027060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.46/4.73 % (4027060)CaDiCaL version: 2.1.3 % 27.46/4.73 % (4027060)Termination reason: Instruction limit % 27.46/4.73 % (4027060)Termination phase: Finite model building constraint generation % 27.46/4.73 % (4027060)Time elapsed: 0.377 s % 27.46/4.73 % (4027060)Peak memory usage: 29 MB % 27.46/4.73 % (4027060)Instructions burned: 866 (million) % 27.46/4.73 % (4027061)Instruction limit reached! % 27.46/4.73 % (4027061)------------------------------ % 27.46/4.73 % (4027061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.29/9.13 % (4027061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.29/9.13 % (4027061)CaDiCaL version: 2.1.3 % 62.29/9.13 % (4027061)Termination reason: Instruction limit % 62.29/9.13 % (4027061)Termination phase: Saturation % 62.29/9.13 % (4027061)Time elapsed: 0.375 s % 62.29/9.13 % (4027061)Peak memory usage: 25 MB % 62.29/9.13 % (4027061)Instructions burned: 1180 (million) % 62.29/9.13 % (4027069)fmb+10_1_sil=64000:random_seed=1640330798:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 62.29/9.13 % (4027068)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3782570271:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 62.29/9.13 % Detected minimum model sizes of [3] % 62.29/9.13 % Detected maximum model sizes of [max] % 62.29/9.13 % TRYING [3] % 62.29/9.13 % TRYING [4] % 62.29/9.13 % (4027064)Instruction limit reached! % 62.29/9.13 % (4027064)------------------------------ % 62.29/9.13 % (4027064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.29/9.13 % (4027064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.29/9.13 % (4027064)CaDiCaL version: 2.1.3 % 62.29/9.13 % (4027064)Termination reason: Instruction limit % 62.29/9.13 % (4027064)Termination phase: Finite model building constraint generation % 62.29/9.13 % (4027064)Time elapsed: 0.412 s % 62.29/9.13 % (4027064)Peak memory usage: 100 MB % 62.29/9.13 % (4027064)Instructions burned: 890 (million) % 62.29/9.13 % (4027072)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=215699523:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 62.29/9.13 % (4027065)Instruction limit reached! % 62.29/9.13 % (4027065)------------------------------ % 62.29/9.13 % (4027065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.29/9.13 % (4027065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.29/9.13 % (4027065)CaDiCaL version: 2.1.3 % 62.29/9.13 % (4027065)Termination reason: Instruction limit % 62.29/9.13 % (4027065)Termination phase: Saturation % 62.29/9.13 % (4027065)Time elapsed: 0.442 s % 62.29/9.13 % (4027065)Peak memory usage: 22 MB % 62.29/9.13 % (4027065)Instructions burned: 693 (million) % 62.29/9.13 % (4027074)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2958292451:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 62.29/9.13 % Detected minimum model sizes of [3] % 62.29/9.13 % Detected maximum model sizes of [max] % 62.29/9.13 % TRYING [20] % 62.29/9.13 % Detected minimum model sizes of [3] % 62.29/9.13 % Detected maximum model sizes of [max] % 62.29/9.13 % TRYING [8] % 62.29/9.13 % (4027068)Instruction limit reached! % 62.29/9.13 % (4027068)------------------------------ % 62.29/9.13 % (4027068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.29/9.13 % (4027068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.29/9.13 % (4027068)CaDiCaL version: 2.1.3 % 62.29/9.13 % (4027068)Termination reason: Instruction limit % 62.29/9.13 % (4027068)Termination phase: Saturation % 62.29/9.13 % (4027068)Time elapsed: 0.451 s % 62.29/9.13 % (4027068)Peak memory usage: 21 MB % 62.29/9.13 % (4027068)Instructions burned: 881 (million) % 62.29/9.13 % (4027076)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1534912825:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 62.29/9.13 % (4027074)Instruction limit reached! % 62.29/9.13 % (4027074)------------------------------ % 62.29/9.13 % (4027074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.29/9.13 % (4027074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.29/9.13 % (4027074)CaDiCaL version: 2.1.3 % 62.29/9.13 % (4027074)Termination reason: Instruction limit % 62.29/9.13 % (4027074)Termination phase: Finite model building constraint generation % 62.29/9.13 % (4027074)Time elapsed: 0.317 s % 62.29/9.13 % (4027074)Peak memory usage: 58 MB % 62.29/9.13 % (4027074)Instructions burned: 921 (million) % 62.29/9.13 % (4027078)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1540641390:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 62.29/9.13 % TRYING [5] % 62.29/9.13 % TRYING [6] % 62.29/9.13 % (4027078)Instruction limit reached! % 62.29/9.13 % (4027078)------------------------------ % 62.29/9.13 % (4027078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 62.29/9.13 % (4027078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.29/9.13 % (4027078)CaDiCaL version: 2.1.3 % 62.29/9.13 % (4027078)Termination reason: Instruction limit % 173.37/24.77 % (4027078)Termination phase: Saturation % 173.37/24.77 % (4027078)Time elapsed: 0.840 s % 173.37/24.77 % (4027078)Peak memory usage: 35 MB % 173.37/24.77 % (4027078)Instructions burned: 1474 (million) % 173.37/24.77 % (4027080)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2633684000:i=6324_2977 on theBenchmark for (2977ds/6324Mi) % 173.37/24.77 % Detected minimum model sizes of [3] % 173.37/24.77 % Detected maximum model sizes of [max] % 173.37/24.77 % (4027080)Cannot represent all propositional literals internally % 173.37/24.77 % (4027080)Refutation not found, incomplete strategy % 173.37/24.77 % (4027080)------------------------------ % 173.37/24.77 % (4027080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.37/24.77 % (4027080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.37/24.77 % (4027080)CaDiCaL version: 2.1.3 % 173.37/24.77 % (4027080)Termination reason: Refutation not found, incomplete strategy % 173.37/24.77 % (4027080)Time elapsed: 0.059 s % 173.37/24.77 % (4027080)Peak memory usage: 13 MB % 173.37/24.77 % (4027080)Instructions burned: 126 (million) % 173.37/24.77 % (4027080)------------------------------ % 173.37/24.77 % (4027080)------------------------------ % 173.37/24.77 % (4027082)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2837940985:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi) % 173.37/24.77 % Detected minimum model sizes of [3] % 173.37/24.77 % Detected maximum model sizes of [max] % 173.37/24.77 % TRYING [16] % 173.37/24.77 % (4027082)Instruction limit reached! % 173.37/24.77 % (4027082)------------------------------ % 173.37/24.77 % (4027082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.37/24.77 % (4027082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.37/24.77 % (4027082)CaDiCaL version: 2.1.3 % 173.37/24.77 % (4027082)Termination reason: Instruction limit % 173.37/24.77 % (4027082)Termination phase: Finite model building constraint generation % 173.37/24.77 % (4027082)Time elapsed: 0.852 s % 173.37/24.77 % (4027082)Peak memory usage: 121 MB % 173.37/24.77 % (4027082)Instructions burned: 2176 (million) % 173.37/24.77 % (4027084)ott-2_1_sil=16000:newcnf=on:random_seed=2148329067:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi) % 173.37/24.77 % TRYING [6] % 173.37/24.77 % (4027084)Instruction limit reached! % 173.37/24.77 % (4027084)------------------------------ % 173.37/24.77 % (4027084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.37/24.77 % (4027084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.37/24.77 % (4027084)CaDiCaL version: 2.1.3 % 173.37/24.77 % (4027084)Termination reason: Instruction limit % 173.37/24.77 % (4027084)Termination phase: Saturation % 173.37/24.77 % (4027084)Time elapsed: 0.368 s % 173.37/24.77 % (4027084)Peak memory usage: 16 MB % 173.37/24.77 % (4027084)Instructions burned: 871 (million) % 173.37/24.77 % (4027086)ott+10_1_sil=32000:tgt=ground:random_seed=525717781:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi) % 173.37/24.77 % (4027076)Instruction limit reached! % 173.37/24.77 % (4027076)------------------------------ % 173.37/24.77 % (4027076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.37/24.77 % (4027076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.37/24.77 % (4027076)CaDiCaL version: 2.1.3 % 173.37/24.77 % (4027076)Termination reason: Instruction limit % 173.37/24.77 % (4027076)Termination phase: Saturation % 173.37/24.77 % (4027076)Time elapsed: 2.774 s % 173.37/24.77 % (4027076)Peak memory usage: 39 MB % 173.37/24.77 % (4027076)Instructions burned: 5131 (million) % 173.37/24.77 % (4027088)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2296054445:i=54282_2960 on theBenchmark for (2960ds/54282Mi) % 173.37/24.77 % Detected minimum model sizes of [3] % 173.37/24.77 % Detected maximum model sizes of [max] % 173.37/24.77 % TRYING [3] % 173.37/24.77 % TRYING [7] % 173.37/24.77 % TRYING [4] % 173.37/24.77 % (4027072)Instruction limit reached! % 173.37/24.77 % (4027072)------------------------------ % 173.37/24.77 % (4027072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.37/24.77 % (4027072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.37/24.77 % (4027072)CaDiCaL version: 2.1.3 % 173.37/24.77 % (4027072)Termination reason: Instruction limit % 173.37/24.77 % (4027072)Termination phase: Finite model building constraint generation % 173.37/24.77 % (4027072)Time elapsed: 3.405 s % 173.37/24.77 % (4027072)Peak memory usage: 583 MB % 173.37/24.77 % (4027072)Instructions burned: 9518 (million) % 173.37/24.77 % (4027090)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=529953740:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 253.76/36.07 % TRYING [5] % 253.76/36.07 % TRYING [6] % 253.76/36.07 % (4027069)Instruction limit reached! % 253.76/36.07 % (4027069)------------------------------ % 253.76/36.07 % (4027069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.07 % (4027069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.07 % (4027069)CaDiCaL version: 2.1.3 % 253.76/36.07 % (4027069)Termination reason: Instruction limit % 253.76/36.07 % (4027069)Termination phase: Finite model building SAT solving % 253.76/36.07 % (4027069)Time elapsed: 5.365 s % 253.76/36.07 % (4027069)Peak memory usage: 281 MB % 253.76/36.07 % (4027069)Instructions burned: 22064 (million) % 253.76/36.07 % (4027092)dis+21_1_sil=32000:sas=cadical:random_seed=99156187:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi) % 253.76/36.07 % (4027086)Instruction limit reached! % 253.76/36.07 % (4027086)------------------------------ % 253.76/36.07 % (4027086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.07 % (4027086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.07 % (4027086)CaDiCaL version: 2.1.3 % 253.76/36.07 % (4027086)Termination reason: Instruction limit % 253.76/36.07 % (4027086)Termination phase: Saturation % 253.76/36.07 % (4027086)Time elapsed: 2.959 s % 253.76/36.07 % (4027086)Peak memory usage: 49 MB % 253.76/36.07 % (4027086)Instructions burned: 5116 (million) % 253.76/36.07 % (4027094)ott+11_1_sil=16000:gs=on:random_seed=640374900:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi) % 253.76/36.07 % (4027090)Instruction limit reached! % 253.76/36.07 % (4027090)------------------------------ % 253.76/36.07 % (4027090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.07 % (4027090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.07 % (4027090)CaDiCaL version: 2.1.3 % 253.76/36.07 % (4027090)Termination reason: Instruction limit % 253.76/36.07 % (4027090)Termination phase: Saturation % 253.76/36.07 % (4027090)Time elapsed: 2.115 s % 253.76/36.07 % (4027090)Peak memory usage: 45 MB % 253.76/36.07 % (4027090)Instructions burned: 3513 (million) % 253.76/36.07 % (4027096)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2401947953:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi) % 253.76/36.07 % Detected minimum model sizes of [3] % 253.76/36.07 % Detected maximum model sizes of [max] % 253.76/36.07 % TRYING [7] % 253.76/36.07 % (4027092)Instruction limit reached! % 253.76/36.07 % (4027092)------------------------------ % 253.76/36.07 % (4027092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.07 % (4027092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.07 % (4027092)CaDiCaL version: 2.1.3 % 253.76/36.07 % (4027092)Termination reason: Instruction limit % 253.76/36.07 % (4027092)Termination phase: Saturation % 253.76/36.07 % (4027092)Time elapsed: 1.135 s % 253.76/36.07 % (4027092)Peak memory usage: 45 MB % 253.76/36.07 % (4027092)Instructions burned: 3774 (million) % 253.76/36.07 % (4027098)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=415230667:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2928 on theBenchmark for (2928ds/4591Mi) % 253.76/36.07 % (4027094)Instruction limit reached! % 253.76/36.07 % (4027094)------------------------------ % 253.76/36.07 % (4027094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.07 % (4027094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.07 % (4027094)CaDiCaL version: 2.1.3 % 253.76/36.07 % (4027094)Termination reason: Instruction limit % 253.76/36.07 % (4027094)Termination phase: Saturation % 253.76/36.07 % (4027094)Time elapsed: 1.263 s % 253.76/36.07 % (4027094)Peak memory usage: 22 MB % 253.76/36.07 % (4027094)Instructions burned: 2252 (million) % 253.76/36.07 % (4027100)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2855349144:i=29340_2921 on theBenchmark for (2921ds/29340Mi) % 253.76/36.07 % TRYING [7] % 253.76/36.07 % (4027098)Instruction limit reached! % 253.76/36.07 % (4027098)------------------------------ % 253.76/36.07 % (4027098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.07 % (4027098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.07 % (4027098)CaDiCaL version: 2.1.3 % 253.76/36.07 % (4027098)Termination reason: Instruction limit % 253.76/36.07 % (4027098)Termination phase: Saturation % 253.76/36.07 % (4027098)Time elapsed: 1.685 s % 253.76/36.07 % (4027098)Peak memory usage: 106 MB % 253.76/36.07 % (4027098)Instructions burned: 4593 (million) % 253.76/36.07 % (4027102)dis-10_1_sil=64000:sas=cadicalTerminated % 300.35/42.64 % Vampire exiting % 300.35/42.64 Terminated %------------------------------------------------------------------------------