%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW475+3 : TPTP v9.3.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:13 PM UTC 2026 % Result : Timeout 300.34s 42.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW475+3 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.25 % Computer : n007.cluster.edu % 0.11/0.25 % Model : x86_64 x86_64 % 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.25 % Memory : 8046.5625MB % 0.11/0.25 % OS : Linux 6.8.0-71-generic % 0.11/0.25 % CPULimit : 300 % 0.11/0.25 % WCLimit : 300 % 0.11/0.25 % DateTime : Mon Sep 28 14:07:40 UTC 2026 % 0.11/0.26 % CPUTime : % 0.11/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.31 Running first-order model finding % 0.24/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.45/3.19 % (2403157)Will run a generic schedule for satisfiability detection. % 19.45/3.19 % (2403167)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3824329107:i=131_2998 on theBenchmark for (2998ds/131Mi) % 19.45/3.19 % (2403163)% WARNING: option uhcvi not known. % 19.45/3.19 % (2403162)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=647390223_2998 on theBenchmark for (2998ds/0Mi) % 19.45/3.19 % (2403163)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=996272239:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi) % 19.45/3.19 % (2403165)dis+10_1_sil=32000:sp=arity:random_seed=726252465:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi) % 19.45/3.19 % (2403168)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1829793056:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi) % 19.45/3.19 % (2403164)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1918161093:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi) % 19.45/3.19 % (2403166)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=643434154:i=116_2998 on theBenchmark for (2998ds/116Mi) % 19.45/3.19 % (2403167)Instruction limit reached! % 19.45/3.19 % (2403167)------------------------------ % 19.45/3.19 % (2403167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.45/3.19 % (2403167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.45/3.19 % (2403167)CaDiCaL version: 2.1.3 % 19.45/3.19 % (2403167)Termination reason: Instruction limit % 19.45/3.19 % (2403167)Termination phase: Saturation % 19.45/3.19 % (2403167)Time elapsed: 0.057 s % 19.45/3.19 % (2403167)Peak memory usage: 15 MB % 19.45/3.19 % (2403167)Instructions burned: 134 (million) % 19.45/3.19 % (2403176)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2993499248:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 19.45/3.19 % (2403165)Instruction limit reached! % 19.45/3.19 % (2403165)------------------------------ % 19.45/3.19 % (2403165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.45/3.19 % (2403165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.45/3.19 % (2403165)CaDiCaL version: 2.1.3 % 19.45/3.19 % (2403165)Termination reason: Instruction limit % 19.45/3.19 % (2403165)Termination phase: Property scanning % 19.45/3.19 % (2403165)Time elapsed: 0.092 s % 19.45/3.19 % (2403165)Peak memory usage: 14 MB % 19.45/3.19 % (2403165)Instructions burned: 104 (million) % 19.45/3.19 % (2403166)Instruction limit reached! % 19.45/3.19 % (2403166)------------------------------ % 19.45/3.19 % (2403166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.45/3.19 % (2403166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.45/3.19 % (2403166)CaDiCaL version: 2.1.3 % 19.45/3.19 % (2403166)Termination reason: Instruction limit % 19.45/3.19 % (2403166)Termination phase: Blocked clause elimination % 19.45/3.19 % (2403166)Time elapsed: 0.102 s % 19.45/3.19 % (2403166)Peak memory usage: 14 MB % 19.45/3.19 % (2403166)Instructions burned: 116 (million) % 19.45/3.19 % (2403178)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=136905704:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 19.45/3.19 % (2403179)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=911896935:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 19.45/3.19 % (2403168)Instruction limit reached! % 19.45/3.19 % (2403168)------------------------------ % 19.45/3.19 % (2403168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.45/3.19 % (2403168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.45/3.19 % (2403168)CaDiCaL version: 2.1.3 % 19.45/3.19 % (2403168)Termination reason: Instruction limit % 19.45/3.19 % (2403168)Termination phase: Saturation % 19.45/3.19 % (2403168)Time elapsed: 0.141 s % 19.45/3.19 % (2403168)Peak memory usage: 16 MB % 19.45/3.19 % (2403168)Instructions burned: 159 (million) % 19.45/3.19 % (2403182)ott-21_1_sil=16000:fs=off:random_seed=1610975316:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 19.45/3.19 % (2403178)Instruction limit reached! % 19.45/3.19 % (2403178)------------------------------ % 19.45/3.19 % (2403178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.45/3.19 % (2403178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.96/6.62 % (2403178)CaDiCaL version: 2.1.3 % 43.96/6.62 % (2403178)Termination reason: Instruction limit % 43.96/6.62 % (2403178)Termination phase: Blocked clause elimination % 43.96/6.62 % (2403178)Time elapsed: 0.116 s % 43.96/6.62 % (2403178)Peak memory usage: 15 MB % 43.96/6.62 % (2403178)Instructions burned: 132 (million) % 43.96/6.62 % (2403186)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3141936881:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 43.96/6.62 % (2403182)Instruction limit reached! % 43.96/6.62 % (2403182)------------------------------ % 43.96/6.62 % (2403182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.96/6.62 % (2403182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.96/6.62 % (2403182)CaDiCaL version: 2.1.3 % 43.96/6.62 % (2403182)Termination reason: Instruction limit % 43.96/6.62 % (2403182)Termination phase: Saturation % 43.96/6.62 % (2403182)Time elapsed: 0.151 s % 43.96/6.62 % (2403182)Peak memory usage: 15 MB % 43.96/6.62 % (2403182)Instructions burned: 180 (million) % 43.96/6.62 % (2403188)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1518851278:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi) % 43.96/6.62 % (2403176)Instruction limit reached! % 43.96/6.62 % (2403176)------------------------------ % 43.96/6.62 % (2403176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.96/6.62 % (2403176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.96/6.62 % (2403176)CaDiCaL version: 2.1.3 % 43.96/6.62 % (2403176)Termination reason: Instruction limit % 43.96/6.62 % (2403176)Termination phase: Finite model building preprocessing % 43.96/6.62 % (2403176)Time elapsed: 0.290 s % 43.96/6.62 % (2403176)Peak memory usage: 23 MB % 43.96/6.62 % (2403176)Instructions burned: 715 (million) % 43.96/6.62 % (2403190)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3952701701:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 43.96/6.62 % (2403186)Instruction limit reached! % 43.96/6.62 % (2403186)------------------------------ % 43.96/6.62 % (2403186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.96/6.62 % (2403186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.96/6.62 % (2403186)CaDiCaL version: 2.1.3 % 43.96/6.62 % (2403186)Termination reason: Instruction limit % 43.96/6.62 % (2403186)Termination phase: Saturation % 43.96/6.62 % (2403186)Time elapsed: 0.432 s % 43.96/6.62 % (2403186)Peak memory usage: 18 MB % 43.96/6.62 % (2403186)Instructions burned: 477 (million) % 43.96/6.62 % (2403192)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4041565616:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 43.96/6.62 % (2403179)Instruction limit reached! % 43.96/6.62 % (2403179)------------------------------ % 43.96/6.62 % (2403179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.96/6.62 % (2403179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.96/6.62 % (2403179)CaDiCaL version: 2.1.3 % 43.96/6.62 % (2403179)Termination reason: Instruction limit % 43.96/6.62 % (2403179)Termination phase: Saturation % 43.96/6.62 % (2403179)Time elapsed: 0.614 s % 43.96/6.62 % (2403179)Peak memory usage: 22 MB % 43.96/6.62 % (2403179)Instructions burned: 684 (million) % 43.96/6.62 % (2403194)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=1491625853:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 43.96/6.62 % (2403190)Instruction limit reached! % 43.96/6.62 % (2403190)------------------------------ % 43.96/6.62 % (2403190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.96/6.62 % (2403190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.96/6.62 % (2403190)CaDiCaL version: 2.1.3 % 43.96/6.62 % (2403190)Termination reason: Instruction limit % 43.96/6.62 % (2403190)Termination phase: Saturation % 43.96/6.62 % (2403190)Time elapsed: 0.664 s % 43.96/6.62 % (2403190)Peak memory usage: 25 MB % 43.96/6.62 % (2403190)Instructions burned: 1179 (million) % 43.96/6.62 % (2403196)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=800795984:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi) % 43.96/6.62 % (2403188)Instruction limit reached! % 43.96/6.62 % (2403188)------------------------------ % 43.96/6.62 % (2403188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 43.96/6.62 % (2403188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/18.01 % (2403188)CaDiCaL version: 2.1.3 % 124.30/18.01 % (2403188)Termination reason: Instruction limit % 124.30/18.01 % (2403188)Termination phase: Finite model building preprocessing % 124.30/18.01 % (2403188)Time elapsed: 0.753 s % 124.30/18.01 % (2403188)Peak memory usage: 24 MB % 124.30/18.01 % (2403188)Instructions burned: 865 (million) % 124.30/18.01 % (2403198)fmb+10_1_sil=64000:random_seed=3477646794:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi) % 124.30/18.01 % Detected minimum model sizes of [4] % 124.30/18.01 % Detected maximum model sizes of [max] % 124.30/18.01 % TRYING [4] % 124.30/18.01 % (2403194)Instruction limit reached! % 124.30/18.01 % (2403194)------------------------------ % 124.30/18.01 % (2403194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/18.01 % (2403194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/18.01 % (2403194)CaDiCaL version: 2.1.3 % 124.30/18.01 % (2403194)Termination reason: Instruction limit % 124.30/18.01 % (2403194)Termination phase: Saturation % 124.30/18.01 % (2403194)Time elapsed: 0.674 s % 124.30/18.01 % (2403194)Peak memory usage: 21 MB % 124.30/18.01 % (2403194)Instructions burned: 692 (million) % 124.30/18.01 % (2403196)Instruction limit reached! % 124.30/18.01 % (2403196)------------------------------ % 124.30/18.01 % (2403196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/18.01 % (2403196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/18.01 % (2403196)CaDiCaL version: 2.1.3 % 124.30/18.01 % (2403196)Termination reason: Instruction limit % 124.30/18.01 % (2403196)Termination phase: Saturation % 124.30/18.01 % (2403196)Time elapsed: 0.403 s % 124.30/18.01 % (2403196)Peak memory usage: 22 MB % 124.30/18.01 % (2403196)Instructions burned: 879 (million) % 124.30/18.01 % (2403200)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4038053449:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi) % 124.30/18.01 % (2403201)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2077504555:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi) % 124.30/18.01 % (2403192)Instruction limit reached! % 124.30/18.01 % (2403192)------------------------------ % 124.30/18.01 % (2403192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/18.01 % (2403192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/18.01 % (2403192)CaDiCaL version: 2.1.3 % 124.30/18.01 % (2403192)Termination reason: Instruction limit % 124.30/18.01 % (2403192)Termination phase: Finite model building preprocessing % 124.30/18.01 % (2403192)Time elapsed: 0.804 s % 124.30/18.01 % (2403192)Peak memory usage: 24 MB % 124.30/18.01 % (2403192)Instructions burned: 889 (million) % 124.30/18.01 % (2403204)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=204137875:i=5131_2983 on theBenchmark for (2983ds/5131Mi) % 124.30/18.01 % (2403201)Instruction limit reached! % 124.30/18.01 % (2403201)------------------------------ % 124.30/18.01 % (2403201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/18.01 % (2403201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/18.01 % (2403201)CaDiCaL version: 2.1.3 % 124.30/18.01 % (2403201)Termination reason: Instruction limit % 124.30/18.01 % (2403201)Termination phase: Finite model building preprocessing % 124.30/18.01 % (2403201)Time elapsed: 0.438 s % 124.30/18.01 % (2403201)Peak memory usage: 25 MB % 124.30/18.01 % (2403201)Instructions burned: 921 (million) % 124.30/18.01 % (2403206)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2927183149:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi) % 124.30/18.01 % Detected minimum model sizes of [4] % 124.30/18.01 % Detected maximum model sizes of [max] % 124.30/18.01 % (2403206)Instruction limit reached! % 124.30/18.01 % (2403206)------------------------------ % 124.30/18.01 % (2403206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.30/18.01 % (2403206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.30/18.01 % (2403206)CaDiCaL version: 2.1.3 % 124.30/18.01 % (2403206)Termination reason: Instruction limit % 124.30/18.01 % (2403206)Termination phase: Saturation % 124.30/18.01 % (2403206)Time elapsed: 0.668 s % 124.30/18.01 % (2403206)Peak memory usage: 24 MB % 124.30/18.01 % (2403206)Instructions burned: 1472 (million) % 124.30/18.01 % (2403208)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1827759030:i=6324_2972 on theBenchmark for (2972ds/6324Mi) % 124.30/18.01 % Detected minimum model sizes of [4] % 124.30/18.01 % Detected maximum model sizes of [max] % 124.30/18.01 % (2403200)Cannot represent all propositional literals internally % 124.30/18.01 % (2403200)Refutation not found, incomplete strategy % 192.38/27.54 % (2403200)------------------------------ % 192.38/27.54 % (2403200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.38/27.54 % (2403200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.38/27.54 % (2403200)CaDiCaL version: 2.1.3 % 192.38/27.54 % (2403200)Termination reason: Refutation not found, incomplete strategy % 192.38/27.54 % (2403200)Time elapsed: 1.241 s % 192.38/27.54 % (2403200)Peak memory usage: 34 MB % 192.38/27.54 % (2403200)Instructions burned: 1375 (million) % 192.38/27.54 % (2403200)------------------------------ % 192.38/27.54 % (2403200)------------------------------ % 192.38/27.54 % (2403210)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2669333965:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi) % 192.38/27.54 % Detected minimum model sizes of [4] % 192.38/27.54 % Detected maximum model sizes of [max] % 192.38/27.54 % (2403208)Cannot represent all propositional literals internally % 192.38/27.54 % (2403208)Refutation not found, incomplete strategy % 192.38/27.54 % (2403208)------------------------------ % 192.38/27.54 % (2403208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.38/27.54 % (2403208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.38/27.54 % (2403208)CaDiCaL version: 2.1.3 % 192.38/27.54 % (2403208)Termination reason: Refutation not found, incomplete strategy % 192.38/27.54 % (2403208)Time elapsed: 0.709 s % 192.38/27.54 % (2403208)Peak memory usage: 37 MB % 192.38/27.54 % (2403208)Instructions burned: 1481 (million) % 192.38/27.54 % (2403208)------------------------------ % 192.38/27.54 % (2403208)------------------------------ % 192.38/27.54 % (2403214)ott-2_1_sil=16000:newcnf=on:random_seed=2947430518:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi) % 192.38/27.54 % (2403214)Instruction limit reached! % 192.38/27.54 % (2403214)------------------------------ % 192.38/27.54 % (2403214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.38/27.54 % (2403214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.38/27.54 % (2403214)CaDiCaL version: 2.1.3 % 192.38/27.54 % (2403214)Termination reason: Instruction limit % 192.38/27.54 % (2403214)Termination phase: Saturation % 192.38/27.54 % (2403214)Time elapsed: 0.434 s % 192.38/27.54 % (2403214)Peak memory usage: 20 MB % 192.38/27.54 % (2403214)Instructions burned: 872 (million) % 192.38/27.54 % (2403216)ott+10_1_sil=32000:tgt=ground:random_seed=2505990895:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi) % 192.38/27.54 % (2403210)Instruction limit reached! % 192.38/27.54 % (2403210)------------------------------ % 192.38/27.54 % (2403210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.38/27.54 % (2403210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.38/27.54 % (2403210)CaDiCaL version: 2.1.3 % 192.38/27.54 % (2403210)Termination reason: Instruction limit % 192.38/27.54 % (2403210)Termination phase: Finite model building preprocessing % 192.38/27.54 % (2403210)Time elapsed: 1.961 s % 192.38/27.54 % (2403210)Peak memory usage: 31 MB % 192.38/27.54 % (2403210)Instructions burned: 2174 (million) % 192.38/27.54 % (2403220)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3070211155:i=54282_2951 on theBenchmark for (2951ds/54282Mi) % 192.38/27.54 % (2403204)Instruction limit reached! % 192.38/27.54 % (2403204)------------------------------ % 192.38/27.54 % (2403204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.38/27.54 % (2403204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.38/27.54 % (2403204)CaDiCaL version: 2.1.3 % 192.38/27.54 % (2403204)Termination reason: Instruction limit % 192.38/27.54 % (2403204)Termination phase: Saturation % 192.38/27.54 % (2403204)Time elapsed: 4.486 s % 192.38/27.54 % (2403204)Peak memory usage: 32 MB % 192.38/27.54 % (2403204)Instructions burned: 5131 (million) % 192.38/27.54 % (2403222)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2848105504:i=3512:aac=none_2937 on theBenchmark for (2937ds/3512Mi) % 192.38/27.54 % Detected minimum model sizes of [4] % 192.38/27.54 % Detected maximum model sizes of [max] % 192.38/27.54 % TRYING [4] % 192.38/27.54 % (2403216)Instruction limit reached! % 192.38/27.54 % (2403216)------------------------------ % 192.38/27.54 % (2403216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.38/27.54 % (2403216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.38/27.54 % (2403216)CaDiCaL version: 2.1.3 % 192.38/27.54 % (2403216)Termination reason: Instruction limit % 192.38/27.54 % (2403216)Termination phase: Saturation % 273.14/38.94 % (2403216)Time elapsed: 2.304 s % 273.14/38.94 % (2403216)Peak memory usage: 31 MB % 273.14/38.94 % (2403216)Instructions burned: 5115 (million) % 273.14/38.94 % (2403224)dis+21_1_sil=32000:sas=cadical:random_seed=632591885:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi) % 273.14/38.94 % TRYING [4] % 273.14/38.94 % (2403224)Instruction limit reached! % 273.14/38.94 % (2403224)------------------------------ % 273.14/38.94 % (2403224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.14/38.94 % (2403224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.14/38.94 % (2403224)CaDiCaL version: 2.1.3 % 273.14/38.94 % (2403224)Termination reason: Instruction limit % 273.14/38.94 % (2403224)Termination phase: Saturation % 273.14/38.94 % (2403224)Time elapsed: 1.874 s % 273.14/38.94 % (2403224)Peak memory usage: 37 MB % 273.14/38.94 % (2403224)Instructions burned: 3774 (million) % 273.14/38.94 % (2403228)ott+11_1_sil=16000:gs=on:random_seed=1196254042:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2917 on theBenchmark for (2917ds/2251Mi) % 273.14/38.94 % (2403228)Instruction limit reached! % 273.14/38.94 % (2403228)------------------------------ % 273.14/38.94 % (2403228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.14/38.94 % (2403228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.14/38.94 % (2403228)CaDiCaL version: 2.1.3 % 273.14/38.94 % (2403228)Termination reason: Instruction limit % 273.14/38.94 % (2403228)Termination phase: Saturation % 273.14/38.94 % (2403228)Time elapsed: 1.081 s % 273.14/38.94 % (2403228)Peak memory usage: 28 MB % 273.14/38.94 % (2403228)Instructions burned: 2252 (million) % 273.14/38.94 % (2403230)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2546290530:fmbsr=1.6:i=67534_2906 on theBenchmark for (2906ds/67534Mi) % 273.14/38.94 % (2403222)Instruction limit reached! % 273.14/38.94 % (2403222)------------------------------ % 273.14/38.94 % (2403222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.14/38.94 % (2403222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.14/38.94 % (2403222)CaDiCaL version: 2.1.3 % 273.14/38.94 % (2403222)Termination reason: Instruction limit % 273.14/38.94 % (2403222)Termination phase: Saturation % 273.14/38.94 % (2403222)Time elapsed: 3.317 s % 273.14/38.94 % (2403222)Peak memory usage: 35 MB % 273.14/38.94 % (2403222)Instructions burned: 3512 (million) % 273.14/38.94 % (2403232)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2449663814:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2904 on theBenchmark for (2904ds/4591Mi) % 273.14/38.94 % Detected minimum model sizes of [4] % 273.14/38.94 % Detected maximum model sizes of [max] % 273.14/38.94 % (2403232)Instruction limit reached! % 273.14/38.94 % (2403232)------------------------------ % 273.14/38.94 % (2403232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.14/38.94 % (2403232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.14/38.94 % (2403232)CaDiCaL version: 2.1.3 % 273.14/38.94 % (2403232)Termination reason: Instruction limit % 273.14/38.94 % (2403232)Termination phase: Saturation % 273.14/38.94 % (2403232)Time elapsed: 3.517 s % 273.14/38.94 % (2403232)Peak memory usage: 46 MB % 273.14/38.94 % (2403232)Instructions burned: 4591 (million) % 273.14/38.94 % (2403340)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3069389665:i=29340_2868 on theBenchmark for (2868ds/29340Mi) % 273.14/38.94 % (2403198)Instruction limit reached! % 273.14/38.94 % (2403198)------------------------------ % 273.14/38.94 % (2403198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.14/38.94 % (2403198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.14/38.94 % (2403198)CaDiCaL version: 2.1.3 % 273.14/38.94 % (2403198)Termination reason: Instruction limit % 273.14/38.94 % (2403198)Termination phase: Finite model building constraint generation % 273.14/38.94 % (2403198)Time elapsed: 13.791 s % 273.14/38.94 % (2403198)Peak memory usage: 1338 MB % 273.14/38.94 % (2403198)Instructions burned: 22062 (million) % 273.14/38.94 % (2403392)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=891451174:i=5211_2847 on theBenchmark for (2847ds/5211Mi) % 273.14/38.94 % (2403392)Instruction limit reached! % 273.14/38.94 % (2403392)------------------------------ % 273.14/38.94 % (2403392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.14/38.94 % (2403392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.14/38.94 % (2403392)CaDiCaL version: 2.1.3 % 273.14/38.94 % (2403392)Termination reason: InstrucTerminated % 300.34/42.84 % Vampire exiting % 300.34/42.84 Terminated %------------------------------------------------------------------------------