%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW472_20 : 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 : n012.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:08 PM UTC 2026 % Result : Timeout 291.70s 41.56s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWW472_20 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 14:04:19 UTC 2026 % 0.00/0.10 % CPUTime : % 0.00/0.10 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.12 Running first-order model finding % 0.09/0.12 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 % 4.26/0.90 % (3393201)Will run a generic schedule for satisfiability detection. % 4.26/0.90 % (3393207)% WARNING: option uhcvi not known. % 4.26/0.90 % (3393208)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=785744002:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 4.26/0.90 % (3393206)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=671432152_2999 on theBenchmark for (2999ds/0Mi) % 4.26/0.90 % (3393207)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1758177029:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 4.26/0.90 % (3393209)dis+10_1_sil=32000:sp=arity:random_seed=3692971539:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 4.26/0.90 % (3393210)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3381259470:i=116_2999 on theBenchmark for (2999ds/116Mi) % 4.26/0.90 % (3393211)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1503224555:i=131_2999 on theBenchmark for (2999ds/131Mi) % 4.26/0.90 % (3393212)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2026280782:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 4.26/0.90 % (3393209)Instruction limit reached! % 4.26/0.90 % (3393209)------------------------------ % 4.26/0.90 % (3393209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.26/0.90 % (3393209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.26/0.90 % (3393209)CaDiCaL version: 2.1.3 % 4.26/0.90 % (3393209)Termination reason: Instruction limit % 4.26/0.90 % (3393209)Termination phase: Saturation % 4.26/0.90 % (3393209)Time elapsed: 0.030 s % 4.26/0.90 % (3393209)Peak memory usage: 13 MB % 4.26/0.90 % (3393209)Instructions burned: 104 (million) % 4.26/0.90 % (3393210)Instruction limit reached! % 4.26/0.90 % (3393210)------------------------------ % 4.26/0.90 % (3393210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.26/0.90 % (3393210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.26/0.90 % (3393210)CaDiCaL version: 2.1.3 % 4.26/0.90 % (3393210)Termination reason: Instruction limit % 4.26/0.90 % (3393210)Termination phase: Saturation % 4.26/0.90 % (3393210)Time elapsed: 0.032 s % 4.26/0.90 % (3393210)Peak memory usage: 13 MB % 4.26/0.90 % (3393210)Instructions burned: 118 (million) % 4.26/0.90 % (3393220)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3211386531:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 4.26/0.90 % (3393211)Instruction limit reached! % 4.26/0.90 % (3393211)------------------------------ % 4.26/0.90 % (3393211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.26/0.90 % (3393211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.26/0.90 % (3393211)CaDiCaL version: 2.1.3 % 4.26/0.90 % (3393211)Termination reason: Instruction limit % 4.26/0.90 % (3393211)Termination phase: Saturation % 4.26/0.90 % (3393211)Time elapsed: 0.043 s % 4.26/0.90 % (3393211)Peak memory usage: 13 MB % 4.26/0.90 % (3393211)Instructions burned: 133 (million) % 4.26/0.90 % (3393221)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2829812948:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 4.26/0.90 % (3393212)Instruction limit reached! % 4.26/0.90 % (3393212)------------------------------ % 4.26/0.90 % (3393212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.26/0.90 % (3393212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.26/0.90 % (3393212)CaDiCaL version: 2.1.3 % 4.26/0.90 % (3393212)Termination reason: Instruction limit % 4.26/0.90 % (3393212)Termination phase: Saturation % 4.26/0.90 % (3393212)Time elapsed: 0.049 s % 4.26/0.90 % (3393212)Peak memory usage: 13 MB % 4.26/0.90 % (3393212)Instructions burned: 162 (million) % 4.26/0.90 % (3393224)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=2430811472:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 4.26/0.90 % (3393225)ott-21_1_sil=16000:fs=off:random_seed=472582712:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 4.26/0.90 % (3393221)Instruction limit reached! % 4.26/0.90 % (3393221)------------------------------ % 4.26/0.90 % (3393221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 4.26/0.90 % (3393221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.26/0.90 % (3393221)CaDiCaL version: 2.1.3 % 11.14/1.85 % (3393221)Termination reason: Instruction limit % 11.14/1.85 % (3393221)Termination phase: Saturation % 11.14/1.85 % (3393221)Time elapsed: 0.042 s % 11.14/1.85 % (3393221)Peak memory usage: 13 MB % 11.14/1.85 % (3393221)Instructions burned: 132 (million) % 11.14/1.85 % (3393228)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3767617603:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 11.14/1.85 % (3393225)Instruction limit reached! % 11.14/1.85 % (3393225)------------------------------ % 11.14/1.85 % (3393225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.14/1.85 % (3393225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/1.85 % (3393225)CaDiCaL version: 2.1.3 % 11.14/1.85 % (3393225)Termination reason: Instruction limit % 11.14/1.85 % (3393225)Termination phase: Saturation % 11.14/1.85 % (3393225)Time elapsed: 0.048 s % 11.14/1.85 % (3393225)Peak memory usage: 13 MB % 11.14/1.85 % (3393225)Instructions burned: 181 (million) % 11.14/1.85 % (3393230)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1714096650:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 11.14/1.85 % TRYING [1] % 11.14/1.85 % TRYING [2] % 11.14/1.85 % TRYING [3] % 11.14/1.85 % (3393220)Instruction limit reached! % 11.14/1.85 % (3393220)------------------------------ % 11.14/1.85 % (3393220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.14/1.85 % (3393220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/1.85 % (3393220)CaDiCaL version: 2.1.3 % 11.14/1.85 % (3393220)Termination reason: Instruction limit % 11.14/1.85 % (3393220)Termination phase: Finite model building constraint generation % 11.14/1.85 % (3393220)Time elapsed: 0.169 s % 11.14/1.85 % (3393220)Peak memory usage: 39 MB % 11.14/1.85 % (3393220)Instructions burned: 716 (million) % 11.14/1.85 % (3393233)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3526563302:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 11.14/1.85 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 11.14/1.85 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 11.14/1.85 % TRYING [1,1,1,1,1,1,1] % 11.14/1.85 % TRYING [1,1,1,1,2,1,1] % 11.14/1.85 % TRYING [1,1,1,1,2,2,1] % 11.14/1.85 % TRYING [1,1,1,1,3,2,1] % 11.14/1.85 % (3393228)Instruction limit reached! % 11.14/1.85 % (3393228)------------------------------ % 11.14/1.85 % (3393228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.14/1.85 % (3393228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/1.85 % (3393228)CaDiCaL version: 2.1.3 % 11.14/1.85 % (3393228)Termination reason: Instruction limit % 11.14/1.85 % (3393228)Termination phase: Saturation % 11.14/1.85 % (3393228)Time elapsed: 0.150 s % 11.14/1.85 % (3393228)Peak memory usage: 14 MB % 11.14/1.85 % (3393228)Instructions burned: 480 (million) % 11.14/1.85 % (3393224)Instruction limit reached! % 11.14/1.85 % (3393224)------------------------------ % 11.14/1.85 % (3393224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.14/1.85 % (3393224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/1.85 % (3393224)CaDiCaL version: 2.1.3 % 11.14/1.85 % (3393224)Termination reason: Instruction limit % 11.14/1.85 % (3393224)Termination phase: Saturation % 11.14/1.85 % (3393224)Time elapsed: 0.197 s % 11.14/1.85 % (3393224)Peak memory usage: 17 MB % 11.14/1.85 % (3393224)Instructions burned: 686 (million) % 11.14/1.85 % TRYING [1,1,1,2,3,2,1] % 11.14/1.85 % (3393235)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1182426393:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 11.14/1.85 % (3393236)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=1726678716: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) % 11.14/1.85 % TRYING [1,1,2,2,3,2,1] % 11.14/1.85 % TRYING [1,2,2,2,3,2,1] % 11.14/1.85 % TRYING [1,3,2,2,3,2,1] % 11.14/1.85 % (3393230)Instruction limit reached! % 11.14/1.85 % (3393230)------------------------------ % 11.14/1.85 % (3393230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.14/1.85 % (3393230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.14/1.85 % (3393230)CaDiCaL version: 2.1.3 % 11.14/1.85 % (3393230)Termination reason: Instruction limit % 11.14/1.85 % (3393230)Termination phase: Finite model building preprocessing % 11.14/1.85 % (3393230)Time elapsed: 0.202 s % 11.14/1.85 % (3393230)Peak memory usage: 20 MB % 11.14/1.85 % (3393230)Instructions burned: 869 (million) % 11.14/1.85 % (3393239)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4081087603:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 37.08/5.42 % TRYING [1,3,2,2,4,2,1] % 37.08/5.42 % TRYING [1,3,2,2,5,2,1] % 37.08/5.42 % TRYING [1,3,2,2,6,2,1] % 37.08/5.42 % (3393235)Instruction limit reached! % 37.08/5.42 % (3393235)------------------------------ % 37.08/5.42 % (3393235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.08/5.42 % (3393235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.08/5.42 % (3393235)CaDiCaL version: 2.1.3 % 37.08/5.42 % (3393235)Termination reason: Instruction limit % 37.08/5.42 % (3393235)Termination phase: Finite model building preprocessing % 37.08/5.42 % (3393235)Time elapsed: 0.208 s % 37.08/5.42 % (3393235)Peak memory usage: 21 MB % 37.08/5.42 % (3393235)Instructions burned: 892 (million) % 37.08/5.42 % TRYING [1,3,2,2,7,2,1] % 37.08/5.42 % (3393241)fmb+10_1_sil=64000:random_seed=2080679246:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 37.08/5.42 % (3393236)Instruction limit reached! % 37.08/5.42 % (3393236)------------------------------ % 37.08/5.42 % (3393236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.08/5.42 % (3393236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.08/5.42 % (3393236)CaDiCaL version: 2.1.3 % 37.08/5.42 % (3393236)Termination reason: Instruction limit % 37.08/5.42 % (3393236)Termination phase: Saturation % 37.08/5.42 % (3393236)Time elapsed: 0.225 s % 37.08/5.42 % (3393236)Peak memory usage: 18 MB % 37.08/5.42 % (3393236)Instructions burned: 695 (million) % 37.08/5.42 % (3393243)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2554585394:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 37.08/5.42 % TRYING [1,3,2,2,8,2,1] % 37.08/5.42 % TRYING [1,3,2,2,9,2,1] % 37.08/5.42 % (3393233)Instruction limit reached! % 37.08/5.42 % (3393233)------------------------------ % 37.08/5.42 % (3393233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.08/5.42 % (3393233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.08/5.42 % (3393233)CaDiCaL version: 2.1.3 % 37.08/5.42 % (3393233)Termination reason: Instruction limit % 37.08/5.42 % (3393233)Termination phase: Saturation % 37.08/5.42 % (3393233)Time elapsed: 0.371 s % 37.08/5.42 % (3393233)Peak memory usage: 19 MB % 37.08/5.42 % (3393233)Instructions burned: 1179 (million) % 37.08/5.42 % (3393245)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2150620268:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 37.08/5.42 % (3393239)Instruction limit reached! % 37.08/5.42 % (3393239)------------------------------ % 37.08/5.42 % (3393239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.08/5.42 % (3393239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.08/5.42 % (3393239)CaDiCaL version: 2.1.3 % 37.08/5.42 % (3393239)Termination reason: Instruction limit % 37.08/5.42 % (3393239)Termination phase: Saturation % 37.08/5.42 % (3393239)Time elapsed: 0.276 s % 37.08/5.42 % (3393239)Peak memory usage: 19 MB % 37.08/5.42 % (3393239)Instructions burned: 880 (million) % 37.08/5.42 % (3393247)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=490846624:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 37.08/5.42 % TRYING [1,3,2,2,10,2,1] % 37.08/5.42 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 37.08/5.42 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 37.08/5.42 % TRYING [1,1,1,1,1,1,1] % 37.08/5.42 % TRYING [1,1,1,1,2,1,1] % 37.08/5.42 % TRYING [1,1,1,1,2,2,1] % 37.08/5.42 % TRYING [1,1,1,1,3,2,1] % 37.08/5.42 % TRYING [1,3,2,2,11,2,1] % 37.08/5.42 % TRYING [1,1,1,1,3,3,1] % 37.08/5.42 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 37.08/5.42 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 37.08/5.42 % fmb_start_size (= 20) larger than a detected sort maximum size! % 37.08/5.42 % (3393243)Refutation not found, incomplete strategy % 37.08/5.42 % (3393243)------------------------------ % 37.08/5.42 % (3393243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.08/5.42 % (3393243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.08/5.42 % (3393243)CaDiCaL version: 2.1.3 % 37.08/5.42 % (3393243)Termination reason: Refutation not found, incomplete strategy % 37.08/5.42 % (3393243)Time elapsed: 0.231 s % 37.08/5.42 % (3393243)Peak memory usage: 21 MB % 37.08/5.42 % (3393243)Instructions burned: 984 (million) % 37.08/5.42 % (3393243)------------------------------ % 37.08/5.42 % (3393243)------------------------------ % 37.08/5.42 % TRYING [1,1,1,2,3,3,1] % 37.08/5.42 % (3393249)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2961298419:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 91.87/13.25 % TRYING [1,1,2,2,3,3,1] % 91.87/13.25 % TRYING [1,1,3,2,3,3,1] % 91.87/13.25 % (3393245)Instruction limit reached! % 91.87/13.25 % (3393245)------------------------------ % 91.87/13.25 % (3393245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.87/13.25 % (3393245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.87/13.25 % (3393245)CaDiCaL version: 2.1.3 % 91.87/13.25 % (3393245)Termination reason: Instruction limit % 91.87/13.25 % (3393245)Termination phase: Finite model building preprocessing % 91.87/13.25 % (3393245)Time elapsed: 0.219 s % 91.87/13.25 % (3393245)Peak memory usage: 21 MB % 91.87/13.25 % (3393245)Instructions burned: 921 (million) % 91.87/13.25 % (3393251)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2398671660:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 91.87/13.25 % TRYING [1,3,2,2,12,2,1] % 91.87/13.25 % TRYING [1,2,3,2,3,3,1] % 91.87/13.25 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 91.87/13.25 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 91.87/13.25 % fmb_start_size (= 77) larger than a detected sort maximum size! % 91.87/13.25 % (3393251)Refutation not found, incomplete strategy % 91.87/13.25 % (3393251)------------------------------ % 91.87/13.25 % (3393251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.87/13.25 % (3393251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.87/13.25 % (3393251)CaDiCaL version: 2.1.3 % 91.87/13.25 % (3393251)Termination reason: Refutation not found, incomplete strategy % 91.87/13.25 % (3393251)Time elapsed: 0.237 s % 91.87/13.25 % (3393251)Peak memory usage: 21 MB % 91.87/13.25 % (3393251)Instructions burned: 1008 (million) % 91.87/13.25 % (3393251)------------------------------ % 91.87/13.25 % (3393251)------------------------------ % 91.87/13.25 % (3393253)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=160747036:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi) % 91.87/13.25 % TRYING [1,3,3,2,3,3,1] % 91.87/13.25 % (3393249)Instruction limit reached! % 91.87/13.25 % (3393249)------------------------------ % 91.87/13.25 % (3393249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.87/13.25 % (3393249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.87/13.25 % (3393249)CaDiCaL version: 2.1.3 % 91.87/13.25 % (3393249)Termination reason: Instruction limit % 91.87/13.25 % (3393249)Termination phase: Saturation % 91.87/13.25 % (3393249)Time elapsed: 0.428 s % 91.87/13.25 % (3393249)Peak memory usage: 23 MB % 91.87/13.25 % (3393249)Instructions burned: 1475 (million) % 91.87/13.25 % (3393255)ott-2_1_sil=16000:newcnf=on:random_seed=3911225899:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2987 on theBenchmark for (2987ds/869Mi) % 91.87/13.25 % (3393253)Cannot represent all propositional literals internally % 91.87/13.25 % (3393253)Refutation not found, incomplete strategy % 91.87/13.25 % (3393253)------------------------------ % 91.87/13.25 % (3393253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.87/13.25 % (3393253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.87/13.25 % (3393253)CaDiCaL version: 2.1.3 % 91.87/13.25 % (3393253)Termination reason: Refutation not found, incomplete strategy % 91.87/13.25 % (3393253)Time elapsed: 0.214 s % 91.87/13.25 % (3393253)Peak memory usage: 21 MB % 91.87/13.25 % (3393253)Instructions burned: 824 (million) % 91.87/13.25 % (3393253)------------------------------ % 91.87/13.25 % (3393253)------------------------------ % 91.87/13.25 % (3393257)ott+10_1_sil=32000:tgt=ground:random_seed=3976691337:i=5114:av=off_2986 on theBenchmark for (2986ds/5114Mi) % 91.87/13.25 % (3393255)Instruction limit reached! % 91.87/13.25 % (3393255)------------------------------ % 91.87/13.25 % (3393255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.87/13.25 % (3393255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.87/13.25 % (3393255)CaDiCaL version: 2.1.3 % 91.87/13.25 % (3393255)Termination reason: Instruction limit % 91.87/13.25 % (3393255)Termination phase: Saturation % 91.87/13.25 % (3393255)Time elapsed: 0.249 s % 91.87/13.25 % (3393255)Peak memory usage: 19 MB % 91.87/13.25 % (3393255)Instructions burned: 869 (million) % 91.87/13.25 % (3393259)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3906714374:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 91.87/13.25 % TRYING [1,4,3,2,3,3,1] % 91.87/13.25 % TRYING [1,4,2,2,12,2,1] % 91.87/13.25 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 91.87/13.25 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 91.87/13.25 % TRYING [1,1,1,1,1,1,1] % 91.87/13.25 % TRYING [1,1,1,1,2,1,1] % 91.87/13.25 % TRYING [1,1,1,1,2,2,1] % 140.97/20.16 % TRYING [1,1,1,1,3,2,1] % 140.97/20.16 % TRYING [1,1,1,2,3,2,1] % 140.97/20.16 % TRYING [1,1,2,2,3,2,1] % 140.97/20.16 % TRYING [1,2,2,2,3,2,1] % 140.97/20.16 % TRYING [1,3,2,2,3,2,1] % 140.97/20.16 % TRYING [1,3,2,2,4,2,1] % 140.97/20.16 % TRYING [1,3,2,2,5,2,1] % 140.97/20.16 % TRYING [1,3,2,2,6,2,1] % 140.97/20.16 % TRYING [1,5,3,2,3,3,1] % 140.97/20.16 % TRYING [1,3,2,2,7,2,1] % 140.97/20.16 % TRYING [1,3,2,2,8,2,1] % 140.97/20.16 % TRYING [1,3,2,2,9,2,1] % 140.97/20.16 % TRYING [1,3,2,2,10,2,1] % 140.97/20.16 % (3393247)Instruction limit reached! % 140.97/20.16 % (3393247)------------------------------ % 140.97/20.16 % (3393247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.97/20.16 % (3393247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.97/20.16 % (3393247)CaDiCaL version: 2.1.3 % 140.97/20.16 % (3393247)Termination reason: Instruction limit % 140.97/20.16 % (3393247)Termination phase: Saturation % 140.97/20.16 % (3393247)Time elapsed: 1.503 s % 140.97/20.16 % (3393247)Peak memory usage: 36 MB % 140.97/20.16 % (3393247)Instructions burned: 5131 (million) % 140.97/20.16 % (3393261)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3229619662:i=3512:aac=none_2978 on theBenchmark for (2978ds/3512Mi) % 140.97/20.16 % TRYING [1,3,2,2,11,2,1] % 140.97/20.16 % TRYING [1,3,2,2,12,2,1] % 140.97/20.16 % TRYING [1,4,4,2,3,3,1] % 140.97/20.16 % (3393257)Instruction limit reached! % 140.97/20.16 % (3393257)------------------------------ % 140.97/20.16 % (3393257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.97/20.16 % (3393257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.97/20.16 % (3393257)CaDiCaL version: 2.1.3 % 140.97/20.16 % (3393257)Termination reason: Instruction limit % 140.97/20.16 % (3393257)Termination phase: Saturation % 140.97/20.16 % (3393257)Time elapsed: 1.531 s % 140.97/20.16 % (3393257)Peak memory usage: 31 MB % 140.97/20.16 % (3393257)Instructions burned: 5117 (million) % 140.97/20.16 % (3393263)dis+21_1_sil=32000:sas=cadical:random_seed=2843077885:i=3773:amm=off_2971 on theBenchmark for (2971ds/3773Mi) % 140.97/20.16 % TRYING [1,4,2,2,12,2,1] % 140.97/20.16 % TRYING [1,5,4,2,3,3,1] % 140.97/20.16 % (3393261)Instruction limit reached! % 140.97/20.16 % (3393261)------------------------------ % 140.97/20.16 % (3393261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.97/20.16 % (3393261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.97/20.16 % (3393261)CaDiCaL version: 2.1.3 % 140.97/20.16 % (3393261)Termination reason: Instruction limit % 140.97/20.16 % (3393261)Termination phase: Saturation % 140.97/20.16 % (3393261)Time elapsed: 1.083 s % 140.97/20.16 % (3393261)Peak memory usage: 33 MB % 140.97/20.16 % (3393261)Instructions burned: 3512 (million) % 140.97/20.16 % (3393265)ott+11_1_sil=16000:gs=on:random_seed=2277469336:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2967 on theBenchmark for (2967ds/2251Mi) % 140.97/20.16 % (3393265)Instruction limit reached! % 140.97/20.16 % (3393265)------------------------------ % 140.97/20.16 % (3393265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.97/20.16 % (3393265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.97/20.16 % (3393265)CaDiCaL version: 2.1.3 % 140.97/20.16 % (3393265)Termination reason: Instruction limit % 140.97/20.16 % (3393265)Termination phase: Saturation % 140.97/20.16 % (3393265)Time elapsed: 0.634 s % 140.97/20.16 % (3393265)Peak memory usage: 26 MB % 140.97/20.16 % (3393265)Instructions burned: 2254 (million) % 140.97/20.16 % (3393267)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2184270054:fmbsr=1.6:i=67534_2960 on theBenchmark for (2960ds/67534Mi) % 140.97/20.16 % TRYING [1,4,5,2,3,3,1] % 140.97/20.16 % (3393263)Instruction limit reached! % 140.97/20.16 % (3393263)------------------------------ % 140.97/20.16 % (3393263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 140.97/20.16 % (3393263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.97/20.16 % (3393263)CaDiCaL version: 2.1.3 % 140.97/20.16 % (3393263)Termination reason: Instruction limit % 140.97/20.16 % (3393263)Termination phase: Saturation % 140.97/20.16 % (3393263)Time elapsed: 1.157 s % 140.97/20.16 % (3393263)Peak memory usage: 38 MB % 140.97/20.16 % (3393263)Instructions burned: 3777 (million) % 140.97/20.16 % (3393269)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=967222438:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2959 on theBenchmark for (2959ds/4591Mi) % 140.97/20.16 % TRYING [7] % 140.97/20.16 % TRYING [1,6,3,2,3,3,1] % 140.97/20.16 % TRYING [1,4,2,2,13,2,1] % 140.97/20.16 % (3393269)Instruction limit reached! % 140.97/20.16 % (3393269)------------------------------ % 140.97/20.16 % (3393269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.37/29.45 % (3393269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.45 % (3393269)CaDiCaL version: 2.1.3 % 206.37/29.45 % (3393269)Termination reason: Instruction limit % 206.37/29.45 % (3393269)Termination phase: Saturation % 206.37/29.45 % (3393269)Time elapsed: 1.235 s % 206.37/29.45 % (3393269)Peak memory usage: 58 MB % 206.37/29.45 % (3393269)Instructions burned: 4591 (million) % 206.37/29.45 % (3393271)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2075023113:i=29340_2946 on theBenchmark for (2946ds/29340Mi) % 206.37/29.45 % TRYING [1,5,5,2,3,3,1] % 206.37/29.45 % (3393241)Instruction limit reached! % 206.37/29.45 % (3393241)------------------------------ % 206.37/29.45 % (3393241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.37/29.45 % (3393241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.45 % (3393241)CaDiCaL version: 2.1.3 % 206.37/29.45 % (3393241)Termination reason: Instruction limit % 206.37/29.45 % (3393241)Termination phase: Finite model building constraint generation % 206.37/29.45 % (3393241)Time elapsed: 5.250 s % 206.37/29.45 % (3393241)Peak memory usage: 102 MB % 206.37/29.45 % (3393241)Instructions burned: 22064 (million) % 206.37/29.45 % (3393273)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=97419708:i=5211_2942 on theBenchmark for (2942ds/5211Mi) % 206.37/29.45 % TRYING [1,4,2,2,13,2,1] % 206.37/29.45 % (3393273)Instruction limit reached! % 206.37/29.45 % (3393273)------------------------------ % 206.37/29.45 % (3393273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.37/29.45 % (3393273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.45 % (3393273)CaDiCaL version: 2.1.3 % 206.37/29.45 % (3393273)Termination reason: Instruction limit % 206.37/29.45 % (3393273)Termination phase: Saturation % 206.37/29.45 % (3393273)Time elapsed: 1.502 s % 206.37/29.45 % (3393273)Peak memory usage: 54 MB % 206.37/29.45 % (3393273)Instructions burned: 5213 (million) % 206.37/29.45 % (3393275)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1418746971:i=5497:nm=2_2927 on theBenchmark for (2927ds/5497Mi) % 206.37/29.45 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 206.37/29.45 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 206.37/29.45 % fmb_start_size (= 17) larger than a detected sort maximum size! % 206.37/29.45 % (3393275)Refutation not found, incomplete strategy % 206.37/29.45 % (3393275)------------------------------ % 206.37/29.45 % (3393275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.37/29.45 % (3393275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.45 % (3393275)CaDiCaL version: 2.1.3 % 206.37/29.45 % (3393275)Termination reason: Refutation not found, incomplete strategy % 206.37/29.45 % (3393275)Time elapsed: 0.211 s % 206.37/29.45 % (3393275)Peak memory usage: 20 MB % 206.37/29.45 % (3393275)Instructions burned: 906 (million) % 206.37/29.45 % (3393275)------------------------------ % 206.37/29.45 % (3393275)------------------------------ % 206.37/29.45 % (3393277)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1868564096:fmbsr=2:i=46332_2924 on theBenchmark for (2924ds/46332Mi) % 206.37/29.45 % TRYING [15] % 206.37/29.45 % (3393271)Instruction limit reached! % 206.37/29.45 % (3393271)------------------------------ % 206.37/29.45 % (3393271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.37/29.45 % (3393271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.45 % (3393271)CaDiCaL version: 2.1.3 % 206.37/29.45 % (3393271)Termination reason: Instruction limit % 206.37/29.45 % (3393271)Termination phase: Saturation % 206.37/29.45 % (3393271)Time elapsed: 7.546 s % 206.37/29.45 % (3393271)Peak memory usage: 266 MB % 206.37/29.45 % (3393271)Instructions burned: 29344 (million) % 206.37/29.45 % (3393279)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1829798362:i=14071_2871 on theBenchmark for (2871ds/14071Mi) % 206.37/29.45 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 206.37/29.45 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 206.37/29.45 % fmb_start_size (= 12) larger than a detected sort maximum size! % 206.37/29.45 % (3393279)Refutation not found, incomplete strategy % 206.37/29.45 % (3393279)------------------------------ % 206.37/29.45 % (3393279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.37/29.45 % (3393279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.37/29.45 % (3393279)CaDiCaL version: 2.1.3 % 206.37/29.45 % (3393279)Termination reason: Refutation not found, incomplete strategy % 206.37/29.45 % (3393279)Time elapsed: 0.236 s % 206.37/29.45 % (3393279)Peak memory usage: 22 MB % 217.79/31.09 % (3393279)Instructions burned: 1005 (million) % 217.79/31.09 % (3393279)------------------------------ % 217.79/31.09 % (3393279)------------------------------ % 217.79/31.09 % (3393281)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1286546232:i=22565:add=on:rawr=on_2868 on theBenchmark for (2868ds/22565Mi) % 217.79/31.09 % (3393259)Instruction limit reached! % 217.79/31.09 % (3393259)------------------------------ % 217.79/31.09 % (3393259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.79/31.09 % (3393259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.79/31.09 % (3393259)CaDiCaL version: 2.1.3 % 217.79/31.09 % (3393259)Termination reason: Instruction limit % 217.79/31.09 % (3393259)Termination phase: Finite model building SAT solving % 217.79/31.09 % (3393259)Time elapsed: 13.327 s % 217.79/31.09 % (3393259)Peak memory usage: 80 MB % 217.79/31.09 % (3393259)Instructions burned: 54284 (million) % 217.79/31.09 % (3393422)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3885725462:i=8173:av=off_2851 on theBenchmark for (2851ds/8173Mi) % 217.79/31.09 % (3393277)Instruction limit reached! % 217.79/31.09 % (3393277)------------------------------ % 217.79/31.09 % (3393277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.79/31.09 % (3393277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.79/31.09 % (3393277)CaDiCaL version: 2.1.3 % 217.79/31.09 % (3393277)Termination reason: Instruction limit % 217.79/31.09 % (3393277)Termination phase: Finite model building constraint generation % 217.79/31.09 % (3393277)Time elapsed: 9.708 s % 217.79/31.09 % (3393277)Peak memory usage: 2853 MB % 217.79/31.09 % (3393277)Instructions burned: 46332 (million) % 217.79/31.09 % (3393593)dis+10_16:1_sil=16000:random_seed=1198891958:i=9155:fsr=off_2823 on theBenchmark for (2823ds/9155Mi) % 217.79/31.09 % (3393422)Instruction limit reached! % 217.79/31.09 % (3393422)------------------------------ % 217.79/31.09 % (3393422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.79/31.09 % (3393422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.79/31.09 % (3393422)CaDiCaL version: 2.1.3 % 217.79/31.09 % (3393422)Termination reason: Instruction limit % 217.79/31.09 % (3393422)Termination phase: Saturation % 217.79/31.09 % (3393422)Time elapsed: 3.658 s % 217.79/31.09 % (3393422)Peak memory usage: 58 MB % 217.79/31.09 % (3393422)Instructions burned: 8173 (million) % 217.79/31.09 % (3393595)ott-3_8_sil=64000:random_seed=2206761554:i=20139:bs=on_2815 on theBenchmark for (2815ds/20139Mi) % 217.79/31.09 % (3393208)Instruction limit reached! % 217.79/31.09 % (3393208)------------------------------ % 217.79/31.09 % (3393208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.79/31.09 % (3393208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.79/31.09 % (3393208)CaDiCaL version: 2.1.3 % 217.79/31.09 % (3393208)Termination reason: Instruction limit % 217.79/31.09 % (3393208)Termination phase: Saturation % 217.79/31.09 % (3393208)Time elapsed: 19.318 s % 217.79/31.09 % (3393208)Peak memory usage: 171 MB % 217.79/31.09 % (3393208)Instructions burned: 88026 (million) % 217.79/31.09 % (3393599)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1779232060:fmbsr=2:i=32576_2806 on theBenchmark for (2806ds/32576Mi) % 217.79/31.09 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 217.79/31.09 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 217.79/31.09 % fmb_start_size (= 9) larger than a detected sort maximum size! % 217.79/31.09 % (3393599)Refutation not found, incomplete strategy % 217.79/31.09 % (3393599)------------------------------ % 217.79/31.09 % (3393599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.79/31.09 % (3393599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.79/31.09 % (3393599)CaDiCaL version: 2.1.3 % 217.79/31.09 % (3393599)Termination reason: Refutation not found, incomplete strategy % 217.79/31.09 % (3393599)Time elapsed: 0.394 s % 217.79/31.09 % (3393599)Peak memory usage: 21 MB % 217.79/31.09 % (3393599)Instructions burned: 1008 (million) % 217.79/31.09 % (3393599)------------------------------ % 217.79/31.09 % (3393599)------------------------------ % 217.79/31.09 % (3393605)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=904631917:i=11404_2802 on theBenchmark for (2802ds/11404Mi) % 217.79/31.09 % (3393281)Instruction limit reached! % 217.79/31.09 % (3393281)------------------------------ % 217.79/31.09 % (3393281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.79/31.09 % (3393281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/39.79 % (3393281)CaDiCaL version: 2.1.3 % 279.02/39.79 % (3393281)Termination reason: Instruction limit % 279.02/39.79 % (3393281)Termination phase: Saturation % 279.02/39.79 % (3393281)Time elapsed: 6.894 s % 279.02/39.79 % (3393281)Peak memory usage: 78 MB % 279.02/39.79 % (3393281)Instructions burned: 22568 (million) % 279.02/39.79 % (3393609)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=55177892:i=14134_2799 on theBenchmark for (2799ds/14134Mi) % 279.02/39.79 % (3393593)Instruction limit reached! % 279.02/39.79 % (3393593)------------------------------ % 279.02/39.79 % (3393593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.02/39.79 % (3393593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/39.79 % (3393593)CaDiCaL version: 2.1.3 % 279.02/39.79 % (3393593)Termination reason: Instruction limit % 279.02/39.79 % (3393593)Termination phase: Saturation % 279.02/39.79 % (3393593)Time elapsed: 4.384 s % 279.02/39.79 % (3393593)Peak memory usage: 59 MB % 279.02/39.79 % (3393593)Instructions burned: 9155 (million) % 279.02/39.79 % (3393613)dis+33_16_sil=32000:sac=on:random_seed=941066132:i=15851:nm=0_2779 on theBenchmark for (2779ds/15851Mi) % 279.02/39.79 % (3393605)Instruction limit reached! % 279.02/39.79 % (3393605)------------------------------ % 279.02/39.79 % (3393605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.02/39.79 % (3393605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/39.79 % (3393605)CaDiCaL version: 2.1.3 % 279.02/39.79 % (3393605)Termination reason: Instruction limit % 279.02/39.79 % (3393605)Termination phase: Saturation % 279.02/39.79 % (3393605)Time elapsed: 6.435 s % 279.02/39.79 % (3393605)Peak memory usage: 95 MB % 279.02/39.79 % (3393605)Instructions burned: 11406 (million) % 279.02/39.79 % (3393627)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=877757649:avsq=on:i=17627:add=on:amm=off_2737 on theBenchmark for (2737ds/17627Mi) % 279.02/39.79 % (3393609)Instruction limit reached! % 279.02/39.79 % (3393609)------------------------------ % 279.02/39.79 % (3393609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.02/39.79 % (3393609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/39.79 % (3393609)CaDiCaL version: 2.1.3 % 279.02/39.79 % (3393609)Termination reason: Instruction limit % 279.02/39.79 % (3393609)Termination phase: Saturation % 279.02/39.79 % (3393609)Time elapsed: 7.142 s % 279.02/39.79 % (3393609)Peak memory usage: 94 MB % 279.02/39.79 % (3393609)Instructions burned: 14135 (million) % 279.02/39.79 % (3393629)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1281248899:s2a=on:i=53295_2727 on theBenchmark for (2727ds/53295Mi) % 279.02/39.79 % (3393613)Instruction limit reached! % 279.02/39.79 % (3393613)------------------------------ % 279.02/39.79 % (3393613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.02/39.79 % (3393613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/39.79 % (3393613)CaDiCaL version: 2.1.3 % 279.02/39.79 % (3393613)Termination reason: Instruction limit % 279.02/39.79 % (3393613)Termination phase: Saturation % 279.02/39.79 % (3393613)Time elapsed: 6.671 s % 279.02/39.79 % (3393613)Peak memory usage: 100 MB % 279.02/39.79 % (3393613)Instructions burned: 15851 (million) % 279.02/39.79 % (3393633)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2052583510:i=26857:ins=20_2712 on theBenchmark for (2712ds/26857Mi) % 279.02/39.79 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 279.02/39.79 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 279.02/39.79 % fmb_start_size (= 16) larger than a detected sort maximum size! % 279.02/39.79 % (3393633)Refutation not found, incomplete strategy % 279.02/39.79 % (3393633)------------------------------ % 279.02/39.79 % (3393633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.02/39.79 % (3393633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.02/39.79 % (3393633)CaDiCaL version: 2.1.3 % 279.02/39.79 % (3393633)Termination reason: Refutation not found, incomplete strategy % 279.02/39.79 % (3393633)Time elapsed: 0.455 s % 279.02/39.79 % (3393633)Peak memory usage: 21 MB % 279.02/39.79 % (3393633)Instructions burned: 1005 (million) % 279.02/39.79 % (3393633)------------------------------ % 279.02/39.79 % (3393633)------------------------------ % 279.02/39.79 % (3393635)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3159650837:i=28120:bs=on:fsr=off_2707 on theBenchmark for (2707ds/28120Mi) % 279.02/39.79 % (3393595)Instruction limit reached! % 279.02/39.79 % (3393595)------------------------------ % 279.02/39.79 % (3393595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.70/41.56 % (3393595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.70/41.56 % (3393595)CaDiCaL version: 2.1.3 % 291.70/41.56 % (3393595)Termination reason: Instruction limit % 291.70/41.56 % (3393595)Termination phase: Saturation % 291.70/41.56 % (3393595)Time elapsed: 10.820 s % 291.70/41.56 % (3393595)Peak memory usage: 73 MB % 291.70/41.56 % (3393595)Instructions burned: 20140 (million) % 291.70/41.56 % (3393637)fmb+10_1_sil=256000:fmbss=7:random_seed=3607464211:fmbsr=1.6:i=182295_2706 on theBenchmark for (2706ds/182295Mi) % 291.70/41.56 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 291.70/41.56 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 291.70/41.56 % fmb_start_size (= 7) larger than a detected sort maximum size! % 291.70/41.56 % (3393637)Refutation not found, incomplete strategy % 291.70/41.56 % (3393637)------------------------------ % 291.70/41.56 % (3393637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.70/41.56 % (3393637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.70/41.56 % (3393637)CaDiCaL version: 2.1.3 % 291.70/41.56 % (3393637)Termination reason: Refutation not found, incomplete strategy % 291.70/41.56 % (3393637)Time elapsed: 0.452 s % 291.70/41.56 % (3393637)Peak memory usage: 21 MB % 291.70/41.56 % (3393637)Instructions burned: 1005 (million) % 291.70/41.56 % (3393637)------------------------------ % 291.70/41.56 % (3393637)------------------------------ % 291.70/41.56 % (3393639)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3363826589:i=44625:gsp=on_2701 on theBenchmark for (2701ds/44625Mi) % 291.70/41.56 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 291.70/41.56 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 291.70/41.56 % fmb_start_size (= 21) larger than a detected sort maximum size! % 291.70/41.56 % (3393639)Refutation not found, incomplete strategy % 291.70/41.56 % (3393639)------------------------------ % 291.70/41.56 % (3393639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.70/41.56 % (3393639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.70/41.56 % (3393639)CaDiCaL version: 2.1.3 % 291.70/41.56 % (3393639)Termination reason: Refutation not found, incomplete strategy % 291.70/41.56 % (3393639)Time elapsed: 0.433 s % 291.70/41.56 % (3393639)Peak memory usage: 21 MB % 291.70/41.56 % (3393639)Instructions burned: 1020 (million) % 291.70/41.56 % (3393639)------------------------------ % 291.70/41.56 % (3393639)------------------------------ % 291.70/41.56 % (3393641)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2380035570:i=160505_2697 on theBenchmark for (2697ds/160505Mi) % 291.70/41.56 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 291.70/41.56 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 291.70/41.56 % fmb_start_size (= 15) larger than a detected sort maximum size! % 291.70/41.56 % (3393641)Refutation not found, incomplete strategy % 291.70/41.56 % (3393641)------------------------------ % 291.70/41.56 % (3393641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.70/41.56 % (3393641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.70/41.56 % (3393641)CaDiCaL version: 2.1.3 % 291.70/41.56 % (3393641)Termination reason: Refutation not found, incomplete strategy % 291.70/41.56 % (3393641)Time elapsed: 0.303 s % 291.70/41.56 % (3393641)Peak memory usage: 21 MB % 291.70/41.56 % (3393641)Instructions burned: 1005 (million) % 291.70/41.56 % (3393641)------------------------------ % 291.70/41.56 % (3393641)------------------------------ % 291.70/41.56 % (3393643)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3882219571:fmbsr=1.3:i=225729_2694 on theBenchmark for (2694ds/225729Mi) % 291.70/41.56 % Detected minimum model sizes of [1,1,1,1,1,1,1] % 291.70/41.56 % Detected maximum model sizes of [max,max,max,2,max,max,max] % 291.70/41.56 % fmb_start_size (= 10) larger than a detected sort maximum size! % 291.70/41.56 % (3393643)Refutation not found, incomplete strategy % 291.70/41.56 % (3393643)------------------------------ % 291.70/41.56 % (3393643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 291.70/41.56 % (3393643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.70/41.56 % (3393643)CaDiCaL version: 2.1.3 % 291.70/41.56 % (3393643)Termination reason: Refutation not found, incomplete strategy % 291.70/41.56 % (3393643)Time elapsed: 0.342 s % 291.70/41.56 % (3393643)Peak memory usage: 21 MB % 291.70/41.56 % (3393643)Instructions burned: 1005 (million) % 291.70/41.56 % (3393643)------------------------------ % 291.70/41.56 % (3393643)------------------------------ % 291.70/41.56 % (3393645)fmb+10_1_sil=256000:tgt=full:sTerminated % 300.24/42.83 % Vampire exiting %------------------------------------------------------------------------------