%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV932-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 : 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 01:26:41 PM UTC 2026 % Result : Timeout 298.95s 42.48s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV932-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.07/0.21 % Computer : n015.cluster.edu % 0.07/0.21 % Model : x86_64 x86_64 % 0.07/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.21 % Memory : 8046.5625MB % 0.07/0.21 % OS : Linux 6.8.0-71-generic % 0.07/0.21 % CPULimit : 300 % 0.07/0.21 % WCLimit : 300 % 0.07/0.21 % DateTime : Mon Sep 28 13:00:47 UTC 2026 % 0.07/0.21 % CPUTime : % 0.07/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.23 Running first-order model finding % 0.07/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 % 7.44/1.36 % (2611405)Will run a generic schedule for satisfiability detection. % 7.44/1.36 % (2611411)% WARNING: option uhcvi not known. % 7.44/1.36 % (2611411)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3423728441:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.44/1.36 % (2611410)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1441045816_2999 on theBenchmark for (2999ds/0Mi) % 7.44/1.36 % (2611412)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4259427125:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.44/1.36 % (2611413)dis+10_1_sil=32000:sp=arity:random_seed=539824304:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.44/1.36 % (2611414)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=225433248:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.44/1.36 % (2611415)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1498026750:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.44/1.36 % (2611416)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2119035847:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.44/1.36 % TRYING [1] % 7.44/1.36 % TRYING [2] % 7.44/1.36 % (2611413)Instruction limit reached! % 7.44/1.36 % (2611413)------------------------------ % 7.44/1.36 % (2611413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.36 % (2611413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.36 % (2611413)CaDiCaL version: 2.1.3 % 7.44/1.36 % (2611413)Termination reason: Instruction limit % 7.44/1.36 % (2611413)Termination phase: Saturation % 7.44/1.36 % (2611413)Time elapsed: 0.064 s % 7.44/1.36 % (2611413)Peak memory usage: 12 MB % 7.44/1.36 % (2611413)Instructions burned: 104 (million) % 7.44/1.36 % (2611414)Instruction limit reached! % 7.44/1.36 % (2611414)------------------------------ % 7.44/1.36 % (2611414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.36 % (2611414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.36 % (2611414)CaDiCaL version: 2.1.3 % 7.44/1.36 % (2611414)Termination reason: Instruction limit % 7.44/1.36 % (2611414)Termination phase: Saturation % 7.44/1.36 % (2611414)Time elapsed: 0.072 s % 7.44/1.36 % (2611414)Peak memory usage: 13 MB % 7.44/1.36 % (2611414)Instructions burned: 117 (million) % 7.44/1.36 % (2611424)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3883781442:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 7.44/1.36 % (2611415)Instruction limit reached! % 7.44/1.36 % (2611415)------------------------------ % 7.44/1.36 % (2611415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.36 % (2611415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.36 % (2611415)CaDiCaL version: 2.1.3 % 7.44/1.36 % (2611415)Termination reason: Instruction limit % 7.44/1.36 % (2611415)Termination phase: Saturation % 7.44/1.36 % (2611415)Time elapsed: 0.086 s % 7.44/1.36 % (2611415)Peak memory usage: 13 MB % 7.44/1.36 % (2611415)Instructions burned: 132 (million) % 7.44/1.36 % (2611425)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2555109578:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 7.44/1.36 % (2611427)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=2532977891:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.44/1.36 % (2611416)Instruction limit reached! % 7.44/1.36 % (2611416)------------------------------ % 7.44/1.36 % (2611416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.36 % (2611416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.44/1.36 % (2611416)CaDiCaL version: 2.1.3 % 7.44/1.36 % (2611416)Termination reason: Instruction limit % 7.44/1.36 % (2611416)Termination phase: Saturation % 7.44/1.36 % (2611416)Time elapsed: 0.107 s % 7.44/1.36 % (2611416)Peak memory usage: 14 MB % 7.44/1.36 % (2611416)Instructions burned: 160 (million) % 7.44/1.36 % (2611430)ott-21_1_sil=16000:fs=off:random_seed=3306812072:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.44/1.36 % TRYING [1] % 7.44/1.36 % TRYING [2] % 7.44/1.36 % (2611425)Instruction limit reached! % 7.44/1.36 % (2611425)------------------------------ % 7.44/1.36 % (2611425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.44/1.36 % (2611425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.95/5.13 % (2611425)CaDiCaL version: 2.1.3 % 33.95/5.13 % (2611425)Termination reason: Instruction limit % 33.95/5.13 % (2611425)Termination phase: Saturation % 33.95/5.13 % (2611425)Time elapsed: 0.078 s % 33.95/5.13 % (2611425)Peak memory usage: 14 MB % 33.95/5.13 % (2611425)Instructions burned: 131 (million) % 33.95/5.13 % (2611432)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3239653928:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 33.95/5.13 % (2611430)Instruction limit reached! % 33.95/5.13 % (2611430)------------------------------ % 33.95/5.13 % (2611430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.95/5.13 % (2611430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.95/5.13 % (2611430)CaDiCaL version: 2.1.3 % 33.95/5.13 % (2611430)Termination reason: Instruction limit % 33.95/5.13 % (2611430)Termination phase: Saturation % 33.95/5.13 % (2611430)Time elapsed: 0.098 s % 33.95/5.13 % (2611430)Peak memory usage: 12 MB % 33.95/5.13 % (2611430)Instructions burned: 181 (million) % 33.95/5.13 % (2611434)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2949235874:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 33.95/5.13 % TRYING [1] % 33.95/5.13 % (2611424)Instruction limit reached! % 33.95/5.13 % (2611424)------------------------------ % 33.95/5.13 % (2611424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.95/5.13 % (2611424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.95/5.13 % (2611424)CaDiCaL version: 2.1.3 % 33.95/5.13 % (2611424)Termination reason: Instruction limit % 33.95/5.13 % (2611424)Termination phase: Finite model building constraint generation % 33.95/5.13 % (2611424)Time elapsed: 0.256 s % 33.95/5.13 % (2611424)Peak memory usage: 21 MB % 33.95/5.13 % (2611424)Instructions burned: 717 (million) % 33.95/5.13 % (2611436)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2871930547:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 33.95/5.13 % (2611427)Instruction limit reached! % 33.95/5.13 % (2611427)------------------------------ % 33.95/5.13 % (2611427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.95/5.13 % (2611427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.95/5.13 % (2611427)CaDiCaL version: 2.1.3 % 33.95/5.13 % (2611427)Termination reason: Instruction limit % 33.95/5.13 % (2611427)Termination phase: Saturation % 33.95/5.13 % (2611427)Time elapsed: 0.264 s % 33.95/5.13 % (2611427)Peak memory usage: 15 MB % 33.95/5.13 % (2611427)Instructions burned: 685 (million) % 33.95/5.13 % (2611438)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=233726310:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 33.95/5.13 % (2611438)Cannot represent all propositional literals internally % 33.95/5.13 % (2611438)Refutation not found, incomplete strategy % 33.95/5.13 % (2611438)------------------------------ % 33.95/5.13 % (2611438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.95/5.13 % (2611438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.95/5.13 % (2611438)CaDiCaL version: 2.1.3 % 33.95/5.13 % (2611438)Termination reason: Refutation not found, incomplete strategy % 33.95/5.13 % (2611438)Time elapsed: 0.059 s % 33.95/5.13 % (2611438)Peak memory usage: 12 MB % 33.95/5.13 % (2611438)Instructions burned: 113 (million) % 33.95/5.13 % (2611438)------------------------------ % 33.95/5.13 % (2611438)------------------------------ % 33.95/5.13 % (2611440)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=1308550440:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 33.95/5.13 % (2611432)Instruction limit reached! % 33.95/5.13 % (2611432)------------------------------ % 33.95/5.13 % (2611432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 33.95/5.13 % (2611432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.95/5.13 % (2611432)CaDiCaL version: 2.1.3 % 33.95/5.13 % (2611432)Termination reason: Instruction limit % 33.95/5.13 % (2611432)Termination phase: Saturation % 33.95/5.13 % (2611432)Time elapsed: 0.305 s % 33.95/5.13 % (2611432)Peak memory usage: 14 MB % 33.95/5.13 % (2611432)Instructions burned: 478 (million) % 33.95/5.13 % (2611442)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1603329232:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 33.95/5.13 % (2611434)Instruction limit reached! % 33.95/5.13 % (2611434)------------------------------ % 72.73/10.58 % (2611434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.58 % (2611434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.58 % (2611434)CaDiCaL version: 2.1.3 % 72.73/10.58 % (2611434)Termination reason: Instruction limit % 72.73/10.58 % (2611434)Termination phase: Finite model building constraint generation % 72.73/10.58 % (2611434)Time elapsed: 0.413 s % 72.73/10.58 % (2611434)Peak memory usage: 100 MB % 72.73/10.58 % (2611434)Instructions burned: 867 (million) % 72.73/10.58 % (2611444)fmb+10_1_sil=64000:random_seed=3114116851:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 72.73/10.58 % TRYING [1] % 72.73/10.58 % (2611440)Instruction limit reached! % 72.73/10.58 % (2611440)------------------------------ % 72.73/10.58 % (2611440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.58 % (2611440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.58 % (2611440)CaDiCaL version: 2.1.3 % 72.73/10.58 % (2611440)Termination reason: Instruction limit % 72.73/10.58 % (2611440)Termination phase: Saturation % 72.73/10.58 % (2611440)Time elapsed: 0.424 s % 72.73/10.58 % (2611440)Peak memory usage: 18 MB % 72.73/10.58 % (2611440)Instructions burned: 693 (million) % 72.73/10.58 % (2611446)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1051220547:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 72.73/10.58 % (2611446)Cannot represent all propositional literals internally % 72.73/10.58 % (2611446)Refutation not found, incomplete strategy % 72.73/10.58 % (2611446)------------------------------ % 72.73/10.58 % (2611446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.58 % (2611446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.58 % (2611446)CaDiCaL version: 2.1.3 % 72.73/10.58 % (2611446)Termination reason: Refutation not found, incomplete strategy % 72.73/10.58 % (2611446)Time elapsed: 0.059 s % 72.73/10.58 % (2611446)Peak memory usage: 12 MB % 72.73/10.58 % (2611446)Instructions burned: 113 (million) % 72.73/10.58 % (2611446)------------------------------ % 72.73/10.58 % (2611446)------------------------------ % 72.73/10.58 % (2611448)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3048734138:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 72.73/10.58 % (2611442)Instruction limit reached! % 72.73/10.58 % (2611442)------------------------------ % 72.73/10.58 % (2611442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.58 % (2611442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.58 % (2611442)CaDiCaL version: 2.1.3 % 72.73/10.58 % (2611442)Termination reason: Instruction limit % 72.73/10.58 % (2611442)Termination phase: Saturation % 72.73/10.58 % (2611442)Time elapsed: 0.498 s % 72.73/10.58 % (2611442)Peak memory usage: 19 MB % 72.73/10.58 % (2611442)Instructions burned: 879 (million) % 72.73/10.58 % (2611436)Instruction limit reached! % 72.73/10.58 % (2611436)------------------------------ % 72.73/10.58 % (2611436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.58 % (2611436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.58 % (2611436)CaDiCaL version: 2.1.3 % 72.73/10.58 % (2611436)Termination reason: Instruction limit % 72.73/10.58 % (2611436)Termination phase: Saturation % 72.73/10.58 % (2611436)Time elapsed: 0.669 s % 72.73/10.58 % (2611436)Peak memory usage: 30 MB % 72.73/10.58 % (2611436)Instructions burned: 1179 (million) % 72.73/10.58 % (2611450)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2505715675:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 72.73/10.58 % (2611451)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1072104799:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi) % 72.73/10.58 % (2611448)Cannot represent all propositional literals internally % 72.73/10.58 % (2611448)Refutation not found, incomplete strategy % 72.73/10.58 % (2611448)------------------------------ % 72.73/10.58 % (2611448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.73/10.58 % (2611448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.58 % (2611448)CaDiCaL version: 2.1.3 % 72.73/10.58 % (2611448)Termination reason: Refutation not found, incomplete strategy % 72.73/10.58 % (2611448)Time elapsed: 0.060 s % 72.73/10.58 % (2611448)Peak memory usage: 12 MB % 72.73/10.58 % (2611448)Instructions burned: 113 (million) % 72.73/10.58 % (2611448)------------------------------ % 72.73/10.58 % (2611448)------------------------------ % 72.73/10.58 % (2611454)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2420150700:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 116.70/16.79 % (2611454)Cannot represent all propositional literals internally % 116.70/16.79 % (2611454)Refutation not found, incomplete strategy % 116.70/16.79 % (2611454)------------------------------ % 116.70/16.79 % (2611454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.70/16.79 % (2611454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.70/16.79 % (2611454)CaDiCaL version: 2.1.3 % 116.70/16.79 % (2611454)Termination reason: Refutation not found, incomplete strategy % 116.70/16.79 % (2611454)Time elapsed: 0.060 s % 116.70/16.79 % (2611454)Peak memory usage: 12 MB % 116.70/16.79 % (2611454)Instructions burned: 116 (million) % 116.70/16.79 % (2611454)------------------------------ % 116.70/16.79 % (2611454)------------------------------ % 116.70/16.79 % (2611456)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1106711968:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi) % 116.70/16.79 % (2611456)Cannot represent all propositional literals internally % 116.70/16.79 % (2611456)Refutation not found, incomplete strategy % 116.70/16.79 % (2611456)------------------------------ % 116.70/16.79 % (2611456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.70/16.79 % (2611456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.70/16.79 % (2611456)CaDiCaL version: 2.1.3 % 116.70/16.79 % (2611456)Termination reason: Refutation not found, incomplete strategy % 116.70/16.79 % (2611456)Time elapsed: 0.511 s % 116.70/16.79 % (2611456)Peak memory usage: 18 MB % 116.70/16.79 % (2611456)Instructions burned: 940 (million) % 116.70/16.79 % (2611456)------------------------------ % 116.70/16.79 % (2611456)------------------------------ % 116.70/16.79 % (2611458)ott-2_1_sil=16000:newcnf=on:random_seed=946759575:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2982 on theBenchmark for (2982ds/869Mi) % 116.70/16.79 % (2611451)Instruction limit reached! % 116.70/16.79 % (2611451)------------------------------ % 116.70/16.79 % (2611451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.70/16.79 % (2611451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.70/16.79 % (2611451)CaDiCaL version: 2.1.3 % 116.70/16.79 % (2611451)Termination reason: Instruction limit % 116.70/16.79 % (2611451)Termination phase: Saturation % 116.70/16.79 % (2611451)Time elapsed: 0.720 s % 116.70/16.79 % (2611451)Peak memory usage: 25 MB % 116.70/16.79 % (2611451)Instructions burned: 1473 (million) % 116.70/16.79 % (2611460)ott+10_1_sil=32000:tgt=ground:random_seed=3151457592:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi) % 116.70/16.79 % (2611458)Instruction limit reached! % 116.70/16.79 % (2611458)------------------------------ % 116.70/16.79 % (2611458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.70/16.79 % (2611458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.70/16.79 % (2611458)CaDiCaL version: 2.1.3 % 116.70/16.79 % (2611458)Termination reason: Instruction limit % 116.70/16.79 % (2611458)Termination phase: Saturation % 116.70/16.79 % (2611458)Time elapsed: 0.522 s % 116.70/16.79 % (2611458)Peak memory usage: 16 MB % 116.70/16.79 % (2611458)Instructions burned: 869 (million) % 116.70/16.79 % (2611462)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2265342921:i=54282_2977 on theBenchmark for (2977ds/54282Mi) % 116.70/16.79 % TRYING [1] % 116.70/16.79 % TRYING [2] % 116.70/16.79 % (2611450)Instruction limit reached! % 116.70/16.79 % (2611450)------------------------------ % 116.70/16.79 % (2611450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.70/16.79 % (2611450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.70/16.79 % (2611450)CaDiCaL version: 2.1.3 % 116.70/16.79 % (2611450)Termination reason: Instruction limit % 116.70/16.79 % (2611450)Termination phase: Saturation % 116.70/16.79 % (2611450)Time elapsed: 2.733 s % 116.70/16.79 % (2611450)Peak memory usage: 49 MB % 116.70/16.79 % (2611450)Instructions burned: 5131 (million) % 116.70/16.79 % (2611464)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3313523986:i=3512:aac=none_2961 on theBenchmark for (2961ds/3512Mi) % 116.70/16.79 % (2611460)Instruction limit reached! % 116.70/16.79 % (2611460)------------------------------ % 116.70/16.79 % (2611460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.70/16.79 % (2611460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.70/16.79 % (2611460)CaDiCaL version: 2.1.3 % 116.70/16.79 % (2611460)Termination reason: Instruction limit % 116.70/16.79 % (2611460)Termination phase: Saturation % 217.23/30.98 % (2611460)Time elapsed: 3.055 s % 217.23/30.98 % (2611460)Peak memory usage: 74 MB % 217.23/30.98 % (2611460)Instructions burned: 5115 (million) % 217.23/30.98 % (2611466)dis+21_1_sil=32000:sas=cadical:random_seed=3154397831:i=3773:amm=off_2950 on theBenchmark for (2950ds/3773Mi) % 217.23/30.98 % (2611464)Instruction limit reached! % 217.23/30.98 % (2611464)------------------------------ % 217.23/30.98 % (2611464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.23/30.98 % (2611464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.23/30.98 % (2611464)CaDiCaL version: 2.1.3 % 217.23/30.98 % (2611464)Termination reason: Instruction limit % 217.23/30.98 % (2611464)Termination phase: Saturation % 217.23/30.98 % (2611464)Time elapsed: 1.893 s % 217.23/30.98 % (2611464)Peak memory usage: 35 MB % 217.23/30.98 % (2611464)Instructions burned: 3513 (million) % 217.23/30.98 % (2611468)ott+11_1_sil=16000:gs=on:random_seed=3040876974:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi) % 217.23/30.98 % (2611468)Instruction limit reached! % 217.23/30.98 % (2611468)------------------------------ % 217.23/30.98 % (2611468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.23/30.98 % (2611468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.23/30.98 % (2611468)CaDiCaL version: 2.1.3 % 217.23/30.98 % (2611468)Termination reason: Instruction limit % 217.23/30.98 % (2611468)Termination phase: Saturation % 217.23/30.98 % (2611468)Time elapsed: 1.080 s % 217.23/30.98 % (2611468)Peak memory usage: 20 MB % 217.23/30.98 % (2611468)Instructions burned: 2252 (million) % 217.23/30.98 % (2611470)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3715242609:fmbsr=1.6:i=67534_2931 on theBenchmark for (2931ds/67534Mi) % 217.23/30.98 % (2611470)Cannot represent all propositional literals internally % 217.23/30.98 % (2611470)Refutation not found, incomplete strategy % 217.23/30.98 % (2611470)------------------------------ % 217.23/30.98 % (2611470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.23/30.98 % (2611470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.23/30.98 % (2611470)CaDiCaL version: 2.1.3 % 217.23/30.98 % (2611470)Termination reason: Refutation not found, incomplete strategy % 217.23/30.98 % (2611470)Time elapsed: 0.072 s % 217.23/30.98 % (2611470)Peak memory usage: 12 MB % 217.23/30.98 % (2611470)Instructions burned: 150 (million) % 217.23/30.98 % (2611470)------------------------------ % 217.23/30.98 % (2611470)------------------------------ % 217.23/30.98 % (2611472)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3600880213:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2930 on theBenchmark for (2930ds/4591Mi) % 217.23/30.98 % (2611466)Instruction limit reached! % 217.23/30.98 % (2611466)------------------------------ % 217.23/30.98 % (2611466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.23/30.98 % (2611466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.23/30.98 % (2611466)CaDiCaL version: 2.1.3 % 217.23/30.98 % (2611466)Termination reason: Instruction limit % 217.23/30.98 % (2611466)Termination phase: Saturation % 217.23/30.98 % (2611466)Time elapsed: 2.071 s % 217.23/30.98 % (2611466)Peak memory usage: 33 MB % 217.23/30.98 % (2611466)Instructions burned: 3774 (million) % 217.23/30.98 % (2611474)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3629477469:i=29340_2930 on theBenchmark for (2930ds/29340Mi) % 217.23/30.98 % (2611472)Instruction limit reached! % 217.23/30.98 % (2611472)------------------------------ % 217.23/30.98 % (2611472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.23/30.98 % (2611472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.23/30.98 % (2611472)CaDiCaL version: 2.1.3 % 217.23/30.98 % (2611472)Termination reason: Instruction limit % 217.23/30.98 % (2611472)Termination phase: Saturation % 217.23/30.98 % (2611472)Time elapsed: 1.753 s % 217.23/30.98 % (2611472)Peak memory usage: 28 MB % 217.23/30.98 % (2611472)Instructions burned: 4592 (million) % 217.23/30.98 % (2611476)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2782656240:i=5211_2912 on theBenchmark for (2912ds/5211Mi) % 217.23/30.98 % (2611444)Instruction limit reached! % 217.23/30.98 % (2611444)------------------------------ % 217.23/30.98 % (2611444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.23/30.98 % (2611444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.23/30.98 % (2611444)CaDiCaL version: 2.1.3 % 257.78/36.61 % (2611444)Termination reason: Instruction limit % 257.78/36.61 % (2611444)Termination phase: Finite model building constraint generation % 257.78/36.61 % (2611444)Time elapsed: 9.613 s % 257.78/36.61 % (2611444)Peak memory usage: 2129 MB % 257.78/36.61 % (2611444)Instructions burned: 22063 (million) % 257.78/36.61 % (2611478)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1577482029:i=5497:nm=2_2893 on theBenchmark for (2893ds/5497Mi) % 257.78/36.61 % (2611478)Cannot represent all propositional literals internally % 257.78/36.61 % (2611478)Refutation not found, incomplete strategy % 257.78/36.61 % (2611478)------------------------------ % 257.78/36.61 % (2611478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.78/36.61 % (2611478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.78/36.61 % (2611478)CaDiCaL version: 2.1.3 % 257.78/36.61 % (2611478)Termination reason: Refutation not found, incomplete strategy % 257.78/36.61 % (2611478)Time elapsed: 0.060 s % 257.78/36.61 % (2611478)Peak memory usage: 12 MB % 257.78/36.61 % (2611478)Instructions burned: 116 (million) % 257.78/36.61 % (2611478)------------------------------ % 257.78/36.61 % (2611478)------------------------------ % 257.78/36.61 % (2611480)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3484837873:fmbsr=2:i=46332_2892 on theBenchmark for (2892ds/46332Mi) % 257.78/36.61 % (2611480)Cannot represent all propositional literals internally % 257.78/36.61 % (2611480)Refutation not found, incomplete strategy % 257.78/36.61 % (2611480)------------------------------ % 257.78/36.61 % (2611480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.78/36.61 % (2611480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.78/36.61 % (2611480)CaDiCaL version: 2.1.3 % 257.78/36.61 % (2611480)Termination reason: Refutation not found, incomplete strategy % 257.78/36.61 % (2611480)Time elapsed: 0.072 s % 257.78/36.61 % (2611480)Peak memory usage: 12 MB % 257.78/36.61 % (2611480)Instructions burned: 150 (million) % 257.78/36.61 % (2611480)------------------------------ % 257.78/36.61 % (2611480)------------------------------ % 257.78/36.61 % (2611482)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=298613523:i=14071_2891 on theBenchmark for (2891ds/14071Mi) % 257.78/36.61 % (2611482)Cannot represent all propositional literals internally % 257.78/36.61 % (2611482)Refutation not found, incomplete strategy % 257.78/36.61 % (2611482)------------------------------ % 257.78/36.61 % (2611482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.78/36.61 % (2611482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.78/36.61 % (2611482)CaDiCaL version: 2.1.3 % 257.78/36.61 % (2611482)Termination reason: Refutation not found, incomplete strategy % 257.78/36.61 % (2611482)Time elapsed: 0.062 s % 257.78/36.61 % (2611482)Peak memory usage: 12 MB % 257.78/36.61 % (2611482)Instructions burned: 122 (million) % 257.78/36.61 % (2611482)------------------------------ % 257.78/36.61 % (2611482)------------------------------ % 257.78/36.61 % (2611484)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1511256754:i=22565:add=on:rawr=on_2890 on theBenchmark for (2890ds/22565Mi) % 257.78/36.61 % (2611476)Instruction limit reached! % 257.78/36.61 % (2611476)------------------------------ % 257.78/36.61 % (2611476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.78/36.61 % (2611476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.78/36.61 % (2611476)CaDiCaL version: 2.1.3 % 257.78/36.61 % (2611476)Termination reason: Instruction limit % 257.78/36.61 % (2611476)Termination phase: Saturation % 257.78/36.61 % (2611476)Time elapsed: 2.813 s % 257.78/36.61 % (2611476)Peak memory usage: 47 MB % 257.78/36.61 % (2611476)Instructions burned: 5211 (million) % 257.78/36.61 % (2611486)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3675910667:i=8173:av=off_2884 on theBenchmark for (2884ds/8173Mi) % 257.78/36.61 % (2611486)Instruction limit reached! % 257.78/36.61 % (2611486)------------------------------ % 257.78/36.61 % (2611486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.78/36.61 % (2611486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.78/36.61 % (2611486)CaDiCaL version: 2.1.3 % 257.78/36.61 % (2611486)Termination reason: Instruction limit % 257.78/36.61 % (2611486)Termination phase: Saturation % 257.78/36.61 % (2611486)Time elapsed: 4.948 s % 257.78/36.61 % (2611486)Peak memory usage: 116 MB % 257.78/36.61 % (2611486)Instructions burned: 8174 (million) % 257.78/36.61 % (2611488)dis+10_16:1_sil=16000:random_seed=2490773979:i=9155:fsr=off_2834 on theBenchmark for (2834ds/9155Mi) % 274.17/38.90 % (2611484)Instruction limit reached! % 274.17/38.90 % (2611484)------------------------------ % 274.17/38.90 % (2611484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.17/38.90 % (2611484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.17/38.90 % (2611484)CaDiCaL version: 2.1.3 % 274.17/38.90 % (2611484)Termination reason: Instruction limit % 274.17/38.90 % (2611484)Termination phase: Saturation % 274.17/38.90 % (2611484)Time elapsed: 9.473 s % 274.17/38.90 % (2611484)Peak memory usage: 103 MB % 274.17/38.90 % (2611484)Instructions burned: 22566 (million) % 274.17/38.90 % (2611490)ott-3_8_sil=64000:random_seed=437685817:i=20139:bs=on_2795 on theBenchmark for (2795ds/20139Mi) % 274.17/38.90 % (2611488)Instruction limit reached! % 274.17/38.90 % (2611488)------------------------------ % 274.17/38.90 % (2611488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.17/38.90 % (2611488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.17/38.90 % (2611488)CaDiCaL version: 2.1.3 % 274.17/38.90 % (2611488)Termination reason: Instruction limit % 274.17/38.90 % (2611488)Termination phase: Saturation % 274.17/38.90 % (2611488)Time elapsed: 4.947 s % 274.17/38.90 % (2611488)Peak memory usage: 69 MB % 274.17/38.90 % (2611488)Instructions burned: 9156 (million) % 274.17/38.90 % (2611492)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2528475780:fmbsr=2:i=32576_2784 on theBenchmark for (2784ds/32576Mi) % 274.17/38.90 % (2611492)Cannot represent all propositional literals internally % 274.17/38.90 % (2611492)Refutation not found, incomplete strategy % 274.17/38.90 % (2611492)------------------------------ % 274.17/38.90 % (2611492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.17/38.90 % (2611492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.17/38.90 % (2611492)CaDiCaL version: 2.1.3 % 274.17/38.90 % (2611492)Termination reason: Refutation not found, incomplete strategy % 274.17/38.90 % (2611492)Time elapsed: 0.063 s % 274.17/38.90 % (2611492)Peak memory usage: 12 MB % 274.17/38.90 % (2611492)Instructions burned: 121 (million) % 274.17/38.90 % (2611492)------------------------------ % 274.17/38.90 % (2611492)------------------------------ % 274.17/38.90 % (2611494)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2653622014:i=11404_2784 on theBenchmark for (2784ds/11404Mi) % 274.17/38.90 % (2611474)Instruction limit reached! % 274.17/38.90 % (2611474)------------------------------ % 274.17/38.90 % (2611474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.17/38.90 % (2611474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.17/38.90 % (2611474)CaDiCaL version: 2.1.3 % 274.17/38.90 % (2611474)Termination reason: Instruction limit % 274.17/38.90 % (2611474)Termination phase: Saturation % 274.17/38.90 % (2611474)Time elapsed: 14.852 s % 274.17/38.90 % (2611474)Peak memory usage: 196 MB % 274.17/38.90 % (2611474)Instructions burned: 29341 (million) % 274.17/38.90 % (2611496)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=468913576:i=14134_2781 on theBenchmark for (2781ds/14134Mi) % 274.17/38.90 % (2611494)Instruction limit reached! % 274.17/38.90 % (2611494)------------------------------ % 274.17/38.90 % (2611494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.17/38.90 % (2611494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.17/38.90 % (2611494)CaDiCaL version: 2.1.3 % 274.17/38.90 % (2611494)Termination reason: Instruction limit % 274.17/38.90 % (2611494)Termination phase: Saturation % 274.17/38.90 % (2611494)Time elapsed: 6.957 s % 274.17/38.90 % (2611494)Peak memory usage: 155 MB % 274.17/38.90 % (2611494)Instructions burned: 11405 (million) % 274.17/38.90 % (2611498)dis+33_16_sil=32000:sac=on:random_seed=1720531236:i=15851:nm=0_2714 on theBenchmark for (2714ds/15851Mi) % 274.17/38.90 % (2611496)Instruction limit reached! % 274.17/38.90 % (2611496)------------------------------ % 274.17/38.90 % (2611496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 274.17/38.90 % (2611496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 274.17/38.90 % (2611496)CaDiCaL version: 2.1.3 % 274.17/38.90 % (2611496)Termination reason: Instruction limit % 274.17/38.90 % (2611496)Termination phase: Saturation % 274.17/38.90 % (2611496)Time elapsed: 8.497 s % 274.17/38.90 % (2611496)Peak memory usage: 194 MB % 274.17/38.90 % (2611496)Instructions burned: 14135 (million) % 274.17/38.90 % (2611500)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3157187476:avsq=on:i=17627:add=on:amm=off_2695 on theBenchmark for (2695ds/17627Mi) % 274.17/38.90 % (2611412)Instruction limit reached! % 283.89/40.38 % (2611412)------------------------------ % 283.89/40.38 % (2611412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.89/40.38 % (2611412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.89/40.38 % (2611412)CaDiCaL version: 2.1.3 % 283.89/40.38 % (2611412)Termination reason: Instruction limit % 283.89/40.38 % (2611412)Termination phase: Saturation % 283.89/40.38 % (2611412)Time elapsed: 30.705 s % 283.89/40.38 % (2611412)Peak memory usage: 242 MB % 283.89/40.38 % (2611412)Instructions burned: 88027 (million) % 283.89/40.38 % (2611490)Instruction limit reached! % 283.89/40.38 % (2611490)------------------------------ % 283.89/40.38 % (2611490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.89/40.38 % (2611490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.89/40.38 % (2611490)CaDiCaL version: 2.1.3 % 283.89/40.38 % (2611490)Termination reason: Instruction limit % 283.89/40.38 % (2611490)Termination phase: Saturation % 283.89/40.38 % (2611490)Time elapsed: 10.277 s % 283.89/40.38 % (2611490)Peak memory usage: 48 MB % 283.89/40.38 % (2611490)Instructions burned: 20139 (million) % 283.89/40.38 % (2611502)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1581329904:s2a=on:i=53295_2692 on theBenchmark for (2692ds/53295Mi) % 283.89/40.38 % (2611504)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2068220377:i=26857:ins=20_2692 on theBenchmark for (2692ds/26857Mi) % 283.89/40.38 % (2611504)Cannot represent all propositional literals internally % 283.89/40.38 % (2611504)Refutation not found, incomplete strategy % 283.89/40.38 % (2611504)------------------------------ % 283.89/40.38 % (2611504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.89/40.38 % (2611504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.89/40.38 % (2611504)CaDiCaL version: 2.1.3 % 283.89/40.38 % (2611504)Termination reason: Refutation not found, incomplete strategy % 283.89/40.38 % (2611504)Time elapsed: 0.059 s % 283.89/40.38 % (2611504)Peak memory usage: 12 MB % 283.89/40.38 % (2611504)Instructions burned: 113 (million) % 283.89/40.38 % (2611504)------------------------------ % 283.89/40.38 % (2611504)------------------------------ % 283.89/40.38 % (2611506)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2942725789:i=28120:bs=on:fsr=off_2691 on theBenchmark for (2691ds/28120Mi) % 283.89/40.38 % (2611462)Instruction limit reached! % 283.89/40.38 % (2611462)------------------------------ % 283.89/40.38 % (2611462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.89/40.38 % (2611462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.89/40.38 % (2611462)CaDiCaL version: 2.1.3 % 283.89/40.38 % (2611462)Termination reason: Instruction limit % 283.89/40.38 % (2611462)Termination phase: Finite model building constraint generation % 283.89/40.38 % (2611462)Time elapsed: 32.524 s % 283.89/40.38 % (2611462)Peak memory usage: 10688 MB % 283.89/40.38 % (2611462)Instructions burned: 54283 (million) % 283.89/40.38 % (2611508)fmb+10_1_sil=256000:fmbss=7:random_seed=2002343764:fmbsr=1.6:i=182295_2637 on theBenchmark for (2637ds/182295Mi) % 283.89/40.38 % (2611508)Cannot represent all propositional literals internally % 283.89/40.38 % (2611508)Refutation not found, incomplete strategy % 283.89/40.38 % (2611508)------------------------------ % 283.89/40.38 % (2611508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.89/40.38 % (2611508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.89/40.38 % (2611508)CaDiCaL version: 2.1.3 % 283.89/40.38 % (2611508)Termination reason: Refutation not found, incomplete strategy % 283.89/40.38 % (2611508)Time elapsed: 0.059 s % 283.89/40.38 % (2611508)Peak memory usage: 12 MB % 283.89/40.38 % (2611508)Instructions burned: 113 (million) % 283.89/40.38 % (2611508)------------------------------ % 283.89/40.38 % (2611508)------------------------------ % 283.89/40.38 % (2611510)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1697836643:i=44625:gsp=on_2637 on theBenchmark for (2637ds/44625Mi) % 283.89/40.38 % (2611510)Cannot represent all propositional literals internally % 283.89/40.38 % (2611510)Refutation not found, incomplete strategy % 283.89/40.38 % (2611510)------------------------------ % 283.89/40.38 % (2611510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 283.89/40.38 % (2611510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.89/40.38 % (2611510)CaDiCaL version: 2.1.3 % 283.89/40.38 % (2611510)Termination reason: Refutation not found, incomplete strategy % 283.89/40.38 % (2611510)Time elapsed: 0.062 s % 298.95/42.48 % (2611510)Peak memory usage: 12 MB % 298.95/42.48 % (2611510)Instructions burned: 118 (million) % 298.95/42.48 % (2611510)------------------------------ % 298.95/42.48 % (2611510)------------------------------ % 298.95/42.48 % (2611512)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4185581326:i=160505_2636 on theBenchmark for (2636ds/160505Mi) % 298.95/42.48 % (2611512)Cannot represent all propositional literals internally % 298.95/42.48 % (2611512)Refutation not found, incomplete strategy % 298.95/42.48 % (2611512)------------------------------ % 298.95/42.48 % (2611512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 298.95/42.48 % (2611512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.95/42.48 % (2611512)CaDiCaL version: 2.1.3 % 298.95/42.48 % (2611512)Termination reason: Refutation not found, incomplete strategy % 298.95/42.48 % (2611512)Time elapsed: 0.059 s % 298.95/42.48 % (2611512)Peak memory usage: 12 MB % 298.95/42.48 % (2611512)Instructions burned: 113 (million) % 298.95/42.48 % (2611512)------------------------------ % 298.95/42.48 % (2611512)------------------------------ % 298.95/42.48 % (2611514)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1974808304:fmbsr=1.3:i=225729_2635 on theBenchmark for (2635ds/225729Mi) % 298.95/42.48 % (2611514)Cannot represent all propositional literals internally % 298.95/42.48 % (2611514)Refutation not found, incomplete strategy % 298.95/42.48 % (2611514)------------------------------ % 298.95/42.48 % (2611514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 298.95/42.48 % (2611514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.95/42.48 % (2611514)CaDiCaL version: 2.1.3 % 298.95/42.48 % (2611514)Termination reason: Refutation not found, incomplete strategy % 298.95/42.48 % (2611514)Time elapsed: 0.063 s % 298.95/42.48 % (2611514)Peak memory usage: 12 MB % 298.95/42.48 % (2611514)Instructions burned: 122 (million) % 298.95/42.48 % (2611514)------------------------------ % 298.95/42.48 % (2611514)------------------------------ % 298.95/42.48 % (2611516)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2310867023:fmbsr=2:i=185024:ins=7_2634 on theBenchmark for (2634ds/185024Mi) % 298.95/42.48 % (2611516)Cannot represent all propositional literals internally % 298.95/42.48 % (2611516)Refutation not found, incomplete strategy % 298.95/42.48 % (2611516)------------------------------ % 298.95/42.48 % (2611516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 298.95/42.48 % (2611516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.95/42.48 % (2611516)CaDiCaL version: 2.1.3 % 298.95/42.48 % (2611516)Termination reason: Refutation not found, incomplete strategy % 298.95/42.48 % (2611516)Time elapsed: 0.063 s % 298.95/42.48 % (2611516)Peak memory usage: 12 MB % 298.95/42.48 % (2611516)Instructions burned: 122 (million) % 298.95/42.48 % (2611516)------------------------------ % 298.95/42.48 % (2611516)------------------------------ % 298.95/42.48 % (2611518)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1160421701:rtra=on_2633 on theBenchmark for (2633ds/0Mi) % 298.95/42.48 % TRYING [1] % 298.95/42.48 % TRYING [2] % 298.95/42.48 % (2611498)Instruction limit reached! % 298.95/42.48 % (2611498)------------------------------ % 298.95/42.48 % (2611498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 298.95/42.48 % (2611498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.95/42.48 % (2611498)CaDiCaL version: 2.1.3 % 298.95/42.48 % (2611498)Termination reason: Instruction limit % 298.95/42.48 % (2611498)Termination phase: Saturation % 298.95/42.48 % (2611498)Time elapsed: 8.455 s % 298.95/42.48 % (2611498)Peak memory usage: 145 MB % 298.95/42.48 % (2611498)Instructions burned: 15852 (million) % 298.95/42.48 % (2611520)% WARNING: option uhcvi not known. % 298.95/42.48 % (2611520)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1394770226:i=271062:add=off:rtra=on:rawr=on_2629 on theBenchmark for (2629ds/271062Mi) % 298.95/42.48 % (2611500)Instruction limit reached! % 298.95/42.48 % (2611500)------------------------------ % 298.95/42.48 % (2611500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 298.95/42.48 % (2611500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.95/42.48 % (2611500)CaDiCaL version: 2.1.3 % 298.95/42.48 % (2611500)Termination reason: Instruction limit % 298.95/42.48 % (2611500)Termination phase: Saturation % 298.95/42.48 % (2611500)Time elapsed: 8.172 s % 298.95/42.48 % (2611500)Peak memory usage: 110 MB % 298.95/42.48 % (2611500)Instructions burned: 17629 (million) % 298.95/42.48 % (2611522)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=oTerminated % 300.31/42.63 % Vampire exiting % 300.31/42.63 Terminated %------------------------------------------------------------------------------