%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM987_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 : n020.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 12:26:20 PM UTC 2026 % Result : Timeout 299.94s 42.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM987_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.39 % Computer : n020.cluster.edu % 0.12/0.39 % Model : x86_64 x86_64 % 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.39 % Memory : 8046.5625MB % 0.12/0.39 % OS : Linux 6.8.0-71-generic % 0.12/0.39 % CPULimit : 300 % 0.12/0.39 % WCLimit : 300 % 0.12/0.39 % DateTime : Sun Sep 27 21:50:05 UTC 2026 % 0.12/0.39 % CPUTime : % 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.12/0.43 Running first-order model finding % 0.12/0.43 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 % 6.95/1.60 % (3791400)Will run a generic schedule for satisfiability detection. % 6.95/1.60 % (3791410)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1951451523:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.95/1.60 % (3791406)% WARNING: option uhcvi not known. % 6.95/1.60 % (3791405)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2944482893_2999 on theBenchmark for (2999ds/0Mi) % 6.95/1.60 % (3791406)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=835322456:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.95/1.60 % (3791407)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=76463856:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.95/1.60 % (3791408)dis+10_1_sil=32000:sp=arity:random_seed=1202721995:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.95/1.60 % (3791409)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3170291968:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.95/1.60 % (3791411)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2049619861:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.95/1.60 % Exception at run slice level % 6.95/1.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.95/1.60 % (3791419)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3685942227:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.95/1.60 % Exception at run slice level % 6.95/1.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.95/1.60 % (3791410)Instruction limit reached! % 6.95/1.60 % (3791410)------------------------------ % 6.95/1.60 % (3791410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.95/1.60 % (3791410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.95/1.60 % (3791410)CaDiCaL version: 2.1.3 % 6.95/1.60 % (3791410)Termination reason: Instruction limit % 6.95/1.60 % (3791410)Termination phase: Saturation % 6.95/1.60 % (3791410)Time elapsed: 0.044 s % 6.95/1.60 % (3791410)Peak memory usage: 12 MB % 6.95/1.60 % (3791410)Instructions burned: 131 (million) % 6.95/1.60 % (3791421)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=13267878:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.95/1.60 % (3791422)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=2062750452:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.95/1.60 % (3791408)Instruction limit reached! % 6.95/1.60 % (3791408)------------------------------ % 6.95/1.60 % (3791408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.95/1.60 % (3791408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.95/1.60 % (3791408)CaDiCaL version: 2.1.3 % 6.95/1.60 % (3791408)Termination reason: Instruction limit % 6.95/1.60 % (3791408)Termination phase: Saturation % 6.95/1.60 % (3791408)Time elapsed: 0.065 s % 6.95/1.60 % (3791408)Peak memory usage: 12 MB % 6.95/1.60 % (3791408)Instructions burned: 104 (million) % 6.95/1.60 % (3791409)Instruction limit reached! % 6.95/1.60 % (3791409)------------------------------ % 6.95/1.60 % (3791409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.95/1.60 % (3791409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.95/1.60 % (3791409)CaDiCaL version: 2.1.3 % 6.95/1.60 % (3791409)Termination reason: Instruction limit % 6.95/1.60 % (3791409)Termination phase: Saturation % 6.95/1.60 % (3791409)Time elapsed: 0.071 s % 6.95/1.60 % (3791409)Peak memory usage: 12 MB % 6.95/1.60 % (3791409)Instructions burned: 117 (million) % 6.95/1.60 % (3791425)ott-21_1_sil=16000:fs=off:random_seed=1003250215:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 6.95/1.60 % (3791426)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=804360642:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 6.95/1.60 % (3791411)Instruction limit reached! % 6.95/1.60 % (3791411)------------------------------ % 6.95/1.60 % (3791411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.95/1.60 % (3791411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.95/1.60 % (3791411)CaDiCaL version: 2.1.3 % 6.95/1.60 % (3791411)Termination reason: Instruction limit % 6.95/1.60 % (3791411)Termination phase: Saturation % 20.24/3.33 % (3791411)Time elapsed: 0.103 s % 20.24/3.33 % (3791411)Peak memory usage: 13 MB % 20.24/3.33 % (3791411)Instructions burned: 160 (million) % 20.24/3.33 % (3791429)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3341041147:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.24/3.33 % Exception at run slice level % 20.24/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.24/3.33 % (3791421)Instruction limit reached! % 20.24/3.33 % (3791421)------------------------------ % 20.24/3.33 % (3791421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.24/3.33 % (3791421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.24/3.33 % (3791421)CaDiCaL version: 2.1.3 % 20.24/3.33 % (3791421)Termination reason: Instruction limit % 20.24/3.33 % (3791421)Termination phase: Saturation % 20.24/3.33 % (3791421)Time elapsed: 0.082 s % 20.24/3.33 % (3791421)Peak memory usage: 13 MB % 20.24/3.33 % (3791421)Instructions burned: 131 (million) % 20.24/3.33 % (3791431)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2991069817:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.24/3.33 % (3791432)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1162598534:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.24/3.33 % Exception at run slice level % 20.24/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.24/3.33 % (3791435)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=871503124: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) % 20.24/3.33 % (3791425)Instruction limit reached! % 20.24/3.33 % (3791425)------------------------------ % 20.24/3.33 % (3791425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.24/3.33 % (3791425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.24/3.33 % (3791425)CaDiCaL version: 2.1.3 % 20.24/3.33 % (3791425)Termination reason: Instruction limit % 20.24/3.33 % (3791425)Termination phase: Saturation % 20.24/3.33 % (3791425)Time elapsed: 0.092 s % 20.24/3.33 % (3791425)Peak memory usage: 13 MB % 20.24/3.33 % (3791425)Instructions burned: 180 (million) % 20.24/3.33 % (3791437)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3109578440:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.24/3.33 % (3791422)Instruction limit reached! % 20.24/3.33 % (3791422)------------------------------ % 20.24/3.33 % (3791422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.24/3.33 % (3791422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.24/3.33 % (3791422)CaDiCaL version: 2.1.3 % 20.24/3.33 % (3791422)Termination reason: Instruction limit % 20.24/3.33 % (3791422)Termination phase: Saturation % 20.24/3.33 % (3791422)Time elapsed: 0.201 s % 20.24/3.33 % (3791422)Peak memory usage: 16 MB % 20.24/3.33 % (3791422)Instructions burned: 686 (million) % 20.24/3.33 % (3791439)fmb+10_1_sil=64000:random_seed=3585500353:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.24/3.33 % (3791439)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.24/3.33 % Exception at run slice level % 20.24/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.24/3.33 % (3791441)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=761143745:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 20.24/3.33 % Exception at run slice level % 20.24/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.24/3.33 % (3791443)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2392434561:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.24/3.33 % Exception at run slice level % 20.24/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.24/3.33 % (3791445)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2293899710:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.24/3.33 % (3791426)Instruction limit reached! % 20.24/3.33 % (3791426)------------------------------ % 20.24/3.33 % (3791426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.24/3.33 % (3791426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.76/10.71 % (3791426)CaDiCaL version: 2.1.3 % 72.76/10.71 % (3791426)Termination reason: Instruction limit % 72.76/10.71 % (3791426)Termination phase: Saturation % 72.76/10.71 % (3791426)Time elapsed: 0.298 s % 72.76/10.71 % (3791426)Peak memory usage: 14 MB % 72.76/10.71 % (3791426)Instructions burned: 477 (million) % 72.76/10.71 % (3791447)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=665033729:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 72.76/10.71 % (3791447)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 72.76/10.71 % (3791435)Instruction limit reached! % 72.76/10.71 % (3791435)------------------------------ % 72.76/10.71 % (3791435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.76/10.71 % (3791435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.76/10.71 % (3791435)CaDiCaL version: 2.1.3 % 72.76/10.71 % (3791435)Termination reason: Instruction limit % 72.76/10.71 % (3791435)Termination phase: Saturation % 72.76/10.71 % (3791435)Time elapsed: 0.398 s % 72.76/10.71 % (3791435)Peak memory usage: 16 MB % 72.76/10.71 % (3791435)Instructions burned: 693 (million) % 72.76/10.71 % (3791449)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3729950002:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 72.76/10.71 % Exception at run slice level % 72.76/10.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.76/10.71 % (3791451)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1565440225:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 72.76/10.71 % Exception at run slice level % 72.76/10.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.76/10.71 % (3791453)ott-2_1_sil=16000:newcnf=on:random_seed=2540476155:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 72.76/10.71 % (3791437)Instruction limit reached! % 72.76/10.71 % (3791437)------------------------------ % 72.76/10.71 % (3791437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.76/10.71 % (3791437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.76/10.71 % (3791437)CaDiCaL version: 2.1.3 % 72.76/10.71 % (3791437)Termination reason: Instruction limit % 72.76/10.71 % (3791437)Termination phase: Saturation % 72.76/10.71 % (3791437)Time elapsed: 0.489 s % 72.76/10.71 % (3791437)Peak memory usage: 19 MB % 72.76/10.71 % (3791437)Instructions burned: 880 (million) % 72.76/10.71 % (3791455)ott+10_1_sil=32000:tgt=ground:random_seed=2526516739:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 72.76/10.71 % (3791431)Instruction limit reached! % 72.76/10.71 % (3791431)------------------------------ % 72.76/10.71 % (3791431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.76/10.71 % (3791431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.76/10.71 % (3791431)CaDiCaL version: 2.1.3 % 72.76/10.71 % (3791431)Termination reason: Instruction limit % 72.76/10.71 % (3791431)Termination phase: Saturation % 72.76/10.71 % (3791431)Time elapsed: 0.685 s % 72.76/10.71 % (3791431)Peak memory usage: 18 MB % 72.76/10.71 % (3791431)Instructions burned: 1180 (million) % 72.76/10.71 % (3791457)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1935214359:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 72.76/10.71 % Exception at run slice level % 72.76/10.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 72.76/10.71 % (3791459)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2056813019:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 72.76/10.71 % (3791447)Instruction limit reached! % 72.76/10.71 % (3791447)------------------------------ % 72.76/10.71 % (3791447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 72.76/10.71 % (3791447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.76/10.71 % (3791447)CaDiCaL version: 2.1.3 % 72.76/10.71 % (3791447)Termination reason: Instruction limit % 72.76/10.71 % (3791447)Termination phase: Saturation % 72.76/10.71 % (3791447)Time elapsed: 0.655 s % 72.76/10.71 % (3791447)Peak memory usage: 21 MB % 72.76/10.71 % (3791447)Instructions burned: 1473 (million) % 72.76/10.71 % (3791461)dis+21_1_sil=32000:sas=cadical:random_seed=2523287983:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 72.76/10.71 % (3791453)Instruction limit reached! % 72.76/10.71 % (3791453)------------------------------ % 72.76/10.71 % (3791453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.10/17.53 % (3791453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.10/17.53 % (3791453)CaDiCaL version: 2.1.3 % 121.10/17.53 % (3791453)Termination reason: Instruction limit % 121.10/17.53 % (3791453)Termination phase: Saturation % 121.10/17.53 % (3791453)Time elapsed: 0.492 s % 121.10/17.53 % (3791453)Peak memory usage: 16 MB % 121.10/17.53 % (3791453)Instructions burned: 869 (million) % 121.10/17.53 % (3791463)ott+11_1_sil=16000:gs=on:random_seed=2684244214:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 121.10/17.53 % (3791445)Instruction limit reached! % 121.10/17.53 % (3791445)------------------------------ % 121.10/17.53 % (3791445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.10/17.53 % (3791445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.10/17.53 % (3791445)CaDiCaL version: 2.1.3 % 121.10/17.53 % (3791445)Termination reason: Instruction limit % 121.10/17.53 % (3791445)Termination phase: Saturation % 121.10/17.53 % (3791445)Time elapsed: 1.453 s % 121.10/17.53 % (3791445)Peak memory usage: 33 MB % 121.10/17.53 % (3791445)Instructions burned: 5131 (million) % 121.10/17.53 % (3791465)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1967348762:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 121.10/17.53 % Exception at run slice level % 121.10/17.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 121.10/17.53 % (3791467)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=578740070:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 121.10/17.53 % (3791463)Instruction limit reached! % 121.10/17.53 % (3791463)------------------------------ % 121.10/17.53 % (3791463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.10/17.53 % (3791463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.10/17.53 % (3791463)CaDiCaL version: 2.1.3 % 121.10/17.53 % (3791463)Termination reason: Instruction limit % 121.10/17.53 % (3791463)Termination phase: Saturation % 121.10/17.53 % (3791463)Time elapsed: 1.164 s % 121.10/17.53 % (3791463)Peak memory usage: 18 MB % 121.10/17.53 % (3791463)Instructions burned: 2251 (million) % 121.10/17.53 % (3791469)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=398284248:i=29340_2976 on theBenchmark for (2976ds/29340Mi) % 121.10/17.53 % (3791459)Instruction limit reached! % 121.10/17.53 % (3791459)------------------------------ % 121.10/17.53 % (3791459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.10/17.53 % (3791459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.10/17.53 % (3791459)CaDiCaL version: 2.1.3 % 121.10/17.53 % (3791459)Termination reason: Instruction limit % 121.10/17.53 % (3791459)Termination phase: Saturation % 121.10/17.53 % (3791459)Time elapsed: 1.935 s % 121.10/17.53 % (3791459)Peak memory usage: 30 MB % 121.10/17.53 % (3791459)Instructions burned: 3512 (million) % 121.10/17.53 % (3791467)Instruction limit reached! % 121.10/17.53 % (3791467)------------------------------ % 121.10/17.53 % (3791467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.10/17.53 % (3791467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.10/17.53 % (3791467)CaDiCaL version: 2.1.3 % 121.10/17.53 % (3791467)Termination reason: Instruction limit % 121.10/17.53 % (3791467)Termination phase: Saturation % 121.10/17.53 % (3791467)Time elapsed: 1.042 s % 121.10/17.53 % (3791467)Peak memory usage: 32 MB % 121.10/17.53 % (3791467)Instructions burned: 4595 (million) % 121.10/17.53 % (3791472)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3874322214:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 121.10/17.53 % (3791471)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=405291673:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 121.10/17.53 % Exception at run slice level % 121.10/17.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 121.10/17.53 % (3791475)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2162433179:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 121.10/17.53 % Exception at run slice level % 121.10/17.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 121.10/17.53 % (3791477)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1152244495:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 121.10/17.53 % Exception at run slice level % 146.15/21.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 146.15/21.11 % (3791479)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4290553656:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 146.15/21.11 % (3791461)Instruction limit reached! % 146.15/21.11 % (3791461)------------------------------ % 146.15/21.11 % (3791461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/21.11 % (3791461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/21.11 % (3791461)CaDiCaL version: 2.1.3 % 146.15/21.11 % (3791461)Termination reason: Instruction limit % 146.15/21.11 % (3791461)Termination phase: Saturation % 146.15/21.11 % (3791461)Time elapsed: 2.003 s % 146.15/21.11 % (3791461)Peak memory usage: 27 MB % 146.15/21.11 % (3791461)Instructions burned: 3774 (million) % 146.15/21.11 % (3791481)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1221261925:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 146.15/21.11 % (3791455)Instruction limit reached! % 146.15/21.11 % (3791455)------------------------------ % 146.15/21.11 % (3791455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/21.11 % (3791455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/21.11 % (3791455)CaDiCaL version: 2.1.3 % 146.15/21.11 % (3791455)Termination reason: Instruction limit % 146.15/21.11 % (3791455)Termination phase: Saturation % 146.15/21.11 % (3791455)Time elapsed: 3.006 s % 146.15/21.11 % (3791455)Peak memory usage: 28 MB % 146.15/21.11 % (3791455)Instructions burned: 5115 (million) % 146.15/21.11 % (3791483)dis+10_16:1_sil=16000:random_seed=2878268625:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 146.15/21.11 % (3791471)Instruction limit reached! % 146.15/21.11 % (3791471)------------------------------ % 146.15/21.11 % (3791471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/21.11 % (3791471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/21.11 % (3791471)CaDiCaL version: 2.1.3 % 146.15/21.11 % (3791471)Termination reason: Instruction limit % 146.15/21.11 % (3791471)Termination phase: Saturation % 146.15/21.11 % (3791471)Time elapsed: 2.775 s % 146.15/21.11 % (3791471)Peak memory usage: 41 MB % 146.15/21.11 % (3791471)Instructions burned: 5211 (million) % 146.15/21.11 % (3791485)ott-3_8_sil=64000:random_seed=617724288:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 146.15/21.11 % (3791481)Instruction limit reached! % 146.15/21.11 % (3791481)------------------------------ % 146.15/21.11 % (3791481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/21.11 % (3791481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/21.11 % (3791481)CaDiCaL version: 2.1.3 % 146.15/21.11 % (3791481)Termination reason: Instruction limit % 146.15/21.11 % (3791481)Termination phase: Saturation % 146.15/21.11 % (3791481)Time elapsed: 4.999 s % 146.15/21.11 % (3791481)Peak memory usage: 36 MB % 146.15/21.11 % (3791481)Instructions burned: 8173 (million) % 146.15/21.11 % (3791487)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1450956185:fmbsr=2:i=32576_2918 on theBenchmark for (2918ds/32576Mi) % 146.15/21.11 % Exception at run slice level % 146.15/21.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 146.15/21.11 % (3791489)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=688736911:i=11404_2918 on theBenchmark for (2918ds/11404Mi) % 146.15/21.11 % (3791483)Instruction limit reached! % 146.15/21.11 % (3791483)------------------------------ % 146.15/21.11 % (3791483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/21.11 % (3791483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/21.11 % (3791483)CaDiCaL version: 2.1.3 % 146.15/21.11 % (3791483)Termination reason: Instruction limit % 146.15/21.11 % (3791483)Termination phase: Saturation % 146.15/21.11 % (3791483)Time elapsed: 4.694 s % 146.15/21.11 % (3791483)Peak memory usage: 56 MB % 146.15/21.11 % (3791483)Instructions burned: 9156 (million) % 146.15/21.11 % (3791491)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=79108719:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 146.15/21.11 % (3791479)Instruction limit reached! % 146.15/21.11 % (3791479)------------------------------ % 146.15/21.11 % (3791479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 146.15/21.11 % (3791479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.15/21.11 % (3791479)CaDiCaL version: 2.1.3 % 146.15/21.11 % (3791479)Termination reason: Instruction limit % 154.42/22.26 % (3791479)Termination phase: Saturation % 154.42/22.26 % (3791479)Time elapsed: 7.372 s % 154.42/22.26 % (3791479)Peak memory usage: 689 MB % 154.42/22.26 % (3791479)Instructions burned: 22567 (million) % 154.42/22.26 % (3791493)dis+33_16_sil=32000:sac=on:random_seed=2437507957:i=15851:nm=0_2896 on theBenchmark for (2896ds/15851Mi) % 154.42/22.26 % (3791493)Instruction limit reached! % 154.42/22.26 % (3791493)------------------------------ % 154.42/22.26 % (3791493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.42/22.26 % (3791493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.42/22.26 % (3791493)CaDiCaL version: 2.1.3 % 154.42/22.26 % (3791493)Termination reason: Instruction limit % 154.42/22.26 % (3791493)Termination phase: Saturation % 154.42/22.26 % (3791493)Time elapsed: 4.518 s % 154.42/22.26 % (3791493)Peak memory usage: 120 MB % 154.42/22.26 % (3791493)Instructions burned: 15852 (million) % 154.42/22.26 % (3791725)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=84677020:avsq=on:i=17627:add=on:amm=off_2851 on theBenchmark for (2851ds/17627Mi) % 154.42/22.26 % (3791489)Instruction limit reached! % 154.42/22.26 % (3791489)------------------------------ % 154.42/22.26 % (3791489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.42/22.26 % (3791489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.42/22.26 % (3791489)CaDiCaL version: 2.1.3 % 154.42/22.26 % (3791489)Termination reason: Instruction limit % 154.42/22.26 % (3791489)Termination phase: Saturation % 154.42/22.26 % (3791489)Time elapsed: 7.183 s % 154.42/22.26 % (3791489)Peak memory usage: 45 MB % 154.42/22.26 % (3791489)Instructions burned: 11404 (million) % 154.42/22.26 % (3791737)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2132238831:s2a=on:i=53295_2846 on theBenchmark for (2846ds/53295Mi) % 154.42/22.26 % (3791469)Instruction limit reached! % 154.42/22.26 % (3791469)------------------------------ % 154.42/22.26 % (3791469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.42/22.26 % (3791469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.42/22.26 % (3791469)CaDiCaL version: 2.1.3 % 154.42/22.26 % (3791469)Termination reason: Instruction limit % 154.42/22.26 % (3791469)Termination phase: Saturation % 154.42/22.26 % (3791469)Time elapsed: 13.687 s % 154.42/22.26 % (3791469)Peak memory usage: 227 MB % 154.42/22.26 % (3791469)Instructions burned: 29340 (million) % 154.42/22.26 % (3791761)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3494916676:i=26857:ins=20_2839 on theBenchmark for (2839ds/26857Mi) % 154.42/22.26 % Exception at run slice level % 154.42/22.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 154.42/22.26 % (3791771)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2855761719:i=28120:bs=on:fsr=off_2838 on theBenchmark for (2838ds/28120Mi) % 154.42/22.26 % (3791491)Instruction limit reached! % 154.42/22.26 % (3791491)------------------------------ % 154.42/22.26 % (3791491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 154.42/22.26 % (3791491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 154.42/22.26 % (3791491)CaDiCaL version: 2.1.3 % 154.42/22.26 % (3791491)Termination reason: Instruction limit % 154.42/22.26 % (3791491)Termination phase: Saturation % 154.42/22.26 % (3791491)Time elapsed: 8.496 s % 154.42/22.26 % (3791491)Peak memory usage: 52 MB % 154.42/22.26 % (3791491)Instructions burned: 14135 (million) % 154.42/22.26 % (3791902)fmb+10_1_sil=256000:fmbss=7:random_seed=3750009278:fmbsr=1.6:i=182295_2829 on theBenchmark for (2829ds/182295Mi) % 154.42/22.26 % Exception at run slice level % 154.42/22.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 154.42/22.26 % (3791904)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=969064850:i=44625:gsp=on_2829 on theBenchmark for (2829ds/44625Mi) % 154.42/22.26 % (3791904)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 154.42/22.26 % Exception at run slice level % 154.42/22.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 154.42/22.26 % (3791906)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=978095941:i=160505_2829 on theBenchmark for (2829ds/160505Mi) % 154.42/22.26 % Exception at run slice level % 154.42/22.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 154.42/22.26 % (3791908)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3358618873:fmbsr=1.3:i=225729_2829 on theBenchmark for (2829ds/225729Mi) % 191.33/27.44 % Exception at run slice level % 191.33/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 191.33/27.44 % (3791910)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2703430698:fmbsr=2:i=185024:ins=7_2829 on theBenchmark for (2829ds/185024Mi) % 191.33/27.44 % Exception at run slice level % 191.33/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 191.33/27.44 % (3791912)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3939609601:rtra=on_2828 on theBenchmark for (2828ds/0Mi) % 191.33/27.44 % Exception at run slice level % 191.33/27.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 191.33/27.44 % (3791914)% WARNING: option uhcvi not known. % 191.33/27.44 % (3791914)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3733238344:i=271062:add=off:rtra=on:rawr=on_2828 on theBenchmark for (2828ds/271062Mi) % 191.33/27.44 % (3791485)Instruction limit reached! % 191.33/27.44 % (3791485)------------------------------ % 191.33/27.44 % (3791485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.33/27.44 % (3791485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.33/27.44 % (3791485)CaDiCaL version: 2.1.3 % 191.33/27.44 % (3791485)Termination reason: Instruction limit % 191.33/27.44 % (3791485)Termination phase: Saturation % 191.33/27.44 % (3791485)Time elapsed: 13.894 s % 191.33/27.44 % (3791485)Peak memory usage: 88 MB % 191.33/27.44 % (3791485)Instructions burned: 20139 (million) % 191.33/27.44 % (3791916)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2704901136:i=176048:add=on:rtra=on:rawr=on_2804 on theBenchmark for (2804ds/176048Mi) % 191.33/27.44 % (3791725)Instruction limit reached! % 191.33/27.44 % (3791725)------------------------------ % 191.33/27.44 % (3791725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.33/27.44 % (3791725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.33/27.44 % (3791725)CaDiCaL version: 2.1.3 % 191.33/27.44 % (3791725)Termination reason: Instruction limit % 191.33/27.45 % (3791725)Termination phase: Saturation % 191.33/27.45 % (3791725)Time elapsed: 5.510 s % 191.33/27.45 % (3791725)Peak memory usage: 251 MB % 191.33/27.45 % (3791725)Instructions burned: 17628 (million) % 191.33/27.45 % (3791918)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3607898717:i=206:fgj=on:rtra=on_2795 on theBenchmark for (2795ds/206Mi) % 191.33/27.45 % (3791918)Instruction limit reached! % 191.33/27.45 % (3791918)------------------------------ % 191.33/27.45 % (3791918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.33/27.45 % (3791918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.33/27.45 % (3791918)CaDiCaL version: 2.1.3 % 191.33/27.45 % (3791918)Termination reason: Instruction limit % 191.33/27.45 % (3791918)Termination phase: Saturation % 191.33/27.45 % (3791918)Time elapsed: 0.066 s % 191.33/27.45 % (3791918)Peak memory usage: 13 MB % 191.33/27.45 % (3791918)Instructions burned: 209 (million) % 191.33/27.45 % (3791920)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2148807932:i=232:rtra=on_2795 on theBenchmark for (2795ds/232Mi) % 191.33/27.45 % (3791920)Instruction limit reached! % 191.33/27.45 % (3791920)------------------------------ % 191.33/27.45 % (3791920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.33/27.45 % (3791920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.33/27.45 % (3791920)CaDiCaL version: 2.1.3 % 191.33/27.45 % (3791920)Termination reason: Instruction limit % 191.33/27.45 % (3791920)Termination phase: Saturation % 191.33/27.45 % (3791920)Time elapsed: 0.077 s % 191.33/27.45 % (3791920)Peak memory usage: 13 MB % 191.33/27.45 % (3791920)Instructions burned: 233 (million) % 191.33/27.45 % (3791922)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2749205080:i=262:rtra=on_2794 on theBenchmark for (2794ds/262Mi) % 191.33/27.45 % (3791922)Instruction limit reached! % 191.33/27.45 % (3791922)------------------------------ % 191.33/27.45 % (3791922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 191.33/27.45 % (3791922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.33/27.45 % (3791922)CaDiCaL version: 2.1.3 % 191.33/27.45 % (3791922)Termination reason: Instruction limit % 191.33/27.45 % (3791922)Termination phase: Saturation % 261.59/37.30 % (3791922)Time elapsed: 0.081 s % 261.59/37.30 % (3791922)Peak memory usage: 14 MB % 261.59/37.30 % (3791922)Instructions burned: 267 (million) % 261.59/37.30 % (3791924)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1113485140:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2793 on theBenchmark for (2793ds/318Mi) % 261.59/37.30 % (3791924)Instruction limit reached! % 261.59/37.30 % (3791924)------------------------------ % 261.59/37.30 % (3791924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.59/37.30 % (3791924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.59/37.30 % (3791924)CaDiCaL version: 2.1.3 % 261.59/37.30 % (3791924)Termination reason: Instruction limit % 261.59/37.30 % (3791924)Termination phase: Saturation % 261.59/37.30 % (3791924)Time elapsed: 0.106 s % 261.59/37.30 % (3791924)Peak memory usage: 14 MB % 261.59/37.30 % (3791924)Instructions burned: 320 (million) % 261.59/37.30 % (3791926)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1210083778:i=1428:nm=2:rtra=on_2792 on theBenchmark for (2792ds/1428Mi) % 261.59/37.30 % Exception at run slice level % 261.59/37.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 261.59/37.30 % (3791928)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1415335404:i=262:bd=preordered:rtra=on:fsd=on_2791 on theBenchmark for (2791ds/262Mi) % 261.59/37.30 % (3791928)Instruction limit reached! % 261.59/37.30 % (3791928)------------------------------ % 261.59/37.30 % (3791928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.59/37.30 % (3791928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.59/37.30 % (3791928)CaDiCaL version: 2.1.3 % 261.59/37.30 % (3791928)Termination reason: Instruction limit % 261.59/37.30 % (3791928)Termination phase: Saturation % 261.59/37.30 % (3791928)Time elapsed: 0.105 s % 261.59/37.30 % (3791928)Peak memory usage: 14 MB % 261.59/37.30 % (3791928)Instructions burned: 265 (million) % 261.59/37.30 % (3791930)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=3229212650:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2790 on theBenchmark for (2790ds/1368Mi) % 261.59/37.30 % (3791930)Instruction limit reached! % 261.59/37.30 % (3791930)------------------------------ % 261.59/37.30 % (3791930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.59/37.30 % (3791930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.59/37.30 % (3791930)CaDiCaL version: 2.1.3 % 261.59/37.30 % (3791930)Termination reason: Instruction limit % 261.59/37.30 % (3791930)Termination phase: Saturation % 261.59/37.30 % (3791930)Time elapsed: 0.396 s % 261.59/37.30 % (3791930)Peak memory usage: 20 MB % 261.59/37.30 % (3791930)Instructions burned: 1368 (million) % 261.59/37.30 % (3791932)ott-21_1_sil=16000:si=on:fs=off:random_seed=2793164456:i=360:av=off:fsr=off:rtra=on_2786 on theBenchmark for (2786ds/360Mi) % 261.59/37.30 % (3791932)Instruction limit reached! % 261.59/37.30 % (3791932)------------------------------ % 261.59/37.30 % (3791932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.59/37.30 % (3791932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.59/37.30 % (3791932)CaDiCaL version: 2.1.3 % 261.59/37.30 % (3791932)Termination reason: Instruction limit % 261.59/37.30 % (3791932)Termination phase: Saturation % 261.59/37.30 % (3791932)Time elapsed: 0.097 s % 261.59/37.30 % (3791932)Peak memory usage: 15 MB % 261.59/37.30 % (3791932)Instructions burned: 364 (million) % 261.59/37.30 % (3791934)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1620325521:i=954:bd=all:rtra=on_2785 on theBenchmark for (2785ds/954Mi) % 261.59/37.30 % (3791934)Instruction limit reached! % 261.59/37.30 % (3791934)------------------------------ % 261.59/37.30 % (3791934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 261.59/37.30 % (3791934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.59/37.30 % (3791934)CaDiCaL version: 2.1.3 % 261.59/37.30 % (3791934)Termination reason: Instruction limit % 261.59/37.30 % (3791934)Termination phase: Saturation % 261.59/37.30 % (3791934)Time elapsed: 0.334 s % 261.59/37.30 % (3791934)Peak memory usage: 16 MB % 261.59/37.30 % (3791934)Instructions burned: 955 (million) % 261.59/37.30 % (3791936)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3953559720:fmbsr=1.3:i=1730:ins=25:rtra=on_2781 on theBenchmark for (2781ds/1730Mi) % 261.59/37.30 % Exception at run slice level % 261.59/37.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.94/42.76 % (3791938)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=807154251:i=2358:rtra=on_2781 on theBenchmark for (2781ds/2358Mi) % 299.94/42.76 % (3791938)Instruction limit reached! % 299.94/42.76 % (3791938)------------------------------ % 299.94/42.76 % (3791938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.94/42.76 % (3791938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.94/42.76 % (3791938)CaDiCaL version: 2.1.3 % 299.94/42.76 % (3791938)Termination reason: Instruction limit % 299.94/42.76 % (3791938)Termination phase: Saturation % 299.94/42.76 % (3791938)Time elapsed: 0.850 s % 299.94/42.76 % (3791938)Peak memory usage: 25 MB % 299.94/42.76 % (3791938)Instructions burned: 2360 (million) % 299.94/42.76 % (3791940)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2415516110:i=1778:ins=1:rtra=on_2773 on theBenchmark for (2773ds/1778Mi) % 299.94/42.76 % Exception at run slice level % 299.94/42.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.94/42.76 % (3791942)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=1401797225:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2772 on theBenchmark for (2772ds/1384Mi) % 299.94/42.76 % (3791942)Instruction limit reached! % 299.94/42.76 % (3791942)------------------------------ % 299.94/42.76 % (3791942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.94/42.76 % (3791942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.94/42.76 % (3791942)CaDiCaL version: 2.1.3 % 299.94/42.76 % (3791942)Termination reason: Instruction limit % 299.94/42.76 % (3791942)Termination phase: Saturation % 299.94/42.76 % (3791942)Time elapsed: 0.473 s % 299.94/42.76 % (3791942)Peak memory usage: 21 MB % 299.94/42.76 % (3791942)Instructions burned: 1386 (million) % 299.94/42.76 % (3791944)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=966897122:i=1758:kws=inv_precedence:fsr=off:rtra=on_2768 on theBenchmark for (2768ds/1758Mi) % 299.94/42.76 % (3791944)Instruction limit reached! % 299.94/42.76 % (3791944)------------------------------ % 299.94/42.76 % (3791944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.94/42.76 % (3791944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.94/42.76 % (3791944)CaDiCaL version: 2.1.3 % 299.94/42.76 % (3791944)Termination reason: Instruction limit % 299.94/42.76 % (3791944)Termination phase: Saturation % 299.94/42.76 % (3791944)Time elapsed: 0.529 s % 299.94/42.76 % (3791944)Peak memory usage: 25 MB % 299.94/42.76 % (3791944)Instructions burned: 1758 (million) % 299.94/42.76 % (3791946)fmb+10_1_sil=64000:si=on:random_seed=1766335720:i=44122:nm=2:rtra=on:gsp=on_2762 on theBenchmark for (2762ds/44122Mi) % 299.94/42.76 % (3791946)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 299.94/42.76 % Exception at run slice level % 299.94/42.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.94/42.76 % (3791948)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3749280046:i=19030:nm=5:rtra=on_2762 on theBenchmark for (2762ds/19030Mi) % 299.94/42.76 % Exception at run slice level % 299.94/42.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.94/42.76 % (3791950)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=691304462:fmbsr=1.7:i=1840:rtra=on_2762 on theBenchmark for (2762ds/1840Mi) % 299.94/42.76 % Exception at run slice level % 299.94/42.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 299.94/42.76 % (3791952)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2631542456:i=10262:rtra=on_2762 on theBenchmark for (2762ds/10262Mi) % 299.94/42.76 % (3791952)Instruction limit reached! % 299.94/42.76 % (3791952)------------------------------ % 299.94/42.76 % (3791952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 299.94/42.76 % (3791952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.94/42.76 % (3791952)CaDiCaL version: 2.1.3 % 299.94/42.76 % (3791952)Termination reason: Instruction limit % 299.94/42.76 % (3791952)Termination phase: Saturation % 299.94/42.76 % (3791952)Time elapsed: 3.223 s % 299.94/42.76 % (3791952)Peak memory usage: 50 MB % 299.94/42.76 % (3791952)Instructions burned: 10265 (million) % 300.63/42.83 % (3791954)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2905004721:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2729 on theBenchmark for (2729ds/2944Mi) % 300.63/42.83 % (3791954)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.63/42.83 % (3791954)Instruction limit reached! % 300.63/42.83 % (3791954)------------------------------ % 300.63/42.83 % (3791954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3791954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3791954)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3791954)Termination reason: Instruction limit % 300.63/42.83 % (3791954)Termination phase: Saturation % 300.63/42.83 % (3791954)Time elapsed: 0.873 s % 300.63/42.83 % (3791954)Peak memory usage: 40 MB % 300.63/42.83 % (3791954)Instructions burned: 2945 (million) % 300.63/42.83 % (3791956)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3158341451:i=12648:rtra=on_2720 on theBenchmark for (2720ds/12648Mi) % 300.63/42.83 % Exception at run slice level % 300.63/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.63/42.83 % (3791958)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1005789631:fmbsr=2.30978:i=4348:rtra=on_2720 on theBenchmark for (2720ds/4348Mi) % 300.63/42.83 % Exception at run slice level % 300.63/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.63/42.83 % (3791960)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3143196307:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2720 on theBenchmark for (2720ds/1738Mi) % 300.63/42.83 % (3791960)Instruction limit reached! % 300.63/42.83 % (3791960)------------------------------ % 300.63/42.83 % (3791960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3791960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3791960)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3791960)Termination reason: Instruction limit % 300.63/42.83 % (3791960)Termination phase: Saturation % 300.63/42.83 % (3791960)Time elapsed: 0.576 s % 300.63/42.83 % (3791960)Peak memory usage: 19 MB % 300.63/42.83 % (3791960)Instructions burned: 1740 (million) % 300.63/42.83 % (3792078)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4143239827:i=10228:av=off:rtra=on_2714 on theBenchmark for (2714ds/10228Mi) % 300.63/42.83 % (3792078)Instruction limit reached! % 300.63/42.83 % (3792078)------------------------------ % 300.63/42.83 % (3792078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3792078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3792078)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3792078)Termination reason: Instruction limit % 300.63/42.83 % (3792078)Termination phase: Saturation % 300.63/42.83 % (3792078)Time elapsed: 3.709 s % 300.63/42.83 % (3792078)Peak memory usage: 36 MB % 300.63/42.83 % (3792078)Instructions burned: 10229 (million) % 300.63/42.83 % (3792307)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=477699033:i=108564:rtra=on_2677 on theBenchmark for (2677ds/108564Mi) % 300.63/42.83 % Exception at run slice level % 300.63/42.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.63/42.83 % (3792309)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2128102639:i=7024:aac=none:rtra=on_2677 on theBenchmark for (2677ds/7024Mi) % 300.63/42.83 % (3792309)Instruction limit reached! % 300.63/42.83 % (3792309)------------------------------ % 300.63/42.83 % (3792309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3792309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.63/42.83 % (3792309)CaDiCaL version: 2.1.3 % 300.63/42.83 % (3792309)Termination reason: Instruction limit % 300.63/42.83 % (3792309)Termination phase: Saturation % 300.63/42.83 % (3792309)Time elapsed: 2.190 s % 300.63/42.83 % (3792309)Peak memory usage: 45 MB % 300.63/42.83 % (3792309)Instructions burned: 7027 (million) % 300.63/42.83 % (3792311)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=747845884:i=7546:rtra=on:amm=off_2655 on theBenchmark for (2655ds/7546Mi) % 300.63/42.83 % (3792311)Instruction limit reached! % 300.63/42.83 % (3792311)------------------------------ % 300.63/42.83 % (3792311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.63/42.83 % (3792311)Linked with Z3 4.14.0.0 3 % 300.63/42.83 Terminated % 300.63/42.83 % Vampire exiting % 300.63/42.83 Terminated %------------------------------------------------------------------------------