%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV852-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 : n016.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:32 PM UTC 2026 % Result : Timeout 300.34s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV852-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.06/0.20 % Computer : n016.cluster.edu % 0.06/0.20 % Model : x86_64 x86_64 % 0.06/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.20 % Memory : 8046.5625MB % 0.06/0.20 % OS : Linux 6.8.0-71-generic % 0.06/0.20 % CPULimit : 300 % 0.06/0.20 % WCLimit : 300 % 0.06/0.20 % DateTime : Mon Sep 28 12:48:54 UTC 2026 % 0.06/0.20 % CPUTime : % 0.06/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.23 Running first-order model finding % 0.06/0.23 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 % 9.25/1.87 % (3596557)Will run a generic schedule for satisfiability detection. % 9.25/1.87 % (3596563)% WARNING: option uhcvi not known. % 9.25/1.87 % (3596562)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2911694487_2999 on theBenchmark for (2999ds/0Mi) % 9.25/1.87 % (3596564)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=515481127:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.25/1.87 % (3596565)dis+10_1_sil=32000:sp=arity:random_seed=2865526894:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.25/1.87 % (3596566)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=810287627:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.25/1.87 % (3596563)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1998750547:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.25/1.87 % (3596567)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3181464197:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.25/1.87 % (3596568)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2548803334:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.25/1.87 % (3596565)Instruction limit reached! % 9.25/1.87 % (3596565)------------------------------ % 9.25/1.87 % (3596565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.25/1.87 % (3596565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.25/1.87 % (3596565)CaDiCaL version: 2.1.3 % 9.25/1.87 % (3596565)Termination reason: Instruction limit % 9.25/1.87 % (3596565)Termination phase: Saturation % 9.25/1.87 % (3596565)Time elapsed: 0.061 s % 9.25/1.87 % (3596565)Peak memory usage: 12 MB % 9.25/1.87 % (3596565)Instructions burned: 105 (million) % 9.25/1.87 % (3596566)Instruction limit reached! % 9.25/1.87 % (3596566)------------------------------ % 9.25/1.87 % (3596566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.25/1.87 % (3596566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.25/1.87 % (3596566)CaDiCaL version: 2.1.3 % 9.25/1.87 % (3596566)Termination reason: Instruction limit % 9.25/1.87 % (3596566)Termination phase: Saturation % 9.25/1.87 % (3596566)Time elapsed: 0.071 s % 9.25/1.87 % (3596566)Peak memory usage: 13 MB % 9.25/1.87 % (3596566)Instructions burned: 117 (million) % 9.25/1.87 % (3596576)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2000426254:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 9.25/1.87 % (3596567)Instruction limit reached! % 9.25/1.87 % (3596567)------------------------------ % 9.25/1.87 % (3596567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.25/1.87 % (3596567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.25/1.87 % (3596567)CaDiCaL version: 2.1.3 % 9.25/1.87 % (3596567)Termination reason: Instruction limit % 9.25/1.87 % (3596567)Termination phase: Saturation % 9.25/1.87 % (3596567)Time elapsed: 0.086 s % 9.25/1.87 % (3596567)Peak memory usage: 13 MB % 9.25/1.87 % (3596567)Instructions burned: 132 (million) % 9.25/1.87 % (3596568)Instruction limit reached! % 9.25/1.87 % (3596568)------------------------------ % 9.25/1.87 % (3596568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.25/1.87 % (3596568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.25/1.87 % (3596568)CaDiCaL version: 2.1.3 % 9.25/1.87 % (3596568)Termination reason: Instruction limit % 9.25/1.87 % (3596568)Termination phase: Saturation % 9.25/1.87 % (3596568)Time elapsed: 0.088 s % 9.25/1.87 % (3596568)Peak memory usage: 13 MB % 9.25/1.87 % (3596568)Instructions burned: 160 (million) % 9.25/1.87 % (3596577)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3012734948:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.25/1.87 % (3596579)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=682702592:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.25/1.87 % (3596580)ott-21_1_sil=16000:fs=off:random_seed=2272122633:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.25/1.87 % (3596577)Instruction limit reached! % 9.25/1.87 % (3596577)------------------------------ % 9.25/1.87 % (3596577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.25/1.87 % (3596577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.25/1.87 % (3596577)CaDiCaL version: 2.1.3 % 41.00/6.06 % (3596577)Termination reason: Instruction limit % 41.00/6.06 % (3596577)Termination phase: Saturation % 41.00/6.06 % (3596577)Time elapsed: 0.082 s % 41.00/6.06 % (3596577)Peak memory usage: 13 MB % 41.00/6.06 % (3596577)Instructions burned: 131 (million) % 41.00/6.06 % (3596584)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=61210333:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 41.00/6.06 % (3596580)Instruction limit reached! % 41.00/6.06 % (3596580)------------------------------ % 41.00/6.06 % (3596580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.00/6.06 % (3596580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.00/6.06 % (3596580)CaDiCaL version: 2.1.3 % 41.00/6.06 % (3596580)Termination reason: Instruction limit % 41.00/6.06 % (3596580)Termination phase: Saturation % 41.00/6.06 % (3596580)Time elapsed: 0.100 s % 41.00/6.06 % (3596580)Peak memory usage: 12 MB % 41.00/6.06 % (3596580)Instructions burned: 180 (million) % 41.00/6.06 % (3596586)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3956878303:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 41.00/6.06 % TRYING [1] % 41.00/6.06 % TRYING [2] % 41.00/6.06 % TRYING [1] % 41.00/6.06 % TRYING [2] % 41.00/6.06 % TRYING [3] % 41.00/6.06 % (3596576)Instruction limit reached! % 41.00/6.06 % (3596576)------------------------------ % 41.00/6.06 % (3596576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.00/6.06 % (3596576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.00/6.06 % (3596576)CaDiCaL version: 2.1.3 % 41.00/6.06 % (3596576)Termination reason: Instruction limit % 41.00/6.06 % (3596576)Termination phase: Finite model building constraint generation % 41.00/6.06 % (3596576)Time elapsed: 0.340 s % 41.00/6.06 % (3596576)Peak memory usage: 32 MB % 41.00/6.06 % (3596576)Instructions burned: 714 (million) % 41.00/6.06 % (3596588)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1910215514:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 41.00/6.06 % TRYING [1] % 41.00/6.06 % (3596584)Instruction limit reached! % 41.00/6.06 % (3596584)------------------------------ % 41.00/6.06 % (3596584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.00/6.06 % (3596584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.00/6.06 % (3596584)CaDiCaL version: 2.1.3 % 41.00/6.06 % (3596584)Termination reason: Instruction limit % 41.00/6.06 % (3596584)Termination phase: Saturation % 41.00/6.06 % (3596584)Time elapsed: 0.304 s % 41.00/6.06 % (3596584)Peak memory usage: 15 MB % 41.00/6.06 % (3596584)Instructions burned: 477 (million) % 41.00/6.06 % (3596579)Instruction limit reached! % 41.00/6.06 % (3596579)------------------------------ % 41.00/6.06 % (3596579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.00/6.06 % (3596579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.00/6.06 % (3596579)CaDiCaL version: 2.1.3 % 41.00/6.06 % (3596579)Termination reason: Instruction limit % 41.00/6.06 % (3596579)Termination phase: Saturation % 41.00/6.06 % (3596579)Time elapsed: 0.408 s % 41.00/6.06 % (3596579)Peak memory usage: 19 MB % 41.00/6.06 % (3596579)Instructions burned: 685 (million) % 41.00/6.06 % TRYING [2] % 41.00/6.06 % (3596590)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=294219112:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 41.00/6.06 % (3596591)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=520748554: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) % 41.00/6.06 % (3596586)Instruction limit reached! % 41.00/6.06 % (3596586)------------------------------ % 41.00/6.06 % (3596586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.00/6.06 % (3596586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.00/6.06 % (3596586)CaDiCaL version: 2.1.3 % 41.00/6.06 % (3596586)Termination reason: Instruction limit % 41.00/6.06 % (3596586)Termination phase: Finite model building SAT solving % 41.00/6.06 % (3596586)Time elapsed: 0.412 s % 41.00/6.06 % (3596586)Peak memory usage: 34 MB % 41.00/6.06 % (3596586)Instructions burned: 866 (million) % 41.00/6.06 % (3596594)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3760771732:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 41.00/6.06 % (3596590)Cannot represent all propositional literals internally % 41.00/6.06 % (3596590)Refutation not found, incomplete strategy % 41.00/6.06 % (3596590)------------------------------ % 91.36/13.13 % (3596590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.36/13.13 % (3596590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.36/13.13 % (3596590)CaDiCaL version: 2.1.3 % 91.36/13.13 % (3596590)Termination reason: Refutation not found, incomplete strategy % 91.36/13.13 % (3596590)Time elapsed: 0.254 s % 91.36/13.13 % (3596590)Peak memory usage: 17 MB % 91.36/13.13 % (3596590)Instructions burned: 505 (million) % 91.36/13.13 % (3596590)------------------------------ % 91.36/13.13 % (3596590)------------------------------ % 91.36/13.13 % (3596596)fmb+10_1_sil=64000:random_seed=3574998613:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi) % 91.36/13.13 % (3596591)Instruction limit reached! % 91.36/13.13 % (3596591)------------------------------ % 91.36/13.13 % (3596591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.36/13.13 % (3596591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.36/13.13 % (3596591)CaDiCaL version: 2.1.3 % 91.36/13.13 % (3596591)Termination reason: Instruction limit % 91.36/13.13 % (3596591)Termination phase: Saturation % 91.36/13.13 % (3596591)Time elapsed: 0.423 s % 91.36/13.13 % (3596591)Peak memory usage: 19 MB % 91.36/13.13 % (3596591)Instructions burned: 693 (million) % 91.36/13.13 % (3596598)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=860345088:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 91.36/13.13 % TRYING [1] % 91.36/13.13 % TRYING [2] % 91.36/13.13 % (3596594)Instruction limit reached! % 91.36/13.13 % (3596594)------------------------------ % 91.36/13.13 % (3596594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.36/13.13 % (3596594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.36/13.13 % (3596594)CaDiCaL version: 2.1.3 % 91.36/13.13 % (3596594)Termination reason: Instruction limit % 91.36/13.13 % (3596594)Termination phase: Saturation % 91.36/13.13 % (3596594)Time elapsed: 0.475 s % 91.36/13.13 % (3596594)Peak memory usage: 19 MB % 91.36/13.13 % (3596594)Instructions burned: 881 (million) % 91.36/13.13 % (3596600)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=325955146:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 91.36/13.13 % (3596588)Instruction limit reached! % 91.36/13.13 % (3596588)------------------------------ % 91.36/13.13 % (3596588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.36/13.13 % (3596588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.36/13.13 % (3596588)CaDiCaL version: 2.1.3 % 91.36/13.13 % (3596588)Termination reason: Instruction limit % 91.36/13.13 % (3596588)Termination phase: Saturation % 91.36/13.13 % (3596588)Time elapsed: 0.722 s % 91.36/13.13 % (3596588)Peak memory usage: 25 MB % 91.36/13.13 % (3596588)Instructions burned: 1180 (million) % 91.36/13.13 % (3596602)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4006089575:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 91.36/13.13 % (3596598)Cannot represent all propositional literals internally % 91.36/13.13 % (3596598)Refutation not found, incomplete strategy % 91.36/13.13 % (3596598)------------------------------ % 91.36/13.13 % (3596598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.36/13.13 % (3596598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.36/13.13 % (3596598)CaDiCaL version: 2.1.3 % 91.36/13.13 % (3596598)Termination reason: Refutation not found, incomplete strategy % 91.36/13.13 % (3596598)Time elapsed: 0.253 s % 91.36/13.13 % (3596598)Peak memory usage: 17 MB % 91.36/13.13 % (3596598)Instructions burned: 496 (million) % 91.36/13.13 % (3596598)------------------------------ % 91.36/13.13 % (3596598)------------------------------ % 91.36/13.13 % (3596604)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2802393598:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi) % 91.36/13.13 % TRYING [8] % 91.36/13.13 % (3596600)Instruction limit reached! % 91.36/13.13 % (3596600)------------------------------ % 91.36/13.13 % (3596600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 91.36/13.13 % (3596600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.36/13.13 % (3596600)CaDiCaL version: 2.1.3 % 91.36/13.13 % (3596600)Termination reason: Instruction limit % 91.36/13.13 % (3596600)Termination phase: Finite model building constraint generation % 91.36/13.13 % (3596600)Time elapsed: 0.401 s % 91.36/13.13 % (3596600)Peak memory usage: 46 MB % 91.36/13.13 % (3596600)Instructions burned: 921 (million) % 91.36/13.13 % (3596606)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=74624153:i=6324_2983 on theBenchmark for (2983ds/6324Mi) % 194.67/27.79 % TRYING [3] % 194.67/27.79 % TRYING [4] % 194.67/27.79 % (3596606)Cannot represent all propositional literals internally % 194.67/27.79 % (3596606)Refutation not found, incomplete strategy % 194.67/27.79 % (3596606)------------------------------ % 194.67/27.79 % (3596606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.79 % (3596606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.79 % (3596606)CaDiCaL version: 2.1.3 % 194.67/27.79 % (3596606)Termination reason: Refutation not found, incomplete strategy % 194.67/27.79 % (3596606)Time elapsed: 0.261 s % 194.67/27.79 % (3596606)Peak memory usage: 17 MB % 194.67/27.79 % (3596606)Instructions burned: 512 (million) % 194.67/27.79 % (3596606)------------------------------ % 194.67/27.79 % (3596606)------------------------------ % 194.67/27.79 % (3596608)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3801347036:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi) % 194.67/27.79 % (3596604)Instruction limit reached! % 194.67/27.79 % (3596604)------------------------------ % 194.67/27.79 % (3596604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.79 % (3596604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.79 % (3596604)CaDiCaL version: 2.1.3 % 194.67/27.79 % (3596604)Termination reason: Instruction limit % 194.67/27.79 % (3596604)Termination phase: Saturation % 194.67/27.79 % (3596604)Time elapsed: 0.835 s % 194.67/27.79 % (3596604)Peak memory usage: 33 MB % 194.67/27.79 % (3596604)Instructions burned: 1473 (million) % 194.67/27.79 % (3596610)ott-2_1_sil=16000:newcnf=on:random_seed=1394336916:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi) % 194.67/27.79 % (3596610)Instruction limit reached! % 194.67/27.79 % (3596610)------------------------------ % 194.67/27.79 % (3596610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.79 % (3596610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.79 % (3596610)CaDiCaL version: 2.1.3 % 194.67/27.79 % (3596610)Termination reason: Instruction limit % 194.67/27.79 % (3596610)Termination phase: Saturation % 194.67/27.79 % (3596610)Time elapsed: 0.505 s % 194.67/27.79 % (3596610)Peak memory usage: 21 MB % 194.67/27.79 % (3596610)Instructions burned: 869 (million) % 194.67/27.79 % (3596612)ott+10_1_sil=32000:tgt=ground:random_seed=91587986:i=5114:av=off_2973 on theBenchmark for (2973ds/5114Mi) % 194.67/27.79 % (3596608)Instruction limit reached! % 194.67/27.79 % (3596608)------------------------------ % 194.67/27.79 % (3596608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.79 % (3596608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.79 % (3596608)CaDiCaL version: 2.1.3 % 194.67/27.79 % (3596608)Termination reason: Instruction limit % 194.67/27.79 % (3596608)Termination phase: Finite model building preprocessing % 194.67/27.79 % (3596608)Time elapsed: 1.103 s % 194.67/27.79 % (3596608)Peak memory usage: 29 MB % 194.67/27.79 % (3596608)Instructions burned: 2176 (million) % 194.67/27.79 % (3596614)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4163366861:i=54282_2969 on theBenchmark for (2969ds/54282Mi) % 194.67/27.79 % TRYING [1] % 194.67/27.79 % TRYING [2] % 194.67/27.79 % TRYING [3] % 194.67/27.79 % (3596602)Instruction limit reached! % 194.67/27.79 % (3596602)------------------------------ % 194.67/27.79 % (3596602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.79 % (3596602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.79 % (3596602)CaDiCaL version: 2.1.3 % 194.67/27.79 % (3596602)Termination reason: Instruction limit % 194.67/27.79 % (3596602)Termination phase: Saturation % 194.67/27.79 % (3596602)Time elapsed: 2.980 s % 194.67/27.79 % (3596602)Peak memory usage: 46 MB % 194.67/27.79 % (3596602)Instructions burned: 5131 (million) % 194.67/27.79 % (3596616)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3649776299:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi) % 194.67/27.79 % TRYING [4] % 194.67/27.79 % (3596612)Instruction limit reached! % 194.67/27.79 % (3596612)------------------------------ % 194.67/27.79 % (3596612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.67/27.79 % (3596612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.67/27.79 % (3596612)CaDiCaL version: 2.1.3 % 194.67/27.79 % (3596612)Termination reason: Instruction limit % 194.67/27.79 % (3596612)Termination phase: Saturation % 194.67/27.79 % (3596612)Time elapsed: 3.113 s % 194.67/27.79 % (3596612)Peak memory usage: 54 MB % 194.67/27.79 % (3596612)Instructions burned: 5114 (million) % 194.67/27.79 % (3596618)dis+21_1_sil=32000:sas=cadical:random_seed=633285718:i=3773:amm=off_2941 on theBenchmark for (2941ds/3773Mi) % 273.84/40.75 % TRYING [4] % 273.84/40.75 % (3596616)Instruction limit reached! % 273.84/40.75 % (3596616)------------------------------ % 273.84/40.75 % (3596616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.84/40.75 % (3596616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.84/40.75 % (3596616)CaDiCaL version: 2.1.3 % 273.84/40.75 % (3596616)Termination reason: Instruction limit % 273.84/40.75 % (3596616)Termination phase: Saturation % 273.84/40.75 % (3596616)Time elapsed: 2.112 s % 273.84/40.75 % (3596616)Peak memory usage: 36 MB % 273.84/40.75 % (3596616)Instructions burned: 3512 (million) % 273.84/40.75 % (3596620)ott+11_1_sil=16000:gs=on:random_seed=1502412037:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi) % 273.84/40.75 % (3596620)Instruction limit reached! % 273.84/40.75 % (3596620)------------------------------ % 273.84/40.75 % (3596620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.84/40.75 % (3596620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.84/40.75 % (3596620)CaDiCaL version: 2.1.3 % 273.84/40.75 % (3596620)Termination reason: Instruction limit % 273.84/40.75 % (3596620)Termination phase: Saturation % 273.84/40.75 % (3596620)Time elapsed: 1.332 s % 273.84/40.75 % (3596620)Peak memory usage: 29 MB % 273.84/40.75 % (3596620)Instructions burned: 2251 (million) % 273.84/40.75 % (3596622)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2079332526:fmbsr=1.6:i=67534_2922 on theBenchmark for (2922ds/67534Mi) % 273.84/40.75 % (3596618)Instruction limit reached! % 273.84/40.75 % (3596618)------------------------------ % 273.84/40.75 % (3596618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.84/40.75 % (3596618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.84/40.75 % (3596618)CaDiCaL version: 2.1.3 % 273.84/40.75 % (3596618)Termination reason: Instruction limit % 273.84/40.75 % (3596618)Termination phase: Saturation % 273.84/40.75 % (3596618)Time elapsed: 2.309 s % 273.84/40.75 % (3596618)Peak memory usage: 38 MB % 273.84/40.75 % (3596618)Instructions burned: 3774 (million) % 273.84/40.75 % (3596624)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2280073361:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2918 on theBenchmark for (2918ds/4591Mi) % 273.84/40.75 % (3596596)Instruction limit reached! % 273.84/40.75 % (3596596)------------------------------ % 273.84/40.75 % (3596596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.84/40.75 % (3596596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.84/40.75 % (3596596)CaDiCaL version: 2.1.3 % 273.84/40.75 % (3596596)Termination reason: Instruction limit % 273.84/40.75 % (3596596)Termination phase: Finite model building constraint generation % 273.84/40.75 % (3596596)Time elapsed: 9.101 s % 273.84/40.75 % (3596596)Peak memory usage: 705 MB % 273.84/40.75 % (3596596)Instructions burned: 22063 (million) % 273.84/40.75 % (3596624)Instruction limit reached! % 273.84/40.75 % (3596624)------------------------------ % 273.84/40.75 % (3596624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.84/40.75 % (3596624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.84/40.75 % (3596624)CaDiCaL version: 2.1.3 % 273.84/40.75 % (3596624)Termination reason: Instruction limit % 273.84/40.75 % (3596624)Termination phase: Saturation % 273.84/40.75 % (3596624)Time elapsed: 1.818 s % 273.84/40.75 % (3596624)Peak memory usage: 35 MB % 273.84/40.75 % (3596624)Instructions burned: 4592 (million) % 273.84/40.75 % (3596626)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=905125329:i=29340_2900 on theBenchmark for (2900ds/29340Mi) % 273.84/40.75 % (3596628)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2026156430:i=5211_2899 on theBenchmark for (2899ds/5211Mi) % 273.84/40.75 % (3596628)Instruction limit reached! % 273.84/40.75 % (3596628)------------------------------ % 273.84/40.75 % (3596628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 273.84/40.75 % (3596628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.84/40.75 % (3596628)CaDiCaL version: 2.1.3 % 273.84/40.75 % (3596628)Termination reason: Instruction limit % 273.84/40.75 % (3596628)Termination phase: Saturation % 273.84/40.75 % (3596628)Time elapsed: 2.821 s % 273.84/40.75 % (3596628)Peak memory usage: 51 MB % 273.84/40.75 % (3596628)Instructions burned: 5213 (million) % 273.84/40.75 % (3596630)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=493051930:i=5497:nm=2_2871 on theBenchmark for (2871ds/5497Mi) % 300.34/42.63 % TRYING [5] % 300.34/42.63 % (3596630)Cannot represent all propositional literals internally % 300.34/42.63 % (3596630)Refutation not found, incomplete strategy % 300.34/42.63 % (3596630)------------------------------ % 300.34/42.63 % (3596630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.34/42.63 % (3596630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.34/42.63 % (3596630)CaDiCaL version: 2.1.3 % 300.34/42.63 % (3596630)Termination reason: Refutation not found, incomplete strategy % 300.34/42.63 % (3596630)Time elapsed: 0.260 s % 300.34/42.63 % (3596630)Peak memory usage: 17 MB % 300.34/42.63 % (3596630)Instructions burned: 512 (million) % 300.34/42.63 % (3596630)------------------------------ % 300.34/42.63 % (3596630)------------------------------ % 300.34/42.63 % (3596632)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=165640993:fmbsr=2:i=46332_2868 on theBenchmark for (2868ds/46332Mi) % 300.34/42.63 % (3596632)Cannot represent all propositional literals internally % 300.34/42.63 % (3596632)Refutation not found, incomplete strategy % 300.34/42.63 % (3596632)------------------------------ % 300.34/42.63 % (3596632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.34/42.63 % (3596632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.34/42.63 % (3596632)CaDiCaL version: 2.1.3 % 300.34/42.63 % (3596632)Termination reason: Refutation not found, incomplete strategy % 300.34/42.63 % (3596632)Time elapsed: 0.256 s % 300.34/42.63 % (3596632)Peak memory usage: 16 MB % 300.34/42.63 % (3596632)Instructions burned: 514 (million) % 300.34/42.63 % (3596632)------------------------------ % 300.34/42.63 % (3596632)------------------------------ % 300.34/42.63 % (3596634)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3586889673:i=14071_2865 on theBenchmark for (2865ds/14071Mi) % 300.34/42.63 % (3596634)Cannot represent all propositional literals internally % 300.34/42.63 % (3596634)Refutation not found, incomplete strategy % 300.34/42.63 % (3596634)------------------------------ % 300.34/42.63 % (3596634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.34/42.63 % (3596634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.34/42.63 % (3596634)CaDiCaL version: 2.1.3 % 300.34/42.63 % (3596634)Termination reason: Refutation not found, incomplete strategy % 300.34/42.63 % (3596634)Time elapsed: 0.251 s % 300.34/42.63 % (3596634)Peak memory usage: 17 MB % 300.34/42.63 % (3596634)Instructions burned: 500 (million) % 300.34/42.63 % (3596634)------------------------------ % 300.34/42.63 % (3596634)------------------------------ % 300.34/42.63 % (3596636)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3663865393:i=22565:add=on:rawr=on_2862 on theBenchmark for (2862ds/22565Mi) % 300.34/42.63 % TRYING [5] % 300.34/42.63 % (3596614)Instruction limit reached! % 300.34/42.63 % (3596614)------------------------------ % 300.34/42.63 % (3596614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.34/42.63 % (3596614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.34/42.63 % (3596614)CaDiCaL version: 2.1.3 % 300.34/42.63 % (3596614)Termination reason: Instruction limit % 300.34/42.63 % (3596614)Termination phase: Finite model building constraint generation % 300.34/42.63 % (3596614)Time elapsed: 19.996 s % 300.34/42.63 % (3596614)Peak memory usage: 1536 MB % 300.34/42.63 % (3596614)Instructions burned: 54284 (million) % 300.34/42.63 % (3596626)Instruction limit reached! % 300.34/42.63 % (3596626)------------------------------ % 300.34/42.63 % (3596626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.34/42.63 % (3596626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.34/42.63 % (3596626)CaDiCaL version: 2.1.3 % 300.34/42.63 % (3596626)Termination reason: Instruction limit % 300.34/42.63 % (3596626)Termination phase: Saturation % 300.34/42.63 % (3596626)Time elapsed: 13.216 s % 300.34/42.63 % (3596626)Peak memory usage: 313 MB % 300.34/42.63 % (3596626)Instructions burned: 29342 (million) % 300.34/42.63 % (3596638)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2879053956:i=8173:av=off_2767 on theBenchmark for (2767ds/8173Mi) % 300.34/42.63 % (3596640)dis+10_16:1_sil=16000:random_seed=744490269:i=9155:fsr=off_2767 on theBenchmark for (2767ds/9155Mi) % 300.34/42.63 % TRYING [7] % 300.34/42.63 % (3596636)Instruction limit reached! % 300.34/42.63 % (3596636)------------------------------ % 300.34/42.63 % (3596636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:0 % 300.34/42.64 Terminated % 300.34/42.64 % Vampire exiting % 300.34/42.64 Terminated %------------------------------------------------------------------------------