%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV830-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.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:26:30 PM UTC 2026 % Result : Timeout 300.29s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV830-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n004.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 12:39:37 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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 % 12.57/2.05 % (326275)Will run a generic schedule for satisfiability detection. % 12.57/2.05 % (326286)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3616571379:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 12.57/2.05 % (326281)% WARNING: option uhcvi not known. % 12.57/2.05 % (326282)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2192421275:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 12.57/2.05 % (326280)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1574391947_2999 on theBenchmark for (2999ds/0Mi) % 12.57/2.05 % (326281)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3645741917:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 12.57/2.05 % (326283)dis+10_1_sil=32000:sp=arity:random_seed=2761857460:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 12.57/2.05 % (326284)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3944334680:i=116_2999 on theBenchmark for (2999ds/116Mi) % 12.57/2.05 % (326285)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2784724294:i=131_2999 on theBenchmark for (2999ds/131Mi) % 12.57/2.05 % (326286)Instruction limit reached! % 12.57/2.05 % (326286)------------------------------ % 12.57/2.05 % (326286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.57/2.05 % (326286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.57/2.05 % (326286)CaDiCaL version: 2.1.3 % 12.57/2.05 % (326286)Termination reason: Instruction limit % 12.57/2.05 % (326286)Termination phase: Saturation % 12.57/2.05 % (326286)Time elapsed: 0.060 s % 12.57/2.05 % (326286)Peak memory usage: 15 MB % 12.57/2.05 % (326286)Instructions burned: 160 (million) % 12.57/2.05 % (326294)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2182993311:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 12.57/2.05 % (326283)Instruction limit reached! % 12.57/2.05 % (326283)------------------------------ % 12.57/2.05 % (326283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.57/2.05 % (326283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.57/2.05 % (326283)CaDiCaL version: 2.1.3 % 12.57/2.05 % (326283)Termination reason: Instruction limit % 12.57/2.05 % (326283)Termination phase: Saturation % 12.57/2.05 % (326283)Time elapsed: 0.065 s % 12.57/2.05 % (326283)Peak memory usage: 13 MB % 12.57/2.05 % (326283)Instructions burned: 103 (million) % 12.57/2.05 % (326284)Instruction limit reached! % 12.57/2.05 % (326284)------------------------------ % 12.57/2.05 % (326284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.57/2.05 % (326284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.57/2.05 % (326284)CaDiCaL version: 2.1.3 % 12.57/2.05 % (326284)Termination reason: Instruction limit % 12.57/2.05 % (326284)Termination phase: Saturation % 12.57/2.05 % (326284)Time elapsed: 0.064 s % 12.57/2.05 % (326284)Peak memory usage: 13 MB % 12.57/2.05 % (326284)Instructions burned: 117 (million) % 12.57/2.05 % (326296)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1990847032:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 12.57/2.05 % (326297)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=2269319214:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 12.57/2.05 % (326285)Instruction limit reached! % 12.57/2.05 % (326285)------------------------------ % 12.57/2.05 % (326285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.57/2.05 % (326285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.57/2.05 % (326285)CaDiCaL version: 2.1.3 % 12.57/2.05 % (326285)Termination reason: Instruction limit % 12.57/2.05 % (326285)Termination phase: Saturation % 12.57/2.05 % (326285)Time elapsed: 0.088 s % 12.57/2.05 % (326285)Peak memory usage: 13 MB % 12.57/2.05 % (326285)Instructions burned: 132 (million) % 12.57/2.05 % (326300)ott-21_1_sil=16000:fs=off:random_seed=1666903913:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 12.57/2.05 % (326296)Instruction limit reached! % 12.57/2.05 % (326296)------------------------------ % 12.57/2.05 % (326296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.57/2.05 % (326296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.57/2.05 % (326296)CaDiCaL version: 2.1.3 % 12.57/2.05 % (326296)Termination reason: Instruction limit % 39.08/5.83 % (326296)Termination phase: Saturation % 39.08/5.83 % (326296)Time elapsed: 0.075 s % 39.08/5.83 % (326296)Peak memory usage: 13 MB % 39.08/5.83 % (326296)Instructions burned: 131 (million) % 39.08/5.83 % (326302)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3997269731:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.08/5.83 % (326300)Instruction limit reached! % 39.08/5.83 % (326300)------------------------------ % 39.08/5.83 % (326300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.08/5.83 % (326300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.08/5.83 % (326300)CaDiCaL version: 2.1.3 % 39.08/5.83 % (326300)Termination reason: Instruction limit % 39.08/5.83 % (326300)Termination phase: Saturation % 39.08/5.83 % (326300)Time elapsed: 0.100 s % 39.08/5.83 % (326300)Peak memory usage: 13 MB % 39.08/5.83 % (326300)Instructions burned: 181 (million) % 39.08/5.83 % (326304)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2953772243:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.08/5.83 % TRYING [1] % 39.08/5.83 % (326294)Instruction limit reached! % 39.08/5.83 % (326294)------------------------------ % 39.08/5.83 % (326294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.08/5.83 % (326294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.08/5.83 % (326294)CaDiCaL version: 2.1.3 % 39.08/5.83 % (326294)Termination reason: Instruction limit % 39.08/5.83 % (326294)Termination phase: Finite model building constraint generation % 39.08/5.83 % (326294)Time elapsed: 0.185 s % 39.08/5.83 % (326294)Peak memory usage: 21 MB % 39.08/5.83 % (326294)Instructions burned: 714 (million) % 39.08/5.83 % (326306)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1952517052:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 39.08/5.83 % TRYING [1] % 39.08/5.83 % TRYING [2] % 39.08/5.83 % (326297)Instruction limit reached! % 39.08/5.83 % (326297)------------------------------ % 39.08/5.83 % (326297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.08/5.83 % (326297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.08/5.83 % (326297)CaDiCaL version: 2.1.3 % 39.08/5.83 % (326297)Termination reason: Instruction limit % 39.08/5.83 % (326297)Termination phase: Saturation % 39.08/5.83 % (326297)Time elapsed: 0.387 s % 39.08/5.83 % (326297)Peak memory usage: 18 MB % 39.08/5.83 % (326297)Instructions burned: 684 (million) % 39.08/5.83 % (326302)Instruction limit reached! % 39.08/5.83 % (326302)------------------------------ % 39.08/5.83 % (326302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.08/5.83 % (326302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.08/5.83 % (326302)CaDiCaL version: 2.1.3 % 39.08/5.83 % (326302)Termination reason: Instruction limit % 39.08/5.83 % (326302)Termination phase: Saturation % 39.08/5.83 % (326302)Time elapsed: 0.303 s % 39.08/5.83 % (326302)Peak memory usage: 15 MB % 39.08/5.83 % (326302)Instructions burned: 477 (million) % 39.08/5.83 % (326308)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2653905134:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 39.08/5.83 % (326309)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=87739933:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 39.08/5.83 % TRYING [3] % 39.08/5.83 % TRYING [1] % 39.08/5.83 % TRYING [2] % 39.08/5.83 % (326304)Instruction limit reached! % 39.08/5.83 % (326304)------------------------------ % 39.08/5.83 % (326304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.08/5.83 % (326304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.08/5.83 % (326304)CaDiCaL version: 2.1.3 % 39.08/5.83 % (326304)Termination reason: Instruction limit % 39.08/5.83 % (326304)Termination phase: Finite model building constraint generation % 39.08/5.83 % (326304)Time elapsed: 0.420 s % 39.08/5.83 % (326304)Peak memory usage: 30 MB % 39.08/5.83 % (326304)Instructions burned: 867 (million) % 39.08/5.83 % (326306)Instruction limit reached! % 39.08/5.83 % (326306)------------------------------ % 39.08/5.83 % (326306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.08/5.83 % (326306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.08/5.83 % (326306)CaDiCaL version: 2.1.3 % 39.08/5.83 % (326306)Termination reason: Instruction limit % 39.08/5.83 % (326306)Termination phase: Saturation % 39.08/5.83 % (326306)Time elapsed: 0.395 s % 39.08/5.83 % (326306)Peak memory usage: 23 MB % 85.73/12.40 % (326306)Instructions burned: 1181 (million) % 85.73/12.40 % (326313)fmb+10_1_sil=64000:random_seed=2266862298:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 85.73/12.40 % (326312)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2700628816:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 85.73/12.40 % (326308)Cannot represent all propositional literals internally % 85.73/12.40 % (326308)Refutation not found, incomplete strategy % 85.73/12.40 % (326308)------------------------------ % 85.73/12.40 % (326308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.73/12.40 % (326308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.73/12.40 % (326308)CaDiCaL version: 2.1.3 % 85.73/12.40 % (326308)Termination reason: Refutation not found, incomplete strategy % 85.73/12.40 % (326308)Time elapsed: 0.345 s % 85.73/12.40 % (326308)Peak memory usage: 21 MB % 85.73/12.40 % (326308)Instructions burned: 700 (million) % 85.73/12.40 % (326308)------------------------------ % 85.73/12.40 % (326308)------------------------------ % 85.73/12.40 % TRYING [1] % 85.73/12.40 % (326316)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=634981932:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 85.73/12.40 % TRYING [2] % 85.73/12.40 % (326309)Instruction limit reached! % 85.73/12.40 % (326309)------------------------------ % 85.73/12.40 % (326309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.73/12.40 % (326309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.73/12.40 % (326309)CaDiCaL version: 2.1.3 % 85.73/12.40 % (326309)Termination reason: Instruction limit % 85.73/12.40 % (326309)Termination phase: Saturation % 85.73/12.40 % (326309)Time elapsed: 0.427 s % 85.73/12.40 % (326309)Peak memory usage: 21 MB % 85.73/12.40 % (326309)Instructions burned: 693 (million) % 85.73/12.40 % (326318)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=257036787:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi) % 85.73/12.40 % (326312)Instruction limit reached! % 85.73/12.40 % (326312)------------------------------ % 85.73/12.40 % (326312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.73/12.40 % (326312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.73/12.40 % (326312)CaDiCaL version: 2.1.3 % 85.73/12.40 % (326312)Termination reason: Instruction limit % 85.73/12.40 % (326312)Termination phase: Saturation % 85.73/12.40 % (326312)Time elapsed: 0.473 s % 85.73/12.40 % (326312)Peak memory usage: 18 MB % 85.73/12.40 % (326312)Instructions burned: 879 (million) % 85.73/12.40 % (326320)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=746463268:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 85.73/12.40 % (326316)Cannot represent all propositional literals internally % 85.73/12.40 % (326316)Refutation not found, incomplete strategy % 85.73/12.40 % (326316)------------------------------ % 85.73/12.40 % (326316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.73/12.40 % (326316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.73/12.40 % (326316)CaDiCaL version: 2.1.3 % 85.73/12.40 % (326316)Termination reason: Refutation not found, incomplete strategy % 85.73/12.40 % (326316)Time elapsed: 0.343 s % 85.73/12.40 % (326316)Peak memory usage: 21 MB % 85.73/12.40 % (326316)Instructions burned: 687 (million) % 85.73/12.40 % (326316)------------------------------ % 85.73/12.40 % (326316)------------------------------ % 85.73/12.40 % (326322)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3056854516:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 85.73/12.40 % TRYING [3] % 85.73/12.40 % TRYING [8] % 85.73/12.40 % (326318)Instruction limit reached! % 85.73/12.40 % (326318)------------------------------ % 85.73/12.40 % (326318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 85.73/12.40 % (326318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.73/12.40 % (326318)CaDiCaL version: 2.1.3 % 85.73/12.40 % (326318)Termination reason: Instruction limit % 85.73/12.40 % (326318)Termination phase: Finite model building constraint generation % 85.73/12.40 % (326318)Time elapsed: 0.423 s % 85.73/12.40 % (326318)Peak memory usage: 35 MB % 85.73/12.40 % (326318)Instructions burned: 923 (million) % 85.73/12.40 % (326324)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1638461339:i=6324_2985 on theBenchmark for (2985ds/6324Mi) % 85.73/12.40 % (326324)Cannot represent all propositional literals internally % 85.73/12.40 % (326324)Refutation not found, incomplete strategy % 85.73/12.40 % (326324)------------------------------ % 169.32/24.13 % (326324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.32/24.13 % (326324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.32/24.13 % (326324)CaDiCaL version: 2.1.3 % 169.32/24.13 % (326324)Termination reason: Refutation not found, incomplete strategy % 169.32/24.13 % (326324)Time elapsed: 0.351 s % 169.32/24.13 % (326324)Peak memory usage: 21 MB % 169.32/24.13 % (326324)Instructions burned: 710 (million) % 169.32/24.13 % (326324)------------------------------ % 169.32/24.13 % (326324)------------------------------ % 169.32/24.13 % (326326)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1707282615:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi) % 169.32/24.13 % (326322)Instruction limit reached! % 169.32/24.13 % (326322)------------------------------ % 169.32/24.13 % (326322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.32/24.13 % (326322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.32/24.13 % (326322)CaDiCaL version: 2.1.3 % 169.32/24.13 % (326322)Termination reason: Instruction limit % 169.32/24.13 % (326322)Termination phase: Saturation % 169.32/24.13 % (326322)Time elapsed: 0.672 s % 169.32/24.13 % (326322)Peak memory usage: 23 MB % 169.32/24.13 % (326322)Instructions burned: 1473 (million) % 169.32/24.13 % (326328)ott-2_1_sil=16000:newcnf=on:random_seed=2664468346:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi) % 169.32/24.13 % TRYING [4] % 169.32/24.13 % (326328)Instruction limit reached! % 169.32/24.13 % (326328)------------------------------ % 169.32/24.13 % (326328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.32/24.13 % (326328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.32/24.13 % (326328)CaDiCaL version: 2.1.3 % 169.32/24.13 % (326328)Termination reason: Instruction limit % 169.32/24.13 % (326328)Termination phase: Saturation % 169.32/24.13 % (326328)Time elapsed: 0.305 s % 169.32/24.13 % (326328)Peak memory usage: 13 MB % 169.32/24.13 % (326328)Instructions burned: 870 (million) % 169.32/24.13 % (326330)ott+10_1_sil=32000:tgt=ground:random_seed=1221306934:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi) % 169.32/24.13 % (326326)Instruction limit reached! % 169.32/24.13 % (326326)------------------------------ % 169.32/24.13 % (326326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.32/24.13 % (326326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.32/24.13 % (326326)CaDiCaL version: 2.1.3 % 169.32/24.13 % (326326)Termination reason: Instruction limit % 169.32/24.13 % (326326)Termination phase: Finite model building preprocessing % 169.32/24.13 % (326326)Time elapsed: 1.073 s % 169.32/24.13 % (326326)Peak memory usage: 27 MB % 169.32/24.13 % (326326)Instructions burned: 2175 (million) % 169.32/24.13 % (326332)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2222907201:i=54282_2970 on theBenchmark for (2970ds/54282Mi) % 169.32/24.13 % TRYING [1] % 169.32/24.13 % TRYING [2] % 169.32/24.13 % TRYING [3] % 169.32/24.13 % (326320)Instruction limit reached! % 169.32/24.13 % (326320)------------------------------ % 169.32/24.13 % (326320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.32/24.13 % (326320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.32/24.13 % (326320)CaDiCaL version: 2.1.3 % 169.32/24.13 % (326320)Termination reason: Instruction limit % 169.32/24.13 % (326320)Termination phase: Saturation % 169.32/24.13 % (326320)Time elapsed: 2.428 s % 169.32/24.13 % (326320)Peak memory usage: 31 MB % 169.32/24.13 % (326320)Instructions burned: 5133 (million) % 169.32/24.13 % (326334)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=8246758:i=3512:aac=none_2963 on theBenchmark for (2963ds/3512Mi) % 169.32/24.13 % TRYING [4] % 169.32/24.13 % TRYING [4] % 169.32/24.13 % (326334)Instruction limit reached! % 169.32/24.13 % (326334)------------------------------ % 169.32/24.13 % (326334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 169.32/24.13 % (326334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.32/24.13 % (326334)CaDiCaL version: 2.1.3 % 169.32/24.13 % (326334)Termination reason: Instruction limit % 169.32/24.13 % (326334)Termination phase: Saturation % 169.32/24.13 % (326334)Time elapsed: 1.670 s % 169.32/24.13 % (326334)Peak memory usage: 24 MB % 169.32/24.13 % (326334)Instructions burned: 3514 (million) % 169.32/24.13 % (326336)dis+21_1_sil=32000:sas=cadical:random_seed=1731031927:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi) % 169.32/24.13 % (326330)Instruction limit reached! % 169.32/24.13 % (326330)------------------------------ % 169.32/24.13 % (326330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.52/35.37 % (326330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.52/35.37 % (326330)CaDiCaL version: 2.1.3 % 248.52/35.37 % (326330)Termination reason: Instruction limit % 248.52/35.37 % (326330)Termination phase: Saturation % 248.52/35.37 % (326330)Time elapsed: 3.284 s % 248.52/35.37 % (326330)Peak memory usage: 55 MB % 248.52/35.37 % (326330)Instructions burned: 5115 (million) % 248.52/35.37 % (326338)ott+11_1_sil=16000:gs=on:random_seed=1932537592:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2943 on theBenchmark for (2943ds/2251Mi) % 248.52/35.37 % (326313)Instruction limit reached! % 248.52/35.37 % (326313)------------------------------ % 248.52/35.37 % (326313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.52/35.37 % (326313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.52/35.37 % (326313)CaDiCaL version: 2.1.3 % 248.52/35.37 % (326313)Termination reason: Instruction limit % 248.52/35.37 % (326313)Termination phase: Finite model building constraint generation % 248.52/35.37 % (326313)Time elapsed: 5.388 s % 248.52/35.37 % (326313)Peak memory usage: 677 MB % 248.52/35.37 % (326313)Instructions burned: 22062 (million) % 248.52/35.37 % (326340)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1153404156:fmbsr=1.6:i=67534_2938 on theBenchmark for (2938ds/67534Mi) % 248.52/35.37 % (326338)Instruction limit reached! % 248.52/35.37 % (326338)------------------------------ % 248.52/35.37 % (326338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.52/35.37 % (326338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.52/35.37 % (326338)CaDiCaL version: 2.1.3 % 248.52/35.37 % (326338)Termination reason: Instruction limit % 248.52/35.37 % (326338)Termination phase: Saturation % 248.52/35.37 % (326338)Time elapsed: 1.330 s % 248.52/35.37 % (326338)Peak memory usage: 28 MB % 248.52/35.37 % (326338)Instructions burned: 2252 (million) % 248.52/35.37 % (326342)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=337446869:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2930 on theBenchmark for (2930ds/4591Mi) % 248.52/35.37 % (326336)Instruction limit reached! % 248.52/35.37 % (326336)------------------------------ % 248.52/35.37 % (326336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.52/35.37 % (326336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.52/35.37 % (326336)CaDiCaL version: 2.1.3 % 248.52/35.37 % (326336)Termination reason: Instruction limit % 248.52/35.37 % (326336)Termination phase: Saturation % 248.52/35.37 % (326336)Time elapsed: 2.211 s % 248.52/35.37 % (326336)Peak memory usage: 36 MB % 248.52/35.37 % (326336)Instructions burned: 3774 (million) % 248.52/35.37 % (326344)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2476337744:i=29340_2924 on theBenchmark for (2924ds/29340Mi) % 248.52/35.37 % (326342)Instruction limit reached! % 248.52/35.37 % (326342)------------------------------ % 248.52/35.37 % (326342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.52/35.37 % (326342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.52/35.37 % (326342)CaDiCaL version: 2.1.3 % 248.52/35.37 % (326342)Termination reason: Instruction limit % 248.52/35.37 % (326342)Termination phase: Saturation % 248.52/35.37 % (326342)Time elapsed: 1.889 s % 248.52/35.37 % (326342)Peak memory usage: 35 MB % 248.52/35.37 % (326342)Instructions burned: 4594 (million) % 248.52/35.37 % (326346)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1353144959:i=5211_2911 on theBenchmark for (2911ds/5211Mi) % 248.52/35.37 % TRYING [5] % 248.52/35.37 % TRYING [7] % 248.52/35.37 % (326346)Instruction limit reached! % 248.52/35.37 % (326346)------------------------------ % 248.52/35.37 % (326346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 248.52/35.37 % (326346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.52/35.37 % (326346)CaDiCaL version: 2.1.3 % 248.52/35.37 % (326346)Termination reason: Instruction limit % 248.52/35.37 % (326346)Termination phase: Saturation % 248.52/35.37 % (326346)Time elapsed: 2.893 s % 248.52/35.37 % (326346)Peak memory usage: 50 MB % 248.52/35.37 % (326346)Instructions burned: 5212 (million) % 248.52/35.37 % (326348)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4290653675:i=5497:nm=2_2882 on theBenchmark for (2882ds/5497Mi) % 248.52/35.37 % (326348)Cannot represent all propositional literals internally % 248.52/35.37 % (326348)Refutation not found, incomplete strategy % 248.52/35.37 % (326348)------------------------------ % 248.52/35.37 % (326348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.89/39.31 % (326348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.89/39.31 % (326348)CaDiCaL version: 2.1.3 % 276.89/39.31 % (326348)Termination reason: Refutation not found, incomplete strategy % 276.89/39.31 % (326348)Time elapsed: 0.353 s % 276.89/39.31 % (326348)Peak memory usage: 21 MB % 276.89/39.31 % (326348)Instructions burned: 710 (million) % 276.89/39.31 % (326348)------------------------------ % 276.89/39.31 % (326348)------------------------------ % 276.89/39.31 % (326350)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=886334221:fmbsr=2:i=46332_2878 on theBenchmark for (2878ds/46332Mi) % 276.89/39.31 % (326350)Cannot represent all propositional literals internally % 276.89/39.31 % (326350)Refutation not found, incomplete strategy % 276.89/39.31 % (326350)------------------------------ % 276.89/39.31 % (326350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.89/39.31 % (326350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.89/39.31 % (326350)CaDiCaL version: 2.1.3 % 276.89/39.31 % (326350)Termination reason: Refutation not found, incomplete strategy % 276.89/39.31 % (326350)Time elapsed: 0.354 s % 276.89/39.31 % (326350)Peak memory usage: 19 MB % 276.89/39.31 % (326350)Instructions burned: 725 (million) % 276.89/39.31 % (326350)------------------------------ % 276.89/39.31 % (326350)------------------------------ % 276.89/39.31 % (326352)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2933730778:i=14071_2874 on theBenchmark for (2874ds/14071Mi) % 276.89/39.31 % TRYING [12] % 276.89/39.31 % TRYING [5] % 276.89/39.31 % (326352)Instruction limit reached! % 276.89/39.31 % (326352)------------------------------ % 276.89/39.31 % (326352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.89/39.31 % (326352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.89/39.31 % (326352)CaDiCaL version: 2.1.3 % 276.89/39.31 % (326352)Termination reason: Instruction limit % 276.89/39.31 % (326352)Termination phase: Finite model building constraint generation % 276.89/39.31 % (326352)Time elapsed: 5.262 s % 276.89/39.31 % (326352)Peak memory usage: 990 MB % 276.89/39.31 % (326352)Instructions burned: 14073 (million) % 276.89/39.31 % (326354)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2926621512:i=22565:add=on:rawr=on_2820 on theBenchmark for (2820ds/22565Mi) % 276.89/39.31 % (326340)Instruction limit reached! % 276.89/39.31 % (326340)------------------------------ % 276.89/39.31 % (326340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.89/39.31 % (326340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.89/39.31 % (326340)CaDiCaL version: 2.1.3 % 276.89/39.31 % (326340)Termination reason: Instruction limit % 276.89/39.31 % (326340)Termination phase: Finite model building constraint generation % 276.89/39.31 % (326340)Time elapsed: 12.911 s % 276.89/39.31 % (326340)Peak memory usage: 3619 MB % 276.89/39.31 % (326340)Instructions burned: 67540 (million) % 276.89/39.31 % (326356)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2299360087:i=8173:av=off_2805 on theBenchmark for (2805ds/8173Mi) % 276.89/39.31 % (326344)Instruction limit reached! % 276.89/39.31 % (326344)------------------------------ % 276.89/39.31 % (326344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.89/39.31 % (326344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.89/39.31 % (326344)CaDiCaL version: 2.1.3 % 276.89/39.31 % (326344)Termination reason: Instruction limit % 276.89/39.31 % (326344)Termination phase: Saturation % 276.89/39.31 % (326344)Time elapsed: 13.308 s % 276.89/39.31 % (326344)Peak memory usage: 321 MB % 276.89/39.31 % (326344)Instructions burned: 29342 (million) % 276.89/39.31 % (326358)dis+10_16:1_sil=16000:random_seed=4215504631:i=9155:fsr=off_2790 on theBenchmark for (2790ds/9155Mi) % 276.89/39.31 % (326356)Instruction limit reached! % 276.89/39.31 % (326356)------------------------------ % 276.89/39.31 % (326356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.89/39.31 % (326356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.89/39.31 % (326356)CaDiCaL version: 2.1.3 % 276.89/39.31 % (326356)Termination reason: Instruction limit % 276.89/39.31 % (326356)Termination phase: Saturation % 276.89/39.31 % (326356)Time elapsed: 2.721 s % 276.89/39.31 % (326356)Peak memory usage: 84 MB % 276.89/39.31 % (326356)Instructions burned: 8176 (million) % 276.89/39.31 % (326360)ott-3_8_sil=64000:random_seed=2537481804:i=20139:bs=on_2778 on theBenchmark for (2778ds/20139Mi) % 276.89/39.31 % (326332)Instruction limitTerminated % 300.29/42.64 % Vampire exiting % 300.29/42.64 Terminated %------------------------------------------------------------------------------