%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM923_2 : 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 : 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 12:26:04 PM UTC 2026 % Result : Timeout 300.59s 43.06s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM923_2 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.34 % Computer : n012.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Sun Sep 27 21:39:19 UTC 2026 % 0.07/0.34 % CPUTime : % 0.07/0.34 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.37 Running first-order model finding % 0.10/0.37 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 % 5.44/1.29 % (2770272)Will run a generic schedule for satisfiability detection. % 5.44/1.29 % (2770278)% WARNING: option uhcvi not known. % 5.44/1.29 % (2770278)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2683833128:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 5.44/1.29 % (2770277)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4007041104_2999 on theBenchmark for (2999ds/0Mi) % 5.44/1.29 % (2770283)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1787935639:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 5.44/1.29 % (2770282)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=304212494:i=131_2999 on theBenchmark for (2999ds/131Mi) % 5.44/1.29 % (2770279)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3551186723:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 5.44/1.29 % (2770281)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1659344604:i=116_2999 on theBenchmark for (2999ds/116Mi) % 5.44/1.29 % (2770280)dis+10_1_sil=32000:sp=arity:random_seed=314096961:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 5.44/1.29 % (2770280)Instruction limit reached! % 5.44/1.29 % (2770280)------------------------------ % 5.44/1.29 % (2770280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.44/1.29 % (2770280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.29 % (2770280)CaDiCaL version: 2.1.3 % 5.44/1.29 % (2770280)Termination reason: Instruction limit % 5.44/1.29 % (2770280)Termination phase: Saturation % 5.44/1.29 % (2770280)Time elapsed: 0.050 s % 5.44/1.29 % (2770280)Peak memory usage: 13 MB % 5.44/1.29 % (2770280)Instructions burned: 104 (million) % 5.44/1.29 % (2770281)Instruction limit reached! % 5.44/1.29 % (2770281)------------------------------ % 5.44/1.29 % (2770281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.44/1.29 % (2770281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.29 % (2770281)CaDiCaL version: 2.1.3 % 5.44/1.29 % (2770281)Termination reason: Instruction limit % 5.44/1.29 % (2770281)Termination phase: Saturation % 5.44/1.29 % (2770281)Time elapsed: 0.056 s % 5.44/1.29 % (2770281)Peak memory usage: 13 MB % 5.44/1.29 % (2770281)Instructions burned: 116 (million) % 5.44/1.29 % (2770282)Instruction limit reached! % 5.44/1.29 % (2770282)------------------------------ % 5.44/1.29 % (2770282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.44/1.29 % (2770282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.29 % (2770282)CaDiCaL version: 2.1.3 % 5.44/1.29 % (2770282)Termination reason: Instruction limit % 5.44/1.29 % (2770282)Termination phase: Saturation % 5.44/1.29 % (2770282)Time elapsed: 0.066 s % 5.44/1.29 % (2770282)Peak memory usage: 13 MB % 5.44/1.29 % (2770282)Instructions burned: 132 (million) % 5.44/1.29 % (2770291)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2826609742:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 5.44/1.29 % (2770283)Instruction limit reached! % 5.44/1.29 % (2770283)------------------------------ % 5.44/1.29 % (2770283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.44/1.29 % (2770283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.29 % (2770283)CaDiCaL version: 2.1.3 % 5.44/1.29 % (2770283)Termination reason: Instruction limit % 5.44/1.29 % (2770283)Termination phase: Saturation % 5.44/1.29 % (2770283)Time elapsed: 0.080 s % 5.44/1.29 % (2770283)Peak memory usage: 14 MB % 5.44/1.29 % (2770283)Instructions burned: 160 (million) % 5.44/1.29 % (2770296)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=4109864041:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 5.44/1.29 % (2770292)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=850405023:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 5.44/1.29 % (2770300)ott-21_1_sil=16000:fs=off:random_seed=3726327551:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 5.44/1.29 % (2770292)Instruction limit reached! % 5.44/1.29 % (2770292)------------------------------ % 5.44/1.29 % (2770292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 5.44/1.29 % (2770292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.44/1.29 % (2770292)CaDiCaL version: 2.1.3 % 21.95/3.57 % (2770292)Termination reason: Instruction limit % 21.95/3.57 % (2770292)Termination phase: Saturation % 21.95/3.57 % (2770292)Time elapsed: 0.052 s % 21.95/3.57 % (2770292)Peak memory usage: 14 MB % 21.95/3.57 % (2770292)Instructions burned: 132 (million) % 21.95/3.57 % (2770300)Instruction limit reached! % 21.95/3.57 % (2770300)------------------------------ % 21.95/3.57 % (2770300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.95/3.57 % (2770300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.57 % (2770300)CaDiCaL version: 2.1.3 % 21.95/3.57 % (2770300)Termination reason: Instruction limit % 21.95/3.57 % (2770300)Termination phase: Saturation % 21.95/3.57 % (2770300)Time elapsed: 0.042 s % 21.95/3.57 % (2770300)Peak memory usage: 13 MB % 21.95/3.57 % (2770300)Instructions burned: 181 (million) % 21.95/3.57 % (2770303)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1886672920:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.95/3.57 % (2770302)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1421567520:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 21.95/3.57 % TRYING [1] % 21.95/3.57 % TRYING [2] % 21.95/3.57 % TRYING [3] % 21.95/3.57 % TRYING [1,1,1,1,1] % 21.95/3.57 % TRYING [2,1,1,1,1] % 21.95/3.57 % (2770291)Instruction limit reached! % 21.95/3.57 % (2770291)------------------------------ % 21.95/3.57 % (2770291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.95/3.57 % (2770291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.57 % (2770291)CaDiCaL version: 2.1.3 % 21.95/3.57 % (2770291)Termination reason: Instruction limit % 21.95/3.57 % (2770291)Termination phase: Finite model building constraint generation % 21.95/3.57 % (2770291)Time elapsed: 0.193 s % 21.95/3.57 % (2770291)Peak memory usage: 30 MB % 21.95/3.57 % (2770291)Instructions burned: 715 (million) % 21.95/3.57 % TRYING [2,1,1,2,1] % 21.95/3.57 % (2770306)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1011663581:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 21.95/3.57 % (2770296)Instruction limit reached! % 21.95/3.57 % (2770296)------------------------------ % 21.95/3.57 % (2770296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.95/3.57 % (2770296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.57 % (2770296)CaDiCaL version: 2.1.3 % 21.95/3.57 % (2770296)Termination reason: Instruction limit % 21.95/3.57 % (2770296)Termination phase: Saturation % 21.95/3.57 % (2770296)Time elapsed: 0.197 s % 21.95/3.57 % (2770296)Peak memory usage: 18 MB % 21.95/3.57 % (2770296)Instructions burned: 685 (million) % 21.95/3.57 % (2770308)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1794595817:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 21.95/3.57 % TRYING [2,1,1,3,1] % 21.95/3.57 % (2770302)Instruction limit reached! % 21.95/3.57 % (2770302)------------------------------ % 21.95/3.57 % (2770302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.95/3.57 % (2770302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.57 % (2770302)CaDiCaL version: 2.1.3 % 21.95/3.57 % (2770302)Termination reason: Instruction limit % 21.95/3.57 % (2770302)Termination phase: Saturation % 21.95/3.57 % (2770302)Time elapsed: 0.157 s % 21.95/3.57 % (2770302)Peak memory usage: 14 MB % 21.95/3.57 % (2770302)Instructions burned: 480 (million) % 21.95/3.57 % (2770310)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=3820658284:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 21.95/3.57 % TRYING [2,1,1,4,1] % 21.95/3.57 % (2770303)Instruction limit reached! % 21.95/3.57 % (2770303)------------------------------ % 21.95/3.57 % (2770303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.95/3.57 % (2770303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.95/3.57 % (2770303)CaDiCaL version: 2.1.3 % 21.95/3.57 % (2770303)Termination reason: Instruction limit % 21.95/3.57 % (2770303)Termination phase: Finite model building preprocessing % 21.95/3.57 % (2770303)Time elapsed: 0.210 s % 21.95/3.57 % (2770303)Peak memory usage: 22 MB % 21.95/3.57 % (2770303)Instructions burned: 865 (million) % 21.95/3.57 % (2770324)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1680832132:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 21.95/3.57 % TRYING [2,1,1,5,1] % 21.95/3.57 % (2770308)Cannot represent all propositional literals internally % 21.95/3.57 % (2770308)Refutation not found, incomplete strategy % 37.14/6.53 % (2770308)------------------------------ % 37.14/6.53 % (2770308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.14/6.53 % (2770308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.14/6.53 % (2770308)CaDiCaL version: 2.1.3 % 37.14/6.53 % (2770308)Termination reason: Refutation not found, incomplete strategy % 37.14/6.53 % (2770308)Time elapsed: 0.213 s % 37.14/6.53 % (2770308)Peak memory usage: 22 MB % 37.14/6.53 % (2770308)Instructions burned: 881 (million) % 37.14/6.53 % (2770308)------------------------------ % 37.14/6.53 % (2770308)------------------------------ % 37.14/6.53 % (2770386)fmb+10_1_sil=64000:random_seed=2944862145:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 37.14/6.53 % (2770310)Instruction limit reached! % 37.14/6.53 % (2770310)------------------------------ % 37.14/6.53 % (2770310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.14/6.53 % (2770310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.14/6.53 % (2770310)CaDiCaL version: 2.1.3 % 37.14/6.53 % (2770310)Termination reason: Instruction limit % 37.14/6.53 % (2770310)Termination phase: Saturation % 37.14/6.53 % (2770310)Time elapsed: 0.230 s % 37.14/6.53 % (2770310)Peak memory usage: 17 MB % 37.14/6.53 % (2770310)Instructions burned: 693 (million) % 37.14/6.53 % (2770405)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=914047234:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 37.14/6.53 % (2770324)Instruction limit reached! % 37.14/6.53 % (2770324)------------------------------ % 37.14/6.53 % (2770324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.14/6.53 % (2770324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.14/6.53 % (2770324)CaDiCaL version: 2.1.3 % 37.14/6.53 % (2770324)Termination reason: Instruction limit % 37.14/6.53 % (2770324)Termination phase: Saturation % 37.14/6.53 % (2770324)Time elapsed: 0.273 s % 37.14/6.53 % (2770324)Peak memory usage: 20 MB % 37.14/6.53 % (2770324)Instructions burned: 880 (million) % 37.14/6.53 % (2770306)Instruction limit reached! % 37.14/6.53 % (2770306)------------------------------ % 37.14/6.53 % (2770306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.14/6.53 % (2770306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.14/6.53 % (2770306)CaDiCaL version: 2.1.3 % 37.14/6.53 % (2770306)Termination reason: Instruction limit % 37.14/6.53 % (2770306)Termination phase: Saturation % 37.14/6.53 % (2770306)Time elapsed: 0.374 s % 37.14/6.53 % (2770306)Peak memory usage: 21 MB % 37.14/6.53 % (2770306)Instructions burned: 1180 (million) % 37.14/6.53 % (2770424)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1525711884:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 37.14/6.53 % (2770425)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3228413164:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 37.14/6.53 % TRYING [1,1,1,1,1] % 37.14/6.53 % TRYING [1,1,1,2,1] % 37.14/6.53 % TRYING [1,1,1,3,1] % 37.14/6.53 % (2770405)Cannot represent all propositional literals internally % 37.14/6.53 % (2770405)Refutation not found, incomplete strategy % 37.14/6.53 % (2770405)------------------------------ % 37.14/6.53 % (2770405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.14/6.53 % (2770405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.14/6.53 % (2770405)CaDiCaL version: 2.1.3 % 37.14/6.53 % (2770405)Termination reason: Refutation not found, incomplete strategy % 37.14/6.53 % (2770405)Time elapsed: 0.200 s % 37.14/6.53 % (2770405)Peak memory usage: 22 MB % 37.14/6.53 % (2770405)Instructions burned: 825 (million) % 37.14/6.53 % (2770405)------------------------------ % 37.14/6.53 % (2770405)------------------------------ % 37.14/6.53 % (2770444)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3756826126:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 37.14/6.53 % TRYING [1,1,1,4,1] % 37.14/6.53 % TRYING [2,1,1,6,1] % 37.14/6.53 % TRYING [8,8,8,8,8] % 37.14/6.53 % (2770424)Instruction limit reached! % 37.14/6.53 % (2770424)------------------------------ % 37.14/6.53 % (2770424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 37.14/6.53 % (2770424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.14/6.53 % (2770424)CaDiCaL version: 2.1.3 % 37.14/6.53 % (2770424)Termination reason: Instruction limit % 37.14/6.53 % (2770424)Termination phase: Finite model building constraint generation % 37.14/6.53 % (2770424)Time elapsed: 0.225 s % 104.45/15.25 % (2770424)Peak memory usage: 25 MB % 104.45/15.25 % (2770424)Instructions burned: 924 (million) % 104.45/15.25 % (2770477)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4131335430:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 104.45/15.25 % TRYING [1,1,1,5,1] % 104.45/15.25 % (2770477)Cannot represent all propositional literals internally % 104.45/15.25 % (2770477)Refutation not found, incomplete strategy % 104.45/15.25 % (2770477)------------------------------ % 104.45/15.25 % (2770477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.45/15.25 % (2770477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.45/15.25 % (2770477)CaDiCaL version: 2.1.3 % 104.45/15.25 % (2770477)Termination reason: Refutation not found, incomplete strategy % 104.45/15.25 % (2770477)Time elapsed: 0.213 s % 104.45/15.25 % (2770477)Peak memory usage: 22 MB % 104.45/15.25 % (2770477)Instructions burned: 872 (million) % 104.45/15.25 % (2770477)------------------------------ % 104.45/15.25 % (2770477)------------------------------ % 104.45/15.25 % (2770479)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2736187026:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi) % 104.45/15.25 % (2770444)Instruction limit reached! % 104.45/15.25 % (2770444)------------------------------ % 104.45/15.25 % (2770444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.45/15.25 % (2770444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.45/15.25 % (2770444)CaDiCaL version: 2.1.3 % 104.45/15.25 % (2770444)Termination reason: Instruction limit % 104.45/15.25 % (2770444)Termination phase: Saturation % 104.45/15.25 % (2770444)Time elapsed: 0.506 s % 104.45/15.25 % (2770444)Peak memory usage: 35 MB % 104.45/15.25 % (2770444)Instructions burned: 1473 (million) % 104.45/15.25 % (2770481)ott-2_1_sil=16000:newcnf=on:random_seed=1726369041:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2986 on theBenchmark for (2986ds/869Mi) % 104.45/15.25 % (2770479)Cannot represent all propositional literals internally % 104.45/15.25 % (2770479)Refutation not found, incomplete strategy % 104.45/15.25 % (2770479)------------------------------ % 104.45/15.25 % (2770479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.45/15.25 % (2770479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.45/15.25 % (2770479)CaDiCaL version: 2.1.3 % 104.45/15.25 % (2770479)Termination reason: Refutation not found, incomplete strategy % 104.45/15.25 % (2770479)Time elapsed: 0.276 s % 104.45/15.25 % (2770479)Peak memory usage: 26 MB % 104.45/15.25 % (2770479)Instructions burned: 1056 (million) % 104.45/15.25 % (2770479)------------------------------ % 104.45/15.25 % (2770479)------------------------------ % 104.45/15.25 % (2770483)ott+10_1_sil=32000:tgt=ground:random_seed=3424436461:i=5114:av=off_2985 on theBenchmark for (2985ds/5114Mi) % 104.45/15.25 % (2770481)Instruction limit reached! % 104.45/15.25 % (2770481)------------------------------ % 104.45/15.25 % (2770481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.45/15.25 % (2770481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.45/15.25 % (2770481)CaDiCaL version: 2.1.3 % 104.45/15.25 % (2770481)Termination reason: Instruction limit % 104.45/15.25 % (2770481)Termination phase: Saturation % 104.45/15.25 % (2770481)Time elapsed: 0.266 s % 104.45/15.25 % (2770481)Peak memory usage: 19 MB % 104.45/15.25 % (2770481)Instructions burned: 870 (million) % 104.45/15.25 % (2770485)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1823490840:i=54282_2984 on theBenchmark for (2984ds/54282Mi) % 104.45/15.25 % TRYING [2,2,1,6,1] % 104.45/15.25 % TRYING [1,1,1,6,1] % 104.45/15.25 % TRYING [1,1,1,1,1] % 104.45/15.25 % TRYING [2,1,1,1,1] % 104.45/15.25 % TRYING [2,1,1,2,1] % 104.45/15.25 % TRYING [2,1,1,3,1] % 104.45/15.25 % TRYING [2,1,1,4,1] % 104.45/15.25 % TRYING [2,1,1,5,1] % 104.45/15.25 % (2770425)Instruction limit reached! % 104.45/15.25 % (2770425)------------------------------ % 104.45/15.25 % (2770425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 104.45/15.25 % (2770425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.45/15.25 % (2770425)CaDiCaL version: 2.1.3 % 104.45/15.25 % (2770425)Termination reason: Instruction limit % 104.45/15.25 % (2770425)Termination phase: Saturation % 104.45/15.25 % (2770425)Time elapsed: 1.602 s % 104.45/15.25 % (2770425)Peak memory usage: 48 MB % 104.45/15.25 % (2770425)Instructions burned: 5131 (million) % 104.45/15.25 % (2770487)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3192342267:i=3512:aac=none_2976 on theBenchmark for (2976ds/3512Mi) % 104.45/15.25 % TRYING [2,1,1,6,1] % 104.45/15.25 % TRYING [2,2,1,6,2] % 104.45/15.25 % TRYING [2,2,2,6,2] % 104.45/15.25 % TRYING [2,2,1,6,1] % 104.45/15.25 % (2770483)Instruction limit reached! % 204.62/29.47 % (2770483)------------------------------ % 204.62/29.47 % (2770483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.62/29.47 % (2770483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.62/29.47 % (2770483)CaDiCaL version: 2.1.3 % 204.62/29.47 % (2770483)Termination reason: Instruction limit % 204.62/29.47 % (2770483)Termination phase: Saturation % 204.62/29.47 % (2770483)Time elapsed: 1.744 s % 204.62/29.47 % (2770483)Peak memory usage: 43 MB % 204.62/29.47 % (2770483)Instructions burned: 5115 (million) % 204.62/29.47 % (2770489)dis+21_1_sil=32000:sas=cadical:random_seed=3423510064:i=3773:amm=off_2968 on theBenchmark for (2968ds/3773Mi) % 204.62/29.47 % (2770487)Instruction limit reached! % 204.62/29.47 % (2770487)------------------------------ % 204.62/29.47 % (2770487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.62/29.47 % (2770487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.62/29.47 % (2770487)CaDiCaL version: 2.1.3 % 204.62/29.47 % (2770487)Termination reason: Instruction limit % 204.62/29.47 % (2770487)Termination phase: Saturation % 204.62/29.47 % (2770487)Time elapsed: 1.112 s % 204.62/29.47 % (2770487)Peak memory usage: 35 MB % 204.62/29.47 % (2770487)Instructions burned: 3518 (million) % 204.62/29.47 % (2770491)ott+11_1_sil=16000:gs=on:random_seed=890990996:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2965 on theBenchmark for (2965ds/2251Mi) % 204.62/29.47 % TRYING [2,2,3,6,2] % 204.62/29.47 % TRYING [2,2,1,6,2] % 204.62/29.47 % (2770491)Instruction limit reached! % 204.62/29.47 % (2770491)------------------------------ % 204.62/29.47 % (2770491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.62/29.47 % (2770491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.62/29.47 % (2770491)CaDiCaL version: 2.1.3 % 204.62/29.47 % (2770491)Termination reason: Instruction limit % 204.62/29.47 % (2770491)Termination phase: Saturation % 204.62/29.47 % (2770491)Time elapsed: 0.792 s % 204.62/29.47 % (2770491)Peak memory usage: 32 MB % 204.62/29.47 % (2770491)Instructions burned: 2253 (million) % 204.62/29.47 % (2770493)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=115410435:fmbsr=1.6:i=67534_2957 on theBenchmark for (2957ds/67534Mi) % 204.62/29.47 % (2770489)Instruction limit reached! % 204.62/29.47 % (2770489)------------------------------ % 204.62/29.47 % (2770489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.62/29.47 % (2770489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.62/29.47 % (2770489)CaDiCaL version: 2.1.3 % 204.62/29.47 % (2770489)Termination reason: Instruction limit % 204.62/29.47 % (2770489)Termination phase: Saturation % 204.62/29.47 % (2770489)Time elapsed: 1.138 s % 204.62/29.47 % (2770489)Peak memory usage: 35 MB % 204.62/29.47 % (2770489)Instructions burned: 3776 (million) % 204.62/29.47 % (2770495)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=331052082:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2956 on theBenchmark for (2956ds/4591Mi) % 204.62/29.47 % TRYING [1,1,1,7,1] % 204.62/29.47 % TRYING [2,3,3,6,2] % 204.62/29.47 % TRYING [2,2,2,6,2] % 204.62/29.47 % TRYING [2,2,3,6,2] % 204.62/29.47 % TRYING [2,4,3,6,2] % 204.62/29.47 % (2770495)Instruction limit reached! % 204.62/29.47 % (2770495)------------------------------ % 204.62/29.47 % (2770495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.62/29.47 % (2770495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.62/29.47 % (2770495)CaDiCaL version: 2.1.3 % 204.62/29.47 % (2770495)Termination reason: Instruction limit % 204.62/29.47 % (2770495)Termination phase: Saturation % 204.62/29.47 % (2770495)Time elapsed: 1.380 s % 204.62/29.47 % (2770495)Peak memory usage: 61 MB % 204.62/29.47 % (2770495)Instructions burned: 4592 (million) % 204.62/29.47 % (2770497)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3404368042:i=29340_2942 on theBenchmark for (2942ds/29340Mi) % 204.62/29.47 % (2770386)Instruction limit reached! % 204.62/29.47 % (2770386)------------------------------ % 204.62/29.47 % (2770386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 204.62/29.47 % (2770386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.62/29.47 % (2770386)CaDiCaL version: 2.1.3 % 204.62/29.47 % (2770386)Termination reason: Instruction limit % 204.62/29.47 % (2770386)Termination phase: Finite model building SAT solving % 204.62/29.47 % (2770386)Time elapsed: 5.567 s % 204.62/29.47 % (2770386)Peak memory usage: 387 MB % 204.62/29.47 % (2770386)Instructions burned: 22062 (million) % 204.62/29.47 % (2770499)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1859255800:i=5211_2938 on theBenchmark for (2938ds/5211Mi) % 235.94/33.96 % TRYING [2,3,3,6,2] % 235.94/33.96 % TRYING [2,5,3,6,2] % 235.94/33.96 % TRYING [2,4,3,6,2] % 235.94/33.96 % (2770499)Instruction limit reached! % 235.94/33.96 % (2770499)------------------------------ % 235.94/33.96 % (2770499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.94/33.96 % (2770499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.94/33.96 % (2770499)CaDiCaL version: 2.1.3 % 235.94/33.96 % (2770499)Termination reason: Instruction limit % 235.94/33.96 % (2770499)Termination phase: Saturation % 235.94/33.96 % (2770499)Time elapsed: 1.477 s % 235.94/33.96 % (2770499)Peak memory usage: 45 MB % 235.94/33.96 % (2770499)Instructions burned: 5212 (million) % 235.94/33.96 % (2770502)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=55818942:i=5497:nm=2_2923 on theBenchmark for (2923ds/5497Mi) % 235.94/33.96 % (2770502)Cannot represent all propositional literals internally % 235.94/33.96 % (2770502)Refutation not found, incomplete strategy % 235.94/33.96 % (2770502)------------------------------ % 235.94/33.96 % (2770502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.94/33.96 % (2770502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.94/33.96 % (2770502)CaDiCaL version: 2.1.3 % 235.94/33.96 % (2770502)Termination reason: Refutation not found, incomplete strategy % 235.94/33.96 % (2770502)Time elapsed: 0.191 s % 235.94/33.96 % (2770502)Peak memory usage: 22 MB % 235.94/33.96 % (2770502)Instructions burned: 781 (million) % 235.94/33.96 % (2770502)------------------------------ % 235.94/33.96 % (2770502)------------------------------ % 235.94/33.96 % (2770504)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3123609227:fmbsr=2:i=46332_2921 on theBenchmark for (2921ds/46332Mi) % 235.94/33.96 % (2770504)Cannot represent all propositional literals internally % 235.94/33.96 % (2770504)Refutation not found, incomplete strategy % 235.94/33.96 % (2770504)------------------------------ % 235.94/33.96 % (2770504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.94/33.96 % (2770504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.94/33.96 % (2770504)CaDiCaL version: 2.1.3 % 235.94/33.96 % (2770504)Termination reason: Refutation not found, incomplete strategy % 235.94/33.96 % (2770504)Time elapsed: 0.118 s % 235.94/33.96 % (2770504)Peak memory usage: 18 MB % 235.94/33.96 % (2770504)Instructions burned: 472 (million) % 235.94/33.96 % (2770504)------------------------------ % 235.94/33.96 % (2770504)------------------------------ % 235.94/33.96 % (2770506)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3783213557:i=14071_2920 on theBenchmark for (2920ds/14071Mi) % 235.94/33.96 % TRYING [12,12,12,12,12] % 235.94/33.96 % TRYING [2,5,3,6,2] % 235.94/33.96 % (2770506)Instruction limit reached! % 235.94/33.96 % (2770506)------------------------------ % 235.94/33.96 % (2770506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.94/33.96 % (2770506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.94/33.96 % (2770506)CaDiCaL version: 2.1.3 % 235.94/33.96 % (2770506)Termination reason: Instruction limit % 235.94/33.96 % (2770506)Termination phase: Finite model building constraint generation % 235.94/33.96 % (2770506)Time elapsed: 2.796 s % 235.94/33.96 % (2770506)Peak memory usage: 890 MB % 235.94/33.96 % (2770506)Instructions burned: 14076 (million) % 235.94/33.96 % (2770508)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3828879726:i=22565:add=on:rawr=on_2891 on theBenchmark for (2891ds/22565Mi) % 235.94/33.96 % TRYING [3,5,3,6,2] % 235.94/33.96 % TRYING [3,5,3,6,2] % 235.94/33.96 % TRYING [7] % 235.94/33.96 % (2770485)Instruction limit reached! % 235.94/33.96 % (2770485)------------------------------ % 235.94/33.96 % (2770485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.94/33.96 % (2770485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.94/33.96 % (2770485)CaDiCaL version: 2.1.3 % 235.94/33.96 % (2770485)Termination reason: Instruction limit % 235.94/33.96 % (2770485)Termination phase: Finite model building constraint generation % 235.94/33.96 % (2770485)Time elapsed: 12.771 s % 235.94/33.96 % (2770485)Peak memory usage: 897 MB % 235.94/33.96 % (2770485)Instructions burned: 54282 (million) % 235.94/33.96 % (2770636)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3928424619:i=8173:av=off_2855 on theBenchmark for (2855ds/8173Mi) % 235.94/33.96 % (2770497)Instruction limit reached! % 235.94/33.96 % (2770497)------------------------------ % 235.94/33.96 % (2770497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200Terminated % 300.59/43.06 % Vampire exiting %------------------------------------------------------------------------------