%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW566_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 : n005.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:40:27 PM UTC 2026 % Result : Timeout 289.64s 41.12s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW566_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.06/0.18 % Computer : n005.cluster.edu % 0.06/0.18 % Model : x86_64 x86_64 % 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.18 % Memory : 8046.5625MB % 0.06/0.18 % OS : Linux 6.8.0-71-generic % 0.06/0.18 % CPULimit : 300 % 0.06/0.18 % WCLimit : 300 % 0.06/0.18 % DateTime : Mon Sep 28 14:19:16 UTC 2026 % 0.06/0.18 % CPUTime : % 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.06/0.22 Running first-order model finding % 0.06/0.22 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.98/1.42 % (811153)Will run a generic schedule for satisfiability detection. % 7.98/1.42 % (811174)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=765361895:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.98/1.42 % (811169)% WARNING: option uhcvi not known. % 7.98/1.42 % (811171)dis+10_1_sil=32000:sp=arity:random_seed=3646971216:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.98/1.42 % (811168)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=156403667_2999 on theBenchmark for (2999ds/0Mi) % 7.98/1.42 % (811169)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1011616442:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.98/1.42 % (811170)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1887817871:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.98/1.42 % (811172)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1861856651:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.98/1.42 % (811173)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=640553900:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.98/1.42 % Exception at run slice level % 7.98/1.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.98/1.42 % (811189)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=677201627:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.98/1.42 % Exception at run slice level % 7.98/1.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.98/1.42 % (811174)Instruction limit reached! % 7.98/1.42 % (811174)------------------------------ % 7.98/1.42 % (811174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.42 % (811174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.42 % (811174)CaDiCaL version: 2.1.3 % 7.98/1.42 % (811174)Termination reason: Instruction limit % 7.98/1.42 % (811174)Termination phase: Saturation % 7.98/1.42 % (811174)Time elapsed: 0.050 s % 7.98/1.42 % (811174)Peak memory usage: 13 MB % 7.98/1.42 % (811174)Instructions burned: 160 (million) % 7.98/1.42 % (811198)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=1288060049:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.98/1.42 % (811197)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1497024947:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.98/1.42 % (811171)Instruction limit reached! % 7.98/1.42 % (811171)------------------------------ % 7.98/1.42 % (811171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.42 % (811171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.42 % (811171)CaDiCaL version: 2.1.3 % 7.98/1.42 % (811171)Termination reason: Instruction limit % 7.98/1.42 % (811171)Termination phase: Saturation % 7.98/1.42 % (811171)Time elapsed: 0.061 s % 7.98/1.42 % (811171)Peak memory usage: 12 MB % 7.98/1.42 % (811171)Instructions burned: 104 (million) % 7.98/1.42 % (811172)Instruction limit reached! % 7.98/1.42 % (811172)------------------------------ % 7.98/1.42 % (811172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.42 % (811172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.42 % (811172)CaDiCaL version: 2.1.3 % 7.98/1.42 % (811172)Termination reason: Instruction limit % 7.98/1.42 % (811172)Termination phase: Saturation % 7.98/1.42 % (811172)Time elapsed: 0.063 s % 7.98/1.42 % (811172)Peak memory usage: 13 MB % 7.98/1.42 % (811172)Instructions burned: 117 (million) % 7.98/1.42 % (811173)Instruction limit reached! % 7.98/1.42 % (811173)------------------------------ % 7.98/1.42 % (811173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.98/1.42 % (811173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.98/1.42 % (811173)CaDiCaL version: 2.1.3 % 7.98/1.42 % (811173)Termination reason: Instruction limit % 7.98/1.42 % (811173)Termination phase: Saturation % 7.98/1.42 % (811173)Time elapsed: 0.078 s % 7.98/1.42 % (811173)Peak memory usage: 13 MB % 7.98/1.42 % (811173)Instructions burned: 132 (million) % 7.98/1.42 % (811204)ott-21_1_sil=16000:fs=off:random_seed=2664744381:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.98/1.42 % (811205)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=685041223:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 18.57/2.94 % (811209)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2671348401:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 18.57/2.94 % Exception at run slice level % 18.57/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.57/2.94 % (811219)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3753195488:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 18.57/2.94 % (811197)Instruction limit reached! % 18.57/2.94 % (811197)------------------------------ % 18.57/2.94 % (811197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.57/2.94 % (811197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.57/2.94 % (811197)CaDiCaL version: 2.1.3 % 18.57/2.94 % (811197)Termination reason: Instruction limit % 18.57/2.94 % (811197)Termination phase: Saturation % 18.57/2.94 % (811197)Time elapsed: 0.082 s % 18.57/2.94 % (811197)Peak memory usage: 13 MB % 18.57/2.94 % (811197)Instructions burned: 131 (million) % 18.57/2.94 % (811228)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=344612251:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 18.57/2.94 % Exception at run slice level % 18.57/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.57/2.94 % (811204)Instruction limit reached! % 18.57/2.94 % (811204)------------------------------ % 18.57/2.94 % (811204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.57/2.94 % (811204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.57/2.94 % (811204)CaDiCaL version: 2.1.3 % 18.57/2.94 % (811204)Termination reason: Instruction limit % 18.57/2.94 % (811204)Termination phase: Saturation % 18.57/2.94 % (811204)Time elapsed: 0.099 s % 18.57/2.94 % (811204)Peak memory usage: 12 MB % 18.57/2.94 % (811204)Instructions burned: 182 (million) % 18.57/2.94 % (811233)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=2292963673: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) % 18.57/2.94 % (811239)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=33265097:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.57/2.94 % (811198)Instruction limit reached! % 18.57/2.94 % (811198)------------------------------ % 18.57/2.94 % (811198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.57/2.94 % (811198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.57/2.94 % (811198)CaDiCaL version: 2.1.3 % 18.57/2.94 % (811198)Termination reason: Instruction limit % 18.57/2.94 % (811198)Termination phase: Saturation % 18.57/2.94 % (811198)Time elapsed: 0.207 s % 18.57/2.94 % (811198)Peak memory usage: 16 MB % 18.57/2.94 % (811198)Instructions burned: 686 (million) % 18.57/2.94 % (811267)fmb+10_1_sil=64000:random_seed=2332243664:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 18.57/2.94 % (811267)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.57/2.94 % Exception at run slice level % 18.57/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.57/2.94 % (811278)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2965738659:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 18.57/2.94 % Exception at run slice level % 18.57/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.57/2.94 % (811288)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2166151492:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.57/2.94 % Exception at run slice level % 18.57/2.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.57/2.94 % (811294)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2423175298:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 18.57/2.94 % (811205)Instruction limit reached! % 18.57/2.94 % (811205)------------------------------ % 18.57/2.94 % (811205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.57/2.94 % (811205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.57/2.94 % (811205)CaDiCaL version: 2.1.3 % 18.57/2.94 % (811205)Termination reason: Instruction limit % 18.57/2.94 % (811205)Termination phase: Saturation % 71.48/10.34 % (811205)Time elapsed: 0.248 s % 71.48/10.34 % (811205)Peak memory usage: 16 MB % 71.48/10.34 % (811205)Instructions burned: 479 (million) % 71.48/10.34 % (811302)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=208051157:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 71.48/10.34 % (811302)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 71.48/10.34 % (811233)Instruction limit reached! % 71.48/10.34 % (811233)------------------------------ % 71.48/10.34 % (811233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.48/10.34 % (811233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.48/10.34 % (811233)CaDiCaL version: 2.1.3 % 71.48/10.34 % (811233)Termination reason: Instruction limit % 71.48/10.34 % (811233)Termination phase: Saturation % 71.48/10.34 % (811233)Time elapsed: 0.398 s % 71.48/10.34 % (811233)Peak memory usage: 18 MB % 71.48/10.34 % (811233)Instructions burned: 693 (million) % 71.48/10.34 % (811304)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2889267530:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 71.48/10.34 % Exception at run slice level % 71.48/10.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.48/10.34 % (811306)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=943508017:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 71.48/10.34 % Exception at run slice level % 71.48/10.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.48/10.34 % (811308)ott-2_1_sil=16000:newcnf=on:random_seed=2814281168:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 71.48/10.34 % (811239)Instruction limit reached! % 71.48/10.34 % (811239)------------------------------ % 71.48/10.34 % (811239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.48/10.34 % (811239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.48/10.34 % (811239)CaDiCaL version: 2.1.3 % 71.48/10.34 % (811239)Termination reason: Instruction limit % 71.48/10.34 % (811239)Termination phase: Saturation % 71.48/10.34 % (811239)Time elapsed: 0.481 s % 71.48/10.34 % (811239)Peak memory usage: 20 MB % 71.48/10.34 % (811239)Instructions burned: 881 (million) % 71.48/10.34 % (811310)ott+10_1_sil=32000:tgt=ground:random_seed=2734817148:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 71.48/10.34 % (811219)Instruction limit reached! % 71.48/10.34 % (811219)------------------------------ % 71.48/10.34 % (811219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.48/10.34 % (811219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.48/10.34 % (811219)CaDiCaL version: 2.1.3 % 71.48/10.34 % (811219)Termination reason: Instruction limit % 71.48/10.34 % (811219)Termination phase: Saturation % 71.48/10.34 % (811219)Time elapsed: 0.649 s % 71.48/10.34 % (811219)Peak memory usage: 21 MB % 71.48/10.34 % (811219)Instructions burned: 1180 (million) % 71.48/10.34 % (811312)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4018150156:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 71.48/10.34 % Exception at run slice level % 71.48/10.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 71.48/10.34 % (811314)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=645144352:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 71.48/10.34 % (811308)Instruction limit reached! % 71.48/10.34 % (811308)------------------------------ % 71.48/10.34 % (811308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.48/10.34 % (811308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.48/10.34 % (811308)CaDiCaL version: 2.1.3 % 71.48/10.34 % (811308)Termination reason: Instruction limit % 71.48/10.34 % (811308)Termination phase: Saturation % 71.48/10.34 % (811308)Time elapsed: 0.494 s % 71.48/10.34 % (811308)Peak memory usage: 18 MB % 71.48/10.34 % (811308)Instructions burned: 870 (million) % 71.48/10.34 % (811302)Instruction limit reached! % 71.48/10.34 % (811302)------------------------------ % 71.48/10.34 % (811302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 71.48/10.34 % (811302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.48/10.34 % (811302)CaDiCaL version: 2.1.3 % 71.48/10.34 % (811302)Termination reason: Instruction limit % 71.48/10.34 % (811302)Termination phase: Saturation % 71.48/10.34 % (811302)Time elapsed: 0.808 s % 103.97/14.96 % (811302)Peak memory usage: 26 MB % 103.97/14.96 % (811302)Instructions burned: 1472 (million) % 103.97/14.96 % (811316)dis+21_1_sil=32000:sas=cadical:random_seed=654778080:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 103.97/14.96 % (811317)ott+11_1_sil=16000:gs=on:random_seed=2438862315:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 103.97/14.96 % (811294)Instruction limit reached! % 103.97/14.96 % (811294)------------------------------ % 103.97/14.96 % (811294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.97/14.96 % (811294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.97/14.96 % (811294)CaDiCaL version: 2.1.3 % 103.97/14.96 % (811294)Termination reason: Instruction limit % 103.97/14.96 % (811294)Termination phase: Saturation % 103.97/14.96 % (811294)Time elapsed: 1.431 s % 103.97/14.96 % (811294)Peak memory usage: 27 MB % 103.97/14.96 % (811294)Instructions burned: 5133 (million) % 103.97/14.96 % (811320)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3349590276:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi) % 103.97/14.96 % Exception at run slice level % 103.97/14.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.97/14.96 % (811322)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2392727461:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 103.97/14.96 % (811317)Instruction limit reached! % 103.97/14.96 % (811317)------------------------------ % 103.97/14.96 % (811317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.97/14.96 % (811317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.97/14.96 % (811317)CaDiCaL version: 2.1.3 % 103.97/14.96 % (811317)Termination reason: Instruction limit % 103.97/14.96 % (811317)Termination phase: Saturation % 103.97/14.96 % (811317)Time elapsed: 1.207 s % 103.97/14.96 % (811317)Peak memory usage: 26 MB % 103.97/14.96 % (811317)Instructions burned: 2252 (million) % 103.97/14.96 % (811324)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2113704886:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 103.97/14.96 % (811322)Instruction limit reached! % 103.97/14.96 % (811322)------------------------------ % 103.97/14.96 % (811322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.97/14.96 % (811322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.97/14.96 % (811322)CaDiCaL version: 2.1.3 % 103.97/14.96 % (811322)Termination reason: Instruction limit % 103.97/14.96 % (811322)Termination phase: Saturation % 103.97/14.96 % (811322)Time elapsed: 0.722 s % 103.97/14.96 % (811322)Peak memory usage: 14 MB % 103.97/14.96 % (811322)Instructions burned: 4598 (million) % 103.97/14.96 % (811326)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=726249049:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 103.97/14.96 % (811314)Instruction limit reached! % 103.97/14.96 % (811314)------------------------------ % 103.97/14.96 % (811314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 103.97/14.96 % (811314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.97/14.96 % (811314)CaDiCaL version: 2.1.3 % 103.97/14.96 % (811314)Termination reason: Instruction limit % 103.97/14.96 % (811314)Termination phase: Saturation % 103.97/14.96 % (811314)Time elapsed: 1.758 s % 103.97/14.96 % (811314)Peak memory usage: 22 MB % 103.97/14.96 % (811314)Instructions burned: 3513 (million) % 103.97/14.96 % (811328)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1634857060:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi) % 103.97/14.96 % Exception at run slice level % 103.97/14.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.97/14.96 % (811330)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1651617993:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi) % 103.97/14.96 % Exception at run slice level % 103.97/14.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.97/14.96 % (811332)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3737249740:i=14071_2973 on theBenchmark for (2973ds/14071Mi) % 103.97/14.96 % Exception at run slice level % 103.97/14.96 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 103.97/14.96 % (811334)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1844610377:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi) % 166.41/23.74 % (811316)Instruction limit reached! % 166.41/23.74 % (811316)------------------------------ % 166.41/23.74 % (811316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.41/23.74 % (811316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/23.74 % (811316)CaDiCaL version: 2.1.3 % 166.41/23.74 % (811316)Termination reason: Instruction limit % 166.41/23.74 % (811316)Termination phase: Saturation % 166.41/23.74 % (811316)Time elapsed: 2.140 s % 166.41/23.74 % (811316)Peak memory usage: 24 MB % 166.41/23.74 % (811316)Instructions burned: 3775 (million) % 166.41/23.74 % (811336)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=992767799:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi) % 166.41/23.74 % (811310)Instruction limit reached! % 166.41/23.74 % (811310)------------------------------ % 166.41/23.74 % (811310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.41/23.74 % (811310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/23.74 % (811310)CaDiCaL version: 2.1.3 % 166.41/23.74 % (811310)Termination reason: Instruction limit % 166.41/23.74 % (811310)Termination phase: Saturation % 166.41/23.74 % (811310)Time elapsed: 2.911 s % 166.41/23.74 % (811310)Peak memory usage: 41 MB % 166.41/23.74 % (811310)Instructions burned: 5116 (million) % 166.41/23.74 % (811338)dis+10_16:1_sil=16000:random_seed=3387834183:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 166.41/23.74 % (811326)Instruction limit reached! % 166.41/23.74 % (811326)------------------------------ % 166.41/23.74 % (811326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.41/23.74 % (811326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/23.74 % (811326)CaDiCaL version: 2.1.3 % 166.41/23.74 % (811326)Termination reason: Instruction limit % 166.41/23.74 % (811326)Termination phase: Saturation % 166.41/23.74 % (811326)Time elapsed: 1.431 s % 166.41/23.74 % (811326)Peak memory usage: 50 MB % 166.41/23.74 % (811326)Instructions burned: 5212 (million) % 166.41/23.74 % (811340)ott-3_8_sil=64000:random_seed=1474500385:i=20139:bs=on_2960 on theBenchmark for (2960ds/20139Mi) % 166.41/23.74 % (811336)Instruction limit reached! % 166.41/23.74 % (811336)------------------------------ % 166.41/23.74 % (811336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.41/23.74 % (811336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/23.74 % (811336)CaDiCaL version: 2.1.3 % 166.41/23.74 % (811336)Termination reason: Instruction limit % 166.41/23.74 % (811336)Termination phase: Saturation % 166.41/23.74 % (811336)Time elapsed: 4.571 s % 166.41/23.74 % (811336)Peak memory usage: 62 MB % 166.41/23.74 % (811336)Instructions burned: 8173 (million) % 166.41/23.74 % (811342)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=396939228:fmbsr=2:i=32576_2920 on theBenchmark for (2920ds/32576Mi) % 166.41/23.74 % Exception at run slice level % 166.41/23.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 166.41/23.74 % (811344)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3823088734:i=11404_2920 on theBenchmark for (2920ds/11404Mi) % 166.41/23.74 % (811338)Instruction limit reached! % 166.41/23.74 % (811338)------------------------------ % 166.41/23.74 % (811338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.41/23.74 % (811338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/23.74 % (811338)CaDiCaL version: 2.1.3 % 166.41/23.74 % (811338)Termination reason: Instruction limit % 166.41/23.74 % (811338)Termination phase: Saturation % 166.41/23.74 % (811338)Time elapsed: 4.761 s % 166.41/23.74 % (811338)Peak memory usage: 33 MB % 166.41/23.74 % (811338)Instructions burned: 9156 (million) % 166.41/23.74 % (811346)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1126830718:i=14134_2915 on theBenchmark for (2915ds/14134Mi) % 166.41/23.74 % (811340)Instruction limit reached! % 166.41/23.74 % (811340)------------------------------ % 166.41/23.74 % (811340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 166.41/23.74 % (811340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.41/23.74 % (811340)CaDiCaL version: 2.1.3 % 166.41/23.74 % (811340)Termination reason: Instruction limit % 166.41/23.74 % (811340)Termination phase: Saturation % 166.41/23.74 % (811340)Time elapsed: 6.115 s % 166.41/23.74 % (811340)Peak memory usage: 89 MB % 166.41/23.74 % (811340)Instructions burned: 20141 (million) % 166.41/23.74 % (811348)dis+33_16_sil=32000:sac=on:random_seed=3899424173:i=15851:nm=0_2898 on theBenchmark for (2898ds/15851Mi) % 189.28/26.92 % (811334)Instruction limit reached! % 189.28/26.92 % (811334)------------------------------ % 189.28/26.92 % (811334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.28/26.92 % (811334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.28/26.92 % (811334)CaDiCaL version: 2.1.3 % 189.28/26.92 % (811334)Termination reason: Instruction limit % 189.28/26.92 % (811334)Termination phase: Saturation % 189.28/26.92 % (811334)Time elapsed: 9.673 s % 189.28/26.92 % (811334)Peak memory usage: 75 MB % 189.28/26.92 % (811334)Instructions burned: 22565 (million) % 189.28/26.92 % (811350)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1787421406:avsq=on:i=17627:add=on:amm=off_2875 on theBenchmark for (2875ds/17627Mi) % 189.28/26.92 % (811346)Instruction limit reached! % 189.28/26.92 % (811346)------------------------------ % 189.28/26.92 % (811346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.28/26.92 % (811346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.28/26.92 % (811346)CaDiCaL version: 2.1.3 % 189.28/26.92 % (811346)Termination reason: Instruction limit % 189.28/26.92 % (811346)Termination phase: Saturation % 189.28/26.92 % (811346)Time elapsed: 5.278 s % 189.28/26.92 % (811346)Peak memory usage: 40 MB % 189.28/26.92 % (811346)Instructions burned: 14135 (million) % 189.28/26.92 % (811354)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=533265471:s2a=on:i=53295_2862 on theBenchmark for (2862ds/53295Mi) % 189.28/26.92 % (811344)Instruction limit reached! % 189.28/26.92 % (811344)------------------------------ % 189.28/26.92 % (811344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.28/26.92 % (811344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.28/26.92 % (811344)CaDiCaL version: 2.1.3 % 189.28/26.92 % (811344)Termination reason: Instruction limit % 189.28/26.92 % (811344)Termination phase: Saturation % 189.28/26.92 % (811344)Time elapsed: 6.464 s % 189.28/26.92 % (811344)Peak memory usage: 81 MB % 189.28/26.92 % (811344)Instructions burned: 11406 (million) % 189.28/26.92 % (811486)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=376862103:i=26857:ins=20_2855 on theBenchmark for (2855ds/26857Mi) % 189.28/26.92 % Exception at run slice level % 189.28/26.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 189.28/26.92 % (811488)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1097874699:i=28120:bs=on:fsr=off_2854 on theBenchmark for (2854ds/28120Mi) % 189.28/26.92 % (811348)Instruction limit reached! % 189.28/26.92 % (811348)------------------------------ % 189.28/26.92 % (811348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 189.28/26.92 % (811348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.28/26.92 % (811348)CaDiCaL version: 2.1.3 % 189.28/26.92 % (811348)Termination reason: Instruction limit % 189.28/26.92 % (811348)Termination phase: Saturation % 189.28/26.92 % (811348)Time elapsed: 4.507 s % 189.28/26.92 % (811348)Peak memory usage: 60 MB % 189.28/26.92 % (811348)Instructions burned: 15853 (million) % 189.28/26.92 % (811499)fmb+10_1_sil=256000:fmbss=7:random_seed=913908975:fmbsr=1.6:i=182295_2853 on theBenchmark for (2853ds/182295Mi) % 189.28/26.92 % Exception at run slice level % 189.28/26.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 189.28/26.92 % (811503)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1839375753:i=44625:gsp=on_2853 on theBenchmark for (2853ds/44625Mi) % 189.28/26.92 % (811503)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 189.28/26.92 % Exception at run slice level % 189.28/26.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 189.28/26.92 % (811508)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3341901227:i=160505_2853 on theBenchmark for (2853ds/160505Mi) % 189.28/26.92 % Exception at run slice level % 189.28/26.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 189.28/26.92 % (811518)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3145294794:fmbsr=1.3:i=225729_2853 on theBenchmark for (2853ds/225729Mi) % 189.28/26.92 % Exception at run slice level % 189.28/26.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 189.28/26.92 % (811529)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3814102957:fmbsr=2:i=185024:ins=7_2852 on theBenchmark for (2852ds/185024Mi) % 236.18/33.56 % Exception at run slice level % 236.18/33.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.18/33.56 % (811538)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2926980526:rtra=on_2852 on theBenchmark for (2852ds/0Mi) % 236.18/33.56 % Exception at run slice level % 236.18/33.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.18/33.56 % (811550)% WARNING: option uhcvi not known. % 236.18/33.56 % (811550)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3033137961:i=271062:add=off:rtra=on:rawr=on_2852 on theBenchmark for (2852ds/271062Mi) % 236.18/33.56 % (811324)Instruction limit reached! % 236.18/33.56 % (811324)------------------------------ % 236.18/33.56 % (811324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.18/33.56 % (811324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.18/33.56 % (811324)CaDiCaL version: 2.1.3 % 236.18/33.56 % (811324)Termination reason: Instruction limit % 236.18/33.56 % (811324)Termination phase: Saturation % 236.18/33.56 % (811324)Time elapsed: 14.891 s % 236.18/33.56 % (811324)Peak memory usage: 137 MB % 236.18/33.56 % (811324)Instructions burned: 29341 (million) % 236.18/33.56 % (811803)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1995074498:i=176048:add=on:rtra=on:rawr=on_2826 on theBenchmark for (2826ds/176048Mi) % 236.18/33.56 % (811350)Instruction limit reached! % 236.18/33.56 % (811350)------------------------------ % 236.18/33.56 % (811350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.18/33.56 % (811350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.18/33.56 % (811350)CaDiCaL version: 2.1.3 % 236.18/33.56 % (811350)Termination reason: Instruction limit % 236.18/33.56 % (811350)Termination phase: Saturation % 236.18/33.56 % (811350)Time elapsed: 10.405 s % 236.18/33.56 % (811350)Peak memory usage: 222 MB % 236.18/33.56 % (811350)Instructions burned: 17627 (million) % 236.18/33.56 % (811805)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1498596376:i=206:fgj=on:rtra=on_2771 on theBenchmark for (2771ds/206Mi) % 236.18/33.56 % (811805)Instruction limit reached! % 236.18/33.56 % (811805)------------------------------ % 236.18/33.56 % (811805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.18/33.56 % (811805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.18/33.56 % (811805)CaDiCaL version: 2.1.3 % 236.18/33.56 % (811805)Termination reason: Instruction limit % 236.18/33.56 % (811805)Termination phase: Saturation % 236.18/33.56 % (811805)Time elapsed: 0.118 s % 236.18/33.56 % (811805)Peak memory usage: 13 MB % 236.18/33.56 % (811805)Instructions burned: 207 (million) % 236.18/33.56 % (811807)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2167063195:i=232:rtra=on_2770 on theBenchmark for (2770ds/232Mi) % 236.18/33.56 % (811807)Instruction limit reached! % 236.18/33.56 % (811807)------------------------------ % 236.18/33.56 % (811807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.18/33.56 % (811807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.18/33.56 % (811807)CaDiCaL version: 2.1.3 % 236.18/33.56 % (811807)Termination reason: Instruction limit % 236.18/33.56 % (811807)Termination phase: Saturation % 236.18/33.56 % (811807)Time elapsed: 0.128 s % 236.18/33.56 % (811807)Peak memory usage: 13 MB % 236.18/33.56 % (811807)Instructions burned: 233 (million) % 236.18/33.56 % (811809)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=4241902319:i=262:rtra=on_2768 on theBenchmark for (2768ds/262Mi) % 236.18/33.56 % (811809)Instruction limit reached! % 236.18/33.56 % (811809)------------------------------ % 236.18/33.56 % (811809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.18/33.56 % (811809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.18/33.56 % (811809)CaDiCaL version: 2.1.3 % 236.18/33.56 % (811809)Termination reason: Instruction limit % 236.18/33.56 % (811809)Termination phase: Saturation % 236.18/33.56 % (811809)Time elapsed: 0.151 s % 236.18/33.56 % (811809)Peak memory usage: 14 MB % 236.18/33.56 % (811809)Instructions burned: 263 (million) % 236.18/33.56 % (811811)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1824465559:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2766 on theBenchmark for (2766ds/318Mi) % 236.18/33.56 % (811811)Instruction limit reached! % 236.18/33.56 % (811811)------------------------------ % 236.18/33.56 % (811811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.64/41.12 % (811811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.64/41.12 % (811811)CaDiCaL version: 2.1.3 % 289.64/41.12 % (811811)Termination reason: Instruction limit % 289.64/41.12 % (811811)Termination phase: Saturation % 289.64/41.12 % (811811)Time elapsed: 0.180 s % 289.64/41.12 % (811811)Peak memory usage: 14 MB % 289.64/41.12 % (811811)Instructions burned: 320 (million) % 289.64/41.12 % (811813)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3070225277:i=1428:nm=2:rtra=on_2764 on theBenchmark for (2764ds/1428Mi) % 289.64/41.12 % Exception at run slice level % 289.64/41.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 289.64/41.12 % (811815)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=778905987:i=262:bd=preordered:rtra=on:fsd=on_2764 on theBenchmark for (2764ds/262Mi) % 289.64/41.12 % (811815)Instruction limit reached! % 289.64/41.12 % (811815)------------------------------ % 289.64/41.12 % (811815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.64/41.12 % (811815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.64/41.12 % (811815)CaDiCaL version: 2.1.3 % 289.64/41.12 % (811815)Termination reason: Instruction limit % 289.64/41.12 % (811815)Termination phase: Saturation % 289.64/41.12 % (811815)Time elapsed: 0.155 s % 289.64/41.12 % (811815)Peak memory usage: 14 MB % 289.64/41.12 % (811815)Instructions burned: 262 (million) % 289.64/41.12 % (811817)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=1280591582:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2762 on theBenchmark for (2762ds/1368Mi) % 289.64/41.12 % (811817)Instruction limit reached! % 289.64/41.12 % (811817)------------------------------ % 289.64/41.12 % (811817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.64/41.12 % (811817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.64/41.12 % (811817)CaDiCaL version: 2.1.3 % 289.64/41.12 % (811817)Termination reason: Instruction limit % 289.64/41.12 % (811817)Termination phase: Saturation % 289.64/41.12 % (811817)Time elapsed: 0.797 s % 289.64/41.12 % (811817)Peak memory usage: 21 MB % 289.64/41.12 % (811817)Instructions burned: 1369 (million) % 289.64/41.12 % (811819)ott-21_1_sil=16000:si=on:fs=off:random_seed=1355656556:i=360:av=off:fsr=off:rtra=on_2754 on theBenchmark for (2754ds/360Mi) % 289.64/41.12 % (811819)Instruction limit reached! % 289.64/41.12 % (811819)------------------------------ % 289.64/41.12 % (811819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.64/41.12 % (811819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.64/41.12 % (811819)CaDiCaL version: 2.1.3 % 289.64/41.12 % (811819)Termination reason: Instruction limit % 289.64/41.12 % (811819)Termination phase: Saturation % 289.64/41.12 % (811819)Time elapsed: 0.193 s % 289.64/41.12 % (811819)Peak memory usage: 13 MB % 289.64/41.12 % (811819)Instructions burned: 360 (million) % 289.64/41.12 % (811821)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1630474852:i=954:bd=all:rtra=on_2752 on theBenchmark for (2752ds/954Mi) % 289.64/41.12 % (811821)Instruction limit reached! % 289.64/41.12 % (811821)------------------------------ % 289.64/41.12 % (811821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.64/41.12 % (811821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.64/41.12 % (811821)CaDiCaL version: 2.1.3 % 289.64/41.12 % (811821)Termination reason: Instruction limit % 289.64/41.12 % (811821)Termination phase: Saturation % 289.64/41.12 % (811821)Time elapsed: 0.503 s % 289.64/41.12 % (811821)Peak memory usage: 21 MB % 289.64/41.12 % (811821)Instructions burned: 955 (million) % 289.64/41.12 % (811823)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2643238385:fmbsr=1.3:i=1730:ins=25:rtra=on_2747 on theBenchmark for (2747ds/1730Mi) % 289.64/41.12 % Exception at run slice level % 289.64/41.12 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 289.64/41.12 % (811825)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=36367638:i=2358:rtra=on_2746 on theBenchmark for (2746ds/2358Mi) % 289.64/41.12 % (811825)Instruction limit reached! % 289.64/41.12 % (811825)------------------------------ % 289.64/41.12 % (811825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 289.64/41.12 % (811825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (811825)CaDiCaL version: 2.1.3 % 300.05/42.53 % (811825)Termination reason: Instruction limit % 300.05/42.53 % (811825)Termination phase: Saturation % 300.05/42.53 % (811825)Time elapsed: 1.368 s % 300.05/42.53 % (811825)Peak memory usage: 26 MB % 300.05/42.53 % (811825)Instructions burned: 2358 (million) % 300.05/42.53 % (811827)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=3377797553:i=1778:ins=1:rtra=on_2732 on theBenchmark for (2732ds/1778Mi) % 300.05/42.53 % Exception at run slice level % 300.05/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.05/42.53 % (811829)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=3162115046:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2732 on theBenchmark for (2732ds/1384Mi) % 300.05/42.53 % (811829)Instruction limit reached! % 300.05/42.53 % (811829)------------------------------ % 300.05/42.53 % (811829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (811829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (811829)CaDiCaL version: 2.1.3 % 300.05/42.53 % (811829)Termination reason: Instruction limit % 300.05/42.53 % (811829)Termination phase: Saturation % 300.05/42.53 % (811829)Time elapsed: 0.815 s % 300.05/42.53 % (811829)Peak memory usage: 22 MB % 300.05/42.53 % (811829)Instructions burned: 1385 (million) % 300.05/42.53 % (811831)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=939691115:i=1758:kws=inv_precedence:fsr=off:rtra=on_2724 on theBenchmark for (2724ds/1758Mi) % 300.05/42.53 % (811831)Instruction limit reached! % 300.05/42.53 % (811831)------------------------------ % 300.05/42.53 % (811831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (811831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (811831)CaDiCaL version: 2.1.3 % 300.05/42.53 % (811831)Termination reason: Instruction limit % 300.05/42.53 % (811831)Termination phase: Saturation % 300.05/42.53 % (811831)Time elapsed: 0.995 s % 300.05/42.53 % (811831)Peak memory usage: 25 MB % 300.05/42.53 % (811831)Instructions burned: 1759 (million) % 300.05/42.53 % (811835)fmb+10_1_sil=64000:si=on:random_seed=461584504:i=44122:nm=2:rtra=on:gsp=on_2714 on theBenchmark for (2714ds/44122Mi) % 300.05/42.53 % (811835)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.05/42.53 % Exception at run slice level % 300.05/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.05/42.53 % (811837)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3197513309:i=19030:nm=5:rtra=on_2713 on theBenchmark for (2713ds/19030Mi) % 300.05/42.53 % Exception at run slice level % 300.05/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.05/42.53 % (811844)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2912624652:fmbsr=1.7:i=1840:rtra=on_2713 on theBenchmark for (2713ds/1840Mi) % 300.05/42.53 % Exception at run slice level % 300.05/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.05/42.53 % (811859)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=585280006:i=10262:rtra=on_2713 on theBenchmark for (2713ds/10262Mi) % 300.05/42.53 % (811488)Instruction limit reached! % 300.05/42.53 % (811488)------------------------------ % 300.05/42.53 % (811488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.05/42.53 % (811488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/42.53 % (811488)CaDiCaL version: 2.1.3 % 300.05/42.53 % (811488)Termination reason: Instruction limit % 300.05/42.53 % (811488)Termination phase: Saturation % 300.05/42.53 % (811488)Time elapsed: 16.650 s % 300.05/42.53 % (811488)Peak memory usage: 101 MB % 300.05/42.53 % (811488)Instructions burned: 28120 (million) % 300.05/42.53 % (812142)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=799083861:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2688 on theBenchmark for (2688ds/2944Mi) % 300.05/42.53 % (812142)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.05/42.53 % (812142)Instruction limit reached! % 300.05/42.53 % (812142)------------------------------ % 300.05/42.53 % (812142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on % 300.05/42.54 Terminated % 300.05/42.54 % Vampire exiting % 300.05/42.54 Terminated %------------------------------------------------------------------------------