%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW472_10 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:07 PM UTC 2026 % Result : Timeout 295.47s 41.92s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW472_10 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.16 % Computer : n019.cluster.edu % 0.11/0.16 % Model : x86_64 x86_64 % 0.11/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.16 % Memory : 8046.5625MB % 0.11/0.16 % OS : Linux 6.8.0-71-generic % 0.11/0.16 % CPULimit : 300 % 0.11/0.16 % WCLimit : 300 % 0.11/0.16 % DateTime : Mon Sep 28 14:04:33 UTC 2026 % 0.11/0.16 % CPUTime : % 0.11/0.16 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.19 Running first-order model finding % 0.11/0.19 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 % 6.83/1.27 % (4017861)Will run a generic schedule for satisfiability detection. % 6.83/1.27 % (4017867)% WARNING: option uhcvi not known. % 6.83/1.27 % (4017871)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=52776218:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.83/1.27 % (4017866)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2289293868_2999 on theBenchmark for (2999ds/0Mi) % 6.83/1.27 % (4017867)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2520515129:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.83/1.27 % (4017869)dis+10_1_sil=32000:sp=arity:random_seed=1498210640:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.83/1.27 % (4017868)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3871973980:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.83/1.27 % (4017872)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3838557738:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.83/1.27 % (4017870)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2578787863:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.83/1.27 % (4017870)Instruction limit reached! % 6.83/1.27 % (4017870)------------------------------ % 6.83/1.27 % (4017870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.27 % (4017870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.27 % (4017870)CaDiCaL version: 2.1.3 % 6.83/1.27 % (4017870)Termination reason: Instruction limit % 6.83/1.27 % (4017870)Termination phase: Saturation % 6.83/1.27 % (4017870)Time elapsed: 0.035 s % 6.83/1.27 % (4017870)Peak memory usage: 13 MB % 6.83/1.27 % (4017870)Instructions burned: 117 (million) % 6.83/1.27 % (4017880)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2051657680:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.83/1.27 % (4017869)Instruction limit reached! % 6.83/1.27 % (4017869)------------------------------ % 6.83/1.27 % (4017869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.27 % (4017869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.27 % (4017869)CaDiCaL version: 2.1.3 % 6.83/1.27 % (4017869)Termination reason: Instruction limit % 6.83/1.27 % (4017869)Termination phase: Saturation % 6.83/1.27 % (4017869)Time elapsed: 0.059 s % 6.83/1.27 % (4017869)Peak memory usage: 12 MB % 6.83/1.27 % (4017869)Instructions burned: 103 (million) % 6.83/1.27 % (4017871)Instruction limit reached! % 6.83/1.27 % (4017871)------------------------------ % 6.83/1.27 % (4017871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.27 % (4017871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.27 % (4017871)CaDiCaL version: 2.1.3 % 6.83/1.27 % (4017871)Termination reason: Instruction limit % 6.83/1.27 % (4017871)Termination phase: Saturation % 6.83/1.27 % (4017871)Time elapsed: 0.072 s % 6.83/1.27 % (4017871)Peak memory usage: 13 MB % 6.83/1.27 % (4017871)Instructions burned: 131 (million) % 6.83/1.27 % (4017882)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1419579957:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 6.83/1.27 % TRYING [1] % 6.83/1.27 % (4017872)Instruction limit reached! % 6.83/1.27 % (4017872)------------------------------ % 6.83/1.27 % (4017872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.83/1.27 % (4017872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.27 % TRYING [2] % 6.83/1.27 % (4017872)CaDiCaL version: 2.1.3 % 6.83/1.27 % (4017872)Termination reason: Instruction limit % 6.83/1.27 % (4017872)Termination phase: Saturation % 6.83/1.27 % (4017872)Time elapsed: 0.091 s % 6.83/1.27 % (4017872)Peak memory usage: 12 MB % 6.83/1.27 % (4017872)Instructions burned: 159 (million) % 6.83/1.27 % (4017883)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=69495863:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 6.83/1.27 % TRYING [3] % 6.83/1.27 % (4017885)ott-21_1_sil=16000:fs=off:random_seed=1408762922:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.83/1.27 % Detected minimum model sizes of [1,1,1,1,1,1] % 6.83/1.27 % Detected maximum model sizes of [2,max,max,max,max,max] % 6.83/1.27 % TRYING [1,1,1,1,1,1] % 6.83/1.27 % TRYING [1,1,1,1,2,1] % 6.83/1.27 % TRYING [4] % 6.83/1.27 % TRYING [1,1,1,1,3,1] % 6.83/1.27 % (4017882)Instruction limit reached! % 6.83/1.27 % (4017882)------------------------------ % 10.50/2.03 % (4017882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.50/2.03 % (4017882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.03 % (4017882)CaDiCaL version: 2.1.3 % 10.50/2.03 % (4017882)Termination reason: Instruction limit % 10.50/2.03 % (4017882)Termination phase: Saturation % 10.50/2.03 % (4017882)Time elapsed: 0.086 s % 10.50/2.03 % (4017882)Peak memory usage: 13 MB % 10.50/2.03 % (4017882)Instructions burned: 132 (million) % 10.50/2.03 % TRYING [1,1,1,2,3,1] % 10.50/2.03 % TRYING [1,1,2,2,3,1] % 10.50/2.03 % (4017888)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3917539054:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 10.50/2.03 % TRYING [2,1,2,2,3,1] % 10.50/2.03 % (4017880)Instruction limit reached! % 10.50/2.03 % (4017880)------------------------------ % 10.50/2.03 % (4017880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.50/2.03 % (4017880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.03 % (4017880)CaDiCaL version: 2.1.3 % 10.50/2.03 % (4017880)Termination reason: Instruction limit % 10.50/2.03 % (4017880)Termination phase: Finite model building constraint generation % 10.50/2.03 % (4017880)Time elapsed: 0.146 s % 10.50/2.03 % (4017880)Peak memory usage: 31 MB % 10.50/2.03 % (4017880)Instructions burned: 718 (million) % 10.50/2.03 % (4017885)Instruction limit reached! % 10.50/2.03 % (4017885)------------------------------ % 10.50/2.03 % (4017885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.50/2.03 % (4017885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.03 % (4017885)CaDiCaL version: 2.1.3 % 10.50/2.03 % (4017885)Termination reason: Instruction limit % 10.50/2.03 % (4017885)Termination phase: Saturation % 10.50/2.03 % (4017885)Time elapsed: 0.090 s % 10.50/2.03 % (4017885)Peak memory usage: 12 MB % 10.50/2.03 % (4017885)Instructions burned: 181 (million) % 10.50/2.03 % TRYING [1,2,2,2,3,1] % 10.50/2.03 % (4017890)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1172663347:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 10.50/2.03 % (4017891)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2675785192:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 10.50/2.03 % TRYING [2,2,2,2,3,1] % 10.50/2.03 % TRYING [2,1,3,2,3,1] % 10.50/2.03 % TRYING [2,3,2,2,3,1] % 10.50/2.03 % Detected minimum model sizes of [1,1,1,1,1,1] % 10.50/2.03 % Detected maximum model sizes of [2,max,max,max,max,max] % 10.50/2.03 % TRYING [1,1,1,1,1,1] % 10.50/2.03 % TRYING [1,1,1,1,2,1] % 10.50/2.03 % TRYING [1,1,1,1,3,1] % 10.50/2.03 % TRYING [1,1,1,2,3,1] % 10.50/2.03 % TRYING [2,2,3,2,3,1] % 10.50/2.03 % TRYING [1,1,1,3,3,1] % 10.50/2.03 % TRYING [1,1,2,3,3,1] % 10.50/2.03 % TRYING [2,4,2,2,3,1] % 10.50/2.03 % TRYING [1,2,2,3,3,1] % 10.50/2.03 % TRYING [2,3,3,2,3,1] % 10.50/2.03 % (4017890)Instruction limit reached! % 10.50/2.03 % (4017890)------------------------------ % 10.50/2.03 % (4017890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.50/2.03 % (4017890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.03 % (4017890)CaDiCaL version: 2.1.3 % 10.50/2.03 % (4017890)Termination reason: Instruction limit % 10.50/2.03 % (4017890)Termination phase: Finite model building SAT solving % 10.50/2.03 % (4017890)Time elapsed: 0.201 s % 10.50/2.03 % (4017890)Peak memory usage: 20 MB % 10.50/2.03 % (4017890)Instructions burned: 868 (million) % 10.50/2.03 % (4017894)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1921620757:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 10.50/2.03 % (4017883)Instruction limit reached! % 10.50/2.03 % (4017883)------------------------------ % 10.50/2.03 % (4017883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.50/2.03 % (4017883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.03 % (4017883)CaDiCaL version: 2.1.3 % 10.50/2.03 % (4017883)Termination reason: Instruction limit % 10.50/2.03 % (4017883)Termination phase: Saturation % 10.50/2.03 % (4017883)Time elapsed: 0.350 s % 10.50/2.03 % (4017883)Peak memory usage: 16 MB % 10.50/2.03 % (4017883)Instructions burned: 685 (million) % 10.50/2.03 % TRYING [2,5,2,2,3,1] % 10.50/2.03 % (4017888)Instruction limit reached! % 10.50/2.03 % (4017888)------------------------------ % 10.50/2.03 % (4017888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 10.50/2.03 % (4017888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.50/2.03 % (4017888)CaDiCaL version: 2.1.3 % 10.50/2.03 % (4017888)Termination reason: Instruction limit % 10.50/2.03 % (4017888)Termination phase: Saturation % 10.50/2.03 % (4017888)Time elapsed: 0.276 s % 10.50/2.03 % (4017888)Peak memory usage: 14 MB % 45.24/6.67 % (4017888)Instructions burned: 477 (million) % 45.24/6.67 % (4017896)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=1618306465:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 45.24/6.67 % (4017897)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=360926207:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 45.24/6.67 % TRYING [2,6,2,2,3,1] % 45.24/6.67 % Detected minimum model sizes of [1,1,1,1,1,1] % 45.24/6.67 % Detected maximum model sizes of [2,max,max,max,max,max] % 45.24/6.67 % fmb_start_size (= 14) larger than a detected sort maximum size! % 45.24/6.67 % (4017894)Refutation not found, incomplete strategy % 45.24/6.67 % (4017894)------------------------------ % 45.24/6.67 % (4017894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.67 % (4017894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.67 % (4017894)CaDiCaL version: 2.1.3 % 45.24/6.67 % (4017894)Termination reason: Refutation not found, incomplete strategy % 45.24/6.67 % (4017894)Time elapsed: 0.083 s % 45.24/6.67 % (4017894)Peak memory usage: 15 MB % 45.24/6.67 % (4017894)Instructions burned: 358 (million) % 45.24/6.67 % (4017894)------------------------------ % 45.24/6.67 % (4017894)------------------------------ % 45.24/6.67 % (4017900)fmb+10_1_sil=64000:random_seed=2984352758:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 45.24/6.67 % TRYING [2,3,4,2,3,1] % 45.24/6.67 % Detected minimum model sizes of [1,1,1,1,1,1] % 45.24/6.67 % Detected maximum model sizes of [2,max,max,max,max,max] % 45.24/6.67 % TRYING [1,1,1,1,1,1] % 45.24/6.67 % TRYING [1,1,1,1,2,1] % 45.24/6.67 % TRYING [1,1,1,1,3,1] % 45.24/6.67 % TRYING [1,1,1,2,3,1] % 45.24/6.67 % TRYING [1,1,1,3,3,1] % 45.24/6.67 % TRYING [1,1,2,3,3,1] % 45.24/6.67 % TRYING [1,2,2,3,3,1] % 45.24/6.67 % TRYING [2,7,2,2,3,1] % 45.24/6.67 % TRYING [2,2,2,3,3,1] % 45.24/6.67 % TRYING [2,6,3,2,3,1] % 45.24/6.67 % TRYING [2,3,2,3,3,1] % 45.24/6.67 % TRYING [2,2,3,3,3,1] % 45.24/6.67 % TRYING [2,8,2,2,3,1] % 45.24/6.67 % (4017896)Instruction limit reached! % 45.24/6.67 % (4017896)------------------------------ % 45.24/6.67 % (4017896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.67 % (4017896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.67 % (4017896)CaDiCaL version: 2.1.3 % 45.24/6.67 % (4017896)Termination reason: Instruction limit % 45.24/6.67 % (4017896)Termination phase: Saturation % 45.24/6.67 % (4017896)Time elapsed: 0.394 s % 45.24/6.67 % (4017896)Peak memory usage: 17 MB % 45.24/6.67 % (4017896)Instructions burned: 692 (million) % 45.24/6.67 % (4017891)Instruction limit reached! % 45.24/6.67 % (4017891)------------------------------ % 45.24/6.67 % (4017891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.67 % (4017891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.67 % (4017891)CaDiCaL version: 2.1.3 % 45.24/6.67 % (4017891)Termination reason: Instruction limit % 45.24/6.67 % (4017891)Termination phase: Saturation % 45.24/6.67 % (4017891)Time elapsed: 0.654 s % 45.24/6.67 % (4017891)Peak memory usage: 20 MB % 45.24/6.67 % (4017891)Instructions burned: 1179 (million) % 45.24/6.67 % (4017902)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1903548073:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 45.24/6.67 % (4017903)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=202820922:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 45.24/6.67 % TRYING [2,3,3,3,3,1] % 45.24/6.67 % TRYING [2,9,2,2,3,1] % 45.24/6.67 % (4017897)Instruction limit reached! % 45.24/6.67 % (4017897)------------------------------ % 45.24/6.67 % (4017897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.24/6.67 % (4017897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.24/6.67 % (4017897)CaDiCaL version: 2.1.3 % 45.24/6.67 % (4017897)Termination reason: Instruction limit % 45.24/6.67 % (4017897)Termination phase: Saturation % 45.24/6.67 % (4017897)Time elapsed: 0.516 s % 45.24/6.67 % (4017897)Peak memory usage: 19 MB % 45.24/6.67 % (4017897)Instructions burned: 880 (million) % 45.24/6.67 % (4017906)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3711988761:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 45.24/6.67 % Detected minimum model sizes of [1,1,1,1,1,1] % 45.24/6.67 % Detected maximum model sizes of [2,max,max,max,max,max] % 45.24/6.67 % fmb_start_size (= 20) larger than a detected sort maximum size! % 45.24/6.67 % (4017902)Refutation not found, incomplete strategy % 45.24/6.67 % (4017902)------------------------------ % 146.67/20.91 % (4017902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.67/20.91 % (4017902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.67/20.91 % (4017902)CaDiCaL version: 2.1.3 % 146.67/20.91 % (4017902)Termination reason: Refutation not found, incomplete strategy % 146.67/20.91 % (4017902)Time elapsed: 0.144 s % 146.67/20.91 % (4017902)Peak memory usage: 14 MB % 146.67/20.91 % (4017902)Instructions burned: 327 (million) % 146.67/20.91 % (4017902)------------------------------ % 146.67/20.91 % (4017902)------------------------------ % 146.67/20.91 % TRYING [2,2,4,3,3,1] % 146.67/20.91 % TRYING [2,4,4,2,3,1] % 146.67/20.91 % (4017908)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3530219919:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi) % 146.67/20.91 % Detected minimum model sizes of [1,1,1,1,1,1] % 146.67/20.91 % Detected maximum model sizes of [2,max,max,max,max,max] % 146.67/20.91 % fmb_start_size (= 8) larger than a detected sort maximum size! % 146.67/20.91 % (4017903)Refutation not found, incomplete strategy % 146.67/20.91 % (4017903)------------------------------ % 146.67/20.91 % (4017903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.67/20.91 % (4017903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.67/20.91 % (4017903)CaDiCaL version: 2.1.3 % 146.67/20.91 % (4017903)Termination reason: Refutation not found, incomplete strategy % 146.67/20.91 % (4017903)Time elapsed: 0.158 s % 146.67/20.91 % (4017903)Peak memory usage: 15 MB % 146.67/20.91 % (4017903)Instructions burned: 356 (million) % 146.67/20.91 % (4017903)------------------------------ % 146.67/20.91 % (4017903)------------------------------ % 146.67/20.91 % (4017910)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=614420015:i=6324_2988 on theBenchmark for (2988ds/6324Mi) % 146.67/20.91 % TRYING [2,4,4,2,4,1] % 146.67/20.91 % TRYING [2,4,3,3,3,1] % 146.67/20.91 % Detected minimum model sizes of [1,1,1,1,1,1] % 146.67/20.91 % Detected maximum model sizes of [2,max,max,max,max,max] % 146.67/20.91 % fmb_start_size (= 77) larger than a detected sort maximum size! % 146.67/20.91 % (4017910)Refutation not found, incomplete strategy % 146.67/20.91 % (4017910)------------------------------ % 146.67/20.91 % (4017910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.67/20.91 % (4017910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.67/20.91 % (4017910)CaDiCaL version: 2.1.3 % 146.67/20.91 % (4017910)Termination reason: Refutation not found, incomplete strategy % 146.67/20.91 % (4017910)Time elapsed: 0.156 s % 146.67/20.91 % (4017910)Peak memory usage: 15 MB % 146.67/20.91 % (4017910)Instructions burned: 354 (million) % 146.67/20.91 % (4017910)------------------------------ % 146.67/20.91 % (4017910)------------------------------ % 146.67/20.91 % (4017912)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=919609986:fmbsr=2.30978:i=2174_2987 on theBenchmark for (2987ds/2174Mi) % 146.67/20.91 % TRYING [2,4,4,2,5,1] % 146.67/20.91 % TRYING [2,3,4,3,3,1] % 146.67/20.91 % TRYING [2,4,4,2,6,1] % 146.67/20.91 % (4017912)Cannot represent all propositional literals internally % 146.67/20.91 % (4017912)Refutation not found, incomplete strategy % 146.67/20.91 % (4017912)------------------------------ % 146.67/20.91 % (4017912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.67/20.91 % (4017912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.67/20.91 % (4017912)CaDiCaL version: 2.1.3 % 146.67/20.91 % (4017912)Termination reason: Refutation not found, incomplete strategy % 146.67/20.91 % (4017912)Time elapsed: 0.218 s % 146.67/20.91 % (4017912)Peak memory usage: 16 MB % 146.67/20.91 % (4017912)Instructions burned: 457 (million) % 146.67/20.91 % (4017912)------------------------------ % 146.67/20.91 % (4017912)------------------------------ % 146.67/20.91 % (4017914)ott-2_1_sil=16000:newcnf=on:random_seed=636026407:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2984 on theBenchmark for (2984ds/869Mi) % 146.67/20.91 % TRYING [2,4,4,2,7,1] % 146.67/20.91 % TRYING [2,4,4,2,8,1] % 146.67/20.91 % (4017908)Instruction limit reached! % 146.67/20.91 % (4017908)------------------------------ % 146.67/20.91 % (4017908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.67/20.91 % (4017908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.67/20.91 % (4017908)CaDiCaL version: 2.1.3 % 146.67/20.91 % (4017908)Termination reason: Instruction limit % 146.67/20.91 % (4017908)Termination phase: Saturation % 146.67/20.91 % (4017908)Time elapsed: 0.714 s % 146.67/20.91 % (4017908)Peak memory usage: 19 MB % 146.67/20.91 % (4017908)Instructions burned: 1472 (million) % 146.67/20.91 % (4017916)ott+10_1_sil=32000:tgt=ground:random_seed=1128667484:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi) % 211.49/30.11 % TRYING [2,4,4,2,9,1] % 211.49/30.11 % (4017914)Instruction limit reached! % 211.49/30.11 % (4017914)------------------------------ % 211.49/30.11 % (4017914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.49/30.11 % (4017914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.49/30.11 % (4017914)CaDiCaL version: 2.1.3 % 211.49/30.11 % (4017914)Termination reason: Instruction limit % 211.49/30.11 % (4017914)Termination phase: Saturation % 211.49/30.11 % (4017914)Time elapsed: 0.420 s % 211.49/30.11 % (4017914)Peak memory usage: 17 MB % 211.49/30.11 % (4017914)Instructions burned: 871 (million) % 211.49/30.11 % (4017918)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3183076430:i=54282_2980 on theBenchmark for (2980ds/54282Mi) % 211.49/30.11 % TRYING [2,4,4,2,10,1] % 211.49/30.11 % TRYING [2,5,3,3,3,1] % 211.49/30.11 % Detected minimum model sizes of [1,1,1,1,1,1] % 211.49/30.11 % Detected maximum model sizes of [2,max,max,max,max,max] % 211.49/30.11 % TRYING [1,1,1,1,1,1] % 211.49/30.11 % TRYING [1,1,1,1,2,1] % 211.49/30.11 % TRYING [1,1,1,1,3,1] % 211.49/30.11 % TRYING [1,1,1,2,3,1] % 211.49/30.11 % TRYING [1,1,2,2,3,1] % 211.49/30.11 % TRYING [2,4,4,3,3,1] % 211.49/30.11 % TRYING [2,1,2,2,3,1] % 211.49/30.11 % TRYING [1,2,2,2,3,1] % 211.49/30.11 % TRYING [2,2,2,2,3,1] % 211.49/30.11 % TRYING [2,4,4,2,11,1] % 211.49/30.11 % TRYING [2,1,3,2,3,1] % 211.49/30.11 % TRYING [2,3,2,2,3,1] % 211.49/30.11 % TRYING [2,2,3,2,3,1] % 211.49/30.11 % TRYING [2,4,2,2,3,1] % 211.49/30.11 % TRYING [2,3,3,2,3,1] % 211.49/30.11 % TRYING [2,5,2,2,3,1] % 211.49/30.11 % TRYING [2,6,2,2,3,1] % 211.49/30.11 % TRYING [2,3,4,2,3,1] % 211.49/30.11 % TRYING [2,4,4,2,12,1] % 211.49/30.11 % TRYING [2,7,2,2,3,1] % 211.49/30.11 % TRYING [2,6,3,2,3,1] % 211.49/30.11 % TRYING [2,8,2,2,3,1] % 211.49/30.11 % TRYING [2,9,2,2,3,1] % 211.49/30.11 % TRYING [2,4,4,2,3,1] % 211.49/30.11 % TRYING [2,4,4,2,4,1] % 211.49/30.11 % TRYING [2,4,4,2,5,1] % 211.49/30.11 % TRYING [2,4,4,2,6,1] % 211.49/30.11 % TRYING [2,2,5,3,3,1] % 211.49/30.11 % TRYING [2,4,4,2,7,1] % 211.49/30.11 % TRYING [2,4,4,2,8,1] % 211.49/30.11 % (4017906)Instruction limit reached! % 211.49/30.11 % (4017906)------------------------------ % 211.49/30.11 % (4017906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.49/30.11 % (4017906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.49/30.11 % (4017906)CaDiCaL version: 2.1.3 % 211.49/30.11 % (4017906)Termination reason: Instruction limit % 211.49/30.11 % (4017906)Termination phase: Saturation % 211.49/30.11 % (4017906)Time elapsed: 2.637 s % 211.49/30.11 % (4017906)Peak memory usage: 30 MB % 211.49/30.11 % (4017906)Instructions burned: 5133 (million) % 211.49/30.11 % TRYING [2,6,3,3,3,1] % 211.49/30.11 % (4017921)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=665572630:i=3512:aac=none_2962 on theBenchmark for (2962ds/3512Mi) % 211.49/30.11 % TRYING [2,4,4,2,9,1] % 211.49/30.11 % TRYING [2,4,4,2,10,1] % 211.49/30.11 % TRYING [2,5,4,3,3,1] % 211.49/30.11 % TRYING [2,4,4,2,11,1] % 211.49/30.11 % TRYING [2,4,4,2,12,1] % 211.49/30.11 % (4017916)Instruction limit reached! % 211.49/30.11 % (4017916)------------------------------ % 211.49/30.11 % (4017916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.49/30.11 % (4017916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.49/30.11 % (4017916)CaDiCaL version: 2.1.3 % 211.49/30.11 % (4017916)Termination reason: Instruction limit % 211.49/30.11 % (4017916)Termination phase: Saturation % 211.49/30.11 % (4017916)Time elapsed: 2.836 s % 211.49/30.11 % (4017916)Peak memory usage: 34 MB % 211.49/30.11 % (4017916)Instructions burned: 5114 (million) % 211.49/30.11 % (4017923)dis+21_1_sil=32000:sas=cadical:random_seed=3966606786:i=3773:amm=off_2953 on theBenchmark for (2953ds/3773Mi) % 211.49/30.11 % TRYING [2,3,5,3,3,1] % 211.49/30.11 % (4017921)Instruction limit reached! % 211.49/30.11 % (4017921)------------------------------ % 211.49/30.11 % (4017921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.49/30.11 % (4017921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.49/30.11 % (4017921)CaDiCaL version: 2.1.3 % 211.49/30.11 % (4017921)Termination reason: Instruction limit % 211.49/30.11 % (4017921)Termination phase: Saturation % 211.49/30.11 % (4017921)Time elapsed: 1.864 s % 211.49/30.11 % (4017921)Peak memory usage: 27 MB % 211.49/30.11 % (4017921)Instructions burned: 3513 (million) % 211.49/30.11 % (4017925)ott+11_1_sil=16000:gs=on:random_seed=2391268594:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2944 on theBenchmark for (2944ds/2251Mi) % 211.49/30.11 % TRYING [2,4,4,2,13,1] % 211.49/30.11 % (4017900)Instruction limit reached! % 211.49/30.11 % (4017900)------------------------------ % 211.49/30.11 % (4017900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 211.49/30.11 % (4017900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.49/30.11 % (4017900)CaDiCaL version: 2.1.3 % 211.49/30.11 % (4017900)Termination reason: Instruction limit % 277.16/39.31 % (4017900)Termination phase: Finite model building SAT solving % 277.16/39.31 % (4017900)Time elapsed: 5.908 s % 277.16/39.31 % (4017900)Peak memory usage: 50 MB % 277.16/39.31 % (4017900)Instructions burned: 22062 (million) % 277.16/39.31 % (4017927)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3133723599:fmbsr=1.6:i=67534_2935 on theBenchmark for (2935ds/67534Mi) % 277.16/39.31 % (4017925)Instruction limit reached! % 277.16/39.31 % (4017925)------------------------------ % 277.16/39.31 % (4017925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.16/39.31 % (4017925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.16/39.31 % (4017925)CaDiCaL version: 2.1.3 % 277.16/39.31 % (4017925)Termination reason: Instruction limit % 277.16/39.31 % (4017925)Termination phase: Saturation % 277.16/39.31 % (4017925)Time elapsed: 1.146 s % 277.16/39.31 % (4017925)Peak memory usage: 23 MB % 277.16/39.31 % (4017925)Instructions burned: 2251 (million) % 277.16/39.31 % (4017923)Instruction limit reached! % 277.16/39.31 % (4017923)------------------------------ % 277.16/39.31 % (4017923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.16/39.31 % (4017923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.16/39.31 % (4017923)CaDiCaL version: 2.1.3 % 277.16/39.31 % (4017923)Termination reason: Instruction limit % 277.16/39.31 % (4017923)Termination phase: Saturation % 277.16/39.31 % (4017923)Time elapsed: 2.084 s % 277.16/39.31 % (4017923)Peak memory usage: 32 MB % 277.16/39.31 % (4017923)Instructions burned: 3773 (million) % 277.16/39.31 % (4017929)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3040416043:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2932 on theBenchmark for (2932ds/4591Mi) % 277.16/39.31 % (4017930)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1000725813:i=29340_2932 on theBenchmark for (2932ds/29340Mi) % 277.16/39.31 % TRYING [7] % 277.16/39.31 % TRYING [2,4,4,2,13,1] % 277.16/39.31 % (4017929)Instruction limit reached! % 277.16/39.31 % (4017929)------------------------------ % 277.16/39.31 % (4017929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.16/39.31 % (4017929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.16/39.32 % (4017929)CaDiCaL version: 2.1.3 % 277.16/39.32 % (4017929)Termination reason: Instruction limit % 277.16/39.32 % (4017929)Termination phase: Saturation % 277.16/39.32 % (4017929)Time elapsed: 2.204 s % 277.16/39.32 % (4017929)Peak memory usage: 47 MB % 277.16/39.32 % (4017929)Instructions burned: 4591 (million) % 277.16/39.32 % (4017933)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=978824590:i=5211_2910 on theBenchmark for (2910ds/5211Mi) % 277.16/39.32 % (4017933)Instruction limit reached! % 277.16/39.32 % (4017933)------------------------------ % 277.16/39.32 % (4017933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.16/39.32 % (4017933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.16/39.32 % (4017933)CaDiCaL version: 2.1.3 % 277.16/39.32 % (4017933)Termination reason: Instruction limit % 277.16/39.32 % (4017933)Termination phase: Saturation % 277.16/39.32 % (4017933)Time elapsed: 2.823 s % 277.16/39.32 % (4017933)Peak memory usage: 50 MB % 277.16/39.32 % (4017933)Instructions burned: 5212 (million) % 277.16/39.32 % (4017935)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1271407085:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi) % 277.16/39.32 % Detected minimum model sizes of [1,1,1,1,1,1] % 277.16/39.32 % Detected maximum model sizes of [2,max,max,max,max,max] % 277.16/39.32 % fmb_start_size (= 17) larger than a detected sort maximum size! % 277.16/39.32 % (4017935)Refutation not found, incomplete strategy % 277.16/39.32 % (4017935)------------------------------ % 277.16/39.32 % (4017935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.16/39.32 % (4017935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.16/39.32 % (4017935)CaDiCaL version: 2.1.3 % 277.16/39.32 % (4017935)Termination reason: Refutation not found, incomplete strategy % 277.16/39.32 % (4017935)Time elapsed: 0.129 s % 277.16/39.32 % (4017935)Peak memory usage: 14 MB % 277.16/39.32 % (4017935)Instructions burned: 292 (million) % 277.16/39.32 % (4017935)------------------------------ % 277.16/39.32 % (4017935)------------------------------ % 277.16/39.32 % (4017937)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4191720887:fmbsr=2:i=46332_2880 on theBenchmark for (2880ds/46332Mi) % 277.16/39.32 % TRYING [15] % 277.16/39.32 % (4017930)Instruction limit reached! % 277.16/39.32 % (4017930)------------------------------ % 295.47/41.92 % (4017930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.47/41.92 % (4017930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.47/41.92 % (4017930)CaDiCaL version: 2.1.3 % 295.47/41.92 % (4017930)Termination reason: Instruction limit % 295.47/41.92 % (4017930)Termination phase: Saturation % 295.47/41.92 % (4017930)Time elapsed: 13.909 s % 295.47/41.92 % (4017930)Peak memory usage: 204 MB % 295.47/41.92 % (4017930)Instructions burned: 29340 (million) % 295.47/41.92 % (4017939)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1869771549:i=14071_2792 on theBenchmark for (2792ds/14071Mi) % 295.47/41.92 % Detected minimum model sizes of [1,1,1,1,1,1] % 295.47/41.92 % Detected maximum model sizes of [2,max,max,max,max,max] % 295.47/41.92 % fmb_start_size (= 12) larger than a detected sort maximum size! % 295.47/41.92 % (4017939)Refutation not found, incomplete strategy % 295.47/41.92 % (4017939)------------------------------ % 295.47/41.92 % (4017939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.47/41.92 % (4017939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.47/41.92 % (4017939)CaDiCaL version: 2.1.3 % 295.47/41.92 % (4017939)Termination reason: Refutation not found, incomplete strategy % 295.47/41.92 % (4017939)Time elapsed: 0.159 s % 295.47/41.92 % (4017939)Peak memory usage: 15 MB % 295.47/41.92 % (4017939)Instructions burned: 356 (million) % 295.47/41.92 % (4017939)------------------------------ % 295.47/41.92 % (4017939)------------------------------ % 295.47/41.92 % (4017941)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1046417117:i=22565:add=on:rawr=on_2790 on theBenchmark for (2790ds/22565Mi) % 295.47/41.92 % (4017918)Instruction limit reached! % 295.47/41.92 % (4017918)------------------------------ % 295.47/41.92 % (4017918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.47/41.92 % (4017918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.47/41.92 % (4017918)CaDiCaL version: 2.1.3 % 295.47/41.92 % (4017918)Termination reason: Instruction limit % 295.47/41.92 % (4017918)Termination phase: Finite model building SAT solving % 295.47/41.92 % (4017918)Time elapsed: 23.460 s % 295.47/41.92 % (4017918)Peak memory usage: 67 MB % 295.47/41.92 % (4017918)Instructions burned: 54285 (million) % 295.47/41.92 % (4017943)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2372802844:i=8173:av=off_2745 on theBenchmark for (2745ds/8173Mi) % 295.47/41.92 % (4017937)Instruction limit reached! % 295.47/41.92 % (4017937)------------------------------ % 295.47/41.92 % (4017937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.47/41.92 % (4017937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.47/41.92 % (4017937)CaDiCaL version: 2.1.3 % 295.47/41.92 % (4017937)Termination reason: Instruction limit % 295.47/41.92 % (4017937)Termination phase: Finite model building constraint generation % 295.47/41.92 % (4017937)Time elapsed: 15.559 s % 295.47/41.92 % (4017937)Peak memory usage: 2395 MB % 295.47/41.92 % (4017937)Instructions burned: 46333 (million) % 295.47/41.92 % (4017927)Instruction limit reached! % 295.47/41.92 % (4017927)------------------------------ % 295.47/41.92 % (4017927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.47/41.92 % (4017927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.47/41.92 % (4017927)CaDiCaL version: 2.1.3 % 295.47/41.92 % (4017927)Termination reason: Instruction limit % 295.47/41.92 % (4017927)Termination phase: Finite model building SAT solving % 295.47/41.92 % (4017927)Time elapsed: 21.279 s % 295.47/41.92 % (4017927)Peak memory usage: 2211 MB % 295.47/41.92 % (4017927)Instructions burned: 67535 (million) % 295.47/41.92 % (4017945)dis+10_16:1_sil=16000:random_seed=2676277225:i=9155:fsr=off_2721 on theBenchmark for (2721ds/9155Mi) % 295.47/41.92 % (4017947)ott-3_8_sil=64000:random_seed=3001793558:i=20139:bs=on_2720 on theBenchmark for (2720ds/20139Mi) % 295.47/41.92 % (4017943)Instruction limit reached! % 295.47/41.92 % (4017943)------------------------------ % 295.47/41.92 % (4017943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.47/41.92 % (4017943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.47/41.92 % (4017943)CaDiCaL version: 2.1.3 % 295.47/41.92 % (4017943)Termination reason: Instruction limit % 295.47/41.92 % (4017943)Termination phase: Saturation % 295.47/41.92 % (4017943)Time elapsed: 4.408 s % 295.47/41.92 % (4017943)Peak memory usage: 49 MB % 295.47/41.92 % (4017943)Instructions burned: 8174 (million) % 295.47/41.92 % (4017949)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=903042470:fmbsr=2:i=32576_2701 on theBenchmark for (2701ds/32576Mi) % 300.25/42.63 % Detected minimum model sizes of [1,1,1,1,1,1] % 300.25/42.63 % Detected maximum model sizes of [2,max,max,max,max,max] % 300.25/42.63 % fmb_start_size (= 9) larger than a detected sort maximum size! % 300.25/42.63 % (4017949)Refutation not found, incomplete strategy % 300.25/42.63 % (4017949)------------------------------ % 300.25/42.63 % (4017949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.63 % (4017949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.63 % (4017949)CaDiCaL version: 2.1.3 % 300.25/42.63 % (4017949)Termination reason: Refutation not found, incomplete strategy % 300.25/42.63 % (4017949)Time elapsed: 0.160 s % 300.25/42.63 % (4017949)Peak memory usage: 15 MB % 300.25/42.63 % (4017949)Instructions burned: 354 (million) % 300.25/42.63 % (4017949)------------------------------ % 300.25/42.63 % (4017949)------------------------------ % 300.25/42.63 % (4017951)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4085757398:i=11404_2699 on theBenchmark for (2699ds/11404Mi) % 300.25/42.63 % (4017945)Instruction limit reached! % 300.25/42.63 % (4017945)------------------------------ % 300.25/42.63 % (4017945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.63 % (4017945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.63 % (4017945)CaDiCaL version: 2.1.3 % 300.25/42.63 % (4017945)Termination reason: Instruction limit % 300.25/42.63 % (4017945)Termination phase: Saturation % 300.25/42.63 % (4017945)Time elapsed: 4.849 s % 300.25/42.63 % (4017945)Peak memory usage: 68 MB % 300.25/42.63 % (4017945)Instructions burned: 9156 (million) % 300.25/42.63 % (4017953)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4265915792:i=14134_2672 on theBenchmark for (2672ds/14134Mi) % 300.25/42.63 % (4017947)Instruction limit reached! % 300.25/42.63 % (4017947)------------------------------ % 300.25/42.63 % (4017947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.63 % (4017947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.63 % (4017947)CaDiCaL version: 2.1.3 % 300.25/42.63 % (4017947)Termination reason: Instruction limit % 300.25/42.63 % (4017947)Termination phase: Saturation % 300.25/42.63 % (4017947)Time elapsed: 6.659 s % 300.25/42.63 % (4017947)Peak memory usage: 82 MB % 300.25/42.63 % (4017947)Instructions burned: 20140 (million) % 300.25/42.63 % (4017955)dis+33_16_sil=32000:sac=on:random_seed=459406675:i=15851:nm=0_2653 on theBenchmark for (2653ds/15851Mi) % 300.25/42.63 % (4017941)Instruction limit reached! % 300.25/42.63 % (4017941)------------------------------ % 300.25/42.63 % (4017941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.63 % (4017941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.63 % (4017941)CaDiCaL version: 2.1.3 % 300.25/42.63 % (4017941)Termination reason: Instruction limit % 300.25/42.63 % (4017941)Termination phase: Saturation % 300.25/42.63 % (4017941)Time elapsed: 14.413 s % 300.25/42.63 % (4017941)Peak memory usage: 156 MB % 300.25/42.63 % (4017941)Instructions burned: 22566 (million) % 300.25/42.63 % (4017957)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3368196204:avsq=on:i=17627:add=on:amm=off_2646 on theBenchmark for (2646ds/17627Mi) % 300.25/42.63 % (4017951)Instruction limit reached! % 300.25/42.63 % (4017951)------------------------------ % 300.25/42.63 % (4017951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.63 % (4017951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.63 % (4017951)CaDiCaL version: 2.1.3 % 300.25/42.63 % (4017951)Termination reason: Instruction limit % 300.25/42.63 % (4017951)Termination phase: Saturation % 300.25/42.63 % (4017951)Time elapsed: 6.520 s % 300.25/42.63 % (4017951)Peak memory usage: 75 MB % 300.25/42.63 % (4017951)Instructions burned: 11405 (million) % 300.25/42.63 % (4017959)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1482951806:s2a=on:i=53295_2633 on theBenchmark for (2633ds/53295Mi) % 300.25/42.63 % (4017955)Instruction limit reached! % 300.25/42.63 % (4017955)------------------------------ % 300.25/42.63 % (4017955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.25/42.63 % (4017955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.25/42.63 % (4017955)CaDiCaL version: 2.1.3 % 300.25/42.63 % (4017955)Termination reason: Instruction limit % 300.25/42.63 % (4017955)Termination phase: Saturation % 300.25/42.63 % (4017955)Time elapsed: 4.446 s % 300.25/42.63 % (4017955)Peak memory usage: 9 % 300.25/42.63 Terminated % 300.25/42.63 % Vampire exiting % 300.25/42.64 Terminated %------------------------------------------------------------------------------