%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM968_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 : n001.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:18 PM UTC 2026 % Result : Timeout 300.13s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM968_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.11/0.38 % Computer : n001.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Sun Sep 27 21:54:31 UTC 2026 % 0.11/0.39 % CPUTime : % 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.11/0.42 Running first-order model finding % 0.11/0.42 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 % 7.01/1.63 % (3994526)Will run a generic schedule for satisfiability detection. % 7.01/1.63 % (3994543)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3435219374:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.01/1.63 % (3994540)% WARNING: option uhcvi not known. % 7.01/1.63 % (3994542)dis+10_1_sil=32000:sp=arity:random_seed=1366944834:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.01/1.63 % (3994539)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2231288153_2999 on theBenchmark for (2999ds/0Mi) % 7.01/1.63 % (3994540)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=899914449:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.01/1.63 % (3994545)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1575216530:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.01/1.63 % (3994541)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=260531604:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.01/1.63 % (3994544)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2819093422:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.01/1.63 % Exception at run slice level % 7.01/1.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.01/1.63 % (3994566)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1601696599:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.01/1.63 % Exception at run slice level % 7.01/1.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.01/1.63 % (3994543)Instruction limit reached! % 7.01/1.63 % (3994543)------------------------------ % 7.01/1.63 % (3994543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.01/1.63 % (3994543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.01/1.63 % (3994543)CaDiCaL version: 2.1.3 % 7.01/1.63 % (3994543)Termination reason: Instruction limit % 7.01/1.63 % (3994543)Termination phase: Saturation % 7.01/1.63 % (3994543)Time elapsed: 0.039 s % 7.01/1.63 % (3994543)Peak memory usage: 13 MB % 7.01/1.63 % (3994543)Instructions burned: 118 (million) % 7.01/1.63 % (3994587)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=2457062300:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.01/1.63 % (3994583)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1460292398:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.01/1.63 % (3994542)Instruction limit reached! % 7.01/1.63 % (3994542)------------------------------ % 7.01/1.63 % (3994542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.01/1.63 % (3994542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.01/1.63 % (3994542)CaDiCaL version: 2.1.3 % 7.01/1.63 % (3994542)Termination reason: Instruction limit % 7.01/1.63 % (3994542)Termination phase: Saturation % 7.01/1.63 % (3994542)Time elapsed: 0.060 s % 7.01/1.63 % (3994542)Peak memory usage: 12 MB % 7.01/1.63 % (3994542)Instructions burned: 104 (million) % 7.01/1.63 % (3994544)Instruction limit reached! % 7.01/1.63 % (3994544)------------------------------ % 7.01/1.63 % (3994544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.01/1.63 % (3994544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.01/1.63 % (3994544)CaDiCaL version: 2.1.3 % 7.01/1.63 % (3994544)Termination reason: Instruction limit % 7.01/1.63 % (3994544)Termination phase: Saturation % 7.01/1.63 % (3994544)Time elapsed: 0.061 s % 7.01/1.63 % (3994544)Peak memory usage: 13 MB % 7.01/1.63 % (3994544)Instructions burned: 131 (million) % 7.01/1.63 % (3994596)ott-21_1_sil=16000:fs=off:random_seed=3011222632:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.01/1.63 % (3994599)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1440239572:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 7.01/1.63 % (3994545)Instruction limit reached! % 7.01/1.63 % (3994545)------------------------------ % 7.01/1.63 % (3994545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.01/1.63 % (3994545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.01/1.63 % (3994545)CaDiCaL version: 2.1.3 % 7.01/1.63 % (3994545)Termination reason: Instruction limit % 7.01/1.63 % (3994545)Termination phase: Saturation % 20.16/3.37 % (3994545)Time elapsed: 0.106 s % 20.16/3.37 % (3994545)Peak memory usage: 13 MB % 20.16/3.37 % (3994545)Instructions burned: 160 (million) % 20.16/3.37 % (3994602)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=772481547:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 20.16/3.37 % Exception at run slice level % 20.16/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.16/3.37 % (3994583)Instruction limit reached! % 20.16/3.37 % (3994583)------------------------------ % 20.16/3.37 % (3994583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.16/3.37 % (3994583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.16/3.37 % (3994583)CaDiCaL version: 2.1.3 % 20.16/3.37 % (3994583)Termination reason: Instruction limit % 20.16/3.37 % (3994583)Termination phase: Saturation % 20.16/3.37 % (3994583)Time elapsed: 0.097 s % 20.16/3.37 % (3994583)Peak memory usage: 13 MB % 20.16/3.37 % (3994583)Instructions burned: 131 (million) % 20.16/3.37 % (3994604)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1042025911:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 20.16/3.37 % (3994605)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2016559737:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 20.16/3.37 % Exception at run slice level % 20.16/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.16/3.37 % (3994596)Instruction limit reached! % 20.16/3.37 % (3994596)------------------------------ % 20.16/3.37 % (3994596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.16/3.37 % (3994596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.16/3.37 % (3994596)CaDiCaL version: 2.1.3 % 20.16/3.37 % (3994596)Termination reason: Instruction limit % 20.16/3.37 % (3994596)Termination phase: Saturation % 20.16/3.37 % (3994596)Time elapsed: 0.089 s % 20.16/3.37 % (3994596)Peak memory usage: 13 MB % 20.16/3.37 % (3994596)Instructions burned: 180 (million) % 20.16/3.37 % (3994608)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=1698551055:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 20.16/3.37 % (3994609)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3639403620:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 20.16/3.37 % (3994587)Instruction limit reached! % 20.16/3.37 % (3994587)------------------------------ % 20.16/3.37 % (3994587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.16/3.37 % (3994587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.16/3.37 % (3994587)CaDiCaL version: 2.1.3 % 20.16/3.37 % (3994587)Termination reason: Instruction limit % 20.16/3.37 % (3994587)Termination phase: Saturation % 20.16/3.37 % (3994587)Time elapsed: 0.186 s % 20.16/3.37 % (3994587)Peak memory usage: 16 MB % 20.16/3.37 % (3994587)Instructions burned: 684 (million) % 20.16/3.37 % (3994612)fmb+10_1_sil=64000:random_seed=2550132633:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 20.16/3.37 % (3994612)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 20.16/3.37 % Exception at run slice level % 20.16/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.16/3.37 % (3994614)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2814107339:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 20.16/3.37 % Exception at run slice level % 20.16/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.16/3.37 % (3994616)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1525327858:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 20.16/3.37 % Exception at run slice level % 20.16/3.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 20.16/3.37 % (3994618)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=603534975:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 20.16/3.37 % (3994599)Instruction limit reached! % 20.16/3.37 % (3994599)------------------------------ % 20.16/3.37 % (3994599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 20.16/3.37 % (3994599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.03 % (3994599)CaDiCaL version: 2.1.3 % 59.19/9.03 % (3994599)Termination reason: Instruction limit % 59.19/9.03 % (3994599)Termination phase: Saturation % 59.19/9.03 % (3994599)Time elapsed: 0.291 s % 59.19/9.03 % (3994599)Peak memory usage: 14 MB % 59.19/9.03 % (3994599)Instructions burned: 478 (million) % 59.19/9.03 % (3994620)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=886298953:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 59.19/9.03 % (3994620)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 59.19/9.03 % (3994608)Instruction limit reached! % 59.19/9.03 % (3994608)------------------------------ % 59.19/9.03 % (3994608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.19/9.03 % (3994608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.03 % (3994608)CaDiCaL version: 2.1.3 % 59.19/9.03 % (3994608)Termination reason: Instruction limit % 59.19/9.03 % (3994608)Termination phase: Saturation % 59.19/9.03 % (3994608)Time elapsed: 0.407 s % 59.19/9.03 % (3994608)Peak memory usage: 18 MB % 59.19/9.03 % (3994608)Instructions burned: 693 (million) % 59.19/9.03 % (3994622)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2095737722:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 59.19/9.03 % Exception at run slice level % 59.19/9.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.19/9.03 % (3994624)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3130030563:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 59.19/9.03 % Exception at run slice level % 59.19/9.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.19/9.03 % (3994626)ott-2_1_sil=16000:newcnf=on:random_seed=1151252026:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 59.19/9.03 % (3994609)Instruction limit reached! % 59.19/9.03 % (3994609)------------------------------ % 59.19/9.03 % (3994609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.19/9.03 % (3994609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.03 % (3994609)CaDiCaL version: 2.1.3 % 59.19/9.03 % (3994609)Termination reason: Instruction limit % 59.19/9.03 % (3994609)Termination phase: Saturation % 59.19/9.03 % (3994609)Time elapsed: 0.510 s % 59.19/9.03 % (3994609)Peak memory usage: 18 MB % 59.19/9.03 % (3994609)Instructions burned: 879 (million) % 59.19/9.03 % (3994628)ott+10_1_sil=32000:tgt=ground:random_seed=1004998834:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 59.19/9.03 % (3994604)Instruction limit reached! % 59.19/9.03 % (3994604)------------------------------ % 59.19/9.03 % (3994604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.19/9.03 % (3994604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.03 % (3994604)CaDiCaL version: 2.1.3 % 59.19/9.03 % (3994604)Termination reason: Instruction limit % 59.19/9.03 % (3994604)Termination phase: Saturation % 59.19/9.03 % (3994604)Time elapsed: 0.660 s % 59.19/9.03 % (3994604)Peak memory usage: 20 MB % 59.19/9.03 % (3994604)Instructions burned: 1180 (million) % 59.19/9.03 % (3994630)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=470601621:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 59.19/9.03 % Exception at run slice level % 59.19/9.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 59.19/9.03 % (3994632)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1769703768:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 59.19/9.03 % (3994620)Instruction limit reached! % 59.19/9.03 % (3994620)------------------------------ % 59.19/9.03 % (3994620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 59.19/9.03 % (3994620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.03 % (3994620)CaDiCaL version: 2.1.3 % 59.19/9.03 % (3994620)Termination reason: Instruction limit % 59.19/9.03 % (3994620)Termination phase: Saturation % 59.19/9.03 % (3994620)Time elapsed: 0.721 s % 59.19/9.03 % (3994620)Peak memory usage: 24 MB % 59.19/9.03 % (3994620)Instructions burned: 1473 (million) % 59.19/9.03 % (3994634)dis+21_1_sil=32000:sas=cadical:random_seed=3792480039:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 59.19/9.03 % (3994626)Instruction limit reached! % 59.19/9.03 % (3994626)------------------------------ % 59.19/9.03 % (3994626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.21/17.63 % (3994626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.21/17.63 % (3994626)CaDiCaL version: 2.1.3 % 121.21/17.63 % (3994626)Termination reason: Instruction limit % 121.21/17.63 % (3994626)Termination phase: Saturation % 121.21/17.63 % (3994626)Time elapsed: 0.493 s % 121.21/17.63 % (3994626)Peak memory usage: 18 MB % 121.21/17.63 % (3994626)Instructions burned: 870 (million) % 121.21/17.63 % (3994636)ott+11_1_sil=16000:gs=on:random_seed=3025207125:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 121.21/17.63 % (3994618)Instruction limit reached! % 121.21/17.63 % (3994618)------------------------------ % 121.21/17.63 % (3994618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.21/17.63 % (3994618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.21/17.63 % (3994618)CaDiCaL version: 2.1.3 % 121.21/17.63 % (3994618)Termination reason: Instruction limit % 121.21/17.63 % (3994618)Termination phase: Saturation % 121.21/17.63 % (3994618)Time elapsed: 1.435 s % 121.21/17.63 % (3994618)Peak memory usage: 40 MB % 121.21/17.63 % (3994618)Instructions burned: 5134 (million) % 121.21/17.63 % (3994638)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=454367159:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 121.21/17.63 % Exception at run slice level % 121.21/17.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 121.21/17.63 % (3994640)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2449274097:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 121.21/17.63 % (3994636)Instruction limit reached! % 121.21/17.63 % (3994636)------------------------------ % 121.21/17.63 % (3994636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.21/17.63 % (3994636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.21/17.63 % (3994636)CaDiCaL version: 2.1.3 % 121.21/17.63 % (3994636)Termination reason: Instruction limit % 121.21/17.63 % (3994636)Termination phase: Saturation % 121.21/17.63 % (3994636)Time elapsed: 1.308 s % 121.21/17.63 % (3994636)Peak memory usage: 28 MB % 121.21/17.63 % (3994636)Instructions burned: 2251 (million) % 121.21/17.63 % (3994642)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1689574532:i=29340_2974 on theBenchmark for (2974ds/29340Mi) % 121.21/17.63 % (3994632)Instruction limit reached! % 121.21/17.63 % (3994632)------------------------------ % 121.21/17.63 % (3994632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.21/17.63 % (3994632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.21/17.63 % (3994632)CaDiCaL version: 2.1.3 % 121.21/17.63 % (3994632)Termination reason: Instruction limit % 121.21/17.63 % (3994632)Termination phase: Saturation % 121.21/17.63 % (3994632)Time elapsed: 1.872 s % 121.21/17.63 % (3994632)Peak memory usage: 30 MB % 121.21/17.63 % (3994632)Instructions burned: 3513 (million) % 121.21/17.63 % (3994644)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2524677830:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 121.21/17.63 % (3994640)Instruction limit reached! % 121.21/17.63 % (3994640)------------------------------ % 121.21/17.63 % (3994640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 121.21/17.63 % (3994640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.21/17.63 % (3994640)CaDiCaL version: 2.1.3 % 121.21/17.63 % (3994640)Termination reason: Instruction limit % 121.21/17.63 % (3994640)Termination phase: Saturation % 121.21/17.63 % (3994640)Time elapsed: 1.093 s % 121.21/17.63 % (3994640)Peak memory usage: 43 MB % 121.21/17.63 % (3994640)Instructions burned: 4592 (million) % 121.21/17.63 % (3994646)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=31056519:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 121.21/17.63 % Exception at run slice level % 121.21/17.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 121.21/17.63 % (3994648)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1646239061:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 121.21/17.63 % Exception at run slice level % 121.21/17.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 121.21/17.63 % (3994650)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=440548448:i=14071_2970 on theBenchmark for (2970ds/14071Mi) % 121.21/17.63 % Exception at run slice level % 198.45/33.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.45/33.12 % (3994652)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1973005586:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 198.45/33.12 % (3994634)Instruction limit reached! % 198.45/33.12 % (3994634)------------------------------ % 198.45/33.12 % (3994634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.45/33.12 % (3994634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.45/33.12 % (3994634)CaDiCaL version: 2.1.3 % 198.45/33.12 % (3994634)Termination reason: Instruction limit % 198.45/33.12 % (3994634)Termination phase: Saturation % 198.45/33.12 % (3994634)Time elapsed: 1.986 s % 198.45/33.12 % (3994634)Peak memory usage: 37 MB % 198.45/33.12 % (3994634)Instructions burned: 3773 (million) % 198.45/33.12 % (3994654)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=583937145:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 198.45/33.12 % (3994628)Instruction limit reached! % 198.45/33.12 % (3994628)------------------------------ % 198.45/33.12 % (3994628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.45/33.12 % (3994628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.45/33.12 % (3994628)CaDiCaL version: 2.1.3 % 198.45/33.12 % (3994628)Termination reason: Instruction limit % 198.45/33.12 % (3994628)Termination phase: Saturation % 198.45/33.12 % (3994628)Time elapsed: 2.963 s % 198.45/33.12 % (3994628)Peak memory usage: 44 MB % 198.45/33.12 % (3994628)Instructions burned: 5115 (million) % 198.45/33.12 % (3994656)dis+10_16:1_sil=16000:random_seed=1130408015:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi) % 198.45/33.12 % (3994644)Instruction limit reached! % 198.45/33.12 % (3994644)------------------------------ % 198.45/33.12 % (3994644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.45/33.12 % (3994644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.45/33.12 % (3994644)CaDiCaL version: 2.1.3 % 198.45/33.12 % (3994644)Termination reason: Instruction limit % 198.45/33.12 % (3994644)Termination phase: Saturation % 198.45/33.12 % (3994644)Time elapsed: 2.895 s % 198.45/33.12 % (3994644)Peak memory usage: 50 MB % 198.45/33.12 % (3994644)Instructions burned: 5211 (million) % 198.45/33.12 % (3994658)ott-3_8_sil=64000:random_seed=2014595231:i=20139:bs=on_2943 on theBenchmark for (2943ds/20139Mi) % 198.45/33.12 % (3994652)Instruction limit reached! % 198.45/33.12 % (3994652)------------------------------ % 198.45/33.12 % (3994652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.45/33.12 % (3994652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.45/33.12 % (3994652)CaDiCaL version: 2.1.3 % 198.45/33.12 % (3994652)Termination reason: Instruction limit % 198.45/33.12 % (3994652)Termination phase: Saturation % 198.45/33.12 % (3994652)Time elapsed: 4.942 s % 198.45/33.12 % (3994652)Peak memory usage: 42 MB % 198.45/33.12 % (3994652)Instructions burned: 22570 (million) % 198.45/33.12 % (3994660)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2686569742:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi) % 198.45/33.12 % Exception at run slice level % 198.45/33.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.45/33.12 % (3994662)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3647023086:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 198.45/33.12 % (3994654)Instruction limit reached! % 198.45/33.12 % (3994654)------------------------------ % 198.45/33.12 % (3994654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.45/33.12 % (3994654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.45/33.12 % (3994654)CaDiCaL version: 2.1.3 % 198.45/33.12 % (3994654)Termination reason: Instruction limit % 198.45/33.12 % (3994654)Termination phase: Saturation % 198.45/33.12 % (3994654)Time elapsed: 5.011 s % 198.45/33.12 % (3994654)Peak memory usage: 67 MB % 198.45/33.12 % (3994654)Instructions burned: 8173 (million) % 198.45/33.12 % (3994664)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=42516364:i=14134_2917 on theBenchmark for (2917ds/14134Mi) % 198.45/33.12 % (3994656)Instruction limit reached! % 198.45/33.12 % (3994656)------------------------------ % 198.45/33.12 % (3994656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.45/33.12 % (3994656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.45/33.12 % (3994656)CaDiCaL version: 2.1.3 % 238.53/34.06 % (3994656)Termination reason: Instruction limit % 238.53/34.06 % (3994656)Termination phase: Saturation % 238.53/34.06 % (3994656)Time elapsed: 4.846 s % 238.53/34.06 % (3994656)Peak memory usage: 56 MB % 238.53/34.06 % (3994656)Instructions burned: 9156 (million) % 238.53/34.06 % (3994666)dis+33_16_sil=32000:sac=on:random_seed=2384893273:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 238.53/34.06 % (3994662)Instruction limit reached! % 238.53/34.06 % (3994662)------------------------------ % 238.53/34.06 % (3994662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.53/34.06 % (3994662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.53/34.06 % (3994662)CaDiCaL version: 2.1.3 % 238.53/34.06 % (3994662)Termination reason: Instruction limit % 238.53/34.06 % (3994662)Termination phase: Saturation % 238.53/34.06 % (3994662)Time elapsed: 3.875 s % 238.53/34.06 % (3994662)Peak memory usage: 71 MB % 238.53/34.06 % (3994662)Instructions burned: 11405 (million) % 238.53/34.06 % (3994668)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4142757834:avsq=on:i=17627:add=on:amm=off_2881 on theBenchmark for (2881ds/17627Mi) % 238.53/34.06 % (3994668)Instruction limit reached! % 238.53/34.06 % (3994668)------------------------------ % 238.53/34.06 % (3994668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.53/34.06 % (3994668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.53/34.06 % (3994668)CaDiCaL version: 2.1.3 % 238.53/34.06 % (3994668)Termination reason: Instruction limit % 238.53/34.06 % (3994668)Termination phase: Saturation % 238.53/34.06 % (3994668)Time elapsed: 5.020 s % 238.53/34.06 % (3994668)Peak memory usage: 122 MB % 238.53/34.06 % (3994668)Instructions burned: 17630 (million) % 238.53/34.06 % (3995029)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1364982148:s2a=on:i=53295_2831 on theBenchmark for (2831ds/53295Mi) % 238.53/34.06 % (3994666)Instruction limit reached! % 238.53/34.06 % (3994666)------------------------------ % 238.53/34.06 % (3994666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.53/34.06 % (3994666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.53/34.06 % (3994666)CaDiCaL version: 2.1.3 % 238.53/34.06 % (3994666)Termination reason: Instruction limit % 238.53/34.06 % (3994666)Termination phase: Saturation % 238.53/34.06 % (3994666)Time elapsed: 8.247 s % 238.53/34.06 % (3994666)Peak memory usage: 122 MB % 238.53/34.06 % (3994666)Instructions burned: 15852 (million) % 238.53/34.06 % (3995031)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=956255928:i=26857:ins=20_2831 on theBenchmark for (2831ds/26857Mi) % 238.53/34.06 % Exception at run slice level % 238.53/34.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 238.53/34.06 % (3995033)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=580724550:i=28120:bs=on:fsr=off_2830 on theBenchmark for (2830ds/28120Mi) % 238.53/34.06 % (3994664)Instruction limit reached! % 238.53/34.06 % (3994664)------------------------------ % 238.53/34.06 % (3994664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.53/34.06 % (3994664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.53/34.06 % (3994664)CaDiCaL version: 2.1.3 % 238.53/34.06 % (3994664)Termination reason: Instruction limit % 238.53/34.06 % (3994664)Termination phase: Saturation % 238.53/34.06 % (3994664)Time elapsed: 8.866 s % 238.53/34.06 % (3994664)Peak memory usage: 83 MB % 238.53/34.06 % (3994664)Instructions burned: 14135 (million) % 238.53/34.06 % (3995035)fmb+10_1_sil=256000:fmbss=7:random_seed=1119959164:fmbsr=1.6:i=182295_2828 on theBenchmark for (2828ds/182295Mi) % 238.53/34.06 % Exception at run slice level % 238.53/34.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 238.53/34.06 % (3995037)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3034791813:i=44625:gsp=on_2828 on theBenchmark for (2828ds/44625Mi) % 238.53/34.06 % (3995037)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 238.53/34.06 % Exception at run slice level % 238.53/34.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 238.53/34.06 % (3995039)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1386560349:i=160505_2828 on theBenchmark for (2828ds/160505Mi) % 238.53/34.06 % Exception at run slice level % 238.53/34.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 238.53/34.06 % (3995041)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=138306451:fmbsr=1.3:i=225729_2828 on theBenchmark for (2828ds/225729Mi) % 253.76/36.28 % Exception at run slice level % 253.76/36.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.76/36.28 % (3995043)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1841548017:fmbsr=2:i=185024:ins=7_2827 on theBenchmark for (2827ds/185024Mi) % 253.76/36.28 % Exception at run slice level % 253.76/36.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.76/36.28 % (3995045)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1907492239:rtra=on_2827 on theBenchmark for (2827ds/0Mi) % 253.76/36.28 % Exception at run slice level % 253.76/36.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.76/36.28 % (3995047)% WARNING: option uhcvi not known. % 253.76/36.28 % (3995047)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3164410802:i=271062:add=off:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/271062Mi) % 253.76/36.28 % (3994658)Instruction limit reached! % 253.76/36.28 % (3994658)------------------------------ % 253.76/36.28 % (3994658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.28 % (3994658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.28 % (3994658)CaDiCaL version: 2.1.3 % 253.76/36.28 % (3994658)Termination reason: Instruction limit % 253.76/36.28 % (3994658)Termination phase: Saturation % 253.76/36.28 % (3994658)Time elapsed: 12.512 s % 253.76/36.28 % (3994658)Peak memory usage: 142 MB % 253.76/36.28 % (3994658)Instructions burned: 20140 (million) % 253.76/36.28 % (3995049)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=294658684:i=176048:add=on:rtra=on:rawr=on_2817 on theBenchmark for (2817ds/176048Mi) % 253.76/36.28 % (3995029)Instruction limit reached! % 253.76/36.28 % (3995029)------------------------------ % 253.76/36.28 % (3995029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.28 % (3995029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.28 % (3995029)CaDiCaL version: 2.1.3 % 253.76/36.28 % (3995029)Termination reason: Instruction limit % 253.76/36.28 % (3995029)Termination phase: Saturation % 253.76/36.28 % (3995029)Time elapsed: 15.478 s % 253.76/36.28 % (3995029)Peak memory usage: 317 MB % 253.76/36.28 % (3995029)Instructions burned: 53295 (million) % 253.76/36.28 % (3995357)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2648677904:i=206:fgj=on:rtra=on_2676 on theBenchmark for (2676ds/206Mi) % 253.76/36.28 % (3995357)Instruction limit reached! % 253.76/36.28 % (3995357)------------------------------ % 253.76/36.28 % (3995357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.28 % (3995357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.28 % (3995357)CaDiCaL version: 2.1.3 % 253.76/36.28 % (3995357)Termination reason: Instruction limit % 253.76/36.28 % (3995357)Termination phase: Saturation % 253.76/36.28 % (3995357)Time elapsed: 0.107 s % 253.76/36.28 % (3995357)Peak memory usage: 13 MB % 253.76/36.28 % (3995357)Instructions burned: 208 (million) % 253.76/36.28 % (3995359)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3242996085:i=232:rtra=on_2674 on theBenchmark for (2674ds/232Mi) % 253.76/36.28 % (3994541)Instruction limit reached! % 253.76/36.28 % (3994541)------------------------------ % 253.76/36.28 % (3994541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.28 % (3994541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.28 % (3994541)CaDiCaL version: 2.1.3 % 253.76/36.28 % (3994541)Termination reason: Instruction limit % 253.76/36.28 % (3994541)Termination phase: Saturation % 253.76/36.28 % (3994541)Time elapsed: 32.535 s % 253.76/36.28 % (3994541)Peak memory usage: 181 MB % 253.76/36.28 % (3994541)Instructions burned: 88025 (million) % 253.76/36.28 % (3995361)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4088923494:i=262:rtra=on_2673 on theBenchmark for (2673ds/262Mi) % 253.76/36.28 % (3995359)Instruction limit reached! % 253.76/36.28 % (3995359)------------------------------ % 253.76/36.28 % (3995359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.76/36.28 % (3995359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.76/36.28 % (3995359)CaDiCaL version: 2.1.3 % 253.76/36.28 % (3995359)Termination reason: Instruction limit % 253.76/36.28 % (3995359)Termination phase:Terminated % 300.13/42.74 % Vampire exiting % 300.13/42.74 Terminated %------------------------------------------------------------------------------