%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV815_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n007.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:28 PM UTC 2026 % Result : Timeout 300.24s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV815_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.18 % Computer : n007.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 12:36:28 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.07/0.21 Running first-order model finding % 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.56/1.54 % (2362397)Will run a generic schedule for satisfiability detection. % 8.56/1.54 % (2362405)dis+10_1_sil=32000:sp=arity:random_seed=4191047488:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.56/1.54 % (2362403)% WARNING: option uhcvi not known. % 8.56/1.54 % (2362402)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2565473376_2999 on theBenchmark for (2999ds/0Mi) % 8.56/1.54 % (2362404)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3591305144:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.56/1.54 % (2362403)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1610091530:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.56/1.54 % (2362406)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1227109744:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.56/1.54 % (2362407)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=465613683:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.56/1.54 % (2362408)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3641923528:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.56/1.54 % Exception at run slice level % 8.56/1.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.56/1.54 % (2362405)Instruction limit reached! % 8.56/1.54 % (2362405)------------------------------ % 8.56/1.54 % (2362405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.56/1.54 % (2362405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.56/1.54 % (2362405)CaDiCaL version: 2.1.3 % 8.56/1.54 % (2362405)Termination reason: Instruction limit % 8.56/1.54 % (2362405)Termination phase: Saturation % 8.56/1.54 % (2362405)Time elapsed: 0.034 s % 8.56/1.54 % (2362405)Peak memory usage: 12 MB % 8.56/1.54 % (2362405)Instructions burned: 106 (million) % 8.56/1.54 % (2362416)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3787422085:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.56/1.54 % Exception at run slice level % 8.56/1.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.56/1.54 % (2362418)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=111483027:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.56/1.54 % (2362419)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=119445611:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.56/1.54 % (2362406)Instruction limit reached! % 8.56/1.54 % (2362406)------------------------------ % 8.56/1.54 % (2362406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.56/1.54 % (2362406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.56/1.54 % (2362406)CaDiCaL version: 2.1.3 % 8.56/1.54 % (2362406)Termination reason: Instruction limit % 8.56/1.54 % (2362406)Termination phase: Saturation % 8.56/1.54 % (2362406)Time elapsed: 0.072 s % 8.56/1.54 % (2362406)Peak memory usage: 13 MB % 8.56/1.54 % (2362406)Instructions burned: 117 (million) % 8.56/1.54 % (2362418)Instruction limit reached! % 8.56/1.54 % (2362418)------------------------------ % 8.56/1.54 % (2362418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.56/1.54 % (2362418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.56/1.54 % (2362418)CaDiCaL version: 2.1.3 % 8.56/1.54 % (2362418)Termination reason: Instruction limit % 8.56/1.54 % (2362418)Termination phase: Saturation % 8.56/1.54 % (2362418)Time elapsed: 0.045 s % 8.56/1.54 % (2362418)Peak memory usage: 13 MB % 8.56/1.54 % (2362418)Instructions burned: 132 (million) % 8.56/1.54 % (2362408)Instruction limit reached! % 8.56/1.54 % (2362408)------------------------------ % 8.56/1.54 % (2362408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.56/1.54 % (2362408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.56/1.54 % (2362408)CaDiCaL version: 2.1.3 % 8.56/1.54 % (2362408)Termination reason: Instruction limit % 8.56/1.54 % (2362408)Termination phase: Saturation % 8.56/1.54 % (2362408)Time elapsed: 0.081 s % 8.56/1.54 % (2362408)Peak memory usage: 12 MB % 8.56/1.54 % (2362408)Instructions burned: 166 (million) % 8.56/1.54 % (2362407)Instruction limit reached! % 8.56/1.54 % (2362407)------------------------------ % 8.56/1.54 % (2362407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.36 % (2362407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.36 % (2362407)CaDiCaL version: 2.1.3 % 21.85/3.36 % (2362407)Termination reason: Instruction limit % 21.85/3.36 % (2362407)Termination phase: Saturation % 21.85/3.36 % (2362407)Time elapsed: 0.082 s % 21.85/3.36 % (2362407)Peak memory usage: 13 MB % 21.85/3.36 % (2362407)Instructions burned: 132 (million) % 21.85/3.36 % (2362422)ott-21_1_sil=16000:fs=off:random_seed=1882510318:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 21.85/3.36 % (2362423)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=730541600:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 21.85/3.36 % (2362425)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3214154387:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.85/3.36 % (2362424)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2565093490:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.85/3.36 % Exception at run slice level % 21.85/3.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.36 % (2362430)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=694425956:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.85/3.36 % Exception at run slice level % 21.85/3.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.36 % (2362432)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=2974623640: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) % 21.85/3.36 % (2362422)Instruction limit reached! % 21.85/3.36 % (2362422)------------------------------ % 21.85/3.36 % (2362422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.36 % (2362422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.36 % (2362422)CaDiCaL version: 2.1.3 % 21.85/3.36 % (2362422)Termination reason: Instruction limit % 21.85/3.36 % (2362422)Termination phase: Saturation % 21.85/3.36 % (2362422)Time elapsed: 0.080 s % 21.85/3.36 % (2362422)Peak memory usage: 12 MB % 21.85/3.36 % (2362422)Instructions burned: 180 (million) % 21.85/3.36 % (2362434)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2088028501:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.85/3.36 % (2362423)Instruction limit reached! % 21.85/3.36 % (2362423)------------------------------ % 21.85/3.36 % (2362423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.36 % (2362423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.85/3.36 % (2362423)CaDiCaL version: 2.1.3 % 21.85/3.36 % (2362423)Termination reason: Instruction limit % 21.85/3.36 % (2362423)Termination phase: Saturation % 21.85/3.36 % (2362423)Time elapsed: 0.155 s % 21.85/3.36 % (2362423)Peak memory usage: 15 MB % 21.85/3.36 % (2362423)Instructions burned: 480 (million) % 21.85/3.36 % (2362436)fmb+10_1_sil=64000:random_seed=154052251:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.85/3.36 % (2362436)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.85/3.36 % Exception at run slice level % 21.85/3.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.36 % (2362438)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=616986:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.85/3.36 % Exception at run slice level % 21.85/3.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.36 % (2362440)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2481115337:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 21.85/3.36 % Exception at run slice level % 21.85/3.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.85/3.36 % (2362442)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=121686950:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.85/3.36 % (2362419)Instruction limit reached! % 21.85/3.36 % (2362419)------------------------------ % 21.85/3.36 % (2362419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.85/3.36 % (2362419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.86/9.54 % (2362419)CaDiCaL version: 2.1.3 % 65.86/9.54 % (2362419)Termination reason: Instruction limit % 65.86/9.54 % (2362419)Termination phase: Saturation % 65.86/9.54 % (2362419)Time elapsed: 0.374 s % 65.86/9.54 % (2362419)Peak memory usage: 18 MB % 65.86/9.54 % (2362419)Instructions burned: 684 (million) % 65.86/9.54 % (2362444)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3814394642:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 65.86/9.54 % (2362444)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 65.86/9.54 % (2362432)Instruction limit reached! % 65.86/9.54 % (2362432)------------------------------ % 65.86/9.54 % (2362432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.86/9.54 % (2362432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.86/9.54 % (2362432)CaDiCaL version: 2.1.3 % 65.86/9.54 % (2362432)Termination reason: Instruction limit % 65.86/9.54 % (2362432)Termination phase: Saturation % 65.86/9.54 % (2362432)Time elapsed: 0.403 s % 65.86/9.54 % (2362432)Peak memory usage: 19 MB % 65.86/9.54 % (2362432)Instructions burned: 693 (million) % 65.86/9.54 % (2362446)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3802536624:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 65.86/9.54 % Exception at run slice level % 65.86/9.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 65.86/9.54 % (2362448)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4087973185:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 65.86/9.54 % Exception at run slice level % 65.86/9.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 65.86/9.54 % (2362450)ott-2_1_sil=16000:newcnf=on:random_seed=1432611846:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 65.86/9.54 % (2362434)Instruction limit reached! % 65.86/9.54 % (2362434)------------------------------ % 65.86/9.54 % (2362434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.86/9.54 % (2362434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.86/9.54 % (2362434)CaDiCaL version: 2.1.3 % 65.86/9.54 % (2362434)Termination reason: Instruction limit % 65.86/9.54 % (2362434)Termination phase: Saturation % 65.86/9.54 % (2362434)Time elapsed: 0.503 s % 65.86/9.54 % (2362434)Peak memory usage: 18 MB % 65.86/9.54 % (2362434)Instructions burned: 880 (million) % 65.86/9.54 % (2362452)ott+10_1_sil=32000:tgt=ground:random_seed=560308440:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 65.86/9.54 % (2362425)Instruction limit reached! % 65.86/9.54 % (2362425)------------------------------ % 65.86/9.54 % (2362425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.86/9.54 % (2362425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.86/9.54 % (2362425)CaDiCaL version: 2.1.3 % 65.86/9.54 % (2362425)Termination reason: Instruction limit % 65.86/9.54 % (2362425)Termination phase: Saturation % 65.86/9.54 % (2362425)Time elapsed: 0.707 s % 65.86/9.54 % (2362425)Peak memory usage: 27 MB % 65.86/9.54 % (2362425)Instructions burned: 1180 (million) % 65.86/9.54 % (2362454)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4114728891:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 65.86/9.54 % Exception at run slice level % 65.86/9.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 65.86/9.54 % (2362456)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2846597644:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 65.86/9.54 % (2362450)Instruction limit reached! % 65.86/9.54 % (2362450)------------------------------ % 65.86/9.54 % (2362450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 65.86/9.54 % (2362450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.86/9.54 % (2362450)CaDiCaL version: 2.1.3 % 65.86/9.54 % (2362450)Termination reason: Instruction limit % 65.86/9.54 % (2362450)Termination phase: Saturation % 65.86/9.54 % (2362450)Time elapsed: 0.508 s % 65.86/9.54 % (2362450)Peak memory usage: 17 MB % 65.86/9.54 % (2362450)Instructions burned: 871 (million) % 65.86/9.54 % (2362458)dis+21_1_sil=32000:sas=cadical:random_seed=3531826401:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 65.86/9.54 % (2362444)Instruction limit reached! % 65.86/9.54 % (2362444)------------------------------ % 65.86/9.54 % (2362444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.73/17.51 % (2362444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.73/17.51 % (2362444)CaDiCaL version: 2.1.3 % 122.73/17.51 % (2362444)Termination reason: Instruction limit % 122.73/17.51 % (2362444)Termination phase: Saturation % 122.73/17.51 % (2362444)Time elapsed: 0.846 s % 122.73/17.51 % (2362444)Peak memory usage: 28 MB % 122.73/17.51 % (2362444)Instructions burned: 1473 (million) % 122.73/17.51 % (2362460)ott+11_1_sil=16000:gs=on:random_seed=1651490223:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi) % 122.73/17.51 % (2362442)Instruction limit reached! % 122.73/17.51 % (2362442)------------------------------ % 122.73/17.51 % (2362442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.73/17.51 % (2362442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.73/17.51 % (2362442)CaDiCaL version: 2.1.3 % 122.73/17.51 % (2362442)Termination reason: Instruction limit % 122.73/17.51 % (2362442)Termination phase: Saturation % 122.73/17.51 % (2362442)Time elapsed: 1.430 s % 122.73/17.51 % (2362442)Peak memory usage: 40 MB % 122.73/17.51 % (2362442)Instructions burned: 5136 (million) % 122.73/17.51 % (2362462)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1696529908:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 122.73/17.51 % Exception at run slice level % 122.73/17.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 122.73/17.51 % (2362464)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=954297334:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 122.73/17.51 % (2362460)Instruction limit reached! % 122.73/17.51 % (2362460)------------------------------ % 122.73/17.51 % (2362460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.73/17.51 % (2362460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.73/17.51 % (2362460)CaDiCaL version: 2.1.3 % 122.73/17.51 % (2362460)Termination reason: Instruction limit % 122.73/17.51 % (2362460)Termination phase: Saturation % 122.73/17.51 % (2362460)Time elapsed: 1.332 s % 122.73/17.51 % (2362460)Peak memory usage: 34 MB % 122.73/17.51 % (2362460)Instructions burned: 2252 (million) % 122.73/17.51 % (2362466)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=805486513:i=29340_2973 on theBenchmark for (2973ds/29340Mi) % 122.73/17.51 % (2362456)Instruction limit reached! % 122.73/17.51 % (2362456)------------------------------ % 122.73/17.51 % (2362456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.73/17.51 % (2362456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.73/17.51 % (2362456)CaDiCaL version: 2.1.3 % 122.73/17.51 % (2362456)Termination reason: Instruction limit % 122.73/17.51 % (2362456)Termination phase: Saturation % 122.73/17.51 % (2362456)Time elapsed: 1.841 s % 122.73/17.51 % (2362456)Peak memory usage: 30 MB % 122.73/17.51 % (2362456)Instructions burned: 3514 (million) % 122.73/17.51 % (2362468)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1620344387:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 122.73/17.51 % (2362464)Instruction limit reached! % 122.73/17.51 % (2362464)------------------------------ % 122.73/17.51 % (2362464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 122.73/17.51 % (2362464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.73/17.51 % (2362464)CaDiCaL version: 2.1.3 % 122.73/17.51 % (2362464)Termination reason: Instruction limit % 122.73/17.51 % (2362464)Termination phase: Saturation % 122.73/17.51 % (2362464)Time elapsed: 1.324 s % 122.73/17.51 % (2362464)Peak memory usage: 61 MB % 122.73/17.51 % (2362464)Instructions burned: 4594 (million) % 122.73/17.51 % (2362470)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3746081795:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi) % 122.73/17.51 % Exception at run slice level % 122.73/17.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 122.73/17.51 % (2362472)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2038971356:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi) % 122.73/17.51 % Exception at run slice level % 122.73/17.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 122.73/17.51 % (2362458)Instruction limit reached! % 122.73/17.51 % (2362458)------------------------------ % 122.73/17.51 % (2362458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.78/21.10 % (2362458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.78/21.10 % (2362458)CaDiCaL version: 2.1.3 % 147.78/21.10 % (2362458)Termination reason: Instruction limit % 147.78/21.10 % (2362458)Termination phase: Saturation % 147.78/21.10 % (2362458)Time elapsed: 1.958 s % 147.78/21.10 % (2362458)Peak memory usage: 32 MB % 147.78/21.10 % (2362458)Instructions burned: 3773 (million) % 147.78/21.10 % (2362474)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3092455028:i=14071_2968 on theBenchmark for (2968ds/14071Mi) % 147.78/21.10 % Exception at run slice level % 147.78/21.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 147.78/21.10 % (2362477)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=920973963:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 147.78/21.10 % (2362475)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2724118811:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi) % 147.78/21.10 % (2362452)Instruction limit reached! % 147.78/21.10 % (2362452)------------------------------ % 147.78/21.10 % (2362452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.78/21.10 % (2362452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.78/21.10 % (2362452)CaDiCaL version: 2.1.3 % 147.78/21.10 % (2362452)Termination reason: Instruction limit % 147.78/21.10 % (2362452)Termination phase: Saturation % 147.78/21.10 % (2362452)Time elapsed: 2.970 s % 147.78/21.10 % (2362452)Peak memory usage: 53 MB % 147.78/21.10 % (2362452)Instructions burned: 5115 (million) % 147.78/21.10 % (2362480)dis+10_16:1_sil=16000:random_seed=3231672484:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 147.78/21.10 % (2362468)Instruction limit reached! % 147.78/21.10 % (2362468)------------------------------ % 147.78/21.10 % (2362468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.78/21.10 % (2362468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.78/21.10 % (2362468)CaDiCaL version: 2.1.3 % 147.78/21.10 % (2362468)Termination reason: Instruction limit % 147.78/21.10 % (2362468)Termination phase: Saturation % 147.78/21.10 % (2362468)Time elapsed: 2.675 s % 147.78/21.10 % (2362468)Peak memory usage: 41 MB % 147.78/21.10 % (2362468)Instructions burned: 5213 (million) % 147.78/21.10 % (2362482)ott-3_8_sil=64000:random_seed=3949414350:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi) % 147.78/21.10 % (2362477)Instruction limit reached! % 147.78/21.10 % (2362477)------------------------------ % 147.78/21.10 % (2362477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.78/21.10 % (2362477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.78/21.10 % (2362477)CaDiCaL version: 2.1.3 % 147.78/21.10 % (2362477)Termination reason: Instruction limit % 147.78/21.10 % (2362477)Termination phase: Saturation % 147.78/21.10 % (2362477)Time elapsed: 2.550 s % 147.78/21.10 % (2362477)Peak memory usage: 78 MB % 147.78/21.10 % (2362477)Instructions burned: 8175 (million) % 147.78/21.10 % (2362484)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=765122643:fmbsr=2:i=32576_2942 on theBenchmark for (2942ds/32576Mi) % 147.78/21.10 % Exception at run slice level % 147.78/21.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 147.78/21.10 % (2362486)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2224923395:i=11404_2942 on theBenchmark for (2942ds/11404Mi) % 147.78/21.10 % (2362480)Instruction limit reached! % 147.78/21.10 % (2362480)------------------------------ % 147.78/21.10 % (2362480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.78/21.10 % (2362480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.78/21.10 % (2362480)CaDiCaL version: 2.1.3 % 147.78/21.10 % (2362480)Termination reason: Instruction limit % 147.78/21.10 % (2362480)Termination phase: Saturation % 147.78/21.10 % (2362480)Time elapsed: 4.579 s % 147.78/21.10 % (2362480)Peak memory usage: 52 MB % 147.78/21.10 % (2362480)Instructions burned: 9156 (million) % 147.78/21.10 % (2362488)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4047269188:i=14134_2916 on theBenchmark for (2916ds/14134Mi) % 147.78/21.10 % (2362486)Instruction limit reached! % 147.78/21.10 % (2362486)------------------------------ % 147.78/21.10 % (2362486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 147.78/21.10 % (2362486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.78/21.10 % (2362486)CaDiCaL version: 2.1.3 % 147.78/21.10 % (2362486)Termination reason: Instruction limit % 161.97/23.12 % (2362486)Termination phase: Saturation % 161.97/23.12 % (2362486)Time elapsed: 3.579 s % 161.97/23.12 % (2362486)Peak memory usage: 94 MB % 161.97/23.12 % (2362486)Instructions burned: 11405 (million) % 161.97/23.12 % (2362490)dis+33_16_sil=32000:sac=on:random_seed=3561141173:i=15851:nm=0_2906 on theBenchmark for (2906ds/15851Mi) % 161.97/23.12 % (2362475)Instruction limit reached! % 161.97/23.12 % (2362475)------------------------------ % 161.97/23.12 % (2362475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.97/23.12 % (2362475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.97/23.12 % (2362475)CaDiCaL version: 2.1.3 % 161.97/23.12 % (2362475)Termination reason: Instruction limit % 161.97/23.12 % (2362475)Termination phase: Saturation % 161.97/23.12 % (2362475)Time elapsed: 8.151 s % 161.97/23.12 % (2362475)Peak memory usage: 50 MB % 161.97/23.12 % (2362475)Instructions burned: 22567 (million) % 161.97/23.12 % (2362492)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4181761246:avsq=on:i=17627:add=on:amm=off_2886 on theBenchmark for (2886ds/17627Mi) % 161.97/23.12 % (2362490)Instruction limit reached! % 161.97/23.12 % (2362490)------------------------------ % 161.97/23.12 % (2362490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.97/23.12 % (2362490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.97/23.12 % (2362490)CaDiCaL version: 2.1.3 % 161.97/23.12 % (2362490)Termination reason: Instruction limit % 161.97/23.12 % (2362490)Termination phase: Saturation % 161.97/23.12 % (2362490)Time elapsed: 4.290 s % 161.97/23.12 % (2362490)Peak memory usage: 94 MB % 161.97/23.12 % (2362490)Instructions burned: 15851 (million) % 161.97/23.12 % (2362494)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3120807933:s2a=on:i=53295_2863 on theBenchmark for (2863ds/53295Mi) % 161.97/23.12 % (2362488)Instruction limit reached! % 161.97/23.12 % (2362488)------------------------------ % 161.97/23.12 % (2362488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.97/23.12 % (2362488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.97/23.12 % (2362488)CaDiCaL version: 2.1.3 % 161.97/23.12 % (2362488)Termination reason: Instruction limit % 161.97/23.12 % (2362488)Termination phase: Saturation % 161.97/23.12 % (2362488)Time elapsed: 7.969 s % 161.97/23.12 % (2362488)Peak memory usage: 106 MB % 161.97/23.12 % (2362488)Instructions burned: 14134 (million) % 161.97/23.12 % (2362496)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1377432972:i=26857:ins=20_2836 on theBenchmark for (2836ds/26857Mi) % 161.97/23.12 % Exception at run slice level % 161.97/23.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.97/23.12 % (2362498)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1934957712:i=28120:bs=on:fsr=off_2836 on theBenchmark for (2836ds/28120Mi) % 161.97/23.12 % (2362482)Instruction limit reached! % 161.97/23.12 % (2362482)------------------------------ % 161.97/23.12 % (2362482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 161.97/23.12 % (2362482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.97/23.12 % (2362482)CaDiCaL version: 2.1.3 % 161.97/23.12 % (2362482)Termination reason: Instruction limit % 161.97/23.12 % (2362482)Termination phase: Saturation % 161.97/23.12 % (2362482)Time elapsed: 11.732 s % 161.97/23.12 % (2362482)Peak memory usage: 121 MB % 161.97/23.12 % (2362482)Instructions burned: 20140 (million) % 161.97/23.12 % (2362500)fmb+10_1_sil=256000:fmbss=7:random_seed=3204607402:fmbsr=1.6:i=182295_2827 on theBenchmark for (2827ds/182295Mi) % 161.97/23.12 % Exception at run slice level % 161.97/23.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.97/23.12 % (2362502)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=355410793:i=44625:gsp=on_2827 on theBenchmark for (2827ds/44625Mi) % 161.97/23.12 % (2362502)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 161.97/23.12 % Exception at run slice level % 161.97/23.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.97/23.12 % (2362504)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3723714166:i=160505_2827 on theBenchmark for (2827ds/160505Mi) % 161.97/23.12 % Exception at run slice level % 161.97/23.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 161.97/23.12 % (2362506)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=404621719:fmbsr=1.3:i=225729_2827 on theBenchmark for (2827ds/225729Mi) % 193.69/27.50 % Exception at run slice level % 193.69/27.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.69/27.50 % (2362508)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=233534225:fmbsr=2:i=185024:ins=7_2826 on theBenchmark for (2826ds/185024Mi) % 193.69/27.50 % Exception at run slice level % 193.69/27.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.69/27.50 % (2362510)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=668341742:rtra=on_2826 on theBenchmark for (2826ds/0Mi) % 193.69/27.50 % Exception at run slice level % 193.69/27.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 193.69/27.50 % (2362512)% WARNING: option uhcvi not known. % 193.69/27.50 % (2362512)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=604772744:i=271062:add=off:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/271062Mi) % 193.69/27.50 % (2362466)Instruction limit reached! % 193.69/27.50 % (2362466)------------------------------ % 193.69/27.50 % (2362466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.50 % (2362466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.50 % (2362466)CaDiCaL version: 2.1.3 % 193.69/27.50 % (2362466)Termination reason: Instruction limit % 193.69/27.50 % (2362466)Termination phase: Saturation % 193.69/27.50 % (2362466)Time elapsed: 16.088 s % 193.69/27.50 % (2362466)Peak memory usage: 152 MB % 193.69/27.50 % (2362466)Instructions burned: 29342 (million) % 193.69/27.50 % (2362514)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1655243437:i=176048:add=on:rtra=on:rawr=on_2811 on theBenchmark for (2811ds/176048Mi) % 193.69/27.50 % (2362492)Instruction limit reached! % 193.69/27.50 % (2362492)------------------------------ % 193.69/27.50 % (2362492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.50 % (2362492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.50 % (2362492)CaDiCaL version: 2.1.3 % 193.69/27.50 % (2362492)Termination reason: Instruction limit % 193.69/27.50 % (2362492)Termination phase: Saturation % 193.69/27.50 % (2362492)Time elapsed: 9.041 s % 193.69/27.50 % (2362492)Peak memory usage: 109 MB % 193.69/27.50 % (2362492)Instructions burned: 17628 (million) % 193.69/27.50 % (2362516)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1633680424:i=206:fgj=on:rtra=on_2796 on theBenchmark for (2796ds/206Mi) % 193.69/27.50 % (2362516)Instruction limit reached! % 193.69/27.50 % (2362516)------------------------------ % 193.69/27.50 % (2362516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.50 % (2362516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.50 % (2362516)CaDiCaL version: 2.1.3 % 193.69/27.50 % (2362516)Termination reason: Instruction limit % 193.69/27.50 % (2362516)Termination phase: Saturation % 193.69/27.50 % (2362516)Time elapsed: 0.119 s % 193.69/27.50 % (2362516)Peak memory usage: 13 MB % 193.69/27.50 % (2362516)Instructions burned: 206 (million) % 193.69/27.50 % (2362518)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2474366250:i=232:rtra=on_2794 on theBenchmark for (2794ds/232Mi) % 193.69/27.50 % (2362518)Instruction limit reached! % 193.69/27.50 % (2362518)------------------------------ % 193.69/27.50 % (2362518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.50 % (2362518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.50 % (2362518)CaDiCaL version: 2.1.3 % 193.69/27.50 % (2362518)Termination reason: Instruction limit % 193.69/27.50 % (2362518)Termination phase: Saturation % 193.69/27.50 % (2362518)Time elapsed: 0.147 s % 193.69/27.50 % (2362518)Peak memory usage: 14 MB % 193.69/27.50 % (2362518)Instructions burned: 233 (million) % 193.69/27.50 % (2362520)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4013032980:i=262:rtra=on_2792 on theBenchmark for (2792ds/262Mi) % 193.69/27.50 % (2362520)Instruction limit reached! % 193.69/27.50 % (2362520)------------------------------ % 193.69/27.50 % (2362520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 193.69/27.50 % (2362520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.69/27.50 % (2362520)CaDiCaL version: 2.1.3 % 193.69/27.50 % (2362520)Termination reason: Instruction limit % 193.69/27.50 % (2362520)Termination phase: Saturation % 228.32/32.46 % (2362520)Time elapsed: 0.163 s % 228.32/32.46 % (2362520)Peak memory usage: 16 MB % 228.32/32.46 % (2362520)Instructions burned: 263 (million) % 228.32/32.46 % (2362522)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2871839628:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2791 on theBenchmark for (2791ds/318Mi) % 228.32/32.46 % (2362522)Instruction limit reached! % 228.32/32.46 % (2362522)------------------------------ % 228.32/32.46 % (2362522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.32/32.46 % (2362522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.32/32.46 % (2362522)CaDiCaL version: 2.1.3 % 228.32/32.46 % (2362522)Termination reason: Instruction limit % 228.32/32.46 % (2362522)Termination phase: Saturation % 228.32/32.46 % (2362522)Time elapsed: 0.157 s % 228.32/32.46 % (2362522)Peak memory usage: 12 MB % 228.32/32.46 % (2362522)Instructions burned: 319 (million) % 228.32/32.46 % (2362524)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3466823021:i=1428:nm=2:rtra=on_2789 on theBenchmark for (2789ds/1428Mi) % 228.32/32.46 % Exception at run slice level % 228.32/32.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 228.32/32.46 % (2362526)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1121890116:i=262:bd=preordered:rtra=on:fsd=on_2789 on theBenchmark for (2789ds/262Mi) % 228.32/32.46 % (2362526)Instruction limit reached! % 228.32/32.46 % (2362526)------------------------------ % 228.32/32.46 % (2362526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.32/32.46 % (2362526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.32/32.46 % (2362526)CaDiCaL version: 2.1.3 % 228.32/32.46 % (2362526)Termination reason: Instruction limit % 228.32/32.46 % (2362526)Termination phase: Saturation % 228.32/32.46 % (2362526)Time elapsed: 0.169 s % 228.32/32.46 % (2362526)Peak memory usage: 15 MB % 228.32/32.46 % (2362526)Instructions burned: 263 (million) % 228.32/32.46 % (2362528)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=1592066731:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2787 on theBenchmark for (2787ds/1368Mi) % 228.32/32.46 % (2362528)Instruction limit reached! % 228.32/32.46 % (2362528)------------------------------ % 228.32/32.46 % (2362528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.32/32.46 % (2362528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.32/32.46 % (2362528)CaDiCaL version: 2.1.3 % 228.32/32.46 % (2362528)Termination reason: Instruction limit % 228.32/32.46 % (2362528)Termination phase: Saturation % 228.32/32.46 % (2362528)Time elapsed: 0.761 s % 228.32/32.46 % (2362528)Peak memory usage: 23 MB % 228.32/32.46 % (2362528)Instructions burned: 1368 (million) % 228.32/32.46 % (2362530)ott-21_1_sil=16000:si=on:fs=off:random_seed=1218653720:i=360:av=off:fsr=off:rtra=on_2779 on theBenchmark for (2779ds/360Mi) % 228.32/32.46 % (2362530)Instruction limit reached! % 228.32/32.46 % (2362530)------------------------------ % 228.32/32.46 % (2362530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.32/32.46 % (2362530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.32/32.46 % (2362530)CaDiCaL version: 2.1.3 % 228.32/32.46 % (2362530)Termination reason: Instruction limit % 228.32/32.46 % (2362530)Termination phase: Saturation % 228.32/32.46 % (2362530)Time elapsed: 0.185 s % 228.32/32.46 % (2362530)Peak memory usage: 14 MB % 228.32/32.46 % (2362530)Instructions burned: 360 (million) % 228.32/32.46 % (2362532)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4229889735:i=954:bd=all:rtra=on_2777 on theBenchmark for (2777ds/954Mi) % 228.32/32.46 % (2362532)Instruction limit reached! % 228.32/32.46 % (2362532)------------------------------ % 228.32/32.46 % (2362532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 228.32/32.46 % (2362532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.32/32.46 % (2362532)CaDiCaL version: 2.1.3 % 228.32/32.46 % (2362532)Termination reason: Instruction limit % 228.32/32.46 % (2362532)Termination phase: Saturation % 228.32/32.46 % (2362532)Time elapsed: 0.585 s % 228.32/32.46 % (2362532)Peak memory usage: 18 MB % 228.32/32.46 % (2362532)Instructions burned: 955 (million) % 228.32/32.46 % (2362534)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2963563006:fmbsr=1.3:i=1730:ins=25:rtra=on_2771 on theBenchmark for (2771ds/1730Mi) % 228.32/32.46 % Exception at run slice level % 228.32/32.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.15/36.54 % (2362536)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1921046247:i=2358:rtra=on_2770 on theBenchmark for (2770ds/2358Mi) % 257.15/36.54 % (2362536)Instruction limit reached! % 257.15/36.54 % (2362536)------------------------------ % 257.15/36.54 % (2362536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.15/36.54 % (2362536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.15/36.54 % (2362536)CaDiCaL version: 2.1.3 % 257.15/36.54 % (2362536)Termination reason: Instruction limit % 257.15/36.54 % (2362536)Termination phase: Saturation % 257.15/36.54 % (2362536)Time elapsed: 1.534 s % 257.15/36.54 % (2362536)Peak memory usage: 42 MB % 257.15/36.54 % (2362536)Instructions burned: 2359 (million) % 257.15/36.54 % (2362538)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=491274980:i=1778:ins=1:rtra=on_2755 on theBenchmark for (2755ds/1778Mi) % 257.15/36.54 % Exception at run slice level % 257.15/36.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.15/36.54 % (2362540)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=463691783:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2755 on theBenchmark for (2755ds/1384Mi) % 257.15/36.54 % (2362540)Instruction limit reached! % 257.15/36.54 % (2362540)------------------------------ % 257.15/36.54 % (2362540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.15/36.54 % (2362540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.15/36.54 % (2362540)CaDiCaL version: 2.1.3 % 257.15/36.54 % (2362540)Termination reason: Instruction limit % 257.15/36.54 % (2362540)Termination phase: Saturation % 257.15/36.54 % (2362540)Time elapsed: 0.847 s % 257.15/36.54 % (2362540)Peak memory usage: 24 MB % 257.15/36.54 % (2362540)Instructions burned: 1384 (million) % 257.15/36.54 % (2362542)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2013363825:i=1758:kws=inv_precedence:fsr=off:rtra=on_2746 on theBenchmark for (2746ds/1758Mi) % 257.15/36.54 % (2362542)Instruction limit reached! % 257.15/36.54 % (2362542)------------------------------ % 257.15/36.54 % (2362542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.15/36.54 % (2362542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.15/36.54 % (2362542)CaDiCaL version: 2.1.3 % 257.15/36.54 % (2362542)Termination reason: Instruction limit % 257.15/36.54 % (2362542)Termination phase: Saturation % 257.15/36.54 % (2362542)Time elapsed: 1.033 s % 257.15/36.54 % (2362542)Peak memory usage: 23 MB % 257.15/36.54 % (2362542)Instructions burned: 1758 (million) % 257.15/36.54 % (2362544)fmb+10_1_sil=64000:si=on:random_seed=4028750153:i=44122:nm=2:rtra=on:gsp=on_2735 on theBenchmark for (2735ds/44122Mi) % 257.15/36.54 % (2362544)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 257.15/36.54 % Exception at run slice level % 257.15/36.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.15/36.54 % (2362546)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1759647082:i=19030:nm=5:rtra=on_2735 on theBenchmark for (2735ds/19030Mi) % 257.15/36.54 % Exception at run slice level % 257.15/36.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.15/36.54 % (2362548)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2966546089:fmbsr=1.7:i=1840:rtra=on_2735 on theBenchmark for (2735ds/1840Mi) % 257.15/36.54 % Exception at run slice level % 257.15/36.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 257.15/36.54 % (2362550)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2596536263:i=10262:rtra=on_2735 on theBenchmark for (2735ds/10262Mi) % 257.15/36.54 % (2362494)Instruction limit reached! % 257.15/36.54 % (2362494)------------------------------ % 257.15/36.54 % (2362494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 257.15/36.54 % (2362494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.15/36.54 % (2362494)CaDiCaL version: 2.1.3 % 257.15/36.54 % (2362494)Termination reason: Instruction limit % 257.15/36.54 % (2362494)Termination phase: Saturation % 257.15/36.54 % (2362494)Time elapsed: 13.635 s % 257.15/36.54 % (2362494)Peak memory usage: 258 MB % 257.15/36.54 % (2Terminated % 300.24/42.54 % Vampire exiting % 300.24/42.54 Terminated %------------------------------------------------------------------------------