%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : CAT033+2 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 09:37:03 AM UTC 2026 % Result : Timeout 300.51s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : CAT033+2 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.00/0.10 % Computer : n012.cluster.edu % 0.00/0.10 % Model : x86_64 x86_64 % 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.10 % Memory : 8046.5625MB % 0.00/0.10 % OS : Linux 6.8.0-71-generic % 0.00/0.10 % CPULimit : 300 % 0.00/0.10 % WCLimit : 300 % 0.00/0.10 % DateTime : Mon Sep 28 21:20:34 UTC 2026 % 0.00/0.10 % CPUTime : % 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.11 Running first-order model finding % 0.08/0.11 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.88/1.66 % (3780674)Will run a generic schedule for satisfiability detection. % 9.88/1.66 % (3780680)% WARNING: option uhcvi not known. % 9.88/1.66 % (3780682)dis+10_1_sil=32000:sp=arity:random_seed=3434630763:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.88/1.66 % (3780680)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2281966430:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.88/1.66 % (3780679)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1693017470_2999 on theBenchmark for (2999ds/0Mi) % 9.88/1.66 % (3780681)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2342393619:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.88/1.66 % (3780683)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2009798868:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.88/1.66 % (3780684)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1949999296:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.88/1.66 % (3780685)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2270389628:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.88/1.66 % (3780682)Instruction limit reached! % 9.88/1.66 % (3780682)------------------------------ % 9.88/1.66 % (3780682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.88/1.66 % (3780682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/1.66 % (3780682)CaDiCaL version: 2.1.3 % 9.88/1.66 % (3780682)Termination reason: Instruction limit % 9.88/1.66 % (3780682)Termination phase: Preprocessing 3 % 9.88/1.66 % (3780682)Time elapsed: 0.039 s % 9.88/1.66 % (3780682)Peak memory usage: 21 MB % 9.88/1.66 % (3780682)Instructions burned: 105 (million) % 9.88/1.66 % (3780683)Instruction limit reached! % 9.88/1.66 % (3780683)------------------------------ % 9.88/1.66 % (3780683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.88/1.66 % (3780683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/1.66 % (3780683)CaDiCaL version: 2.1.3 % 9.88/1.66 % (3780683)Termination reason: Instruction limit % 9.88/1.66 % (3780683)Termination phase: NewCNF % 9.88/1.66 % (3780683)Time elapsed: 0.043 s % 9.88/1.66 % (3780683)Peak memory usage: 22 MB % 9.88/1.66 % (3780683)Instructions burned: 116 (million) % 9.88/1.66 % (3780684)Instruction limit reached! % 9.88/1.66 % (3780684)------------------------------ % 9.88/1.66 % (3780684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.88/1.66 % (3780684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/1.66 % (3780684)CaDiCaL version: 2.1.3 % 9.88/1.66 % (3780684)Termination reason: Instruction limit % 9.88/1.66 % (3780684)Termination phase: Preprocessing 3 % 9.88/1.66 % (3780684)Time elapsed: 0.049 s % 9.88/1.66 % (3780684)Peak memory usage: 22 MB % 9.88/1.66 % (3780684)Instructions burned: 134 (million) % 9.88/1.66 % (3780693)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=154271153:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 9.88/1.66 % (3780694)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3487116090:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.88/1.66 % (3780685)Instruction limit reached! % 9.88/1.66 % (3780685)------------------------------ % 9.88/1.66 % (3780685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.88/1.66 % (3780685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/1.66 % (3780685)CaDiCaL version: 2.1.3 % 9.88/1.66 % (3780685)Termination reason: Instruction limit % 9.88/1.66 % (3780685)Termination phase: Property scanning % 9.88/1.66 % (3780685)Time elapsed: 0.060 s % 9.88/1.66 % (3780685)Peak memory usage: 24 MB % 9.88/1.66 % (3780685)Instructions burned: 160 (million) % 9.88/1.66 % (3780696)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=335840442:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.88/1.66 % (3780699)ott-21_1_sil=16000:fs=off:random_seed=3306341331:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.88/1.66 % (3780694)Instruction limit reached! % 9.88/1.66 % (3780694)------------------------------ % 9.88/1.66 % (3780694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.88/1.66 % (3780694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.44 % (3780694)CaDiCaL version: 2.1.3 % 15.15/2.44 % (3780694)Termination reason: Instruction limit % 15.15/2.44 % (3780694)Termination phase: Preprocessing 3 % 15.15/2.44 % (3780694)Time elapsed: 0.048 s % 15.15/2.44 % (3780694)Peak memory usage: 22 MB % 15.15/2.44 % (3780694)Instructions burned: 132 (million) % 15.15/2.44 % (3780701)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3859397970:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 15.15/2.44 % (3780699)Instruction limit reached! % 15.15/2.44 % (3780699)------------------------------ % 15.15/2.44 % (3780699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.15/2.44 % (3780699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.44 % (3780699)CaDiCaL version: 2.1.3 % 15.15/2.44 % (3780699)Termination reason: Instruction limit % 15.15/2.44 % (3780699)Termination phase: Property scanning % 15.15/2.44 % (3780699)Time elapsed: 0.065 s % 15.15/2.44 % (3780699)Peak memory usage: 24 MB % 15.15/2.44 % (3780699)Instructions burned: 184 (million) % 15.15/2.44 % (3780703)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3301405599:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 15.15/2.44 % (3780701)Instruction limit reached! % 15.15/2.44 % (3780701)------------------------------ % 15.15/2.44 % (3780701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.15/2.44 % (3780701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.44 % (3780701)CaDiCaL version: 2.1.3 % 15.15/2.44 % (3780701)Termination reason: Instruction limit % 15.15/2.44 % (3780701)Termination phase: Saturation % 15.15/2.44 % (3780701)Time elapsed: 0.139 s % 15.15/2.44 % (3780701)Peak memory usage: 27 MB % 15.15/2.44 % (3780701)Instructions burned: 478 (million) % 15.15/2.44 % (3780696)Instruction limit reached! % 15.15/2.44 % (3780696)------------------------------ % 15.15/2.44 % (3780696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.15/2.44 % (3780696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.44 % (3780696)CaDiCaL version: 2.1.3 % 15.15/2.44 % (3780696)Termination reason: Instruction limit % 15.15/2.44 % (3780696)Termination phase: Saturation % 15.15/2.44 % (3780696)Time elapsed: 0.192 s % 15.15/2.44 % (3780696)Peak memory usage: 30 MB % 15.15/2.44 % (3780696)Instructions burned: 688 (million) % 15.15/2.44 % (3780693)Instruction limit reached! % 15.15/2.44 % (3780693)------------------------------ % 15.15/2.44 % (3780693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.15/2.44 % (3780693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.44 % (3780693)CaDiCaL version: 2.1.3 % 15.15/2.44 % (3780693)Termination reason: Instruction limit % 15.15/2.44 % (3780693)Termination phase: Finite model building preprocessing % 15.15/2.44 % (3780693)Time elapsed: 0.205 s % 15.15/2.44 % (3780693)Peak memory usage: 34 MB % 15.15/2.44 % (3780693)Instructions burned: 717 (million) % 15.15/2.44 % (3780705)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4064145614:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 15.15/2.44 % (3780706)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2311379053:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 15.15/2.44 % (3780707)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=2214870135:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 15.15/2.44 % (3780703)Instruction limit reached! % 15.15/2.44 % (3780703)------------------------------ % 15.15/2.44 % (3780703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.15/2.44 % (3780703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.44 % (3780703)CaDiCaL version: 2.1.3 % 15.15/2.44 % (3780703)Termination reason: Instruction limit % 15.15/2.44 % (3780703)Termination phase: Finite model building preprocessing % 15.15/2.44 % (3780703)Time elapsed: 0.243 s % 15.15/2.44 % (3780703)Peak memory usage: 32 MB % 15.15/2.44 % (3780703)Instructions burned: 867 (million) % 15.15/2.44 % (3780711)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1165451614:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi) % 15.15/2.44 % (3780707)Instruction limit reached! % 15.15/2.44 % (3780707)------------------------------ % 15.15/2.44 % (3780707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 15.15/2.44 % (3780707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.72/3.61 % (3780707)CaDiCaL version: 2.1.3 % 23.72/3.61 % (3780707)Termination reason: Instruction limit % 23.72/3.61 % (3780707)Termination phase: Saturation % 23.72/3.61 % (3780707)Time elapsed: 0.202 s % 23.72/3.61 % (3780707)Peak memory usage: 32 MB % 23.72/3.61 % (3780707)Instructions burned: 693 (million) % 23.72/3.61 % (3780713)fmb+10_1_sil=64000:random_seed=1025475440:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 23.72/3.61 % (3780706)Instruction limit reached! % 23.72/3.61 % (3780706)------------------------------ % 23.72/3.61 % (3780706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.72/3.61 % (3780706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.72/3.61 % (3780706)CaDiCaL version: 2.1.3 % 23.72/3.61 % (3780706)Termination reason: Instruction limit % 23.72/3.61 % (3780706)Termination phase: Finite model building preprocessing % 23.72/3.61 % (3780706)Time elapsed: 0.248 s % 23.72/3.61 % (3780706)Peak memory usage: 32 MB % 23.72/3.61 % (3780706)Instructions burned: 892 (million) % 23.72/3.61 % (3780715)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2185275845:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 23.72/3.61 % (3780705)Instruction limit reached! % 23.72/3.61 % (3780705)------------------------------ % 23.72/3.61 % (3780705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.72/3.61 % (3780705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.72/3.61 % (3780705)CaDiCaL version: 2.1.3 % 23.72/3.61 % (3780705)Termination reason: Instruction limit % 23.72/3.61 % (3780705)Termination phase: Saturation % 23.72/3.61 % (3780705)Time elapsed: 0.348 s % 23.72/3.61 % (3780705)Peak memory usage: 40 MB % 23.72/3.61 % (3780705)Instructions burned: 1179 (million) % 23.72/3.61 % (3780717)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3043251356:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 23.72/3.61 % (3780711)Instruction limit reached! % 23.72/3.61 % (3780711)------------------------------ % 23.72/3.61 % (3780711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.72/3.61 % (3780711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.72/3.61 % (3780711)CaDiCaL version: 2.1.3 % 23.72/3.61 % (3780711)Termination reason: Instruction limit % 23.72/3.61 % (3780711)Termination phase: Saturation % 23.72/3.61 % (3780711)Time elapsed: 0.244 s % 23.72/3.61 % (3780711)Peak memory usage: 37 MB % 23.72/3.61 % (3780711)Instructions burned: 884 (million) % 23.72/3.61 % (3780719)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1141106919:i=5131_2992 on theBenchmark for (2992ds/5131Mi) % 23.72/3.61 % (3780717)Instruction limit reached! % 23.72/3.61 % (3780717)------------------------------ % 23.72/3.61 % (3780717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.72/3.61 % (3780717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.72/3.61 % (3780717)CaDiCaL version: 2.1.3 % 23.72/3.61 % (3780717)Termination reason: Instruction limit % 23.72/3.61 % (3780717)Termination phase: Finite model building preprocessing % 23.72/3.61 % (3780717)Time elapsed: 0.251 s % 23.72/3.61 % (3780717)Peak memory usage: 32 MB % 23.72/3.61 % (3780717)Instructions burned: 922 (million) % 23.72/3.61 % (3780721)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=430512278:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 23.72/3.61 % (3780721)Instruction limit reached! % 23.72/3.61 % (3780721)------------------------------ % 23.72/3.61 % (3780721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.72/3.61 % (3780721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.72/3.61 % (3780721)CaDiCaL version: 2.1.3 % 23.72/3.61 % (3780721)Termination reason: Instruction limit % 23.72/3.61 % (3780721)Termination phase: Saturation % 23.72/3.61 % (3780721)Time elapsed: 0.381 s % 23.72/3.61 % (3780721)Peak memory usage: 33 MB % 23.72/3.61 % (3780721)Instructions burned: 1474 (million) % 23.72/3.61 % (3780723)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1870038840:i=6324_2986 on theBenchmark for (2986ds/6324Mi) % 23.72/3.61 % Detected minimum model sizes of [5] % 23.72/3.61 % Detected maximum model sizes of [max] % 23.72/3.61 % (3780713)Cannot represent all propositional literals internally % 23.72/3.61 % (3780713)Refutation not found, incomplete strategy % 23.72/3.61 % (3780713)------------------------------ % 23.72/3.61 % (3780713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/6.00 % (3780713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.00 % (3780713)CaDiCaL version: 2.1.3 % 39.57/6.00 % (3780713)Termination reason: Refutation not found, incomplete strategy % 39.57/6.00 % (3780713)Time elapsed: 0.971 s % 39.57/6.00 % (3780713)Peak memory usage: 65 MB % 39.57/6.00 % (3780713)Instructions burned: 3498 (million) % 39.57/6.00 % (3780713)------------------------------ % 39.57/6.00 % (3780713)------------------------------ % 39.57/6.00 % (3780725)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1372465643:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi) % 39.57/6.00 % Detected minimum model sizes of [5] % 39.57/6.00 % Detected maximum model sizes of [max] % 39.57/6.00 % (3780679)Cannot represent all propositional literals internally % 39.57/6.00 % (3780679)Refutation not found, incomplete strategy % 39.57/6.00 % (3780679)------------------------------ % 39.57/6.00 % (3780679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/6.00 % (3780679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.00 % (3780679)CaDiCaL version: 2.1.3 % 39.57/6.00 % (3780679)Termination reason: Refutation not found, incomplete strategy % 39.57/6.00 % (3780679)Time elapsed: 1.483 s % 39.57/6.00 % (3780679)Peak memory usage: 81 MB % 39.57/6.00 % (3780679)Instructions burned: 5400 (million) % 39.57/6.00 % (3780679)------------------------------ % 39.57/6.00 % (3780679)------------------------------ % 39.57/6.00 % (3780727)ott-2_1_sil=16000:newcnf=on:random_seed=44150028:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2984 on theBenchmark for (2984ds/869Mi) % 39.57/6.00 % (3780727)Instruction limit reached! % 39.57/6.00 % (3780727)------------------------------ % 39.57/6.00 % (3780727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/6.00 % (3780727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.00 % (3780727)CaDiCaL version: 2.1.3 % 39.57/6.00 % (3780727)Termination reason: Instruction limit % 39.57/6.00 % (3780727)Termination phase: Saturation % 39.57/6.00 % (3780727)Time elapsed: 0.234 s % 39.57/6.00 % (3780727)Peak memory usage: 32 MB % 39.57/6.00 % (3780727)Instructions burned: 870 (million) % 39.57/6.00 % (3780729)ott+10_1_sil=32000:tgt=ground:random_seed=3130541328:i=5114:av=off_2981 on theBenchmark for (2981ds/5114Mi) % 39.57/6.01 % Detected minimum model sizes of [5] % 39.57/6.01 % Detected maximum model sizes of [max] % 39.57/6.01 % (3780715)Cannot represent all propositional literals internally % 39.57/6.01 % (3780715)Refutation not found, incomplete strategy % 39.57/6.01 % (3780715)------------------------------ % 39.57/6.01 % (3780715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/6.01 % (3780715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.01 % (3780715)CaDiCaL version: 2.1.3 % 39.57/6.01 % (3780715)Termination reason: Refutation not found, incomplete strategy % 39.57/6.01 % (3780715)Time elapsed: 1.305 s % 39.57/6.01 % (3780715)Peak memory usage: 76 MB % 39.57/6.01 % (3780715)Instructions burned: 4775 (million) % 39.57/6.01 % (3780715)------------------------------ % 39.57/6.01 % (3780715)------------------------------ % 39.57/6.01 % (3780731)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2677527474:i=54282_2980 on theBenchmark for (2980ds/54282Mi) % 39.57/6.01 % (3780725)Instruction limit reached! % 39.57/6.01 % (3780725)------------------------------ % 39.57/6.01 % (3780725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/6.01 % (3780725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.01 % (3780725)CaDiCaL version: 2.1.3 % 39.57/6.01 % (3780725)Termination reason: Instruction limit % 39.57/6.01 % (3780725)Termination phase: Finite model building preprocessing % 39.57/6.01 % (3780725)Time elapsed: 0.591 s % 39.57/6.01 % (3780725)Peak memory usage: 48 MB % 39.57/6.01 % (3780725)Instructions burned: 2177 (million) % 39.57/6.01 % (3780733)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2931553429:i=3512:aac=none_2978 on theBenchmark for (2978ds/3512Mi) % 39.57/6.01 % (3780719)Instruction limit reached! % 39.57/6.01 % (3780719)------------------------------ % 39.57/6.01 % (3780719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.57/6.01 % (3780719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.57/6.01 % (3780719)CaDiCaL version: 2.1.3 % 39.57/6.01 % (3780719)Termination reason: Instruction limit % 39.57/6.01 % (3780719)Termination phase: Saturation % 39.57/6.01 % (3780719)Time elapsed: 1.570 s % 39.57/6.01 % (3780719)Peak memory usage: 77 MB % 65.01/9.41 % (3780719)Instructions burned: 5131 (million) % 65.01/9.41 % (3780735)dis+21_1_sil=32000:sas=cadical:random_seed=1188136603:i=3773:amm=off_2976 on theBenchmark for (2976ds/3773Mi) % 65.01/9.41 % Detected minimum model sizes of [5] % 65.01/9.41 % Detected maximum model sizes of [max] % 65.01/9.41 % (3780723)Cannot represent all propositional literals internally % 65.01/9.41 % (3780723)Refutation not found, incomplete strategy % 65.01/9.41 % (3780723)------------------------------ % 65.01/9.41 % (3780723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.01/9.41 % (3780723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.01/9.41 % (3780723)CaDiCaL version: 2.1.3 % 65.01/9.41 % (3780723)Termination reason: Refutation not found, incomplete strategy % 65.01/9.41 % (3780723)Time elapsed: 1.475 s % 65.01/9.41 % (3780723)Peak memory usage: 80 MB % 65.01/9.41 % (3780723)Instructions burned: 5394 (million) % 65.01/9.41 % (3780723)------------------------------ % 65.01/9.41 % (3780723)------------------------------ % 65.01/9.41 % (3780737)ott+11_1_sil=16000:gs=on:random_seed=1306839976:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2971 on theBenchmark for (2971ds/2251Mi) % 65.01/9.41 % (3780733)Instruction limit reached! % 65.01/9.41 % (3780733)------------------------------ % 65.01/9.41 % (3780733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.01/9.41 % (3780733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.01/9.41 % (3780733)CaDiCaL version: 2.1.3 % 65.01/9.41 % (3780733)Termination reason: Instruction limit % 65.01/9.41 % (3780733)Termination phase: Saturation % 65.01/9.41 % (3780733)Time elapsed: 1.065 s % 65.01/9.41 % (3780733)Peak memory usage: 59 MB % 65.01/9.41 % (3780733)Instructions burned: 3515 (million) % 65.01/9.41 % (3780739)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=930964220:fmbsr=1.6:i=67534_2967 on theBenchmark for (2967ds/67534Mi) % 65.01/9.41 % (3780735)Instruction limit reached! % 65.01/9.41 % (3780735)------------------------------ % 65.01/9.41 % (3780735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.01/9.41 % (3780735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.01/9.41 % (3780735)CaDiCaL version: 2.1.3 % 65.01/9.41 % (3780735)Termination reason: Instruction limit % 65.01/9.41 % (3780735)Termination phase: Saturation % 65.01/9.41 % (3780735)Time elapsed: 1.048 s % 65.01/9.41 % (3780735)Peak memory usage: 68 MB % 65.01/9.41 % (3780735)Instructions burned: 3773 (million) % 65.01/9.41 % (3780741)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3521963677:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 65.01/9.41 % (3780737)Instruction limit reached! % 65.01/9.41 % (3780737)------------------------------ % 65.01/9.41 % (3780737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.01/9.41 % (3780737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.01/9.41 % (3780737)CaDiCaL version: 2.1.3 % 65.01/9.41 % (3780737)Termination reason: Instruction limit % 65.01/9.41 % (3780737)Termination phase: Saturation % 65.01/9.41 % (3780737)Time elapsed: 0.563 s % 65.01/9.41 % (3780737)Peak memory usage: 39 MB % 65.01/9.41 % (3780737)Instructions burned: 2254 (million) % 65.01/9.41 % Detected minimum model sizes of [5] % 65.01/9.41 % Detected maximum model sizes of [max] % 65.01/9.41 % (3780731)Cannot represent all propositional literals internally % 65.01/9.41 % (3780731)Refutation not found, incomplete strategy % 65.01/9.41 % (3780731)------------------------------ % 65.01/9.41 % (3780731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.01/9.41 % (3780731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.01/9.41 % (3780731)CaDiCaL version: 2.1.3 % 65.01/9.41 % (3780731)Termination reason: Refutation not found, incomplete strategy % 65.01/9.41 % (3780731)Time elapsed: 1.493 s % 65.01/9.41 % (3780731)Peak memory usage: 81 MB % 65.01/9.41 % (3780731)Instructions burned: 5399 (million) % 65.01/9.41 % (3780731)------------------------------ % 65.01/9.41 % (3780731)------------------------------ % 65.01/9.41 % (3780743)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1450067986:i=29340_2965 on theBenchmark for (2965ds/29340Mi) % 65.01/9.41 % (3780745)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2639381463:i=5211_2965 on theBenchmark for (2965ds/5211Mi) % 65.01/9.41 % (3780729)Instruction limit reached! % 65.01/9.41 % (3780729)------------------------------ % 98.28/14.18 % (3780729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.28/14.18 % (3780729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.28/14.18 % (3780729)CaDiCaL version: 2.1.3 % 98.28/14.18 % (3780729)Termination reason: Instruction limit % 98.28/14.18 % (3780729)Termination phase: Saturation % 98.28/14.18 % (3780729)Time elapsed: 1.659 s % 98.28/14.18 % (3780729)Peak memory usage: 89 MB % 98.28/14.18 % (3780729)Instructions burned: 5115 (million) % 98.28/14.18 % (3780747)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1353211380:i=5497:nm=2_2964 on theBenchmark for (2964ds/5497Mi) % 98.28/14.18 % (3780745)Instruction limit reached! % 98.28/14.18 % (3780745)------------------------------ % 98.28/14.18 % (3780745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.28/14.18 % (3780745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.28/14.18 % (3780745)CaDiCaL version: 2.1.3 % 98.28/14.18 % (3780745)Termination reason: Instruction limit % 98.28/14.18 % (3780745)Termination phase: Saturation % 98.28/14.18 % (3780745)Time elapsed: 1.004 s % 98.28/14.18 % (3780745)Peak memory usage: 50 MB % 98.28/14.18 % (3780745)Instructions burned: 5211 (million) % 98.28/14.18 % (3780749)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=196052950:fmbsr=2:i=46332_2955 on theBenchmark for (2955ds/46332Mi) % 98.28/14.18 % Detected minimum model sizes of [5] % 98.28/14.18 % Detected maximum model sizes of [max] % 98.28/14.18 % (3780747)Cannot represent all propositional literals internally % 98.28/14.18 % (3780747)Refutation not found, incomplete strategy % 98.28/14.18 % (3780747)------------------------------ % 98.28/14.18 % (3780747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.28/14.18 % (3780747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.28/14.18 % (3780747)CaDiCaL version: 2.1.3 % 98.28/14.18 % (3780747)Termination reason: Refutation not found, incomplete strategy % 98.28/14.18 % (3780747)Time elapsed: 1.020 s % 98.28/14.18 % (3780747)Peak memory usage: 67 MB % 98.28/14.18 % (3780747)Instructions burned: 3650 (million) % 98.28/14.18 % (3780747)------------------------------ % 98.28/14.18 % (3780747)------------------------------ % 98.28/14.18 % (3780751)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3854275873:i=14071_2954 on theBenchmark for (2954ds/14071Mi) % 98.28/14.18 % Detected minimum model sizes of [5] % 98.28/14.18 % Detected maximum model sizes of [max] % 98.28/14.18 % (3780739)Cannot represent all propositional literals internally % 98.28/14.18 % (3780739)Refutation not found, incomplete strategy % 98.28/14.18 % (3780739)------------------------------ % 98.28/14.18 % (3780739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.28/14.18 % (3780739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.28/14.18 % (3780739)CaDiCaL version: 2.1.3 % 98.28/14.18 % (3780739)Termination reason: Refutation not found, incomplete strategy % 98.28/14.18 % (3780739)Time elapsed: 1.415 s % 98.28/14.18 % (3780739)Peak memory usage: 70 MB % 98.28/14.18 % (3780739)Instructions burned: 5313 (million) % 98.28/14.18 % (3780739)------------------------------ % 98.28/14.18 % (3780739)------------------------------ % 98.28/14.18 % (3780753)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=335826677:i=22565:add=on:rawr=on_2953 on theBenchmark for (2953ds/22565Mi) % 98.28/14.18 % (3780741)Instruction limit reached! % 98.28/14.18 % (3780741)------------------------------ % 98.28/14.18 % (3780741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.28/14.18 % (3780741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.28/14.18 % (3780741)CaDiCaL version: 2.1.3 % 98.28/14.18 % (3780741)Termination reason: Instruction limit % 98.28/14.18 % (3780741)Termination phase: Saturation % 98.28/14.18 % (3780741)Time elapsed: 1.631 s % 98.28/14.18 % (3780741)Peak memory usage: 115 MB % 98.28/14.18 % (3780741)Instructions burned: 4591 (million) % 98.28/14.18 % (3780755)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2898547829:i=8173:av=off_2949 on theBenchmark for (2949ds/8173Mi) % 98.28/14.18 % Detected minimum model sizes of [5] % 98.28/14.18 % Detected maximum model sizes of [max] % 98.28/14.18 % (3780749)Cannot represent all propositional literals internally % 98.28/14.18 % (3780749)Refutation not found, incomplete strategy % 98.28/14.18 % (3780749)------------------------------ % 98.28/14.18 % (3780749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 98.28/14.18 % (3780749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.86/17.73 % (3780749)CaDiCaL version: 2.1.3 % 122.86/17.73 % (3780749)Termination reason: Refutation not found, incomplete strategy % 122.86/17.73 % (3780749)Time elapsed: 1.407 s % 122.86/17.73 % (3780749)Peak memory usage: 70 MB % 122.86/17.73 % (3780749)Instructions burned: 5312 (million) % 122.86/17.73 % (3780749)------------------------------ % 122.86/17.73 % (3780749)------------------------------ % 122.86/17.73 % (3780757)dis+10_16:1_sil=16000:random_seed=2053719420:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi) % 122.86/17.73 % Detected minimum model sizes of [5] % 122.86/17.73 % Detected maximum model sizes of [max] % 122.86/17.73 % (3780751)Cannot represent all propositional literals internally % 122.86/17.73 % (3780751)Refutation not found, incomplete strategy % 122.86/17.73 % (3780751)------------------------------ % 122.86/17.73 % (3780751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.86/17.73 % (3780751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.86/17.73 % (3780751)CaDiCaL version: 2.1.3 % 122.86/17.73 % (3780751)Termination reason: Refutation not found, incomplete strategy % 122.86/17.73 % (3780751)Time elapsed: 1.405 s % 122.86/17.73 % (3780751)Peak memory usage: 78 MB % 122.86/17.73 % (3780751)Instructions burned: 5170 (million) % 122.86/17.73 % (3780751)------------------------------ % 122.86/17.73 % (3780751)------------------------------ % 122.86/17.73 % (3780759)ott-3_8_sil=64000:random_seed=2175990019:i=20139:bs=on_2940 on theBenchmark for (2940ds/20139Mi) % 122.86/17.73 % (3780755)Instruction limit reached! % 122.86/17.73 % (3780755)------------------------------ % 122.86/17.73 % (3780755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.86/17.73 % (3780755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.86/17.73 % (3780755)CaDiCaL version: 2.1.3 % 122.86/17.73 % (3780755)Termination reason: Instruction limit % 122.86/17.73 % (3780755)Termination phase: Saturation % 122.86/17.73 % (3780755)Time elapsed: 2.659 s % 122.86/17.73 % (3780755)Peak memory usage: 197 MB % 122.86/17.73 % (3780755)Instructions burned: 8175 (million) % 122.86/17.73 % (3780761)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3348821283:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 122.86/17.73 % (3780753)Instruction limit reached! % 122.86/17.73 % (3780753)------------------------------ % 122.86/17.73 % (3780753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.86/17.73 % (3780753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.86/17.73 % (3780753)CaDiCaL version: 2.1.3 % 122.86/17.73 % (3780753)Termination reason: Instruction limit % 122.86/17.73 % (3780753)Termination phase: Saturation % 122.86/17.73 % (3780753)Time elapsed: 3.421 s % 122.86/17.73 % (3780753)Peak memory usage: 61 MB % 122.86/17.73 % (3780753)Instructions burned: 22569 (million) % 122.86/17.73 % (3780763)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=875909739:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 122.86/17.73 % (3780757)Instruction limit reached! % 122.86/17.73 % (3780757)------------------------------ % 122.86/17.73 % (3780757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.86/17.73 % (3780757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.86/17.73 % (3780757)CaDiCaL version: 2.1.3 % 122.86/17.73 % (3780757)Termination reason: Instruction limit % 122.86/17.73 % (3780757)Termination phase: Saturation % 122.86/17.73 % (3780757)Time elapsed: 2.728 s % 122.86/17.73 % (3780757)Peak memory usage: 99 MB % 122.86/17.73 % (3780757)Instructions burned: 9158 (million) % 122.86/17.73 % (3780765)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3863611820:i=14134_2913 on theBenchmark for (2913ds/14134Mi) % 122.86/17.73 % Detected minimum model sizes of [5] % 122.86/17.73 % Detected maximum model sizes of [max] % 122.86/17.73 % (3780761)Cannot represent all propositional literals internally % 122.86/17.73 % (3780761)Refutation not found, incomplete strategy % 122.86/17.73 % (3780761)------------------------------ % 122.86/17.73 % (3780761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.86/17.73 % (3780761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.86/17.73 % (3780761)CaDiCaL version: 2.1.3 % 122.86/17.73 % (3780761)Termination reason: Refutation not found, incomplete strategy % 122.86/17.73 % (3780761)Time elapsed: 1.522 s % 122.86/17.73 % (3780761)Peak memory usage: 80 MB % 122.86/17.73 % (3780761)Instructions burned: 5395 (million) % 122.86/17.73 % (3780761)------------------------------ % 122.86/17.73 % (3780761)------------------------------ % 122.86/17.73 % (3780767)dis+33_16_sil=32000:sac=on:random_seed=4100120195:i=15851:nm=0_2907 on theBenchmark for (2907ds/15851Mi) % 150.33/21.60 % (3780743)Instruction limit reached! % 150.33/21.60 % (3780743)------------------------------ % 150.33/21.60 % (3780743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.33/21.60 % (3780743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.33/21.60 % (3780743)CaDiCaL version: 2.1.3 % 150.33/21.60 % (3780743)Termination reason: Instruction limit % 150.33/21.60 % (3780743)Termination phase: Saturation % 150.33/21.60 % (3780743)Time elapsed: 8.451 s % 150.33/21.60 % (3780743)Peak memory usage: 781 MB % 150.33/21.60 % (3780743)Instructions burned: 29343 (million) % 150.33/21.60 % (3780763)Instruction limit reached! % 150.33/21.60 % (3780763)------------------------------ % 150.33/21.60 % (3780763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.33/21.60 % (3780763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.33/21.60 % (3780763)CaDiCaL version: 2.1.3 % 150.33/21.60 % (3780763)Termination reason: Instruction limit % 150.33/21.60 % (3780763)Termination phase: Saturation % 150.33/21.60 % (3780763)Time elapsed: 3.808 s % 150.33/21.60 % (3780763)Peak memory usage: 166 MB % 150.33/21.60 % (3780763)Instructions burned: 11404 (million) % 150.33/21.60 % (3780769)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2265871369:avsq=on:i=17627:add=on:amm=off_2880 on theBenchmark for (2880ds/17627Mi) % 150.33/21.60 % (3780771)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1620792155:s2a=on:i=53295_2880 on theBenchmark for (2880ds/53295Mi) % 150.33/21.60 % (3780759)Instruction limit reached! % 150.33/21.60 % (3780759)------------------------------ % 150.33/21.60 % (3780759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.33/21.60 % (3780759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.33/21.60 % (3780759)CaDiCaL version: 2.1.3 % 150.33/21.60 % (3780759)Termination reason: Instruction limit % 150.33/21.60 % (3780759)Termination phase: Saturation % 150.33/21.60 % (3780759)Time elapsed: 6.621 s % 150.33/21.60 % (3780759)Peak memory usage: 128 MB % 150.33/21.60 % (3780759)Instructions burned: 20142 (million) % 150.33/21.60 % (3780773)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2406855073:i=26857:ins=20_2873 on theBenchmark for (2873ds/26857Mi) % 150.33/21.60 % (3780765)Instruction limit reached! % 150.33/21.60 % (3780765)------------------------------ % 150.33/21.60 % (3780765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.33/21.60 % (3780765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.33/21.60 % (3780765)CaDiCaL version: 2.1.3 % 150.33/21.60 % (3780765)Termination reason: Instruction limit % 150.33/21.60 % (3780765)Termination phase: Saturation % 150.33/21.60 % (3780765)Time elapsed: 4.927 s % 150.33/21.60 % (3780765)Peak memory usage: 159 MB % 150.33/21.60 % (3780765)Instructions burned: 14134 (million) % 150.33/21.60 % (3780775)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=447174288:i=28120:bs=on:fsr=off_2864 on theBenchmark for (2864ds/28120Mi) % 150.33/21.60 % (3780767)Instruction limit reached! % 150.33/21.60 % (3780767)------------------------------ % 150.33/21.60 % (3780767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.33/21.60 % (3780767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.33/21.60 % (3780767)CaDiCaL version: 2.1.3 % 150.33/21.60 % (3780767)Termination reason: Instruction limit % 150.33/21.60 % (3780767)Termination phase: Saturation % 150.33/21.60 % (3780767)Time elapsed: 4.675 s % 150.33/21.60 % (3780767)Peak memory usage: 220 MB % 150.33/21.60 % (3780767)Instructions burned: 15855 (million) % 150.33/21.60 % (3780777)fmb+10_1_sil=256000:fmbss=7:random_seed=2584194152:fmbsr=1.6:i=182295_2860 on theBenchmark for (2860ds/182295Mi) % 150.33/21.60 % Detected minimum model sizes of [5] % 150.33/21.60 % Detected maximum model sizes of [max] % 150.33/21.60 % (3780773)Cannot represent all propositional literals internally % 150.33/21.60 % (3780773)Refutation not found, incomplete strategy % 150.33/21.60 % (3780773)------------------------------ % 150.33/21.60 % (3780773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.33/21.60 % (3780773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.33/21.60 % (3780773)CaDiCaL version: 2.1.3 % 150.33/21.60 % (3780773)Termination reason: Refutation not found, incomplete strategy % 150.33/21.60 % (3780773)Time elapsed: 1.420 s % 150.33/21.60 % (3780773)Peak memory usage: 78 MB % 150.33/21.60 % (3780773)Instructions burned: 5171 (million) % 150.33/21.60 % (3780773)------------------------------ % 150.33/21.60 % (3780773)------------------------------ % 162.35/23.25 % (3780779)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3227073174:i=44625:gsp=on_2859 on theBenchmark for (2859ds/44625Mi) % 162.35/23.25 % Detected minimum model sizes of [5] % 162.35/23.25 % Detected maximum model sizes of [max] % 162.35/23.25 % (3780777)Cannot represent all propositional literals internally % 162.35/23.25 % (3780777)Refutation not found, incomplete strategy % 162.35/23.25 % (3780777)------------------------------ % 162.35/23.25 % (3780777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.25 % (3780777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.25 % (3780777)CaDiCaL version: 2.1.3 % 162.35/23.25 % (3780777)Termination reason: Refutation not found, incomplete strategy % 162.35/23.25 % (3780777)Time elapsed: 1.428 s % 162.35/23.25 % (3780777)Peak memory usage: 78 MB % 162.35/23.25 % (3780777)Instructions burned: 5170 (million) % 162.35/23.25 % (3780777)------------------------------ % 162.35/23.25 % (3780777)------------------------------ % 162.35/23.25 % (3780781)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=390383003:i=160505_2845 on theBenchmark for (2845ds/160505Mi) % 162.35/23.25 % Detected minimum model sizes of [5] % 162.35/23.25 % Detected maximum model sizes of [max] % 162.35/23.25 % (3780779)Cannot represent all propositional literals internally % 162.35/23.25 % (3780779)Refutation not found, incomplete strategy % 162.35/23.25 % (3780779)------------------------------ % 162.35/23.25 % (3780779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.25 % (3780779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.25 % (3780779)CaDiCaL version: 2.1.3 % 162.35/23.25 % (3780779)Termination reason: Refutation not found, incomplete strategy % 162.35/23.25 % (3780779)Time elapsed: 2.071 s % 162.35/23.25 % (3780779)Peak memory usage: 101 MB % 162.35/23.25 % (3780779)Instructions burned: 7541 (million) % 162.35/23.25 % (3780779)------------------------------ % 162.35/23.25 % (3780779)------------------------------ % 162.35/23.25 % (3780783)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=388710738:fmbsr=1.3:i=225729_2838 on theBenchmark for (2838ds/225729Mi) % 162.35/23.25 % (3780769)Instruction limit reached! % 162.35/23.25 % (3780769)------------------------------ % 162.35/23.25 % (3780769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.25 % (3780769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.25 % (3780769)CaDiCaL version: 2.1.3 % 162.35/23.25 % (3780769)Termination reason: Instruction limit % 162.35/23.25 % (3780769)Termination phase: Saturation % 162.35/23.25 % (3780769)Time elapsed: 4.531 s % 162.35/23.25 % (3780769)Peak memory usage: 124 MB % 162.35/23.25 % (3780769)Instructions burned: 17628 (million) % 162.35/23.25 % (3780785)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=4227419648:fmbsr=2:i=185024:ins=7_2835 on theBenchmark for (2835ds/185024Mi) % 162.35/23.25 % Detected minimum model sizes of [5] % 162.35/23.25 % Detected maximum model sizes of [max] % 162.35/23.25 % (3780781)Cannot represent all propositional literals internally % 162.35/23.25 % (3780781)Refutation not found, incomplete strategy % 162.35/23.25 % (3780781)------------------------------ % 162.35/23.25 % (3780781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.25 % (3780781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.25 % (3780781)CaDiCaL version: 2.1.3 % 162.35/23.25 % (3780781)Termination reason: Refutation not found, incomplete strategy % 162.35/23.25 % (3780781)Time elapsed: 1.428 s % 162.35/23.25 % (3780781)Peak memory usage: 78 MB % 162.35/23.25 % (3780781)Instructions burned: 5170 (million) % 162.35/23.25 % (3780781)------------------------------ % 162.35/23.25 % (3780781)------------------------------ % 162.35/23.25 % (3780787)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=447664014:rtra=on_2831 on theBenchmark for (2831ds/0Mi) % 162.35/23.25 % Detected minimum model sizes of [5] % 162.35/23.25 % Detected maximum model sizes of [max] % 162.35/23.25 % (3780783)Cannot represent all propositional literals internally % 162.35/23.25 % (3780783)Refutation not found, incomplete strategy % 162.35/23.25 % (3780783)------------------------------ % 162.35/23.25 % (3780783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 162.35/23.25 % (3780783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.35/23.25 % (3780783)CaDiCaL version: 2.1.3 % 162.35/23.25 % (3780783)Termination reason: Refutation not found, incomplete strategy % 162.35/23.25 % (3780783)Time elapsed: 1.422 s % 162.35/23.25 % (3780783)Peak memory usage: 78 MB % 162.35/23.25 % (3780783)Instructions burned: 5170 (million) % 162.35/23.25 % (3780783)------------------------------ % 173.63/24.95 % (3780783)------------------------------ % 173.63/24.95 % (3780789)% WARNING: option uhcvi not known. % 173.63/24.95 % (3780789)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3042701107:i=271062:add=off:rtra=on:rawr=on_2823 on theBenchmark for (2823ds/271062Mi) % 173.63/24.95 % Detected minimum model sizes of [5] % 173.63/24.95 % Detected maximum model sizes of [max] % 173.63/24.95 % (3780785)Cannot represent all propositional literals internally % 173.63/24.95 % (3780785)Refutation not found, incomplete strategy % 173.63/24.95 % (3780785)------------------------------ % 173.63/24.95 % (3780785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.63/24.95 % (3780785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.63/24.95 % (3780785)CaDiCaL version: 2.1.3 % 173.63/24.95 % (3780785)Termination reason: Refutation not found, incomplete strategy % 173.63/24.95 % (3780785)Time elapsed: 1.433 s % 173.63/24.95 % (3780785)Peak memory usage: 78 MB % 173.63/24.95 % (3780785)Instructions burned: 5171 (million) % 173.63/24.95 % (3780785)------------------------------ % 173.63/24.95 % (3780785)------------------------------ % 173.63/24.95 % (3780791)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2916032726:i=176048:add=on:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/176048Mi) % 173.63/24.95 % (3780681)Instruction limit reached! % 173.63/24.95 % (3780681)------------------------------ % 173.63/24.95 % (3780681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.63/24.95 % (3780681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.63/24.95 % (3780681)CaDiCaL version: 2.1.3 % 173.63/24.95 % (3780681)Termination reason: Instruction limit % 173.63/24.95 % (3780681)Termination phase: Saturation % 173.63/24.95 % (3780681)Time elapsed: 20.892 s % 173.63/24.95 % (3780681)Peak memory usage: 547 MB % 173.63/24.95 % (3780681)Instructions burned: 88026 (million) % 173.63/24.95 % (3780793)dis+10_1_sil=32000:si=on:sp=arity:random_seed=309179997:i=206:fgj=on:rtra=on_2789 on theBenchmark for (2789ds/206Mi) % 173.63/24.95 % (3780793)Instruction limit reached! % 173.63/24.95 % (3780793)------------------------------ % 173.63/24.95 % (3780793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.63/24.95 % (3780793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.63/24.95 % (3780793)CaDiCaL version: 2.1.3 % 173.63/24.95 % (3780793)Termination reason: Instruction limit % 173.63/24.95 % (3780793)Termination phase: Property scanning % 173.63/24.95 % (3780793)Time elapsed: 0.090 s % 173.63/24.95 % (3780793)Peak memory usage: 27 MB % 173.63/24.95 % (3780793)Instructions burned: 208 (million) % 173.63/24.95 % (3780795)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3475607288:i=232:rtra=on_2788 on theBenchmark for (2788ds/232Mi) % 173.63/24.95 % (3780795)Instruction limit reached! % 173.63/24.95 % (3780795)------------------------------ % 173.63/24.95 % (3780795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.63/24.95 % (3780795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.63/24.95 % (3780795)CaDiCaL version: 2.1.3 % 173.63/24.95 % (3780795)Termination reason: Instruction limit % 173.63/24.95 % (3780795)Termination phase: Property scanning % 173.63/24.95 % (3780795)Time elapsed: 0.090 s % 173.63/24.95 % (3780795)Peak memory usage: 27 MB % 173.63/24.95 % (3780795)Instructions burned: 233 (million) % 173.63/24.95 % (3780797)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3771300019:i=262:rtra=on_2787 on theBenchmark for (2787ds/262Mi) % 173.63/24.95 % (3780797)Instruction limit reached! % 173.63/24.95 % (3780797)------------------------------ % 173.63/24.95 % (3780797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 173.63/24.95 % (3780797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.63/24.95 % (3780797)CaDiCaL version: 2.1.3 % 173.63/24.95 % (3780797)Termination reason: Instruction limit % 173.63/24.95 % (3780797)Termination phase: Property scanning % 173.63/24.95 % (3780797)Time elapsed: 0.106 s % 173.63/24.95 % (3780797)Peak memory usage: 27 MB % 173.63/24.95 % (3780797)Instructions burned: 262 (million) % 173.63/24.95 % (3780799)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1013758602:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2786 on theBenchmark for (2786ds/318Mi) % 173.63/24.95 % (3780799)Instruction limit reached! % 173.63/24.95 % (3780799)------------------------------ % 173.63/24.95 % (3780799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.45/31.04 % (3780799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.45/31.04 % (3780799)CaDiCaL version: 2.1.3 % 217.45/31.04 % (3780799)Termination reason: Instruction limit % 217.45/31.04 % (3780799)Termination phase: Function definition elimination % 217.45/31.04 % (3780799)Time elapsed: 0.116 s % 217.45/31.04 % (3780799)Peak memory usage: 27 MB % 217.45/31.04 % (3780799)Instructions burned: 323 (million) % 217.45/31.04 % (3780801)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3433890204:i=1428:nm=2:rtra=on_2785 on theBenchmark for (2785ds/1428Mi) % 217.45/31.04 % (3780801)Instruction limit reached! % 217.45/31.04 % (3780801)------------------------------ % 217.45/31.04 % (3780801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.45/31.04 % (3780801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.45/31.04 % (3780801)CaDiCaL version: 2.1.3 % 217.45/31.04 % (3780801)Termination reason: Instruction limit % 217.45/31.04 % (3780801)Termination phase: Function definition elimination % 217.45/31.04 % (3780801)Time elapsed: 0.323 s % 217.45/31.04 % (3780801)Peak memory usage: 29 MB % 217.45/31.04 % (3780801)Instructions burned: 1433 (million) % 217.45/31.04 % (3780803)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2917160019:i=262:bd=preordered:rtra=on:fsd=on_2781 on theBenchmark for (2781ds/262Mi) % 217.45/31.04 % (3780803)Instruction limit reached! % 217.45/31.04 % (3780803)------------------------------ % 217.45/31.04 % (3780803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.45/31.04 % (3780803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.45/31.04 % (3780803)CaDiCaL version: 2.1.3 % 217.45/31.04 % (3780803)Termination reason: Instruction limit % 217.45/31.04 % (3780803)Termination phase: Property scanning % 217.45/31.04 % (3780803)Time elapsed: 0.102 s % 217.45/31.04 % (3780803)Peak memory usage: 27 MB % 217.45/31.04 % (3780803)Instructions burned: 263 (million) % 217.45/31.04 % (3780805)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=65709062:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2780 on theBenchmark for (2780ds/1368Mi) % 217.45/31.04 % (3780805)Instruction limit reached! % 217.45/31.04 % (3780805)------------------------------ % 217.45/31.04 % (3780805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.45/31.04 % (3780805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.45/31.04 % (3780805)CaDiCaL version: 2.1.3 % 217.45/31.04 % (3780805)Termination reason: Instruction limit % 217.45/31.04 % (3780805)Termination phase: Function definition elimination % 217.45/31.04 % (3780805)Time elapsed: 0.323 s % 217.45/31.04 % (3780805)Peak memory usage: 27 MB % 217.45/31.04 % (3780805)Instructions burned: 1369 (million) % 217.45/31.04 % (3780807)ott-21_1_sil=16000:si=on:fs=off:random_seed=3052642462:i=360:av=off:fsr=off:rtra=on_2777 on theBenchmark for (2777ds/360Mi) % 217.45/31.04 % (3780807)Instruction limit reached! % 217.45/31.04 % (3780807)------------------------------ % 217.45/31.04 % (3780807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.45/31.04 % (3780807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.45/31.04 % (3780807)CaDiCaL version: 2.1.3 % 217.45/31.04 % (3780807)Termination reason: Instruction limit % 217.45/31.04 % (3780807)Termination phase: Function definition elimination % 217.45/31.04 % (3780807)Time elapsed: 0.119 s % 217.45/31.04 % (3780807)Peak memory usage: 27 MB % 217.45/31.04 % (3780807)Instructions burned: 360 (million) % 217.45/31.04 % (3780809)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1415978610:i=954:bd=all:rtra=on_2776 on theBenchmark for (2776ds/954Mi) % 217.45/31.04 % (3780809)Instruction limit reached! % 217.45/31.04 % (3780809)------------------------------ % 217.45/31.04 % (3780809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 217.45/31.04 % (3780809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.45/31.04 % (3780809)CaDiCaL version: 2.1.3 % 217.45/31.04 % (3780809)Termination reason: Instruction limit % 217.45/31.04 % (3780809)Termination phase: Saturation % 217.45/31.04 % (3780809)Time elapsed: 0.333 s % 217.45/31.04 % (3780809)Peak memory usage: 33 MB % 217.45/31.04 % (3780809)Instructions burned: 954 (million) % 217.45/31.04 % (3780811)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1893884294:fmbsr=1.3:i=1730:ins=25:rtra=on_2772 on theBenchmark for (2772ds/1730Mi) % 217.45/31.04 % (3780811)Instruction limit reached! % 217.45/31.04 % (3780811)------------------------------ % 254.00/36.24 % (3780811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.00/36.24 % (3780811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.00/36.24 % (3780811)CaDiCaL version: 2.1.3 % 254.00/36.24 % (3780811)Termination reason: Instruction limit % 254.00/36.24 % (3780811)Termination phase: Function definition elimination % 254.00/36.24 % (3780811)Time elapsed: 0.379 s % 254.00/36.24 % (3780811)Peak memory usage: 27 MB % 254.00/36.24 % (3780811)Instructions burned: 1732 (million) % 254.00/36.24 % (3780813)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3538053816:i=2358:rtra=on_2768 on theBenchmark for (2768ds/2358Mi) % 254.00/36.24 % (3780813)Instruction limit reached! % 254.00/36.24 % (3780813)------------------------------ % 254.00/36.24 % (3780813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.00/36.24 % (3780813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.00/36.24 % (3780813)CaDiCaL version: 2.1.3 % 254.00/36.24 % (3780813)Termination reason: Instruction limit % 254.00/36.24 % (3780813)Termination phase: Saturation % 254.00/36.24 % (3780813)Time elapsed: 0.810 s % 254.00/36.24 % (3780813)Peak memory usage: 54 MB % 254.00/36.24 % (3780813)Instructions burned: 2360 (million) % 254.00/36.24 % (3780815)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2579329075:i=1778:ins=1:rtra=on_2760 on theBenchmark for (2760ds/1778Mi) % 254.00/36.24 % (3780775)Instruction limit reached! % 254.00/36.24 % (3780775)------------------------------ % 254.00/36.24 % (3780775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.00/36.24 % (3780775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.00/36.24 % (3780775)CaDiCaL version: 2.1.3 % 254.00/36.24 % (3780775)Termination reason: Instruction limit % 254.00/36.24 % (3780775)Termination phase: Saturation % 254.00/36.24 % (3780775)Time elapsed: 10.552 s % 254.00/36.24 % (3780775)Peak memory usage: 338 MB % 254.00/36.24 % (3780775)Instructions burned: 28121 (million) % 254.00/36.24 % (3780817)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2074103078:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2758 on theBenchmark for (2758ds/1384Mi) % 254.00/36.24 % (3780815)Instruction limit reached! % 254.00/36.24 % (3780815)------------------------------ % 254.00/36.24 % (3780815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.00/36.24 % (3780815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.00/36.24 % (3780815)CaDiCaL version: 2.1.3 % 254.00/36.24 % (3780815)Termination reason: Instruction limit % 254.00/36.24 % (3780815)Termination phase: Function definition elimination % 254.00/36.24 % (3780815)Time elapsed: 0.382 s % 254.00/36.24 % (3780815)Peak memory usage: 27 MB % 254.00/36.24 % (3780815)Instructions burned: 1783 (million) % 254.00/36.24 % (3780819)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3604389151:i=1758:kws=inv_precedence:fsr=off:rtra=on_2756 on theBenchmark for (2756ds/1758Mi) % 254.00/36.24 % (3780817)Instruction limit reached! % 254.00/36.24 % (3780817)------------------------------ % 254.00/36.24 % (3780817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.00/36.24 % (3780817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.00/36.24 % (3780817)CaDiCaL version: 2.1.3 % 254.00/36.24 % (3780817)Termination reason: Instruction limit % 254.00/36.24 % (3780817)Termination phase: Function definition elimination % 254.00/36.24 % (3780817)Time elapsed: 0.308 s % 254.00/36.24 % (3780817)Peak memory usage: 27 MB % 254.00/36.24 % (3780817)Instructions burned: 1386 (million) % 254.00/36.24 % (3780821)fmb+10_1_sil=64000:si=on:random_seed=2708732807:i=44122:nm=2:rtra=on:gsp=on_2754 on theBenchmark for (2754ds/44122Mi) % 254.00/36.24 % (3780819)Instruction limit reached! % 254.00/36.24 % (3780819)------------------------------ % 254.00/36.24 % (3780819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 254.00/36.24 % (3780819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.00/36.24 % (3780819)CaDiCaL version: 2.1.3 % 254.00/36.24 % (3780819)Termination reason: Instruction limit % 254.00/36.24 % (3780819)Termination phase: Saturation % 254.00/36.24 % (3780819)Time elapsed: 0.453 s % 254.00/36.24 % (3780819)Peak memory usage: 40 MB % 254.00/36.24 % (3780819)Instructions burned: 1763 (million) % 254.00/36.24 % (3780823)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=824685988:i=19030:nm=5:rtra=on_2751 on theBenchmark for (2751ds/19030Mi) % 300.51/42.83 % (3780771)Instruction limit reached! % 300.51/42.83 % (3780771)------------------------------ % 300.51/42.83 % (3780771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.83 % (3780771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.83 % (3780771)CaDiCaL version: 2.1.3 % 300.51/42.83 % (3780771)Termination reason: Instruction limit % 300.51/42.83 % (3780771)Termination phase: Saturation % 300.51/42.83 % (3780771)Time elapsed: 15.032 s % 300.51/42.83 % (3780771)Peak memory usage: 219 MB % 300.51/42.83 % (3780771)Instructions burned: 53299 (million) % 300.51/42.83 % (3780825)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1190980031:fmbsr=1.7:i=1840:rtra=on_2729 on theBenchmark for (2729ds/1840Mi) % 300.51/42.83 % (3780825)Instruction limit reached! % 300.51/42.83 % (3780825)------------------------------ % 300.51/42.83 % (3780825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.83 % (3780825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.83 % (3780825)CaDiCaL version: 2.1.3 % 300.51/42.83 % (3780825)Termination reason: Instruction limit % 300.51/42.83 % (3780825)Termination phase: Function definition elimination % 300.51/42.83 % (3780825)Time elapsed: 0.394 s % 300.51/42.83 % (3780825)Peak memory usage: 27 MB % 300.51/42.83 % (3780825)Instructions burned: 1842 (million) % 300.51/42.83 % (3780827)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3824212547:i=10262:rtra=on_2725 on theBenchmark for (2725ds/10262Mi) % 300.51/42.83 % (3780827)Instruction limit reached! % 300.51/42.83 % (3780827)------------------------------ % 300.51/42.83 % (3780827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.83 % (3780827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.83 % (3780827)CaDiCaL version: 2.1.3 % 300.51/42.83 % (3780827)Termination reason: Instruction limit % 300.51/42.83 % (3780827)Termination phase: Property scanning % 300.51/42.83 % (3780827)Time elapsed: 1.871 s % 300.51/42.83 % (3780827)Peak memory usage: 28 MB % 300.51/42.83 % (3780827)Instructions burned: 10263 (million) % 300.51/42.83 % (3780829)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3434144323:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2706 on theBenchmark for (2706ds/2944Mi) % 300.51/42.83 % (3780821)Instruction limit reached! % 300.51/42.83 % (3780821)------------------------------ % 300.51/42.83 % (3780821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.83 % (3780821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.83 % (3780821)CaDiCaL version: 2.1.3 % 300.51/42.83 % (3780821)Termination reason: Instruction limit % 300.51/42.83 % (3780821)Termination phase: Finite model building preprocessing % 300.51/42.83 % (3780821)Time elapsed: 5.579 s % 300.51/42.83 % (3780821)Peak memory usage: 84 MB % 300.51/42.83 % (3780821)Instructions burned: 44123 (million) % 300.51/42.83 % (3780831)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3931297261:i=12648:rtra=on_2698 on theBenchmark for (2698ds/12648Mi) % 300.51/42.83 % (3780829)Instruction limit reached! % 300.51/42.83 % (3780829)------------------------------ % 300.51/42.83 % (3780829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.83 % (3780829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.83 % (3780829)CaDiCaL version: 2.1.3 % 300.51/42.83 % (3780829)Termination reason: Instruction limit % 300.51/42.83 % (3780829)Termination phase: Saturation % 300.51/42.83 % (3780829)Time elapsed: 0.834 s % 300.51/42.83 % (3780829)Peak memory usage: 40 MB % 300.51/42.83 % (3780829)Instructions burned: 2944 (million) % 300.51/42.83 % (3780833)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2747535801:fmbsr=2.30978:i=4348:rtra=on_2698 on theBenchmark for (2698ds/4348Mi) % 300.51/42.83 % (3780823)Instruction limit reached! % 300.51/42.83 % (3780823)------------------------------ % 300.51/42.83 % (3780823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.51/42.83 % (3780823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.51/42.83 % (3780823)CaDiCaL version: 2.1.3 % 300.51/42.83 % (3780823)Termination reason: Instruction limit % 300.51/42.83 % (3780823)Termination phase: Finite model building preprocessing % 300.51/42.83 % (3780823)Time elapsed: 6.066 s % 300.51/42.83 % (3780823)Peak memory usage: 62 MB % 300.51/42.83 % (3780823)Instructions burned: 19030 (million) % 300.51/42.83 % (3780835)ott-2_1_sil=16000:si % 300.51/42.83 Terminated % 300.51/42.83 % Vampire exiting %------------------------------------------------------------------------------