%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV783_5 : TPTP v9.3.1. Released v6.0.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:24 PM UTC 2026 % Result : Timeout 300.01s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV783_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.17 % Computer : n015.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 12:35:17 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.20 Running first-order model finding % 0.08/0.20 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.43/1.37 % (2600336)Will run a generic schedule for satisfiability detection. % 7.43/1.37 % (2600343)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1292127885:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.43/1.37 % (2600342)% WARNING: option uhcvi not known. % 7.43/1.37 % (2600341)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2300567081_2999 on theBenchmark for (2999ds/0Mi) % 7.43/1.37 % (2600342)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3095250891:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.43/1.37 % (2600344)dis+10_1_sil=32000:sp=arity:random_seed=3369685798:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.43/1.37 % (2600345)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2393284125:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.43/1.37 % (2600347)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1995243423:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.43/1.37 % (2600346)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=25476134:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.43/1.37 % Exception at run slice level % 7.43/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.43/1.37 % (2600355)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3884064931:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.43/1.37 % Exception at run slice level % 7.43/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.43/1.37 % (2600357)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=971683633:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.43/1.37 % (2600344)Instruction limit reached! % 7.43/1.37 % (2600344)------------------------------ % 7.43/1.37 % (2600344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.37 % (2600344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.37 % (2600344)CaDiCaL version: 2.1.3 % 7.43/1.37 % (2600344)Termination reason: Instruction limit % 7.43/1.37 % (2600344)Termination phase: Saturation % 7.43/1.37 % (2600344)Time elapsed: 0.057 s % 7.43/1.37 % (2600344)Peak memory usage: 12 MB % 7.43/1.37 % (2600344)Instructions burned: 104 (million) % 7.43/1.37 % (2600345)Instruction limit reached! % 7.43/1.37 % (2600345)------------------------------ % 7.43/1.37 % (2600345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.37 % (2600345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.37 % (2600345)CaDiCaL version: 2.1.3 % 7.43/1.37 % (2600345)Termination reason: Instruction limit % 7.43/1.37 % (2600345)Termination phase: Saturation % 7.43/1.37 % (2600345)Time elapsed: 0.062 s % 7.43/1.37 % (2600345)Peak memory usage: 12 MB % 7.43/1.37 % (2600345)Instructions burned: 117 (million) % 7.43/1.37 % (2600346)Instruction limit reached! % 7.43/1.37 % (2600346)------------------------------ % 7.43/1.37 % (2600346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.37 % (2600346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.37 % (2600346)CaDiCaL version: 2.1.3 % 7.43/1.37 % (2600346)Termination reason: Instruction limit % 7.43/1.37 % (2600346)Termination phase: Saturation % 7.43/1.37 % (2600346)Time elapsed: 0.071 s % 7.43/1.37 % (2600346)Peak memory usage: 12 MB % 7.43/1.37 % (2600346)Instructions burned: 132 (million) % 7.43/1.37 % (2600359)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=407123338:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.43/1.37 % (2600347)Instruction limit reached! % 7.43/1.37 % (2600347)------------------------------ % 7.43/1.37 % (2600347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.43/1.37 % (2600347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.43/1.37 % (2600347)CaDiCaL version: 2.1.3 % 7.43/1.37 % (2600347)Termination reason: Instruction limit % 7.43/1.37 % (2600347)Termination phase: Saturation % 7.43/1.37 % (2600347)Time elapsed: 0.079 s % 7.43/1.37 % (2600347)Peak memory usage: 13 MB % 7.43/1.37 % (2600347)Instructions burned: 161 (million) % 7.43/1.37 % (2600360)ott-21_1_sil=16000:fs=off:random_seed=750641254:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.43/1.37 % (2600361)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3888891672:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 22.37/3.44 % (2600363)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=788056418:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 22.37/3.44 % Exception at run slice level % 22.37/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.37/3.44 % (2600367)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=298112409:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 22.37/3.44 % (2600357)Instruction limit reached! % 22.37/3.44 % (2600357)------------------------------ % 22.37/3.44 % (2600357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.37/3.44 % (2600357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.37/3.44 % (2600357)CaDiCaL version: 2.1.3 % 22.37/3.44 % (2600357)Termination reason: Instruction limit % 22.37/3.44 % (2600357)Termination phase: Saturation % 22.37/3.44 % (2600357)Time elapsed: 0.071 s % 22.37/3.44 % (2600357)Peak memory usage: 12 MB % 22.37/3.44 % (2600357)Instructions burned: 132 (million) % 22.37/3.44 % (2600369)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3802273055:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 22.37/3.44 % Exception at run slice level % 22.37/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.37/3.44 % (2600360)Instruction limit reached! % 22.37/3.44 % (2600360)------------------------------ % 22.37/3.44 % (2600360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.37/3.44 % (2600360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.37/3.44 % (2600360)CaDiCaL version: 2.1.3 % 22.37/3.44 % (2600360)Termination reason: Instruction limit % 22.37/3.44 % (2600360)Termination phase: Saturation % 22.37/3.44 % (2600360)Time elapsed: 0.087 s % 22.37/3.44 % (2600360)Peak memory usage: 12 MB % 22.37/3.44 % (2600360)Instructions burned: 181 (million) % 22.37/3.44 % (2600371)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=3745624786:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 22.37/3.44 % (2600372)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3936183269:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 22.37/3.44 % (2600361)Instruction limit reached! % 22.37/3.44 % (2600361)------------------------------ % 22.37/3.44 % (2600361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.37/3.44 % (2600361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.37/3.44 % (2600361)CaDiCaL version: 2.1.3 % 22.37/3.44 % (2600361)Termination reason: Instruction limit % 22.37/3.44 % (2600361)Termination phase: Saturation % 22.37/3.44 % (2600361)Time elapsed: 0.246 s % 22.37/3.44 % (2600361)Peak memory usage: 13 MB % 22.37/3.44 % (2600361)Instructions burned: 478 (million) % 22.37/3.44 % (2600375)fmb+10_1_sil=64000:random_seed=1621542122:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 22.37/3.44 % (2600375)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 22.37/3.44 % Exception at run slice level % 22.37/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.37/3.44 % (2600377)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1475406619:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi) % 22.37/3.44 % Exception at run slice level % 22.37/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 22.37/3.44 % (2600359)Instruction limit reached! % 22.37/3.44 % (2600359)------------------------------ % 22.37/3.44 % (2600359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 22.37/3.44 % (2600359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.37/3.44 % (2600359)CaDiCaL version: 2.1.3 % 22.37/3.44 % (2600359)Termination reason: Instruction limit % 22.37/3.44 % (2600359)Termination phase: Saturation % 22.37/3.44 % (2600359)Time elapsed: 0.323 s % 22.37/3.44 % (2600359)Peak memory usage: 14 MB % 22.37/3.44 % (2600359)Instructions burned: 685 (million) % 22.37/3.44 % (2600379)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3591485281:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi) % 22.37/3.44 % Exception at run slice level % 22.37/3.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 95.68/13.72 % (2600380)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1831788648:i=5131_2995 on theBenchmark for (2995ds/5131Mi) % 95.68/13.72 % (2600382)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1284283751:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 95.68/13.72 % (2600382)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 95.68/13.72 % (2600371)Instruction limit reached! % 95.68/13.72 % (2600371)------------------------------ % 95.68/13.72 % (2600371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.72 % (2600371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.72 % (2600371)CaDiCaL version: 2.1.3 % 95.68/13.72 % (2600371)Termination reason: Instruction limit % 95.68/13.72 % (2600371)Termination phase: Saturation % 95.68/13.72 % (2600371)Time elapsed: 0.395 s % 95.68/13.72 % (2600371)Peak memory usage: 17 MB % 95.68/13.72 % (2600371)Instructions burned: 693 (million) % 95.68/13.72 % (2600385)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3575255850:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 95.68/13.72 % Exception at run slice level % 95.68/13.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 95.68/13.72 % (2600387)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=956803795:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 95.68/13.72 % Exception at run slice level % 95.68/13.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 95.68/13.72 % (2600389)ott-2_1_sil=16000:newcnf=on:random_seed=3349478711:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 95.68/13.72 % (2600372)Instruction limit reached! % 95.68/13.72 % (2600372)------------------------------ % 95.68/13.72 % (2600372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.72 % (2600372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.72 % (2600372)CaDiCaL version: 2.1.3 % 95.68/13.72 % (2600372)Termination reason: Instruction limit % 95.68/13.72 % (2600372)Termination phase: Saturation % 95.68/13.72 % (2600372)Time elapsed: 0.498 s % 95.68/13.72 % (2600372)Peak memory usage: 18 MB % 95.68/13.72 % (2600372)Instructions burned: 881 (million) % 95.68/13.72 % (2600391)ott+10_1_sil=32000:tgt=ground:random_seed=2579312707:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 95.68/13.72 % (2600367)Instruction limit reached! % 95.68/13.72 % (2600367)------------------------------ % 95.68/13.72 % (2600367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.72 % (2600367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.72 % (2600367)CaDiCaL version: 2.1.3 % 95.68/13.72 % (2600367)Termination reason: Instruction limit % 95.68/13.72 % (2600367)Termination phase: Saturation % 95.68/13.72 % (2600367)Time elapsed: 0.658 s % 95.68/13.72 % (2600367)Peak memory usage: 18 MB % 95.68/13.72 % (2600367)Instructions burned: 1180 (million) % 95.68/13.72 % (2600393)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=268482086:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 95.68/13.72 % Exception at run slice level % 95.68/13.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 95.68/13.72 % (2600395)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=189565944:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 95.68/13.72 % (2600389)Instruction limit reached! % 95.68/13.72 % (2600389)------------------------------ % 95.68/13.72 % (2600389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 95.68/13.72 % (2600389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.68/13.72 % (2600389)CaDiCaL version: 2.1.3 % 95.68/13.72 % (2600389)Termination reason: Instruction limit % 95.68/13.72 % (2600389)Termination phase: Saturation % 95.68/13.72 % (2600389)Time elapsed: 0.399 s % 95.68/13.72 % (2600389)Peak memory usage: 14 MB % 95.68/13.72 % (2600389)Instructions burned: 870 (million) % 95.68/13.72 % (2600397)dis+21_1_sil=32000:sas=cadical:random_seed=160269233:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 95.68/13.72 % (2600382)Instruction limit reached! % 95.68/13.72 % (2600382)------------------------------ % 95.68/13.72 % (2600382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.42/18.33 % (2600382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.42/18.33 % (2600382)CaDiCaL version: 2.1.3 % 128.42/18.33 % (2600382)Termination reason: Instruction limit % 128.42/18.33 % (2600382)Termination phase: Saturation % 128.42/18.33 % (2600382)Time elapsed: 0.681 s % 128.42/18.33 % (2600382)Peak memory usage: 18 MB % 128.42/18.33 % (2600382)Instructions burned: 1473 (million) % 128.42/18.33 % (2600399)ott+11_1_sil=16000:gs=on:random_seed=653752912:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 128.42/18.33 % (2600399)Instruction limit reached! % 128.42/18.33 % (2600399)------------------------------ % 128.42/18.33 % (2600399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.42/18.33 % (2600399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.42/18.33 % (2600399)CaDiCaL version: 2.1.3 % 128.42/18.33 % (2600399)Termination reason: Instruction limit % 128.42/18.33 % (2600399)Termination phase: Saturation % 128.42/18.33 % (2600399)Time elapsed: 1.132 s % 128.42/18.33 % (2600399)Peak memory usage: 17 MB % 128.42/18.33 % (2600399)Instructions burned: 2251 (million) % 128.42/18.33 % (2600401)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1818971918:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi) % 128.42/18.33 % Exception at run slice level % 128.42/18.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 128.42/18.33 % (2600403)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3731642532:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi) % 128.42/18.33 % (2600395)Instruction limit reached! % 128.42/18.33 % (2600395)------------------------------ % 128.42/18.33 % (2600395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.42/18.33 % (2600395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.42/18.33 % (2600395)CaDiCaL version: 2.1.3 % 128.42/18.33 % (2600395)Termination reason: Instruction limit % 128.42/18.33 % (2600395)Termination phase: Saturation % 128.42/18.33 % (2600395)Time elapsed: 1.766 s % 128.42/18.33 % (2600395)Peak memory usage: 25 MB % 128.42/18.33 % (2600395)Instructions burned: 3513 (million) % 128.42/18.33 % (2600405)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1294476755:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 128.42/18.33 % (2600380)Instruction limit reached! % 128.42/18.33 % (2600380)------------------------------ % 128.42/18.33 % (2600380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.42/18.33 % (2600380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.42/18.33 % (2600380)CaDiCaL version: 2.1.3 % 128.42/18.33 % (2600380)Termination reason: Instruction limit % 128.42/18.33 % (2600380)Termination phase: Saturation % 128.42/18.33 % (2600380)Time elapsed: 2.530 s % 128.42/18.33 % (2600380)Peak memory usage: 28 MB % 128.42/18.33 % (2600380)Instructions burned: 5131 (million) % 128.42/18.33 % (2600407)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=223876102:i=5211_2970 on theBenchmark for (2970ds/5211Mi) % 128.42/18.33 % (2600397)Instruction limit reached! % 128.42/18.33 % (2600397)------------------------------ % 128.42/18.33 % (2600397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 128.42/18.33 % (2600397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 128.42/18.34 % (2600397)CaDiCaL version: 2.1.3 % 128.42/18.34 % (2600397)Termination reason: Instruction limit % 128.42/18.34 % (2600397)Termination phase: Saturation % 128.42/18.34 % (2600397)Time elapsed: 2.043 s % 128.42/18.34 % (2600397)Peak memory usage: 34 MB % 128.42/18.34 % (2600397)Instructions burned: 3774 (million) % 128.42/18.34 % (2600409)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3900167471:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 128.42/18.34 % Exception at run slice level % 128.42/18.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 128.42/18.34 % (2600411)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=665783599:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 128.42/18.34 % Exception at run slice level % 128.42/18.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 128.42/18.34 % (2600413)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2471817297:i=14071_2967 on theBenchmark for (2967ds/14071Mi) % 128.42/18.34 % Exception at run slice level % 194.54/27.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 194.54/27.70 % (2600415)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=196829380:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi) % 194.54/27.70 % (2600391)Instruction limit reached! % 194.54/27.70 % (2600391)------------------------------ % 194.54/27.70 % (2600391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.54/27.70 % (2600391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.54/27.70 % (2600391)CaDiCaL version: 2.1.3 % 194.54/27.70 % (2600391)Termination reason: Instruction limit % 194.54/27.70 % (2600391)Termination phase: Saturation % 194.54/27.70 % (2600391)Time elapsed: 2.658 s % 194.54/27.70 % (2600391)Peak memory usage: 19 MB % 194.54/27.70 % (2600391)Instructions burned: 5115 (million) % 194.54/27.70 % (2600417)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3436179237:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi) % 194.54/27.70 % (2600403)Instruction limit reached! % 194.54/27.70 % (2600403)------------------------------ % 194.54/27.70 % (2600403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.54/27.70 % (2600403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.54/27.70 % (2600403)CaDiCaL version: 2.1.3 % 194.54/27.70 % (2600403)Termination reason: Instruction limit % 194.54/27.70 % (2600403)Termination phase: Saturation % 194.54/27.70 % (2600403)Time elapsed: 1.878 s % 194.54/27.70 % (2600403)Peak memory usage: 27 MB % 194.54/27.70 % (2600403)Instructions burned: 4593 (million) % 194.54/27.70 % (2600419)dis+10_16:1_sil=16000:random_seed=1413057129:i=9155:fsr=off_2957 on theBenchmark for (2957ds/9155Mi) % 194.54/27.70 % (2600407)Instruction limit reached! % 194.54/27.70 % (2600407)------------------------------ % 194.54/27.70 % (2600407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.54/27.70 % (2600407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.54/27.70 % (2600407)CaDiCaL version: 2.1.3 % 194.54/27.70 % (2600407)Termination reason: Instruction limit % 194.54/27.70 % (2600407)Termination phase: Saturation % 194.54/27.70 % (2600407)Time elapsed: 2.697 s % 194.54/27.70 % (2600407)Peak memory usage: 42 MB % 194.54/27.70 % (2600407)Instructions burned: 5213 (million) % 194.54/27.70 % (2600421)ott-3_8_sil=64000:random_seed=3515916154:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi) % 194.54/27.70 % (2600417)Instruction limit reached! % 194.54/27.70 % (2600417)------------------------------ % 194.54/27.70 % (2600417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.54/27.70 % (2600417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.54/27.70 % (2600417)CaDiCaL version: 2.1.3 % 194.54/27.70 % (2600417)Termination reason: Instruction limit % 194.54/27.70 % (2600417)Termination phase: Saturation % 194.54/27.70 % (2600417)Time elapsed: 4.475 s % 194.54/27.70 % (2600417)Peak memory usage: 41 MB % 194.54/27.70 % (2600417)Instructions burned: 8173 (million) % 194.54/27.70 % (2600423)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3533848772:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 194.54/27.70 % Exception at run slice level % 194.54/27.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 194.54/27.70 % (2600425)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1330885478:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 194.54/27.70 % (2600419)Instruction limit reached! % 194.54/27.70 % (2600419)------------------------------ % 194.54/27.70 % (2600419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.54/27.70 % (2600419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.54/27.70 % (2600419)CaDiCaL version: 2.1.3 % 194.54/27.70 % (2600419)Termination reason: Instruction limit % 194.54/27.70 % (2600419)Termination phase: Saturation % 194.54/27.70 % (2600419)Time elapsed: 4.628 s % 194.54/27.70 % (2600419)Peak memory usage: 52 MB % 194.54/27.70 % (2600419)Instructions burned: 9157 (million) % 194.54/27.70 % (2600427)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2045945067:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 194.54/27.70 % (2600415)Instruction limit reached! % 194.54/27.70 % (2600415)------------------------------ % 194.54/27.70 % (2600415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 194.54/27.70 % (2600415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.54/27.70 % (2600415)CaDiCaL version: 2.1.3 % 202.33/28.83 % (2600415)Termination reason: Instruction limit % 202.33/28.83 % (2600415)Termination phase: Saturation % 202.33/28.83 % (2600415)Time elapsed: 10.258 s % 202.33/28.83 % (2600415)Peak memory usage: 32 MB % 202.33/28.83 % (2600415)Instructions burned: 22565 (million) % 202.33/28.83 % (2600545)dis+33_16_sil=32000:sac=on:random_seed=381511308:i=15851:nm=0_2864 on theBenchmark for (2864ds/15851Mi) % 202.33/28.83 % (2600425)Instruction limit reached! % 202.33/28.83 % (2600425)------------------------------ % 202.33/28.83 % (2600425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.83 % (2600425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.83 % (2600425)CaDiCaL version: 2.1.3 % 202.33/28.83 % (2600425)Termination reason: Instruction limit % 202.33/28.83 % (2600425)Termination phase: Saturation % 202.33/28.83 % (2600425)Time elapsed: 7.013 s % 202.33/28.83 % (2600425)Peak memory usage: 94 MB % 202.33/28.83 % (2600425)Instructions burned: 11404 (million) % 202.33/28.83 % (2600677)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1873039390:avsq=on:i=17627:add=on:amm=off_2850 on theBenchmark for (2850ds/17627Mi) % 202.33/28.83 % (2600421)Instruction limit reached! % 202.33/28.83 % (2600421)------------------------------ % 202.33/28.83 % (2600421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.83 % (2600421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.83 % (2600421)CaDiCaL version: 2.1.3 % 202.33/28.83 % (2600421)Termination reason: Instruction limit % 202.33/28.83 % (2600421)Termination phase: Saturation % 202.33/28.83 % (2600421)Time elapsed: 9.387 s % 202.33/28.83 % (2600421)Peak memory usage: 27 MB % 202.33/28.83 % (2600421)Instructions burned: 20139 (million) % 202.33/28.83 % (2600679)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=652188450:s2a=on:i=53295_2848 on theBenchmark for (2848ds/53295Mi) % 202.33/28.83 % (2600405)Instruction limit reached! % 202.33/28.83 % (2600405)------------------------------ % 202.33/28.83 % (2600405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.83 % (2600405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.83 % (2600405)CaDiCaL version: 2.1.3 % 202.33/28.83 % (2600405)Termination reason: Instruction limit % 202.33/28.83 % (2600405)Termination phase: Saturation % 202.33/28.83 % (2600405)Time elapsed: 13.379 s % 202.33/28.83 % (2600405)Peak memory usage: 58 MB % 202.33/28.83 % (2600405)Instructions burned: 29342 (million) % 202.33/28.83 % (2600700)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1515651565:i=26857:ins=20_2839 on theBenchmark for (2839ds/26857Mi) % 202.33/28.83 % Exception at run slice level % 202.33/28.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.33/28.83 % (2600703)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2144409863:i=28120:bs=on:fsr=off_2839 on theBenchmark for (2839ds/28120Mi) % 202.33/28.83 % (2600427)Instruction limit reached! % 202.33/28.83 % (2600427)------------------------------ % 202.33/28.83 % (2600427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.83 % (2600427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.83 % (2600427)CaDiCaL version: 2.1.3 % 202.33/28.83 % (2600427)Termination reason: Instruction limit % 202.33/28.83 % (2600427)Termination phase: Saturation % 202.33/28.83 % (2600427)Time elapsed: 9.065 s % 202.33/28.83 % (2600427)Peak memory usage: 75 MB % 202.33/28.83 % (2600427)Instructions burned: 14136 (million) % 202.33/28.83 % (2600730)fmb+10_1_sil=256000:fmbss=7:random_seed=4255452164:fmbsr=1.6:i=182295_2820 on theBenchmark for (2820ds/182295Mi) % 202.33/28.83 % Exception at run slice level % 202.33/28.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.33/28.83 % (2600732)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2431049126:i=44625:gsp=on_2819 on theBenchmark for (2819ds/44625Mi) % 202.33/28.83 % (2600732)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 202.33/28.83 % Exception at run slice level % 202.33/28.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.33/28.83 % (2600734)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3182823815:i=160505_2819 on theBenchmark for (2819ds/160505Mi) % 202.33/28.83 % Exception at run slice level % 202.33/28.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 202.33/28.83 % (2600737)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3453679967:fmbsr=1.3:i=225729_2819 on theBenchmark for (2819ds/225729Mi) % 216.45/30.89 % Exception at run slice level % 216.45/30.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 216.45/30.89 % (2600739)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1909846866:fmbsr=2:i=185024:ins=7_2818 on theBenchmark for (2818ds/185024Mi) % 216.45/30.89 % Exception at run slice level % 216.45/30.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 216.45/30.89 % (2600741)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4049540318:rtra=on_2818 on theBenchmark for (2818ds/0Mi) % 216.45/30.89 % Exception at run slice level % 216.45/30.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 216.45/30.89 % (2600744)% WARNING: option uhcvi not known. % 216.45/30.89 % (2600744)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2766233749:i=271062:add=off:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/271062Mi) % 216.45/30.89 % (2600545)Instruction limit reached! % 216.45/30.89 % (2600545)------------------------------ % 216.45/30.89 % (2600545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.45/30.89 % (2600545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.45/30.89 % (2600545)CaDiCaL version: 2.1.3 % 216.45/30.89 % (2600545)Termination reason: Instruction limit % 216.45/30.89 % (2600545)Termination phase: Saturation % 216.45/30.89 % (2600545)Time elapsed: 10.988 s % 216.45/30.89 % (2600545)Peak memory usage: 33 MB % 216.45/30.89 % (2600545)Instructions burned: 15852 (million) % 216.45/30.89 % (2600769)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1563998492:i=176048:add=on:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/176048Mi) % 216.45/30.89 % (2600343)Instruction limit reached! % 216.45/30.89 % (2600343)------------------------------ % 216.45/30.89 % (2600343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.45/30.89 % (2600343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.45/30.89 % (2600343)CaDiCaL version: 2.1.3 % 216.45/30.89 % (2600343)Termination reason: Instruction limit % 216.45/30.89 % (2600343)Termination phase: Saturation % 216.45/30.89 % (2600343)Time elapsed: 26.995 s % 216.45/30.89 % (2600343)Peak memory usage: 78 MB % 216.45/30.89 % (2600343)Instructions burned: 88026 (million) % 216.45/30.89 % (2600773)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3059214813:i=206:fgj=on:rtra=on_2729 on theBenchmark for (2729ds/206Mi) % 216.45/30.89 % (2600773)Instruction limit reached! % 216.45/30.89 % (2600773)------------------------------ % 216.45/30.89 % (2600773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.45/30.89 % (2600773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.45/30.89 % (2600773)CaDiCaL version: 2.1.3 % 216.45/30.89 % (2600773)Termination reason: Instruction limit % 216.45/30.89 % (2600773)Termination phase: Saturation % 216.45/30.89 % (2600773)Time elapsed: 0.111 s % 216.45/30.89 % (2600773)Peak memory usage: 13 MB % 216.45/30.89 % (2600773)Instructions burned: 207 (million) % 216.45/30.89 % (2600776)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2007878585:i=232:rtra=on_2728 on theBenchmark for (2728ds/232Mi) % 216.45/30.89 % (2600776)Instruction limit reached! % 216.45/30.89 % (2600776)------------------------------ % 216.45/30.89 % (2600776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.45/30.89 % (2600776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.45/30.89 % (2600776)CaDiCaL version: 2.1.3 % 216.45/30.89 % (2600776)Termination reason: Instruction limit % 216.45/30.89 % (2600776)Termination phase: Saturation % 216.45/30.89 % (2600776)Time elapsed: 0.141 s % 216.45/30.89 % (2600776)Peak memory usage: 13 MB % 216.45/30.89 % (2600776)Instructions burned: 233 (million) % 216.45/30.89 % (2600779)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3203970495:i=262:rtra=on_2726 on theBenchmark for (2726ds/262Mi) % 216.45/30.89 % (2600779)Instruction limit reached! % 216.45/30.89 % (2600779)------------------------------ % 216.45/30.89 % (2600779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 216.45/30.89 % (2600779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.45/30.89 % (2600779)CaDiCaL version: 2.1.3 % 216.45/30.89 % (2600779)Termination reason: Instruction limit % 216.45/30.89 % (2600779)Termination phase: Saturation % 281.89/39.93 % (2600779)Time elapsed: 0.116 s % 281.89/39.93 % (2600779)Peak memory usage: 12 MB % 281.89/39.93 % (2600779)Instructions burned: 264 (million) % 281.89/39.93 % (2600781)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=971942084:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2725 on theBenchmark for (2725ds/318Mi) % 281.89/39.93 % (2600781)Instruction limit reached! % 281.89/39.93 % (2600781)------------------------------ % 281.89/39.93 % (2600781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.89/39.93 % (2600781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.89/39.93 % (2600781)CaDiCaL version: 2.1.3 % 281.89/39.93 % (2600781)Termination reason: Instruction limit % 281.89/39.93 % (2600781)Termination phase: Saturation % 281.89/39.93 % (2600781)Time elapsed: 0.214 s % 281.89/39.93 % (2600781)Peak memory usage: 13 MB % 281.89/39.93 % (2600781)Instructions burned: 318 (million) % 281.89/39.93 % (2600783)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2477479875:i=1428:nm=2:rtra=on_2722 on theBenchmark for (2722ds/1428Mi) % 281.89/39.93 % Exception at run slice level % 281.89/39.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 281.89/39.93 % (2600785)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3309516605:i=262:bd=preordered:rtra=on:fsd=on_2722 on theBenchmark for (2722ds/262Mi) % 281.89/39.93 % (2600677)Instruction limit reached! % 281.89/39.93 % (2600677)------------------------------ % 281.89/39.93 % (2600677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.89/39.93 % (2600677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.89/39.93 % (2600677)CaDiCaL version: 2.1.3 % 281.89/39.93 % (2600677)Termination reason: Instruction limit % 281.89/39.93 % (2600677)Termination phase: Saturation % 281.89/39.93 % (2600677)Time elapsed: 12.828 s % 281.89/39.93 % (2600677)Peak memory usage: 28 MB % 281.89/39.93 % (2600677)Instructions burned: 17627 (million) % 281.89/39.93 % (2600787)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=3885610736:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2721 on theBenchmark for (2721ds/1368Mi) % 281.89/39.93 % (2600785)Instruction limit reached! % 281.89/39.93 % (2600785)------------------------------ % 281.89/39.93 % (2600785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.89/39.93 % (2600785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.89/39.93 % (2600785)CaDiCaL version: 2.1.3 % 281.89/39.93 % (2600785)Termination reason: Instruction limit % 281.89/39.93 % (2600785)Termination phase: Saturation % 281.89/39.93 % (2600785)Time elapsed: 0.139 s % 281.89/39.93 % (2600785)Peak memory usage: 13 MB % 281.89/39.93 % (2600785)Instructions burned: 263 (million) % 281.89/39.93 % (2600789)ott-21_1_sil=16000:si=on:fs=off:random_seed=3719102829:i=360:av=off:fsr=off:rtra=on_2720 on theBenchmark for (2720ds/360Mi) % 281.89/39.93 % (2600789)Instruction limit reached! % 281.89/39.93 % (2600789)------------------------------ % 281.89/39.93 % (2600789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.89/39.93 % (2600789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.89/39.93 % (2600789)CaDiCaL version: 2.1.3 % 281.89/39.93 % (2600789)Termination reason: Instruction limit % 281.89/39.93 % (2600789)Termination phase: Saturation % 281.89/39.93 % (2600789)Time elapsed: 0.162 s % 281.89/39.93 % (2600789)Peak memory usage: 13 MB % 281.89/39.93 % (2600789)Instructions burned: 361 (million) % 281.89/39.93 % (2600791)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=630013950:i=954:bd=all:rtra=on_2718 on theBenchmark for (2718ds/954Mi) % 281.89/39.93 % (2600791)Instruction limit reached! % 281.89/39.93 % (2600791)------------------------------ % 281.89/39.93 % (2600791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 281.89/39.93 % (2600791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.89/39.93 % (2600791)CaDiCaL version: 2.1.3 % 281.89/39.93 % (2600791)Termination reason: Instruction limit % 281.89/39.93 % (2600791)Termination phase: Saturation % 281.89/39.93 % (2600791)Time elapsed: 0.460 s % 281.89/39.93 % (2600791)Peak memory usage: 14 MB % 281.89/39.93 % (2600791)Instructions burned: 954 (million) % 281.89/39.93 % (2600794)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3142649988:fmbsr=1.3:i=1730:ins=25:rtra=on_2714 on theBenchmark for (2714ds/1730Mi) % 281.89/39.93 % Exception at run slice level % 281.89/39.93 User error: Finite model building is currentTerminated % 300.01/42.53 % Vampire exiting % 300.01/42.54 Terminated %------------------------------------------------------------------------------