%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM286-3 : TPTP v9.3.1. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n015.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:18:15 PM UTC 2026 % Result : Timeout 300.63s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM286-3 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.37 % Computer : n015.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sun Sep 27 19:31:31 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.41 Running first-order model finding % 0.11/0.41 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 % 8.67/1.94 % (1962273)Will run a generic schedule for satisfiability detection. % 8.67/1.94 % (1962278)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=702577151_2999 on theBenchmark for (2999ds/0Mi) % 8.67/1.94 % (1962279)% WARNING: option uhcvi not known. % 8.67/1.94 % (1962279)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1129287781:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.67/1.94 % (1962280)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1654292214:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.67/1.94 % (1962281)dis+10_1_sil=32000:sp=arity:random_seed=3708194950:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.67/1.94 % (1962282)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3654872892:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.67/1.94 % (1962284)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=331434411:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.67/1.94 % (1962283)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2270439652:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.67/1.94 % (1962281)Instruction limit reached! % 8.67/1.94 % (1962281)------------------------------ % 8.67/1.94 % (1962281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.67/1.94 % (1962281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.67/1.94 % (1962281)CaDiCaL version: 2.1.3 % 8.67/1.94 % (1962281)Termination reason: Instruction limit % 8.67/1.94 % (1962281)Termination phase: Saturation % 8.67/1.94 % (1962281)Time elapsed: 0.062 s % 8.67/1.94 % (1962281)Peak memory usage: 13 MB % 8.67/1.94 % (1962281)Instructions burned: 104 (million) % 8.67/1.94 % (1962282)Instruction limit reached! % 8.67/1.94 % (1962282)------------------------------ % 8.67/1.94 % (1962282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.67/1.94 % (1962282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.67/1.94 % (1962282)CaDiCaL version: 2.1.3 % 8.67/1.94 % (1962282)Termination reason: Instruction limit % 8.67/1.94 % (1962282)Termination phase: Saturation % 8.67/1.94 % (1962282)Time elapsed: 0.066 s % 8.67/1.94 % (1962282)Peak memory usage: 13 MB % 8.67/1.94 % (1962282)Instructions burned: 118 (million) % 8.67/1.94 % TRYING [1] % 8.67/1.94 % (1962283)Instruction limit reached! % 8.67/1.94 % (1962283)------------------------------ % 8.67/1.94 % (1962283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.67/1.94 % (1962283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.67/1.94 % (1962283)CaDiCaL version: 2.1.3 % 8.67/1.94 % (1962283)Termination reason: Instruction limit % 8.67/1.94 % (1962283)Termination phase: Saturation % 8.67/1.94 % (1962283)Time elapsed: 0.071 s % 8.67/1.94 % (1962283)Peak memory usage: 13 MB % 8.67/1.94 % (1962283)Instructions burned: 131 (million) % 8.67/1.94 % TRYING [2] % 8.67/1.94 % (1962292)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1868929771:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.67/1.94 % (1962293)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2759513309:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.67/1.94 % (1962284)Instruction limit reached! % 8.67/1.94 % (1962284)------------------------------ % 8.67/1.94 % (1962284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.67/1.94 % (1962284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.67/1.94 % (1962284)CaDiCaL version: 2.1.3 % 8.67/1.94 % (1962284)Termination reason: Instruction limit % 8.67/1.94 % (1962284)Termination phase: Saturation % 8.67/1.94 % (1962284)Time elapsed: 0.091 s % 8.67/1.94 % (1962284)Peak memory usage: 16 MB % 8.67/1.94 % (1962284)Instructions burned: 159 (million) % 8.67/1.94 % (1962294)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=2600580904:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.67/1.94 % TRYING [3] % 8.67/1.94 % (1962297)ott-21_1_sil=16000:fs=off:random_seed=2676952681:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.67/1.94 % (1962293)Instruction limit reached! % 8.67/1.94 % (1962293)------------------------------ % 8.67/1.94 % (1962293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.67/1.94 % (1962293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.72/5.69 % (1962293)CaDiCaL version: 2.1.3 % 36.72/5.69 % (1962293)Termination reason: Instruction limit % 36.72/5.69 % (1962293)Termination phase: Saturation % 36.72/5.69 % (1962293)Time elapsed: 0.080 s % 36.72/5.69 % (1962293)Peak memory usage: 13 MB % 36.72/5.69 % (1962293)Instructions burned: 132 (million) % 36.72/5.69 % (1962300)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3781224726:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 36.72/5.69 % (1962297)Instruction limit reached! % 36.72/5.69 % (1962297)------------------------------ % 36.72/5.69 % (1962297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.72/5.69 % (1962297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.72/5.69 % (1962297)CaDiCaL version: 2.1.3 % 36.72/5.69 % (1962297)Termination reason: Instruction limit % 36.72/5.69 % (1962297)Termination phase: Saturation % 36.72/5.69 % (1962297)Time elapsed: 0.094 s % 36.72/5.69 % (1962297)Peak memory usage: 13 MB % 36.72/5.69 % (1962297)Instructions burned: 182 (million) % 36.72/5.69 % (1962302)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2702649575:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 36.72/5.69 % TRYING [1] % 36.72/5.69 % TRYING [2] % 36.72/5.69 % TRYING [3] % 36.72/5.69 % TRYING [4] % 36.72/5.69 % (1962292)Instruction limit reached! % 36.72/5.69 % (1962292)------------------------------ % 36.72/5.69 % (1962292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.72/5.69 % (1962292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.72/5.69 % (1962292)CaDiCaL version: 2.1.3 % 36.72/5.69 % (1962292)Termination reason: Instruction limit % 36.72/5.69 % (1962292)Termination phase: Finite model building constraint generation % 36.72/5.69 % (1962292)Time elapsed: 0.285 s % 36.72/5.69 % (1962292)Peak memory usage: 25 MB % 36.72/5.69 % (1962292)Instructions burned: 717 (million) % 36.72/5.69 % TRYING [1] % 36.72/5.69 % TRYING [2] % 36.72/5.69 % (1962304)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2594670599:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 36.72/5.69 % (1962294)Instruction limit reached! % 36.72/5.69 % (1962294)------------------------------ % 36.72/5.69 % (1962294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.72/5.69 % (1962294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.72/5.69 % (1962294)CaDiCaL version: 2.1.3 % 36.72/5.69 % (1962294)Termination reason: Instruction limit % 36.72/5.69 % (1962294)Termination phase: Saturation % 36.72/5.69 % (1962294)Time elapsed: 0.392 s % 36.72/5.69 % (1962294)Peak memory usage: 19 MB % 36.72/5.69 % (1962294)Instructions burned: 684 (million) % 36.72/5.69 % (1962306)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2034174845:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 36.72/5.69 % (1962300)Instruction limit reached! % 36.72/5.69 % (1962300)------------------------------ % 36.72/5.69 % (1962300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.72/5.69 % (1962300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.72/5.69 % (1962300)CaDiCaL version: 2.1.3 % 36.72/5.69 % (1962300)Termination reason: Instruction limit % 36.72/5.69 % (1962300)Termination phase: Saturation % 36.72/5.69 % (1962300)Time elapsed: 0.332 s % 36.72/5.69 % (1962300)Peak memory usage: 15 MB % 36.72/5.69 % (1962300)Instructions burned: 478 (million) % 36.72/5.69 % (1962308)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=3297959217: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) % 36.72/5.69 % TRYING [3] % 36.72/5.69 % (1962302)Instruction limit reached! % 36.72/5.69 % (1962302)------------------------------ % 36.72/5.69 % (1962302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 36.72/5.69 % (1962302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.72/5.69 % (1962302)CaDiCaL version: 2.1.3 % 36.72/5.69 % (1962302)Termination reason: Instruction limit % 36.72/5.69 % (1962302)Termination phase: Finite model building constraint generation % 36.72/5.69 % (1962302)Time elapsed: 0.393 s % 36.72/5.69 % (1962302)Peak memory usage: 27 MB % 36.72/5.69 % (1962302)Instructions burned: 868 (million) % 36.72/5.69 % (1962310)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1923178130:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 36.72/5.69 % (1962306)Cannot represent all propositional literals internally % 36.72/5.69 % (1962306)Refutation not found, incomplete strategy % 88.49/12.90 % (1962306)------------------------------ % 88.49/12.90 % (1962306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.90 % (1962306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.90 % (1962306)CaDiCaL version: 2.1.3 % 88.49/12.90 % (1962306)Termination reason: Refutation not found, incomplete strategy % 88.49/12.90 % (1962306)Time elapsed: 0.144 s % 88.49/12.90 % (1962306)Peak memory usage: 13 MB % 88.49/12.90 % (1962306)Instructions burned: 296 (million) % 88.49/12.90 % (1962306)------------------------------ % 88.49/12.90 % (1962306)------------------------------ % 88.49/12.90 % (1962312)fmb+10_1_sil=64000:random_seed=203836943:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 88.49/12.90 % TRYING [1] % 88.49/12.90 % TRYING [2] % 88.49/12.90 % (1962308)Instruction limit reached! % 88.49/12.90 % (1962308)------------------------------ % 88.49/12.90 % (1962308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.90 % (1962308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.90 % (1962308)CaDiCaL version: 2.1.3 % 88.49/12.90 % (1962308)Termination reason: Instruction limit % 88.49/12.90 % (1962308)Termination phase: Saturation % 88.49/12.90 % (1962308)Time elapsed: 0.392 s % 88.49/12.90 % (1962308)Peak memory usage: 25 MB % 88.49/12.90 % (1962308)Instructions burned: 693 (million) % 88.49/12.90 % (1962314)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3790379971:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 88.49/12.90 % TRYING [3] % 88.49/12.90 % (1962304)Instruction limit reached! % 88.49/12.90 % (1962304)------------------------------ % 88.49/12.90 % (1962304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.90 % (1962304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.90 % (1962304)CaDiCaL version: 2.1.3 % 88.49/12.90 % (1962304)Termination reason: Instruction limit % 88.49/12.90 % (1962304)Termination phase: Saturation % 88.49/12.90 % (1962304)Time elapsed: 0.691 s % 88.49/12.90 % (1962304)Peak memory usage: 27 MB % 88.49/12.90 % (1962304)Instructions burned: 1180 (million) % 88.49/12.90 % (1962314)Cannot represent all propositional literals internally % 88.49/12.90 % (1962314)Refutation not found, incomplete strategy % 88.49/12.90 % (1962314)------------------------------ % 88.49/12.90 % (1962314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.90 % (1962314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.90 % (1962314)CaDiCaL version: 2.1.3 % 88.49/12.90 % (1962314)Termination reason: Refutation not found, incomplete strategy % 88.49/12.90 % (1962314)Time elapsed: 0.146 s % 88.49/12.90 % (1962314)Peak memory usage: 13 MB % 88.49/12.90 % (1962314)Instructions burned: 299 (million) % 88.49/12.90 % (1962316)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2145010101:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 88.49/12.90 % (1962314)------------------------------ % 88.49/12.90 % (1962314)------------------------------ % 88.49/12.90 % (1962310)Instruction limit reached! % 88.49/12.90 % (1962310)------------------------------ % 88.49/12.90 % (1962310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.90 % (1962310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.90 % (1962310)CaDiCaL version: 2.1.3 % 88.49/12.90 % (1962310)Termination reason: Instruction limit % 88.49/12.90 % (1962310)Termination phase: Saturation % 88.49/12.91 % (1962310)Time elapsed: 0.462 s % 88.49/12.91 % (1962310)Peak memory usage: 20 MB % 88.49/12.91 % (1962310)Instructions burned: 881 (million) % 88.49/12.91 % (1962318)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=988786213:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 88.49/12.91 % (1962319)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3735169233:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 88.49/12.91 % TRYING [8] % 88.49/12.91 % (1962316)Instruction limit reached! % 88.49/12.91 % (1962316)------------------------------ % 88.49/12.91 % (1962316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.49/12.91 % (1962316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.49/12.91 % (1962316)CaDiCaL version: 2.1.3 % 88.49/12.91 % (1962316)Termination reason: Instruction limit % 88.49/12.91 % (1962316)Termination phase: Finite model building constraint generation % 88.49/12.91 % (1962316)Time elapsed: 0.354 s % 88.49/12.91 % (1962316)Peak memory usage: 56 MB % 88.49/12.91 % (1962316)Instructions burned: 922 (million) % 88.49/12.91 % (1962322)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3690917694:i=6324_2985 on theBenchmark for (2985ds/6324Mi) % 180.00/25.87 % (1962322)Cannot represent all propositional literals internally % 180.00/25.87 % (1962322)Refutation not found, incomplete strategy % 180.00/25.87 % (1962322)------------------------------ % 180.00/25.87 % (1962322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.00/25.87 % (1962322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.00/25.87 % (1962322)CaDiCaL version: 2.1.3 % 180.00/25.87 % (1962322)Termination reason: Refutation not found, incomplete strategy % 180.00/25.87 % (1962322)Time elapsed: 0.148 s % 180.00/25.87 % (1962322)Peak memory usage: 13 MB % 180.00/25.87 % (1962322)Instructions burned: 303 (million) % 180.00/25.87 % (1962322)------------------------------ % 180.00/25.87 % (1962322)------------------------------ % 180.00/25.87 % (1962324)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=216620882:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi) % 180.00/25.87 % (1962319)Instruction limit reached! % 180.00/25.87 % (1962319)------------------------------ % 180.00/25.87 % (1962319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.00/25.87 % (1962319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.00/25.87 % (1962319)CaDiCaL version: 2.1.3 % 180.00/25.87 % (1962319)Termination reason: Instruction limit % 180.00/25.87 % (1962319)Termination phase: Saturation % 180.00/25.87 % (1962319)Time elapsed: 0.653 s % 180.00/25.87 % (1962319)Peak memory usage: 24 MB % 180.00/25.87 % (1962319)Instructions burned: 1474 (million) % 180.00/25.87 % (1962326)ott-2_1_sil=16000:newcnf=on:random_seed=868441203:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi) % 180.00/25.87 % (1962326)Instruction limit reached! % 180.00/25.87 % (1962326)------------------------------ % 180.00/25.87 % (1962326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.00/25.87 % (1962326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.00/25.87 % (1962326)CaDiCaL version: 2.1.3 % 180.00/25.87 % (1962326)Termination reason: Instruction limit % 180.00/25.87 % (1962326)Termination phase: Saturation % 180.00/25.87 % (1962326)Time elapsed: 0.515 s % 180.00/25.87 % (1962326)Peak memory usage: 23 MB % 180.00/25.87 % (1962326)Instructions burned: 870 (million) % 180.00/25.87 % (1962328)ott+10_1_sil=32000:tgt=ground:random_seed=3295626599:i=5114:av=off_2976 on theBenchmark for (2976ds/5114Mi) % 180.00/25.87 % (1962324)Cannot represent all propositional literals internally % 180.00/25.87 % (1962324)Refutation not found, incomplete strategy % 180.00/25.87 % (1962324)------------------------------ % 180.00/25.87 % (1962324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.00/25.87 % (1962324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.00/25.87 % (1962324)CaDiCaL version: 2.1.3 % 180.00/25.87 % (1962324)Termination reason: Refutation not found, incomplete strategy % 180.00/25.87 % (1962324)Time elapsed: 0.831 s % 180.00/25.87 % (1962324)Peak memory usage: 19 MB % 180.00/25.87 % (1962324)Instructions burned: 1625 (million) % 180.00/25.87 % (1962324)------------------------------ % 180.00/25.87 % (1962324)------------------------------ % 180.00/25.87 % (1962331)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1482474380:i=54282_2974 on theBenchmark for (2974ds/54282Mi) % 180.00/25.87 % TRYING [4] % 180.00/25.87 % TRYING [5] % 180.00/25.87 % TRYING [1] % 180.00/25.87 % TRYING [2] % 180.00/25.87 % TRYING [3] % 180.00/25.87 % TRYING [4] % 180.00/25.87 % (1962318)Instruction limit reached! % 180.00/25.87 % (1962318)------------------------------ % 180.00/25.87 % (1962318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.00/25.87 % (1962318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.00/25.87 % (1962318)CaDiCaL version: 2.1.3 % 180.00/25.87 % (1962318)Termination reason: Instruction limit % 180.00/25.87 % (1962318)Termination phase: Saturation % 180.00/25.87 % (1962318)Time elapsed: 2.861 s % 180.00/25.87 % (1962318)Peak memory usage: 43 MB % 180.00/25.87 % (1962318)Instructions burned: 5131 (million) % 180.00/25.87 % (1962333)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1011498281:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi) % 180.00/25.87 % (1962328)Instruction limit reached! % 180.00/25.87 % (1962328)------------------------------ % 180.00/25.87 % (1962328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 180.00/25.87 % (1962328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.00/25.87 % (1962328)CaDiCaL version: 2.1.3 % 180.00/25.87 % (1962328)Termination reason: Instruction limit % 265.13/37.84 % (1962328)Termination phase: Saturation % 265.13/37.84 % (1962328)Time elapsed: 2.891 s % 265.13/37.84 % (1962328)Peak memory usage: 69 MB % 265.13/37.84 % (1962328)Instructions burned: 5114 (million) % 265.13/37.84 % (1962335)dis+21_1_sil=32000:sas=cadical:random_seed=4237027196:i=3773:amm=off_2947 on theBenchmark for (2947ds/3773Mi) % 265.13/37.84 % (1962333)Instruction limit reached! % 265.13/37.84 % (1962333)------------------------------ % 265.13/37.84 % (1962333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.13/37.84 % (1962333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.13/37.84 % (1962333)CaDiCaL version: 2.1.3 % 265.13/37.84 % (1962333)Termination reason: Instruction limit % 265.13/37.84 % (1962333)Termination phase: Saturation % 265.13/37.84 % (1962333)Time elapsed: 1.953 s % 265.13/37.84 % (1962333)Peak memory usage: 34 MB % 265.13/37.84 % (1962333)Instructions burned: 3512 (million) % 265.13/37.84 % (1962337)ott+11_1_sil=16000:gs=on:random_seed=3314307143:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2939 on theBenchmark for (2939ds/2251Mi) % 265.13/37.84 % TRYING [5] % 265.13/37.84 % (1962335)Instruction limit reached! % 265.13/37.84 % (1962335)------------------------------ % 265.13/37.84 % (1962335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.13/37.84 % (1962335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.13/37.84 % (1962335)CaDiCaL version: 2.1.3 % 265.13/37.84 % (1962335)Termination reason: Instruction limit % 265.13/37.84 % (1962335)Termination phase: Saturation % 265.13/37.84 % (1962335)Time elapsed: 2.164 s % 265.13/37.84 % (1962335)Peak memory usage: 46 MB % 265.13/37.84 % (1962335)Instructions burned: 3774 (million) % 265.13/37.84 % (1962337)Instruction limit reached! % 265.13/37.84 % (1962337)------------------------------ % 265.13/37.84 % (1962337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.13/37.84 % (1962337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.13/37.84 % (1962337)CaDiCaL version: 2.1.3 % 265.13/37.84 % (1962337)Termination reason: Instruction limit % 265.13/37.84 % (1962337)Termination phase: Saturation % 265.13/37.84 % (1962337)Time elapsed: 1.449 s % 265.13/37.84 % (1962337)Peak memory usage: 48 MB % 265.13/37.84 % (1962337)Instructions burned: 2252 (million) % 265.13/37.84 % (1962339)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3656116117:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi) % 265.13/37.84 % (1962340)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=244143456:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi) % 265.13/37.84 % (1962340)Instruction limit reached! % 265.13/37.84 % (1962340)------------------------------ % 265.13/37.84 % (1962340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.13/37.84 % (1962340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.13/37.84 % (1962340)CaDiCaL version: 2.1.3 % 265.13/37.84 % (1962340)Termination reason: Instruction limit % 265.13/37.84 % (1962340)Termination phase: Saturation % 265.13/37.84 % (1962340)Time elapsed: 1.797 s % 265.13/37.84 % (1962340)Peak memory usage: 28 MB % 265.13/37.84 % (1962340)Instructions burned: 4591 (million) % 265.13/37.84 % (1962343)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2745645282:i=29340_2907 on theBenchmark for (2907ds/29340Mi) % 265.13/37.84 % (1962312)Instruction limit reached! % 265.13/37.84 % (1962312)------------------------------ % 265.13/37.84 % (1962312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.13/37.84 % (1962312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.13/37.84 % (1962312)CaDiCaL version: 2.1.3 % 265.13/37.84 % (1962312)Termination reason: Instruction limit % 265.13/37.84 % (1962312)Termination phase: Finite model building SAT solving % 265.13/37.84 % (1962312)Time elapsed: 9.116 s % 265.13/37.84 % (1962312)Peak memory usage: 471 MB % 265.13/37.84 % (1962312)Instructions burned: 22062 (million) % 265.13/37.84 % (1962345)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2439173851:i=5211_2901 on theBenchmark for (2901ds/5211Mi) % 265.13/37.84 % TRYING [7] % 265.13/37.84 % (1962345)Instruction limit reached! % 265.13/37.84 % (1962345)------------------------------ % 265.13/37.84 % (1962345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.13/37.84 % (1962345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.13/37.84 % (1962345)CaDiCaL version: 2.1.3 % 265.13/37.84 % (1962345)Termination reason: Instruction limit % 300.63/42.83 % (1962345)Termination phase: Saturation % 300.63/42.83 % (1962345)Time elapsed: 2.573 s % 300.63/42.83 % (1962345)Peak memory usage: 51 MB % 300.63/42.83 % (1962345)Instructions burned: 5213 (million) % 300.63/42.83 % (1962347)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2840767001:i=5497:nm=2_2875 on theBenchmark for (2875ds/5497Mi) % 300.63/42.83 % (1962347)Cannot represent all propositional literals internally % 300.63/42.83 % (1962347)Refutation not found, incomplete strategy % 300.63/42.83 % (1962347)------------------------------ % 300.63/42.83 % (1962347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (1962347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (1962347)CaDiCaL version: 2.1.3 % 300.63/42.83 % (1962347)Termination reason: Refutation not found, incomplete strategy % 300.63/42.83 % (1962347)Time elapsed: 0.149 s % 300.63/42.83 % (1962347)Peak memory usage: 13 MB % 300.63/42.83 % (1962347)Instructions burned: 303 (million) % 300.63/42.83 % (1962347)------------------------------ % 300.63/42.83 % (1962347)------------------------------ % 300.63/42.83 % (1962350)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2261816681:fmbsr=2:i=46332_2873 on theBenchmark for (2873ds/46332Mi) % 300.63/42.83 % (1962350)Cannot represent all propositional literals internally % 300.63/42.83 % (1962350)Refutation not found, incomplete strategy % 300.63/42.83 % (1962350)------------------------------ % 300.63/42.83 % (1962350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (1962350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (1962350)CaDiCaL version: 2.1.3 % 300.63/42.83 % (1962350)Termination reason: Refutation not found, incomplete strategy % 300.63/42.83 % (1962350)Time elapsed: 0.146 s % 300.63/42.83 % (1962350)Peak memory usage: 13 MB % 300.63/42.83 % (1962350)Instructions burned: 299 (million) % 300.63/42.83 % (1962350)------------------------------ % 300.63/42.83 % (1962350)------------------------------ % 300.63/42.83 % (1962370)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2865669210:i=14071_2871 on theBenchmark for (2871ds/14071Mi) % 300.63/42.83 % TRYING [12] % 300.63/42.83 % (1962370)Instruction limit reached! % 300.63/42.83 % (1962370)------------------------------ % 300.63/42.83 % (1962370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (1962370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (1962370)CaDiCaL version: 2.1.3 % 300.63/42.83 % (1962370)Termination reason: Instruction limit % 300.63/42.83 % (1962370)Termination phase: Finite model building constraint generation % 300.63/42.83 % (1962370)Time elapsed: 4.863 s % 300.63/42.83 % (1962370)Peak memory usage: 876 MB % 300.63/42.83 % (1962370)Instructions burned: 14073 (million) % 300.63/42.83 % (1962744)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1380378226:i=22565:add=on:rawr=on_2821 on theBenchmark for (2821ds/22565Mi) % 300.63/42.83 % TRYING [6] % 300.63/42.83 % (1962331)Instruction limit reached! % 300.63/42.83 % (1962331)------------------------------ % 300.63/42.83 % (1962331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (1962331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (1962331)CaDiCaL version: 2.1.3 % 300.63/42.83 % (1962331)Termination reason: Instruction limit % 300.63/42.83 % (1962331)Termination phase: Finite model building constraint generation % 300.63/42.83 % (1962331)Time elapsed: 17.954 s % 300.63/42.83 % (1962331)Peak memory usage: 1577 MB % 300.63/42.83 % (1962331)Instructions burned: 54284 (million) % 300.63/42.83 % (1962746)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2511165416:i=8173:av=off_2792 on theBenchmark for (2792ds/8173Mi) % 300.63/42.83 % (1962343)Instruction limit reached! % 300.63/42.83 % (1962343)------------------------------ % 300.63/42.83 % (1962343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (1962343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (1962343)CaDiCaL version: 2.1.3 % 300.63/42.83 % (1962343)Termination reason: Instruction limit % 300.63/42.83 % (1962343)Termination phase: Saturation % 300.63/42.83 % (1962343)Time elapsed: 13.832 s % 300.63/42.83 % (1962343)Peak memory usage: 416 MB % 300.63/42.83 % (1962343)Instructions burned: 29340 (million) % 300.63/42.83 % (1962748)dis+10_16:1_sil=16000:random_seed=719492015:i=9155:fsr=off_2767 on theBenchmark for (2767ds/9155Mi) % 300.63/42.83 % (1962746)Instruction limit reached! % 300.63/42.83 % (1962746)------------------------------ % 300.63/42.83 % (1962746)Ver % 300.63/42.84 Terminated % 300.63/42.84 % Vampire exiting %------------------------------------------------------------------------------