%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW471^2 : TPTP v9.3.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n010.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 : Wed Sep 30 08:40:21 AM UTC 2026 % Result : Timeout 300.53s 42.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW471^2 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.13/0.28 % Computer : n010.cluster.edu % 0.13/0.28 % Model : x86_64 x86_64 % 0.13/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.28 % Memory : 8046.5625MB % 0.13/0.28 % OS : Linux 6.8.0-71-generic % 0.13/0.28 % CPULimit : 300 % 0.13/0.28 % WCLimit : 300 % 0.13/0.28 % DateTime : Tue Sep 29 16:05:18 UTC 2026 % 0.13/0.28 % CPUTime : % 0.13/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.29/0.33 Running first-order model finding % 0.29/0.34 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 % 8.18/1.78 % (3049536)Will run a generic schedule for satisfiability detection. % 8.18/1.78 % (3049541)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1178011855_2999 on theBenchmark for (2999ds/0Mi) % 8.18/1.78 % (3049542)% WARNING: option uhcvi not known. % 8.18/1.78 % (3049545)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3575872169:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.18/1.78 % (3049547)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=62758976:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.18/1.78 % (3049544)dis+10_1_sil=32000:sp=arity:random_seed=2463576625:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.18/1.78 % (3049542)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2254969799:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.18/1.78 % (3049543)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3660985158:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.18/1.78 % (3049546)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3353175342:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.18/1.78 % (3049545)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.18/1.78 % (3049542)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 8.18/1.78 % Exception at run slice level % 8.18/1.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.18/1.78 % (3049544)Instruction limit reached! % 8.18/1.78 % (3049544)------------------------------ % 8.18/1.78 % (3049544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.78 % (3049544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.78 % (3049544)CaDiCaL version: 2.1.3 % 8.18/1.78 % (3049544)Termination reason: Instruction limit % 8.18/1.78 % (3049544)Termination phase: Preprocessing 3 % 8.18/1.78 % (3049544)Time elapsed: 0.081 s % 8.18/1.78 % (3049544)Peak memory usage: 12 MB % 8.18/1.78 % (3049544)Instructions burned: 103 (million) % 8.18/1.78 % (3049545)Instruction limit reached! % 8.18/1.78 % (3049545)------------------------------ % 8.18/1.78 % (3049545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.78 % (3049545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.78 % (3049545)CaDiCaL version: 2.1.3 % 8.18/1.78 % (3049545)Termination reason: Instruction limit % 8.18/1.78 % (3049545)Termination phase: Property scanning % 8.18/1.78 % (3049545)Time elapsed: 0.092 s % 8.18/1.78 % (3049545)Peak memory usage: 12 MB % 8.18/1.78 % (3049545)Instructions burned: 116 (million) % 8.18/1.78 % (3049546)Instruction limit reached! % 8.18/1.78 % (3049546)------------------------------ % 8.18/1.78 % (3049546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.78 % (3049546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.78 % (3049546)CaDiCaL version: 2.1.3 % 8.18/1.78 % (3049546)Termination reason: Instruction limit % 8.18/1.78 % (3049546)Termination phase: Property scanning % 8.18/1.78 % (3049546)Time elapsed: 0.106 s % 8.18/1.78 % (3049546)Peak memory usage: 12 MB % 8.18/1.78 % (3049546)Instructions burned: 131 (million) % 8.18/1.78 % (3049556)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1217577924:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.18/1.78 % (3049555)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=456678342:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 8.18/1.78 % (3049547)Instruction limit reached! % 8.18/1.78 % (3049547)------------------------------ % 8.18/1.78 % (3049547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.18/1.78 % (3049547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.18/1.78 % (3049547)CaDiCaL version: 2.1.3 % 8.18/1.78 % (3049547)Termination reason: Instruction limit % 8.18/1.78 % (3049547)Termination phase: Function definition elimination % 8.18/1.78 % (3049547)Time elapsed: 0.119 s % 8.18/1.78 % (3049547)Peak memory usage: 13 MB % 8.18/1.78 % (3049547)Instructions burned: 159 (million) % 8.18/1.78 % (3049557)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=1604919167:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 8.18/1.78 % (3049558)ott-21_1_sil=16000:fs=off:random_seed=3222222863:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 31.32/4.91 % (3049561)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=477226743:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 31.32/4.91 % (3049542)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 31.32/4.91 % (3049557)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.32/4.91 % (3049556)Instruction limit reached! % 31.32/4.91 % (3049556)------------------------------ % 31.32/4.91 % (3049556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.32/4.91 % (3049556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.32/4.91 % (3049556)CaDiCaL version: 2.1.3 % 31.32/4.91 % (3049556)Termination reason: Instruction limit % 31.32/4.91 % (3049556)Termination phase: Property scanning % 31.32/4.91 % (3049556)Time elapsed: 0.100 s % 31.32/4.91 % (3049556)Peak memory usage: 12 MB % 31.32/4.91 % (3049556)Instructions burned: 131 (million) % 31.32/4.91 % Exception at run slice level % 31.32/4.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.32/4.91 % (3049566)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1426733779:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 31.32/4.91 % (3049565)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=303934252:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 31.32/4.91 % (3049558)Instruction limit reached! % 31.32/4.91 % (3049558)------------------------------ % 31.32/4.91 % (3049558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.32/4.91 % (3049558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.32/4.91 % (3049558)CaDiCaL version: 2.1.3 % 31.32/4.91 % (3049558)Termination reason: Instruction limit % 31.32/4.91 % (3049558)Termination phase: Property scanning % 31.32/4.91 % (3049558)Time elapsed: 0.140 s % 31.32/4.91 % (3049558)Peak memory usage: 12 MB % 31.32/4.91 % (3049558)Instructions burned: 180 (million) % 31.32/4.91 % (3049557)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 31.32/4.91 % (3049569)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2468034359:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 31.32/4.91 % Exception at run slice level % 31.32/4.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.32/4.91 % (3049571)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=4126773495:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 31.32/4.91 % Exception at run slice level % 31.32/4.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 31.32/4.91 % (3049573)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1375538701:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 31.32/4.91 % (3049571)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.32/4.91 % (3049561)Instruction limit reached! % 31.32/4.91 % (3049561)------------------------------ % 31.32/4.91 % (3049561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.32/4.91 % (3049561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.32/4.91 % (3049561)CaDiCaL version: 2.1.3 % 31.32/4.91 % (3049561)Termination reason: Instruction limit % 31.32/4.91 % (3049561)Termination phase: Saturation % 31.32/4.91 % (3049561)Time elapsed: 0.421 s % 31.32/4.91 % (3049561)Peak memory usage: 15 MB % 31.32/4.91 % (3049561)Instructions burned: 477 (million) % 31.32/4.91 % (3049575)fmb+10_1_sil=64000:random_seed=3954719317:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 31.32/4.91 % (3049573)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 31.32/4.91 % (3049557)Instruction limit reached! % 31.32/4.91 % (3049557)------------------------------ % 31.32/4.91 % (3049557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.32/4.91 % (3049557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.32/4.91 % (3049557)CaDiCaL version: 2.1.3 % 31.32/4.91 % (3049557)Termination reason: Instruction limit % 31.32/4.91 % (3049557)Termination phase: Saturation % 31.32/4.91 % (3049557)Time elapsed: 0.580 s % 88.87/12.98 % (3049557)Peak memory usage: 16 MB % 88.87/12.98 % (3049557)Instructions burned: 684 (million) % 88.87/12.98 % (3049575)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 88.87/12.98 % (3049577)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1266802390:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 88.87/12.98 % (3049566)Instruction limit reached! % 88.87/12.98 % (3049566)------------------------------ % 88.87/12.98 % (3049566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.87/12.98 % (3049566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.87/12.98 % (3049566)CaDiCaL version: 2.1.3 % 88.87/12.98 % (3049566)Termination reason: Instruction limit % 88.87/12.98 % (3049566)Termination phase: Saturation % 88.87/12.98 % (3049566)Time elapsed: 0.532 s % 88.87/12.98 % (3049566)Peak memory usage: 21 MB % 88.87/12.98 % (3049566)Instructions burned: 1179 (million) % 88.87/12.98 % Exception at run slice level % 88.87/12.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 88.87/12.98 % (3049579)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2958451826:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 88.87/12.98 % (3049580)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=677708582:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 88.87/12.98 % (3049580)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 88.87/12.98 % Exception at run slice level % 88.87/12.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 88.87/12.98 % (3049583)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4227754548:i=1472:ins=7:fdi=8:gsp=on_2990 on theBenchmark for (2990ds/1472Mi) % 88.87/12.98 % Exception at run slice level % 88.87/12.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 88.87/12.98 % (3049585)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=879635565:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 88.87/12.98 % (3049583)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 88.87/12.98 % (3049583)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 88.87/12.98 % (3049571)Instruction limit reached! % 88.87/12.98 % (3049571)------------------------------ % 88.87/12.98 % (3049571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.87/12.98 % (3049571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.87/12.98 % (3049571)CaDiCaL version: 2.1.3 % 88.87/12.98 % (3049571)Termination reason: Instruction limit % 88.87/12.98 % (3049571)Termination phase: Saturation % 88.87/12.98 % (3049571)Time elapsed: 0.617 s % 88.87/12.98 % (3049571)Peak memory usage: 18 MB % 88.87/12.98 % (3049571)Instructions burned: 693 (million) % 88.87/12.98 % (3049587)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2634322942:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi) % 88.87/12.98 % Exception at run slice level % 88.87/12.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 88.87/12.98 % (3049589)ott-2_1_sil=16000:newcnf=on:random_seed=2514761993:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2987 on theBenchmark for (2987ds/869Mi) % 88.87/12.98 % (3049589)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 88.87/12.98 % Exception at run slice level % 88.87/12.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 88.87/12.98 % (3049573)Instruction limit reached! % 88.87/12.98 % (3049573)------------------------------ % 88.87/12.98 % (3049573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 88.87/12.98 % (3049573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.87/12.98 % (3049573)CaDiCaL version: 2.1.3 % 88.87/12.98 % (3049573)Termination reason: Instruction limit % 88.87/12.98 % (3049573)Termination phase: Saturation % 88.87/12.98 % (3049573)Time elapsed: 0.747 s % 88.87/12.98 % (3049573)Peak memory usage: 19 MB % 88.87/12.98 % (3049573)Instructions burned: 879 (million) % 88.87/12.98 % (3049591)ott+10_1_sil=32000:tgt=ground:random_seed=2831104478:i=5114:av=off_2986 on theBenchmark for (2986ds/5114Mi) % 88.87/12.98 % (3049592)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=571128664:i=54282_2985 on theBenchmark for (2985ds/54282Mi) % 171.07/24.51 % Exception at run slice level % 171.07/24.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 171.07/24.51 % (3049595)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3370150776:i=3512:aac=none_2983 on theBenchmark for (2983ds/3512Mi) % 171.07/24.51 % (3049583)Instruction limit reached! % 171.07/24.51 % (3049583)------------------------------ % 171.07/24.51 % (3049583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.07/24.51 % (3049583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.07/24.51 % (3049583)CaDiCaL version: 2.1.3 % 171.07/24.51 % (3049583)Termination reason: Instruction limit % 171.07/24.51 % (3049583)Termination phase: Saturation % 171.07/24.51 % (3049583)Time elapsed: 0.710 s % 171.07/24.51 % (3049583)Peak memory usage: 24 MB % 171.07/24.51 % (3049583)Instructions burned: 1472 (million) % 171.07/24.51 % (3049597)dis+21_1_sil=32000:sas=cadical:random_seed=2153397733:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi) % 171.07/24.51 % (3049595)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 171.07/24.51 % (3049589)Instruction limit reached! % 171.07/24.51 % (3049589)------------------------------ % 171.07/24.51 % (3049589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.07/24.51 % (3049589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.07/24.51 % (3049589)CaDiCaL version: 2.1.3 % 171.07/24.51 % (3049589)Termination reason: Instruction limit % 171.07/24.51 % (3049589)Termination phase: Saturation % 171.07/24.51 % (3049589)Time elapsed: 0.703 s % 171.07/24.51 % (3049589)Peak memory usage: 19 MB % 171.07/24.51 % (3049589)Instructions burned: 869 (million) % 171.07/24.51 % (3049600)ott+11_1_sil=16000:gs=on:random_seed=2265756232:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 171.07/24.51 % (3049600)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 171.07/24.51 % (3049597)Instruction limit reached! % 171.07/24.51 % (3049597)------------------------------ % 171.07/24.51 % (3049597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.07/24.51 % (3049597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.07/24.51 % (3049597)CaDiCaL version: 2.1.3 % 171.07/24.51 % (3049597)Termination reason: Instruction limit % 171.07/24.51 % (3049597)Termination phase: Saturation % 171.07/24.51 % (3049597)Time elapsed: 1.691 s % 171.07/24.51 % (3049597)Peak memory usage: 30 MB % 171.07/24.51 % (3049597)Instructions burned: 3775 (million) % 171.07/24.51 % (3049602)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2093483340:fmbsr=1.6:i=67534_2965 on theBenchmark for (2965ds/67534Mi) % 171.07/24.51 % Exception at run slice level % 171.07/24.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 171.07/24.51 % (3049604)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1680330168:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2963 on theBenchmark for (2963ds/4591Mi) % 171.07/24.51 % (3049600)Instruction limit reached! % 171.07/24.51 % (3049600)------------------------------ % 171.07/24.51 % (3049600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.07/24.51 % (3049600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.07/24.51 % (3049600)CaDiCaL version: 2.1.3 % 171.07/24.51 % (3049600)Termination reason: Instruction limit % 171.07/24.51 % (3049600)Termination phase: Saturation % 171.07/24.51 % (3049600)Time elapsed: 1.889 s % 171.07/24.51 % (3049600)Peak memory usage: 24 MB % 171.07/24.51 % (3049600)Instructions burned: 2252 (million) % 171.07/24.51 % (3049606)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3261913594:i=29340_2961 on theBenchmark for (2961ds/29340Mi) % 171.07/24.51 % (3049595)Instruction limit reached! % 171.07/24.51 % (3049595)------------------------------ % 171.07/24.51 % (3049595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 171.07/24.51 % (3049595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.07/24.51 % (3049595)CaDiCaL version: 2.1.3 % 171.07/24.51 % (3049595)Termination reason: Instruction limit % 171.07/24.51 % (3049595)Termination phase: Saturation % 171.07/24.51 % (3049595)Time elapsed: 2.866 s % 171.07/24.51 % (3049595)Peak memory usage: 25 MB % 171.07/24.51 % (3049595)Instructions burned: 3513 (million) % 171.07/24.51 % (3049608)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=394663831:i=5211_2954 on theBenchmark for (2954ds/5211Mi) % 176.74/25.33 % (3049580)Instruction limit reached! % 176.74/25.33 % (3049580)------------------------------ % 176.74/25.33 % (3049580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.74/25.33 % (3049580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.74/25.33 % (3049580)CaDiCaL version: 2.1.3 % 176.74/25.33 % (3049580)Termination reason: Instruction limit % 176.74/25.33 % (3049580)Termination phase: Saturation % 176.74/25.33 % (3049580)Time elapsed: 4.263 s % 176.74/25.33 % (3049580)Peak memory usage: 37 MB % 176.74/25.33 % (3049580)Instructions burned: 5131 (million) % 176.74/25.33 % (3049610)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3634805267:i=5497:nm=2_2948 on theBenchmark for (2948ds/5497Mi) % 176.74/25.33 % Exception at run slice level % 176.74/25.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.74/25.33 % (3049612)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3966449958:fmbsr=2:i=46332_2945 on theBenchmark for (2945ds/46332Mi) % 176.74/25.33 % Exception at run slice level % 176.74/25.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.74/25.33 % (3049604)Instruction limit reached! % 176.74/25.33 % (3049604)------------------------------ % 176.74/25.33 % (3049604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.74/25.33 % (3049604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.74/25.33 % (3049604)CaDiCaL version: 2.1.3 % 176.74/25.33 % (3049604)Termination reason: Instruction limit % 176.74/25.33 % (3049604)Termination phase: Saturation % 176.74/25.33 % (3049604)Time elapsed: 1.953 s % 176.74/25.33 % (3049604)Peak memory usage: 27 MB % 176.74/25.33 % (3049604)Instructions burned: 4592 (million) % 176.74/25.33 % (3049614)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=381722035:i=14071_2943 on theBenchmark for (2943ds/14071Mi) % 176.74/25.33 % (3049615)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1135068108:i=22565:add=on:rawr=on_2943 on theBenchmark for (2943ds/22565Mi) % 176.74/25.33 % (3049591)Instruction limit reached! % 176.74/25.33 % (3049591)------------------------------ % 176.74/25.33 % (3049591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.74/25.33 % (3049591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.74/25.33 % (3049591)CaDiCaL version: 2.1.3 % 176.74/25.33 % (3049591)Termination reason: Instruction limit % 176.74/25.33 % (3049591)Termination phase: Saturation % 176.74/25.33 % (3049591)Time elapsed: 4.240 s % 176.74/25.33 % (3049591)Peak memory usage: 51 MB % 176.74/25.33 % (3049591)Instructions burned: 5114 (million) % 176.74/25.33 % (3049618)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3270018778:i=8173:av=off_2943 on theBenchmark for (2943ds/8173Mi) % 176.74/25.33 % Exception at run slice level % 176.74/25.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 176.74/25.33 % (3049620)dis+10_16:1_sil=16000:random_seed=987686286:i=9155:fsr=off_2941 on theBenchmark for (2941ds/9155Mi) % 176.74/25.33 % (3049608)Instruction limit reached! % 176.74/25.33 % (3049608)------------------------------ % 176.74/25.33 % (3049608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.74/25.33 % (3049608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.74/25.33 % (3049608)CaDiCaL version: 2.1.3 % 176.74/25.33 % (3049608)Termination reason: Instruction limit % 176.74/25.33 % (3049608)Termination phase: Saturation % 176.74/25.33 % (3049608)Time elapsed: 4.341 s % 176.74/25.33 % (3049608)Peak memory usage: 46 MB % 176.74/25.33 % (3049608)Instructions burned: 5212 (million) % 176.74/25.33 % (3049622)ott-3_8_sil=64000:random_seed=1615846749:i=20139:bs=on_2910 on theBenchmark for (2910ds/20139Mi) % 176.74/25.33 % (3049618)Instruction limit reached! % 176.74/25.33 % (3049618)------------------------------ % 176.74/25.33 % (3049618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 176.74/25.33 % (3049618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.74/25.33 % (3049618)CaDiCaL version: 2.1.3 % 176.74/25.33 % (3049618)Termination reason: Instruction limit % 176.74/25.33 % (3049618)Termination phase: Saturation % 176.74/25.33 % (3049618)Time elapsed: 6.872 s % 176.74/25.33 % (3049618)Peak memory usage: 56 MB % 176.74/25.33 % (3049618)Instructions burned: 8174 (million) % 176.74/25.33 % (3049624)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3878338386:fmbsr=2:i=32576_2874 on theBenchmark for (2874ds/32576Mi) % 182.13/26.11 % Exception at run slice level % 182.13/26.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.13/26.11 % (3049626)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3900789500:i=11404_2871 on theBenchmark for (2871ds/11404Mi) % 182.13/26.11 % (3049620)Instruction limit reached! % 182.13/26.11 % (3049620)------------------------------ % 182.13/26.11 % (3049620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.13/26.11 % (3049620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.13/26.11 % (3049620)CaDiCaL version: 2.1.3 % 182.13/26.11 % (3049620)Termination reason: Instruction limit % 182.13/26.11 % (3049620)Termination phase: Saturation % 182.13/26.11 % (3049620)Time elapsed: 7.358 s % 182.13/26.11 % (3049620)Peak memory usage: 55 MB % 182.13/26.11 % (3049620)Instructions burned: 9156 (million) % 182.13/26.11 % (3049631)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3452961715:i=14134_2867 on theBenchmark for (2867ds/14134Mi) % 182.13/26.11 % (3049631)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 182.13/26.11 % (3049615)Instruction limit reached! % 182.13/26.11 % (3049615)------------------------------ % 182.13/26.11 % (3049615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.13/26.11 % (3049615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.13/26.11 % (3049615)CaDiCaL version: 2.1.3 % 182.13/26.11 % (3049615)Termination reason: Instruction limit % 182.13/26.11 % (3049615)Termination phase: Saturation % 182.13/26.11 % (3049615)Time elapsed: 9.113 s % 182.13/26.11 % (3049615)Peak memory usage: 149 MB % 182.13/26.11 % (3049615)Instructions burned: 22565 (million) % 182.13/26.11 % (3049633)dis+33_16_sil=32000:sac=on:random_seed=3323430707:i=15851:nm=0_2852 on theBenchmark for (2852ds/15851Mi) % 182.13/26.11 % (3049633)Instruction limit reached! % 182.13/26.11 % (3049633)------------------------------ % 182.13/26.11 % (3049633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.13/26.11 % (3049633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.13/26.11 % (3049633)CaDiCaL version: 2.1.3 % 182.13/26.11 % (3049633)Termination reason: Instruction limit % 182.13/26.11 % (3049633)Termination phase: Saturation % 182.13/26.11 % (3049633)Time elapsed: 4.844 s % 182.13/26.11 % (3049633)Peak memory usage: 16 MB % 182.13/26.11 % (3049633)Instructions burned: 15855 (million) % 182.13/26.11 % (3049635)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2761483583:avsq=on:i=17627:add=on:amm=off_2803 on theBenchmark for (2803ds/17627Mi) % 182.13/26.11 % (3049626)Instruction limit reached! % 182.13/26.11 % (3049626)------------------------------ % 182.13/26.11 % (3049626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.13/26.11 % (3049626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.13/26.11 % (3049626)CaDiCaL version: 2.1.3 % 182.13/26.11 % (3049626)Termination reason: Instruction limit % 182.13/26.11 % (3049626)Termination phase: Saturation % 182.13/26.11 % (3049626)Time elapsed: 9.629 s % 182.13/26.11 % (3049626)Peak memory usage: 69 MB % 182.13/26.11 % (3049626)Instructions burned: 11405 (million) % 182.13/26.11 % (3049637)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1796430742:s2a=on:i=53295_2774 on theBenchmark for (2774ds/53295Mi) % 182.13/26.11 % (3049631)Instruction limit reached! % 182.13/26.11 % (3049631)------------------------------ % 182.13/26.11 % (3049631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.13/26.11 % (3049631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.13/26.11 % (3049631)CaDiCaL version: 2.1.3 % 182.13/26.11 % (3049631)Termination reason: Instruction limit % 182.13/26.11 % (3049631)Termination phase: Saturation % 182.13/26.11 % (3049631)Time elapsed: 10.571 s % 182.13/26.11 % (3049631)Peak memory usage: 77 MB % 182.13/26.11 % (3049631)Instructions burned: 14135 (million) % 182.13/26.11 % (3049792)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2507845735:i=26857:ins=20_2761 on theBenchmark for (2761ds/26857Mi) % 182.13/26.11 % Exception at run slice level % 182.13/26.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.13/26.11 % (3049794)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1714214238:i=28120:bs=on:fsr=off_2760 on theBenchmark for (2760ds/28120Mi) % 182.13/26.11 % (3049622)Instruction limit reached! % 192.92/27.66 % (3049622)------------------------------ % 192.92/27.66 % (3049622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.92/27.66 % (3049622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.92/27.66 % (3049622)CaDiCaL version: 2.1.3 % 192.92/27.66 % (3049622)Termination reason: Instruction limit % 192.92/27.66 % (3049622)Termination phase: Saturation % 192.92/27.66 % (3049622)Time elapsed: 15.217 s % 192.92/27.66 % (3049622)Peak memory usage: 67 MB % 192.92/27.66 % (3049622)Instructions burned: 20141 (million) % 192.92/27.66 % (3049796)fmb+10_1_sil=256000:fmbss=7:random_seed=1485192010:fmbsr=1.6:i=182295_2758 on theBenchmark for (2758ds/182295Mi) % 192.92/27.66 % Exception at run slice level % 192.92/27.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.92/27.66 % (3049798)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3900456957:i=44625:gsp=on_2757 on theBenchmark for (2757ds/44625Mi) % 192.92/27.66 % (3049798)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 192.92/27.66 % (3049798)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 192.92/27.66 % Exception at run slice level % 192.92/27.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.92/27.66 % (3049800)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4263032283:i=160505_2756 on theBenchmark for (2756ds/160505Mi) % 192.92/27.66 % Exception at run slice level % 192.92/27.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.92/27.66 % (3049802)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1501326596:fmbsr=1.3:i=225729_2755 on theBenchmark for (2755ds/225729Mi) % 192.92/27.66 % Exception at run slice level % 192.92/27.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.92/27.66 % (3049804)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1295681084:fmbsr=2:i=185024:ins=7_2753 on theBenchmark for (2753ds/185024Mi) % 192.92/27.66 % Exception at run slice level % 192.92/27.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.92/27.66 % (3049806)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3137468958:rtra=on_2752 on theBenchmark for (2752ds/0Mi) % 192.92/27.66 % Exception at run slice level % 192.92/27.66 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 192.92/27.66 % (3049808)% WARNING: option uhcvi not known. % 192.92/27.66 % (3049808)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=534470349:i=271062:add=off:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/271062Mi) % 192.92/27.66 % (3049606)Instruction limit reached! % 192.92/27.66 % (3049606)------------------------------ % 192.92/27.66 % (3049606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.92/27.66 % (3049606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.92/27.66 % (3049606)CaDiCaL version: 2.1.3 % 192.92/27.66 % (3049606)Termination reason: Instruction limit % 192.92/27.66 % (3049606)Termination phase: Saturation % 192.92/27.66 % (3049606)Time elapsed: 20.919 s % 192.92/27.66 % (3049606)Peak memory usage: 32 MB % 192.92/27.66 % (3049606)Instructions burned: 29340 (million) % 192.92/27.66 % (3049810)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2734714270:i=176048:add=on:rtra=on:rawr=on_2751 on theBenchmark for (2751ds/176048Mi) % 192.92/27.66 % (3049808)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 192.92/27.66 % (3049808)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 192.92/27.66 % (3049635)Instruction limit reached! % 192.92/27.66 % (3049635)------------------------------ % 192.92/27.66 % (3049635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 192.92/27.66 % (3049635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.92/27.66 % (3049635)CaDiCaL version: 2.1.3 % 192.92/27.66 % (3049635)Termination reason: Instruction limit % 192.92/27.66 % (3049635)Termination phase: Saturation % 192.92/27.66 % (3049635)Time elapsed: 5.236 s % 192.92/27.66 % (3049635)Peak memory usage: 39 MB % 192.92/27.66 % (3049635)Instructions burned: 17629 (million) % 192.92/27.66 % (3049812)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1509276994:i=206:fgj=on:rtra=on_2750 on theBenchmark for (2750ds/206Mi) % 233.73/33.32 % (3049812)Instruction limit reached! % 233.73/33.32 % (3049812)------------------------------ % 233.73/33.32 % (3049812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.73/33.32 % (3049812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/33.32 % (3049812)CaDiCaL version: 2.1.3 % 233.73/33.32 % (3049812)Termination reason: Instruction limit % 233.73/33.32 % (3049812)Termination phase: Property scanning % 233.73/33.32 % (3049812)Time elapsed: 0.049 s % 233.73/33.32 % (3049812)Peak memory usage: 13 MB % 233.73/33.32 % (3049812)Instructions burned: 208 (million) % 233.73/33.32 % (3049814)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2101502272:i=232:rtra=on_2749 on theBenchmark for (2749ds/232Mi) % 233.73/33.32 % (3049814)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 233.73/33.32 % (3049814)Instruction limit reached! % 233.73/33.32 % (3049814)------------------------------ % 233.73/33.32 % (3049814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.73/33.32 % (3049814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/33.32 % (3049814)CaDiCaL version: 2.1.3 % 233.73/33.32 % (3049814)Termination reason: Instruction limit % 233.73/33.32 % (3049814)Termination phase: Saturation % 233.73/33.32 % (3049814)Time elapsed: 0.054 s % 233.73/33.32 % (3049814)Peak memory usage: 14 MB % 233.73/33.32 % (3049814)Instructions burned: 234 (million) % 233.73/33.32 % (3049816)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=106159955:i=262:rtra=on_2749 on theBenchmark for (2749ds/262Mi) % 233.73/33.32 % (3049816)Instruction limit reached! % 233.73/33.32 % (3049816)------------------------------ % 233.73/33.32 % (3049816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.73/33.32 % (3049816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/33.32 % (3049816)CaDiCaL version: 2.1.3 % 233.73/33.32 % (3049816)Termination reason: Instruction limit % 233.73/33.32 % (3049816)Termination phase: Saturation % 233.73/33.32 % (3049816)Time elapsed: 0.062 s % 233.73/33.32 % (3049816)Peak memory usage: 15 MB % 233.73/33.32 % (3049816)Instructions burned: 263 (million) % 233.73/33.32 % (3049818)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3058442879:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2748 on theBenchmark for (2748ds/318Mi) % 233.73/33.32 % (3049818)Instruction limit reached! % 233.73/33.32 % (3049818)------------------------------ % 233.73/33.32 % (3049818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.73/33.32 % (3049818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/33.32 % (3049818)CaDiCaL version: 2.1.3 % 233.73/33.32 % (3049818)Termination reason: Instruction limit % 233.73/33.32 % (3049818)Termination phase: Saturation % 233.73/33.32 % (3049818)Time elapsed: 0.080 s % 233.73/33.32 % (3049818)Peak memory usage: 16 MB % 233.73/33.32 % (3049818)Instructions burned: 321 (million) % 233.73/33.32 % (3049820)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4267517398:i=1428:nm=2:rtra=on_2747 on theBenchmark for (2747ds/1428Mi) % 233.73/33.32 % Exception at run slice level % 233.73/33.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.73/33.32 % (3049822)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3853953263:i=262:bd=preordered:rtra=on:fsd=on_2746 on theBenchmark for (2746ds/262Mi) % 233.73/33.32 % (3049822)Instruction limit reached! % 233.73/33.32 % (3049822)------------------------------ % 233.73/33.32 % (3049822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.73/33.32 % (3049822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.73/33.32 % (3049822)CaDiCaL version: 2.1.3 % 233.73/33.32 % (3049822)Termination reason: Instruction limit % 233.73/33.32 % (3049822)Termination phase: Saturation % 233.73/33.32 % (3049822)Time elapsed: 0.062 s % 233.73/33.32 % (3049822)Peak memory usage: 15 MB % 233.73/33.32 % (3049822)Instructions burned: 263 (million) % 233.73/33.32 % (3049824)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=2493141793:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2745 on theBenchmark for (2745ds/1368Mi) % 233.73/33.32 % (3049824)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 233.73/33.32 % (3049824)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 233.73/33.32 % (3049824)Instruction Terminated % 300.53/42.83 % Vampire exiting % 300.53/42.84 Terminated %------------------------------------------------------------------------------