%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV276-1 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n019.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:20:42 PM UTC 2026 % Result : Timeout 293.64s 41.87s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV276-1 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.17 % Computer : n019.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 10:22:49 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 Running first-order model finding % 0.09/0.19 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.02/1.76 % (3910642)Will run a generic schedule for satisfiability detection. % 9.02/1.76 % (3910648)% WARNING: option uhcvi not known. % 9.02/1.76 % (3910648)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2675064568:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.02/1.76 % (3910647)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2999968543_2999 on theBenchmark for (2999ds/0Mi) % 9.02/1.76 % (3910650)dis+10_1_sil=32000:sp=arity:random_seed=869395388:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.02/1.76 % (3910649)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=528536976:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.02/1.76 % (3910652)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2190570440:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.02/1.76 % (3910651)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=277177438:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.02/1.76 % (3910653)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3851277164:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.02/1.76 % (3910650)Instruction limit reached! % 9.02/1.76 % (3910650)------------------------------ % 9.02/1.76 % (3910650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.02/1.76 % (3910650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.02/1.76 % (3910650)CaDiCaL version: 2.1.3 % 9.02/1.76 % (3910650)Termination reason: Instruction limit % 9.02/1.76 % (3910650)Termination phase: Saturation % 9.02/1.76 % (3910650)Time elapsed: 0.060 s % 9.02/1.76 % (3910650)Peak memory usage: 15 MB % 9.02/1.76 % (3910650)Instructions burned: 103 (million) % 9.02/1.76 % (3910651)Instruction limit reached! % 9.02/1.76 % (3910651)------------------------------ % 9.02/1.76 % (3910651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.02/1.76 % (3910651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.02/1.76 % (3910651)CaDiCaL version: 2.1.3 % 9.02/1.76 % (3910651)Termination reason: Instruction limit % 9.02/1.76 % (3910651)Termination phase: Saturation % 9.02/1.76 % (3910651)Time elapsed: 0.063 s % 9.02/1.76 % (3910651)Peak memory usage: 16 MB % 9.02/1.76 % (3910651)Instructions burned: 117 (million) % 9.02/1.76 % (3910652)Instruction limit reached! % 9.02/1.76 % (3910652)------------------------------ % 9.02/1.76 % (3910652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.02/1.76 % (3910652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.02/1.76 % (3910652)CaDiCaL version: 2.1.3 % 9.02/1.76 % (3910652)Termination reason: Instruction limit % 9.02/1.76 % (3910652)Termination phase: Saturation % 9.02/1.76 % (3910652)Time elapsed: 0.074 s % 9.02/1.76 % (3910652)Peak memory usage: 16 MB % 9.02/1.76 % (3910652)Instructions burned: 131 (million) % 9.02/1.76 % (3910661)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=227762974:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 9.02/1.76 % (3910662)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=396040099:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.02/1.76 % (3910663)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=3091326133:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.02/1.76 % (3910653)Instruction limit reached! % 9.02/1.76 % (3910653)------------------------------ % 9.02/1.76 % (3910653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.02/1.76 % (3910653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.02/1.76 % (3910653)CaDiCaL version: 2.1.3 % 9.02/1.76 % (3910653)Termination reason: Instruction limit % 9.02/1.76 % (3910653)Termination phase: Saturation % 9.02/1.76 % (3910653)Time elapsed: 0.102 s % 9.02/1.76 % (3910653)Peak memory usage: 17 MB % 9.02/1.76 % (3910653)Instructions burned: 159 (million) % 9.02/1.76 % (3910667)ott-21_1_sil=16000:fs=off:random_seed=672595397:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 9.02/1.76 % (3910662)Instruction limit reached! % 9.02/1.76 % (3910662)------------------------------ % 9.02/1.76 % (3910662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.02/1.76 % (3910662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.02/1.76 % (3910662)CaDiCaL version: 2.1.3 % 42.83/6.33 % (3910662)Termination reason: Instruction limit % 42.83/6.33 % (3910662)Termination phase: Saturation % 42.83/6.33 % (3910662)Time elapsed: 0.075 s % 42.83/6.33 % (3910662)Peak memory usage: 16 MB % 42.83/6.33 % (3910662)Instructions burned: 131 (million) % 42.83/6.33 % (3910669)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3960855858:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 42.83/6.33 % (3910667)Instruction limit reached! % 42.83/6.33 % (3910667)------------------------------ % 42.83/6.33 % (3910667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.83/6.33 % (3910667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.83/6.33 % (3910667)CaDiCaL version: 2.1.3 % 42.83/6.33 % (3910667)Termination reason: Instruction limit % 42.83/6.33 % (3910667)Termination phase: Saturation % 42.83/6.33 % (3910667)Time elapsed: 0.096 s % 42.83/6.33 % (3910667)Peak memory usage: 16 MB % 42.83/6.33 % (3910667)Instructions burned: 180 (million) % 42.83/6.33 % (3910671)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=236175480:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 42.83/6.33 % TRYING [1] % 42.83/6.33 % TRYING [2] % 42.83/6.33 % TRYING [1] % 42.83/6.33 % TRYING [2] % 42.83/6.33 % (3910661)Instruction limit reached! % 42.83/6.33 % (3910661)------------------------------ % 42.83/6.33 % (3910661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.83/6.33 % (3910661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.83/6.33 % (3910661)CaDiCaL version: 2.1.3 % 42.83/6.33 % (3910661)Termination reason: Instruction limit % 42.83/6.33 % (3910661)Termination phase: Finite model building constraint generation % 42.83/6.33 % (3910661)Time elapsed: 0.337 s % 42.83/6.33 % (3910661)Peak memory usage: 26 MB % 42.83/6.33 % (3910661)Instructions burned: 714 (million) % 42.83/6.33 % (3910673)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=871220292:i=1179_2994 on theBenchmark for (2994ds/1179Mi) % 42.83/6.33 % (3910669)Instruction limit reached! % 42.83/6.33 % (3910669)------------------------------ % 42.83/6.33 % (3910669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.83/6.33 % (3910669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.83/6.33 % (3910669)CaDiCaL version: 2.1.3 % 42.83/6.33 % (3910669)Termination reason: Instruction limit % 42.83/6.33 % (3910669)Termination phase: Saturation % 42.83/6.33 % (3910669)Time elapsed: 0.294 s % 42.83/6.33 % (3910669)Peak memory usage: 17 MB % 42.83/6.33 % (3910669)Instructions burned: 478 (million) % 42.83/6.33 % (3910675)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=699499109:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 42.83/6.33 % (3910663)Instruction limit reached! % 42.83/6.33 % (3910663)------------------------------ % 42.83/6.33 % (3910663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.83/6.33 % (3910663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.83/6.33 % (3910663)CaDiCaL version: 2.1.3 % 42.83/6.33 % (3910663)Termination reason: Instruction limit % 42.83/6.33 % (3910663)Termination phase: Saturation % 42.83/6.33 % (3910663)Time elapsed: 0.404 s % 42.83/6.33 % (3910663)Peak memory usage: 21 MB % 42.83/6.33 % (3910663)Instructions burned: 684 (million) % 42.83/6.33 % (3910677)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=1457580654: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) % 42.83/6.33 % TRYING [1] % 42.83/6.33 % (3910671)Instruction limit reached! % 42.83/6.33 % (3910671)------------------------------ % 42.83/6.33 % (3910671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 42.83/6.33 % (3910671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.83/6.33 % (3910671)CaDiCaL version: 2.1.3 % 42.83/6.33 % (3910671)Termination reason: Instruction limit % 42.83/6.33 % (3910671)Termination phase: Finite model building constraint generation % 42.83/6.33 % (3910671)Time elapsed: 0.422 s % 42.83/6.33 % (3910671)Peak memory usage: 42 MB % 42.83/6.33 % (3910671)Instructions burned: 867 (million) % 42.83/6.33 % (3910679)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=74411968:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 42.83/6.33 % (3910675)Cannot represent all propositional literals internally % 42.83/6.33 % (3910675)Refutation not found, incomplete strategy % 42.83/6.33 % (3910675)------------------------------ % 42.83/6.33 % (3910675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.35/10.64 % (3910675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.35/10.64 % (3910675)CaDiCaL version: 2.1.3 % 73.35/10.64 % (3910675)Termination reason: Refutation not found, incomplete strategy % 73.35/10.64 % (3910675)Time elapsed: 0.305 s % 73.35/10.64 % (3910675)Peak memory usage: 25 MB % 73.35/10.64 % (3910675)Instructions burned: 620 (million) % 73.35/10.64 % (3910675)------------------------------ % 73.35/10.64 % (3910675)------------------------------ % 73.35/10.64 % (3910681)fmb+10_1_sil=64000:random_seed=1137954408:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 73.35/10.64 % (3910677)Instruction limit reached! % 73.35/10.64 % (3910677)------------------------------ % 73.35/10.64 % (3910677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.35/10.64 % (3910677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.35/10.64 % (3910677)CaDiCaL version: 2.1.3 % 73.35/10.64 % (3910677)Termination reason: Instruction limit % 73.35/10.64 % (3910677)Termination phase: Saturation % 73.35/10.64 % (3910677)Time elapsed: 0.408 s % 73.35/10.64 % (3910677)Peak memory usage: 24 MB % 73.35/10.64 % (3910677)Instructions burned: 692 (million) % 73.35/10.64 % (3910683)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4158168355:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 73.35/10.64 % (3910679)Instruction limit reached! % 73.35/10.64 % (3910679)------------------------------ % 73.35/10.64 % (3910679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.35/10.64 % (3910679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.35/10.64 % (3910679)CaDiCaL version: 2.1.3 % 73.35/10.64 % (3910679)Termination reason: Instruction limit % 73.35/10.64 % (3910679)Termination phase: Saturation % 73.35/10.64 % (3910679)Time elapsed: 0.425 s % 73.35/10.64 % (3910679)Peak memory usage: 21 MB % 73.35/10.64 % (3910679)Instructions burned: 879 (million) % 73.35/10.64 % (3910685)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1003491250:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi) % 73.35/10.64 % TRYING [1] % 73.35/10.64 % (3910673)Instruction limit reached! % 73.35/10.64 % (3910673)------------------------------ % 73.35/10.64 % (3910673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.35/10.64 % (3910673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.35/10.64 % (3910673)CaDiCaL version: 2.1.3 % 73.35/10.64 % (3910673)Termination reason: Instruction limit % 73.35/10.64 % (3910673)Termination phase: Saturation % 73.35/10.64 % (3910673)Time elapsed: 0.756 s % 73.35/10.64 % (3910673)Peak memory usage: 28 MB % 73.35/10.64 % (3910673)Instructions burned: 1179 (million) % 73.35/10.64 % (3910687)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3662846741:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 73.35/10.64 % (3910683)Cannot represent all propositional literals internally % 73.35/10.64 % (3910683)Refutation not found, incomplete strategy % 73.35/10.64 % (3910683)------------------------------ % 73.35/10.64 % (3910683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.35/10.64 % (3910683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.35/10.64 % (3910683)CaDiCaL version: 2.1.3 % 73.35/10.64 % (3910683)Termination reason: Refutation not found, incomplete strategy % 73.35/10.64 % (3910683)Time elapsed: 0.304 s % 73.35/10.64 % (3910683)Peak memory usage: 24 MB % 73.35/10.64 % (3910683)Instructions burned: 616 (million) % 73.35/10.64 % (3910683)------------------------------ % 73.35/10.64 % (3910683)------------------------------ % 73.35/10.64 % (3910689)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2803468054:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 73.35/10.64 % (3910685)Cannot represent all propositional literals internally % 73.35/10.64 % (3910685)Refutation not found, incomplete strategy % 73.35/10.64 % (3910685)------------------------------ % 73.35/10.64 % (3910685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 73.35/10.64 % (3910685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.35/10.64 % (3910685)CaDiCaL version: 2.1.3 % 73.35/10.64 % (3910685)Termination reason: Refutation not found, incomplete strategy % 73.35/10.64 % (3910685)Time elapsed: 0.303 s % 73.35/10.64 % (3910685)Peak memory usage: 24 MB % 73.35/10.64 % (3910685)Instructions burned: 616 (million) % 73.35/10.64 % (3910685)------------------------------ % 73.35/10.64 % (3910685)------------------------------ % 73.35/10.64 % (3910691)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1510979076:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 82.08/11.99 % TRYING [2] % 82.08/11.99 % (3910691)Cannot represent all propositional literals internally % 82.08/11.99 % (3910691)Refutation not found, incomplete strategy % 82.08/11.99 % (3910691)------------------------------ % 82.08/11.99 % (3910691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.08/11.99 % (3910691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.08/11.99 % (3910691)CaDiCaL version: 2.1.3 % 82.08/11.99 % (3910691)Termination reason: Refutation not found, incomplete strategy % 82.08/11.99 % (3910691)Time elapsed: 0.314 s % 82.08/11.99 % (3910691)Peak memory usage: 24 MB % 82.08/11.99 % (3910691)Instructions burned: 636 (million) % 82.08/11.99 % (3910691)------------------------------ % 82.08/11.99 % (3910691)------------------------------ % 82.08/11.99 % (3910693)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4244537951:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi) % 82.08/11.99 % (3910689)Instruction limit reached! % 82.08/11.99 % (3910689)------------------------------ % 82.08/11.99 % (3910689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.08/11.99 % (3910689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.08/11.99 % (3910689)CaDiCaL version: 2.1.3 % 82.08/11.99 % (3910689)Termination reason: Instruction limit % 82.08/11.99 % (3910689)Termination phase: Saturation % 82.08/11.99 % (3910689)Time elapsed: 0.877 s % 82.08/11.99 % (3910689)Peak memory usage: 34 MB % 82.08/11.99 % (3910689)Instructions burned: 1473 (million) % 82.08/11.99 % (3910695)ott-2_1_sil=16000:newcnf=on:random_seed=3313668725:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2977 on theBenchmark for (2977ds/869Mi) % 82.08/11.99 % (3910695)Instruction limit reached! % 82.08/11.99 % (3910695)------------------------------ % 82.08/11.99 % (3910695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.08/11.99 % (3910695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.08/11.99 % (3910695)CaDiCaL version: 2.1.3 % 82.08/11.99 % (3910695)Termination reason: Instruction limit % 82.08/11.99 % (3910695)Termination phase: Saturation % 82.08/11.99 % (3910695)Time elapsed: 0.477 s % 82.08/11.99 % (3910695)Peak memory usage: 21 MB % 82.08/11.99 % (3910695)Instructions burned: 869 (million) % 82.08/11.99 % (3910697)ott+10_1_sil=32000:tgt=ground:random_seed=1548931168:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi) % 82.08/11.99 % (3910693)Instruction limit reached! % 82.08/11.99 % (3910693)------------------------------ % 82.08/11.99 % (3910693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.08/11.99 % (3910693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.08/11.99 % (3910693)CaDiCaL version: 2.1.3 % 82.08/11.99 % (3910693)Termination reason: Instruction limit % 82.08/11.99 % (3910693)Termination phase: Finite model building preprocessing % 82.08/11.99 % (3910693)Time elapsed: 1.091 s % 82.08/11.99 % (3910693)Peak memory usage: 39 MB % 82.08/11.99 % (3910693)Instructions burned: 2175 (million) % 82.08/11.99 % (3910699)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=831288368:i=54282_2970 on theBenchmark for (2970ds/54282Mi) % 82.08/11.99 % TRYING [1] % 82.08/11.99 % TRYING [2] % 82.08/11.99 % (3910687)Instruction limit reached! % 82.08/11.99 % (3910687)------------------------------ % 82.08/11.99 % (3910687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.08/11.99 % (3910687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.08/11.99 % (3910687)CaDiCaL version: 2.1.3 % 82.08/11.99 % (3910687)Termination reason: Instruction limit % 82.08/11.99 % (3910687)Termination phase: Saturation % 82.08/11.99 % (3910687)Time elapsed: 3.137 s % 82.08/11.99 % (3910687)Peak memory usage: 55 MB % 82.08/11.99 % (3910687)Instructions burned: 5132 (million) % 82.08/11.99 % (3910701)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2919022918:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi) % 82.08/11.99 % (3910697)Instruction limit reached! % 82.08/11.99 % (3910697)------------------------------ % 82.08/11.99 % (3910697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 82.08/11.99 % (3910697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.08/11.99 % (3910697)CaDiCaL version: 2.1.3 % 82.08/11.99 % (3910697)Termination reason: Instruction limit % 82.08/11.99 % (3910697)Termination phase: Saturation % 82.08/11.99 % (3910697)Time elapsed: 3.354 s % 82.08/11.99 % (3910697)Peak memory usage: 66 MB % 82.08/11.99 % (3910697)Instructions burned: 5114 (million) % 157.18/24.25 % (3910703)dis+21_1_sil=32000:sas=cadical:random_seed=2292399412:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi) % 157.18/24.25 % (3910701)Instruction limit reached! % 157.18/24.25 % (3910701)------------------------------ % 157.18/24.25 % (3910701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.18/24.25 % (3910701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.18/24.25 % (3910701)CaDiCaL version: 2.1.3 % 157.18/24.25 % (3910701)Termination reason: Instruction limit % 157.18/24.25 % (3910701)Termination phase: Saturation % 157.18/24.25 % (3910701)Time elapsed: 2.204 s % 157.18/24.25 % (3910701)Peak memory usage: 47 MB % 157.18/24.25 % (3910701)Instructions burned: 3512 (million) % 157.18/24.25 % (3910705)ott+11_1_sil=16000:gs=on:random_seed=3465718907:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi) % 157.18/24.25 % (3910647)Cannot represent all propositional literals internally % 157.18/24.25 % (3910705)Instruction limit reached! % 157.18/24.25 % (3910705)------------------------------ % 157.18/24.25 % (3910705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.18/24.25 % (3910705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.18/24.25 % (3910705)CaDiCaL version: 2.1.3 % 157.18/24.25 % (3910705)Termination reason: Instruction limit % 157.18/24.25 % (3910705)Termination phase: Saturation % 157.18/24.25 % (3910705)Time elapsed: 1.408 s % 157.18/24.25 % (3910705)Peak memory usage: 44 MB % 157.18/24.25 % (3910705)Instructions burned: 2252 (million) % 157.18/24.25 % (3910707)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1157364683:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi) % 157.18/24.25 % (3910703)Instruction limit reached! % 157.18/24.25 % (3910703)------------------------------ % 157.18/24.25 % (3910703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.18/24.25 % (3910703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.18/24.25 % (3910703)CaDiCaL version: 2.1.3 % 157.18/24.25 % (3910703)Termination reason: Instruction limit % 157.18/24.25 % (3910703)Termination phase: Saturation % 157.18/24.25 % (3910703)Time elapsed: 2.248 s % 157.18/24.25 % (3910703)Peak memory usage: 41 MB % 157.18/24.25 % (3910703)Instructions burned: 3773 (million) % 157.18/24.25 % (3910709)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1796514168:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi) % 157.18/24.25 % (3910707)Cannot represent all propositional literals internally % 157.18/24.25 % (3910707)Refutation not found, incomplete strategy % 157.18/24.25 % (3910707)------------------------------ % 157.18/24.25 % (3910707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.18/24.25 % (3910707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.18/24.25 % (3910707)CaDiCaL version: 2.1.3 % 157.18/24.25 % (3910707)Termination reason: Refutation not found, incomplete strategy % 157.18/24.25 % (3910707)Time elapsed: 0.318 s % 157.18/24.25 % (3910707)Peak memory usage: 22 MB % 157.18/24.25 % (3910707)Instructions burned: 645 (million) % 157.18/24.25 % (3910707)------------------------------ % 157.18/24.25 % (3910707)------------------------------ % 157.18/24.25 % (3910711)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=302963943:i=29340_2915 on theBenchmark for (2915ds/29340Mi) % 157.18/24.25 % (3910647)Refutation not found, incomplete strategy % 157.18/24.25 % (3910647)------------------------------ % 157.18/24.25 % (3910647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.18/24.25 % (3910647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.18/24.25 % (3910647)CaDiCaL version: 2.1.3 % 157.18/24.25 % (3910647)Termination reason: Refutation not found, incomplete strategy % 157.18/24.25 % (3910647)Time elapsed: 8.697 s % 157.18/24.25 % (3910647)Peak memory usage: 980 MB % 157.18/24.25 % (3910647)Instructions burned: 14765 (million) % 157.18/24.25 % (3910647)------------------------------ % 157.18/24.25 % (3910647)------------------------------ % 157.18/24.25 % (3910713)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2818055176:i=5211_2911 on theBenchmark for (2911ds/5211Mi) % 157.18/24.25 % (3910709)Instruction limit reached! % 157.18/24.25 % (3910709)------------------------------ % 157.18/24.25 % (3910709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.18/24.25 % (3910709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.80/28.60 % (3910709)CaDiCaL version: 2.1.3 % 200.80/28.60 % (3910709)Termination reason: Instruction limit % 200.80/28.60 % (3910709)Termination phase: Saturation % 200.80/28.60 % (3910709)Time elapsed: 2.008 s % 200.80/28.60 % (3910709)Peak memory usage: 42 MB % 200.80/28.60 % (3910709)Instructions burned: 4592 (million) % 200.80/28.60 % (3910715)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3778699335:i=5497:nm=2_2895 on theBenchmark for (2895ds/5497Mi) % 200.80/28.60 % (3910715)Cannot represent all propositional literals internally % 200.80/28.60 % (3910715)Refutation not found, incomplete strategy % 200.80/28.60 % (3910715)------------------------------ % 200.80/28.60 % (3910715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.80/28.60 % (3910715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.80/28.60 % (3910715)CaDiCaL version: 2.1.3 % 200.80/28.60 % (3910715)Termination reason: Refutation not found, incomplete strategy % 200.80/28.60 % (3910715)Time elapsed: 0.316 s % 200.80/28.60 % (3910715)Peak memory usage: 24 MB % 200.80/28.60 % (3910715)Instructions burned: 636 (million) % 200.80/28.60 % (3910715)------------------------------ % 200.80/28.60 % (3910715)------------------------------ % 200.80/28.60 % (3910717)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3449623767:fmbsr=2:i=46332_2892 on theBenchmark for (2892ds/46332Mi) % 200.80/28.60 % (3910699)Cannot represent all propositional literals internally % 200.80/28.60 % (3910717)Cannot represent all propositional literals internally % 200.80/28.60 % (3910717)Refutation not found, incomplete strategy % 200.80/28.60 % (3910717)------------------------------ % 200.80/28.60 % (3910717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.80/28.60 % (3910717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.80/28.60 % (3910717)CaDiCaL version: 2.1.3 % 200.80/28.60 % (3910717)Termination reason: Refutation not found, incomplete strategy % 200.80/28.60 % (3910717)Time elapsed: 0.316 s % 200.80/28.60 % (3910717)Peak memory usage: 22 MB % 200.80/28.60 % (3910717)Instructions burned: 644 (million) % 200.80/28.60 % (3910717)------------------------------ % 200.80/28.60 % (3910717)------------------------------ % 200.80/28.60 % (3910719)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3942474246:i=14071_2888 on theBenchmark for (2888ds/14071Mi) % 200.80/28.60 % (3910713)Instruction limit reached! % 200.80/28.60 % (3910713)------------------------------ % 200.80/28.60 % (3910713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.80/28.60 % (3910713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.80/28.60 % (3910713)CaDiCaL version: 2.1.3 % 200.80/28.60 % (3910713)Termination reason: Instruction limit % 200.80/28.60 % (3910713)Termination phase: Saturation % 200.80/28.60 % (3910713)Time elapsed: 2.512 s % 200.80/28.60 % (3910713)Peak memory usage: 43 MB % 200.80/28.60 % (3910713)Instructions burned: 5211 (million) % 200.80/28.60 % (3910721)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=847574334:i=22565:add=on:rawr=on_2885 on theBenchmark for (2885ds/22565Mi) % 200.80/28.60 % (3910719)Cannot represent all propositional literals internally % 200.80/28.60 % (3910719)Refutation not found, incomplete strategy % 200.80/28.60 % (3910719)------------------------------ % 200.80/28.60 % (3910719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.80/28.60 % (3910719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.80/28.60 % (3910719)CaDiCaL version: 2.1.3 % 200.80/28.60 % (3910719)Termination reason: Refutation not found, incomplete strategy % 200.80/28.60 % (3910719)Time elapsed: 0.309 s % 200.80/28.60 % (3910719)Peak memory usage: 24 MB % 200.80/28.60 % (3910719)Instructions burned: 617 (million) % 200.80/28.60 % (3910719)------------------------------ % 200.80/28.60 % (3910719)------------------------------ % 200.80/28.60 % (3910723)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2395788407:i=8173:av=off_2885 on theBenchmark for (2885ds/8173Mi) % 200.80/28.60 % (3910699)Refutation not found, incomplete strategy % 200.80/28.60 % (3910699)------------------------------ % 200.80/28.60 % (3910699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.80/28.60 % (3910699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.80/28.60 % (3910699)CaDiCaL version: 2.1.3 % 200.80/28.60 % (3910699)Termination reason: Refutation not found, incomplete strategy % 200.80/28.60 % (3910699)Time elapsed: 8.766 s % 200.80/28.60 % (3910699)Peak memory usage: 980 MB % 200.80/28.60 % (3910699)Instructions burned: 14766 (million) % 200.80/28.60 % (3910699)------------------------------ % 233.75/33.25 % (3910699)------------------------------ % 233.75/33.25 % (3910725)dis+10_16:1_sil=16000:random_seed=1505410500:i=9155:fsr=off_2881 on theBenchmark for (2881ds/9155Mi) % 233.75/33.25 % (3910681)Instruction limit reached! % 233.75/33.25 % (3910681)------------------------------ % 233.75/33.25 % (3910681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.75/33.25 % (3910681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.75/33.25 % (3910681)CaDiCaL version: 2.1.3 % 233.75/33.25 % (3910681)Termination reason: Instruction limit % 233.75/33.25 % (3910681)Termination phase: Finite model building SAT solving % 233.75/33.25 % (3910681)Time elapsed: 13.541 s % 233.75/33.25 % (3910681)Peak memory usage: 741 MB % 233.75/33.25 % (3910681)Instructions burned: 22062 (million) % 233.75/33.25 % (3910727)ott-3_8_sil=64000:random_seed=4071843842:i=20139:bs=on_2854 on theBenchmark for (2854ds/20139Mi) % 233.75/33.25 % (3910723)Instruction limit reached! % 233.75/33.25 % (3910723)------------------------------ % 233.75/33.25 % (3910723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.75/33.25 % (3910723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.75/33.25 % (3910723)CaDiCaL version: 2.1.3 % 233.75/33.25 % (3910723)Termination reason: Instruction limit % 233.75/33.25 % (3910723)Termination phase: Saturation % 233.75/33.25 % (3910723)Time elapsed: 5.402 s % 233.75/33.25 % (3910723)Peak memory usage: 104 MB % 233.75/33.25 % (3910723)Instructions burned: 8173 (million) % 233.75/33.25 % (3910729)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=607279011:fmbsr=2:i=32576_2831 on theBenchmark for (2831ds/32576Mi) % 233.75/33.25 % (3910725)Instruction limit reached! % 233.75/33.25 % (3910725)------------------------------ % 233.75/33.25 % (3910725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.75/33.25 % (3910725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.75/33.25 % (3910725)CaDiCaL version: 2.1.3 % 233.75/33.25 % (3910725)Termination reason: Instruction limit % 233.75/33.25 % (3910725)Termination phase: Saturation % 233.75/33.25 % (3910725)Time elapsed: 5.200 s % 233.75/33.25 % (3910725)Peak memory usage: 90 MB % 233.75/33.25 % (3910725)Instructions burned: 9157 (million) % 233.75/33.25 % (3910731)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2377221445:i=11404_2828 on theBenchmark for (2828ds/11404Mi) % 233.75/33.25 % (3910729)Cannot represent all propositional literals internally % 233.75/33.25 % (3910729)Refutation not found, incomplete strategy % 233.75/33.25 % (3910729)------------------------------ % 233.75/33.25 % (3910729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.75/33.25 % (3910729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.75/33.25 % (3910729)CaDiCaL version: 2.1.3 % 233.75/33.25 % (3910729)Termination reason: Refutation not found, incomplete strategy % 233.75/33.25 % (3910729)Time elapsed: 0.314 s % 233.75/33.25 % (3910729)Peak memory usage: 24 MB % 233.75/33.25 % (3910729)Instructions burned: 637 (million) % 233.75/33.25 % (3910729)------------------------------ % 233.75/33.25 % (3910729)------------------------------ % 233.75/33.25 % (3910733)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=484356414:i=14134_2827 on theBenchmark for (2827ds/14134Mi) % 233.75/33.25 % (3910711)Instruction limit reached! % 233.75/33.25 % (3910711)------------------------------ % 233.75/33.25 % (3910711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.75/33.25 % (3910711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.75/33.25 % (3910711)CaDiCaL version: 2.1.3 % 233.75/33.25 % (3910711)Termination reason: Instruction limit % 233.75/33.25 % (3910711)Termination phase: Saturation % 233.75/33.25 % (3910711)Time elapsed: 13.506 s % 233.75/33.25 % (3910711)Peak memory usage: 446 MB % 233.75/33.25 % (3910711)Instructions burned: 29342 (million) % 233.75/33.25 % (3910735)dis+33_16_sil=32000:sac=on:random_seed=4294267046:i=15851:nm=0_2779 on theBenchmark for (2779ds/15851Mi) % 233.75/33.25 % (3910721)Instruction limit reached! % 233.75/33.25 % (3910721)------------------------------ % 233.75/33.25 % (3910721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.75/33.25 % (3910721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.75/33.25 % (3910721)CaDiCaL version: 2.1.3 % 233.75/33.25 % (3910721)Termination reason: Instruction limit % 233.75/33.25 % (3910721)Termination phase: Saturation % 233.75/33.25 % (3910721)Time elapsed: 12.525 s % 233.75/33.25 % (3910721)Peak memory usage: 345 MB % 233.75/33.25 % (3910721)Instructions burned: 22568 (million) % 233.75/33.25 % (3910737)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1517392811:avsq=on:i=17627:add=on:amm=off_2759 on theBenchmark for (2759ds/17627Mi) % 277.73/39.48 % (3910731)Instruction limit reached! % 277.73/39.48 % (3910731)------------------------------ % 277.73/39.48 % (3910731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.73/39.48 % (3910731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.73/39.48 % (3910731)CaDiCaL version: 2.1.3 % 277.73/39.48 % (3910731)Termination reason: Instruction limit % 277.73/39.48 % (3910731)Termination phase: Saturation % 277.73/39.48 % (3910731)Time elapsed: 7.819 s % 277.73/39.48 % (3910731)Peak memory usage: 238 MB % 277.73/39.48 % (3910731)Instructions burned: 11404 (million) % 277.73/39.48 % (3910739)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=600893936:s2a=on:i=53295_2750 on theBenchmark for (2750ds/53295Mi) % 277.73/39.48 % (3910733)Instruction limit reached! % 277.73/39.48 % (3910733)------------------------------ % 277.73/39.48 % (3910733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.73/39.48 % (3910733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.73/39.48 % (3910733)CaDiCaL version: 2.1.3 % 277.73/39.48 % (3910733)Termination reason: Instruction limit % 277.73/39.48 % (3910733)Termination phase: Saturation % 277.73/39.48 % (3910733)Time elapsed: 9.220 s % 277.73/39.48 % (3910733)Peak memory usage: 128 MB % 277.73/39.48 % (3910733)Instructions burned: 14135 (million) % 277.73/39.48 % (3910741)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1653223653:i=26857:ins=20_2735 on theBenchmark for (2735ds/26857Mi) % 277.73/39.48 % (3910741)Cannot represent all propositional literals internally % 277.73/39.48 % (3910741)Refutation not found, incomplete strategy % 277.73/39.48 % (3910741)------------------------------ % 277.73/39.48 % (3910741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.73/39.48 % (3910741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.73/39.48 % (3910741)CaDiCaL version: 2.1.3 % 277.73/39.48 % (3910741)Termination reason: Refutation not found, incomplete strategy % 277.73/39.48 % (3910741)Time elapsed: 0.304 s % 277.73/39.48 % (3910741)Peak memory usage: 24 MB % 277.73/39.48 % (3910741)Instructions burned: 616 (million) % 277.73/39.48 % (3910741)------------------------------ % 277.73/39.48 % (3910741)------------------------------ % 277.73/39.48 % (3910743)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3769830896:i=28120:bs=on:fsr=off_2731 on theBenchmark for (2731ds/28120Mi) % 277.73/39.48 % (3910727)Instruction limit reached! % 277.73/39.48 % (3910727)------------------------------ % 277.73/39.48 % (3910727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.73/39.48 % (3910727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.73/39.48 % (3910727)CaDiCaL version: 2.1.3 % 277.73/39.48 % (3910727)Termination reason: Instruction limit % 277.73/39.48 % (3910727)Termination phase: Saturation % 277.73/39.48 % (3910727)Time elapsed: 13.143 s % 277.73/39.48 % (3910727)Peak memory usage: 118 MB % 277.73/39.48 % (3910727)Instructions burned: 20139 (million) % 277.73/39.48 % (3910745)fmb+10_1_sil=256000:fmbss=7:random_seed=3057738057:fmbsr=1.6:i=182295_2722 on theBenchmark for (2722ds/182295Mi) % 277.73/39.48 % (3910745)Cannot represent all propositional literals internally % 277.73/39.48 % (3910745)Refutation not found, incomplete strategy % 277.73/39.48 % (3910745)------------------------------ % 277.73/39.48 % (3910745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.73/39.48 % (3910745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.73/39.48 % (3910745)CaDiCaL version: 2.1.3 % 277.73/39.48 % (3910745)Termination reason: Refutation not found, incomplete strategy % 277.73/39.48 % (3910745)Time elapsed: 0.310 s % 277.73/39.48 % (3910745)Peak memory usage: 24 MB % 277.73/39.48 % (3910745)Instructions burned: 616 (million) % 277.73/39.48 % (3910745)------------------------------ % 277.73/39.48 % (3910745)------------------------------ % 277.73/39.48 % (3910747)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2720918325:i=44625:gsp=on_2719 on theBenchmark for (2719ds/44625Mi) % 277.73/39.48 % (3910747)Cannot represent all propositional literals internally % 277.73/39.48 % (3910747)Refutation not found, incomplete strategy % 277.73/39.48 % (3910747)------------------------------ % 277.73/39.48 % (3910747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 277.73/39.48 % (3910747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/41.87 % (3910747)CaDiCaL version: 2.1.3 % 293.64/41.87 % (3910747)Termination reason: Refutation not found, incomplete strategy % 293.64/41.87 % (3910747)Time elapsed: 0.307 s % 293.64/41.87 % (3910747)Peak memory usage: 24 MB % 293.64/41.87 % (3910747)Instructions burned: 623 (million) % 293.64/41.87 % (3910747)------------------------------ % 293.64/41.87 % (3910747)------------------------------ % 293.64/41.87 % (3910749)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=823763309:i=160505_2715 on theBenchmark for (2715ds/160505Mi) % 293.64/41.87 % (3910749)Cannot represent all propositional literals internally % 293.64/41.87 % (3910749)Refutation not found, incomplete strategy % 293.64/41.87 % (3910749)------------------------------ % 293.64/41.87 % (3910749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.64/41.87 % (3910749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/41.87 % (3910749)CaDiCaL version: 2.1.3 % 293.64/41.87 % (3910749)Termination reason: Refutation not found, incomplete strategy % 293.64/41.87 % (3910749)Time elapsed: 0.304 s % 293.64/41.87 % (3910749)Peak memory usage: 24 MB % 293.64/41.87 % (3910749)Instructions burned: 616 (million) % 293.64/41.87 % (3910749)------------------------------ % 293.64/41.87 % (3910749)------------------------------ % 293.64/41.87 % (3910751)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=687815246:fmbsr=1.3:i=225729_2712 on theBenchmark for (2712ds/225729Mi) % 293.64/41.87 % (3910751)Cannot represent all propositional literals internally % 293.64/41.87 % (3910751)Refutation not found, incomplete strategy % 293.64/41.87 % (3910751)------------------------------ % 293.64/41.87 % (3910751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.64/41.87 % (3910751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/41.87 % (3910751)CaDiCaL version: 2.1.3 % 293.64/41.87 % (3910751)Termination reason: Refutation not found, incomplete strategy % 293.64/41.87 % (3910751)Time elapsed: 0.305 s % 293.64/41.87 % (3910751)Peak memory usage: 24 MB % 293.64/41.87 % (3910751)Instructions burned: 617 (million) % 293.64/41.87 % (3910751)------------------------------ % 293.64/41.87 % (3910751)------------------------------ % 293.64/41.87 % (3910753)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1368684402:fmbsr=2:i=185024:ins=7_2709 on theBenchmark for (2709ds/185024Mi) % 293.64/41.87 % (3910753)Cannot represent all propositional literals internally % 293.64/41.87 % (3910753)Refutation not found, incomplete strategy % 293.64/41.87 % (3910753)------------------------------ % 293.64/41.87 % (3910753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.64/41.87 % (3910753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/41.87 % (3910753)CaDiCaL version: 2.1.3 % 293.64/41.87 % (3910753)Termination reason: Refutation not found, incomplete strategy % 293.64/41.87 % (3910753)Time elapsed: 0.306 s % 293.64/41.87 % (3910753)Peak memory usage: 24 MB % 293.64/41.87 % (3910753)Instructions burned: 617 (million) % 293.64/41.87 % (3910753)------------------------------ % 293.64/41.87 % (3910753)------------------------------ % 293.64/41.87 % (3910755)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1201863237:rtra=on_2705 on theBenchmark for (2705ds/0Mi) % 293.64/41.87 % TRYING [1] % 293.64/41.87 % TRYING [2] % 293.64/41.87 % (3910735)Instruction limit reached! % 293.64/41.87 % (3910735)------------------------------ % 293.64/41.87 % (3910735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.64/41.87 % (3910735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/41.87 % (3910735)CaDiCaL version: 2.1.3 % 293.64/41.87 % (3910735)Termination reason: Instruction limit % 293.64/41.87 % (3910735)Termination phase: Saturation % 293.64/41.87 % (3910735)Time elapsed: 7.999 s % 293.64/41.87 % (3910735)Peak memory usage: 175 MB % 293.64/41.87 % (3910735)Instructions burned: 15852 (million) % 293.64/41.87 % (3910757)% WARNING: option uhcvi not known. % 293.64/41.87 % (3910757)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1039363586:i=271062:add=off:rtra=on:rawr=on_2699 on theBenchmark for (2699ds/271062Mi) % 293.64/41.87 % (3910737)Instruction limit reached! % 293.64/41.87 % (3910737)------------------------------ % 293.64/41.87 % (3910737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 293.64/41.87 % (3910737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.64/41.87 % (3910737)CaDiCaL version: 2.1.3 % 293.64/41.87 % (3910737)Termination reason: Instruction limit % 293.64/41.87 % (3910737)Termination phase: Saturation % 293.64/41.87 % (3910737)Time elapsed: 8.998 s % 293.64/41.87 % (3910737)Peak memory usage: 120 MB % 293.64/41.87 % (3910737)Instructions burned: 17628 (million) % 300.10/42.63 % (3910759)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3497836628:i=176048:add=on:rtra=on:rawr=on_2669 on theBenchmark for (2669ds/176048Mi) % 300.10/42.63 % (3910649)Instruction limit reached! % 300.10/42.63 % (3910649)------------------------------ % 300.10/42.63 % (3910649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.10/42.63 % (3910649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.10/42.63 % (3910649)CaDiCaL version: 2.1.3 % 300.10/42.63 % (3910649)Termination reason: Instruction limit % 300.10/42.63 % (3910649)Termination phase: Saturation % 300.10/42.63 % (3910649)Time elapsed: 37.734 s % 300.10/42.63 % (3910649)Peak memory usage: 332 MB % 300.10/42.63 % (3910649)Instructions burned: 88026 (million) % 300.10/42.63 % (3910762)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2193546391:i=206:fgj=on:rtra=on_2621 on theBenchmark for (2621ds/206Mi) % 300.10/42.63 % (3910762)Instruction limit reached! % 300.10/42.63 % (3910762)------------------------------ % 300.10/42.63 % (3910762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.10/42.63 % (3910762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.10/42.63 % (3910762)CaDiCaL version: 2.1.3 % 300.10/42.63 % (3910762)Termination reason: Instruction limit % 300.10/42.63 % (3910762)Termination phase: Saturation % 300.10/42.63 % (3910762)Time elapsed: 0.136 s % 300.10/42.63 % (3910762)Peak memory usage: 17 MB % 300.10/42.63 % (3910762)Instructions burned: 206 (million) % 300.10/42.63 % (3910764)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=22702615:i=232:rtra=on_2619 on theBenchmark for (2619ds/232Mi) % 300.10/42.63 % (3910764)Instruction limit reached! % 300.10/42.63 % (3910764)------------------------------ % 300.10/42.63 % (3910764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.10/42.63 % (3910764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.10/42.63 % (3910764)CaDiCaL version: 2.1.3 % 300.10/42.63 % (3910764)Termination reason: Instruction limit % 300.10/42.63 % (3910764)Termination phase: Saturation % 300.10/42.63 % (3910764)Time elapsed: 0.146 s % 300.10/42.63 % (3910764)Peak memory usage: 17 MB % 300.10/42.63 % (3910764)Instructions burned: 232 (million) % 300.10/42.63 % (3910766)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1607270127:i=262:rtra=on_2617 on theBenchmark for (2617ds/262Mi) % 300.10/42.63 % (3910766)Instruction limit reached! % 300.10/42.63 % (3910766)------------------------------ % 300.10/42.63 % (3910766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.10/42.63 % (3910766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.10/42.63 % (3910766)CaDiCaL version: 2.1.3 % 300.10/42.63 % (3910766)Termination reason: Instruction limit % 300.10/42.63 % (3910766)Termination phase: Saturation % 300.10/42.63 % (3910766)Time elapsed: 0.167 s % 300.10/42.63 % (3910766)Peak memory usage: 19 MB % 300.10/42.63 % (3910766)Instructions burned: 263 (million) % 300.10/42.63 % (3910768)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3160646304:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2616 on theBenchmark for (2616ds/318Mi) % 300.10/42.63 % (3910768)Instruction limit reached! % 300.10/42.63 % (3910768)------------------------------ % 300.10/42.63 % (3910768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.10/42.63 % (3910768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.10/42.63 % (3910768)CaDiCaL version: 2.1.3 % 300.10/42.63 % (3910768)Termination reason: Instruction limit % 300.10/42.63 % (3910768)Termination phase: Saturation % 300.10/42.63 % (3910768)Time elapsed: 0.218 s % 300.10/42.63 % (3910768)Peak memory usage: 19 MB % 300.10/42.63 % (3910768)Instructions burned: 319 (million) % 300.10/42.63 % (3910770)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=88982794:i=1428:nm=2:rtra=on_2613 on theBenchmark for (2613ds/1428Mi) % 300.10/42.63 % TRYING [1] % 300.10/42.63 % TRYING [2] % 300.10/42.63 % (3910770)Instruction limit reached! % 300.10/42.63 % (3910770)------------------------------ % 300.10/42.63 % (3910770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.10/42.63 % (3910770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.10/42.63 % (3910770)CaDiCaL version: 2.1.3 % 300.10/42.63 % (3910770)Termination reason: Instruction limit % 300.10/42.63 % (3910770)Termination phase: Finite model building constraint generation % 300.10/42.63 % (3910770)Time elapsed: 0.625 s % 300.10/42.63 % (3910770)Peak memory us % 300.10/42.63 Terminated % 300.10/42.63 % Vampire exiting % 300.10/42.63 Terminated %------------------------------------------------------------------------------