%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW477^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 : n014.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:23 AM UTC 2026 % Result : Timeout 300.11s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW477^2 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.17/0.32 % Computer : n014.cluster.edu % 0.17/0.32 % Model : x86_64 x86_64 % 0.17/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.32 % Memory : 8046.5625MB % 0.17/0.32 % OS : Linux 6.8.0-71-generic % 0.17/0.32 % CPULimit : 300 % 0.17/0.32 % WCLimit : 300 % 0.17/0.32 % DateTime : Tue Sep 29 16:06:30 UTC 2026 % 0.17/0.32 % CPUTime : % 0.17/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.17/0.36 Running first-order model finding % 0.17/0.36 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 % 12.19/2.18 % (2857053)Will run a generic schedule for satisfiability detection. % 12.19/2.18 % (2857058)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3512633236_2999 on theBenchmark for (2999ds/0Mi) % 12.19/2.18 % (2857061)dis+10_1_sil=32000:sp=arity:random_seed=260756626:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 12.19/2.18 % (2857059)% WARNING: option uhcvi not known. % 12.19/2.18 % (2857059)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=612521693:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 12.19/2.18 % (2857060)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=567163631:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 12.19/2.18 % (2857062)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2494890884:i=116_2999 on theBenchmark for (2999ds/116Mi) % 12.19/2.18 % (2857063)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1945659586:i=131_2999 on theBenchmark for (2999ds/131Mi) % 12.19/2.18 % (2857064)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=668943752:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 12.19/2.18 % (2857061)Instruction limit reached! % 12.19/2.18 % (2857061)------------------------------ % 12.19/2.18 % (2857061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.19/2.18 % (2857061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.18 % (2857061)CaDiCaL version: 2.1.3 % 12.19/2.18 % (2857061)Termination reason: Instruction limit % 12.19/2.18 % (2857061)Termination phase: Property scanning % 12.19/2.18 % (2857061)Time elapsed: 0.049 s % 12.19/2.18 % (2857061)Peak memory usage: 12 MB % 12.19/2.18 % (2857061)Instructions burned: 103 (million) % 12.19/2.18 % (2857072)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3463373573:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 12.19/2.18 % (2857062)Instruction limit reached! % 12.19/2.18 % (2857062)------------------------------ % 12.19/2.18 % (2857062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.19/2.18 % (2857062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.18 % (2857062)CaDiCaL version: 2.1.3 % 12.19/2.18 % (2857062)Termination reason: Instruction limit % 12.19/2.18 % (2857062)Termination phase: Property scanning % 12.19/2.18 % (2857062)Time elapsed: 0.090 s % 12.19/2.18 % (2857062)Peak memory usage: 11 MB % 12.19/2.18 % (2857062)Instructions burned: 117 (million) % 12.19/2.18 % (2857059)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 12.19/2.18 % (2857063)Instruction limit reached! % 12.19/2.18 % (2857063)------------------------------ % 12.19/2.18 % (2857063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.19/2.18 % (2857063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.18 % (2857063)CaDiCaL version: 2.1.3 % 12.19/2.18 % (2857063)Termination reason: Instruction limit % 12.19/2.18 % (2857063)Termination phase: Naming % 12.19/2.18 % (2857063)Time elapsed: 0.100 s % 12.19/2.18 % (2857063)Peak memory usage: 12 MB % 12.19/2.18 % (2857063)Instructions burned: 131 (million) % 12.19/2.18 % Exception at run slice level % 12.19/2.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 12.19/2.18 % (2857074)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3459597559:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi) % 12.19/2.18 % (2857064)Instruction limit reached! % 12.19/2.18 % (2857064)------------------------------ % 12.19/2.18 % (2857064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 12.19/2.18 % (2857064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.19/2.18 % (2857064)CaDiCaL version: 2.1.3 % 12.19/2.18 % (2857064)Termination reason: Instruction limit % 12.19/2.18 % (2857064)Termination phase: Preprocessing 3 % 12.19/2.18 % (2857064)Time elapsed: 0.129 s % 12.19/2.18 % (2857064)Peak memory usage: 13 MB % 12.19/2.18 % (2857064)Instructions burned: 160 (million) % 12.19/2.18 % (2857075)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=3573153584:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi) % 12.19/2.18 % (2857076)ott-21_1_sil=16000:fs=off:random_seed=3283610654:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi) % 12.19/2.18 % (2857078)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=881284611:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 34.36/5.34 % (2857076)Instruction limit reached! % 34.36/5.34 % (2857076)------------------------------ % 34.36/5.34 % (2857076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.36/5.34 % (2857076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.36/5.34 % (2857076)CaDiCaL version: 2.1.3 % 34.36/5.34 % (2857076)Termination reason: Instruction limit % 34.36/5.34 % (2857076)Termination phase: Property scanning % 34.36/5.34 % (2857076)Time elapsed: 0.074 s % 34.36/5.34 % (2857076)Peak memory usage: 13 MB % 34.36/5.34 % (2857076)Instructions burned: 181 (million) % 34.36/5.34 % (2857074)Instruction limit reached! % 34.36/5.34 % (2857074)------------------------------ % 34.36/5.34 % (2857074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.36/5.34 % (2857074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.36/5.34 % (2857074)CaDiCaL version: 2.1.3 % 34.36/5.34 % (2857074)Termination reason: Instruction limit % 34.36/5.34 % (2857074)Termination phase: Preprocessing 3 % 34.36/5.34 % (2857074)Time elapsed: 0.101 s % 34.36/5.34 % (2857074)Peak memory usage: 12 MB % 34.36/5.34 % (2857074)Instructions burned: 131 (million) % 34.36/5.34 % (2857082)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3811333243:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 34.36/5.34 % Exception at run slice level % 34.36/5.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.36/5.34 % (2857059)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 34.36/5.34 % (2857083)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1332958620:i=1179_2996 on theBenchmark for (2996ds/1179Mi) % 34.36/5.34 % (2857075)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 34.36/5.34 % (2857085)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3070464425:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 34.36/5.34 % Exception at run slice level % 34.36/5.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.36/5.34 % (2857088)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=1295440908:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 34.36/5.34 % (2857075)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 34.36/5.34 % (2857088)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 34.36/5.34 % Exception at run slice level % 34.36/5.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.36/5.34 % (2857078)Instruction limit reached! % 34.36/5.34 % (2857078)------------------------------ % 34.36/5.34 % (2857078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.36/5.34 % (2857078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.36/5.34 % (2857078)CaDiCaL version: 2.1.3 % 34.36/5.34 % (2857078)Termination reason: Instruction limit % 34.36/5.34 % (2857078)Termination phase: Saturation % 34.36/5.34 % (2857078)Time elapsed: 0.399 s % 34.36/5.34 % (2857078)Peak memory usage: 16 MB % 34.36/5.34 % (2857078)Instructions burned: 477 (million) % 34.36/5.34 % (2857090)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2714597152:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 34.36/5.34 % (2857091)fmb+10_1_sil=64000:random_seed=2627960314:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 34.36/5.34 % (2857088)Instruction limit reached! % 34.36/5.34 % (2857088)------------------------------ % 34.36/5.34 % (2857088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.36/5.34 % (2857088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.36/5.34 % (2857088)CaDiCaL version: 2.1.3 % 34.36/5.34 % (2857088)Termination reason: Instruction limit % 34.36/5.34 % (2857088)Termination phase: Saturation % 34.36/5.34 % (2857088)Time elapsed: 0.295 s % 34.36/5.34 % (2857088)Peak memory usage: 19 MB % 34.36/5.34 % (2857088)Instructions burned: 692 (million) % 34.36/5.34 % (2857090)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 34.36/5.34 % (2857075)Instruction limit reached! % 64.44/9.62 % (2857075)------------------------------ % 64.44/9.62 % (2857075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.44/9.62 % (2857075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.44/9.62 % (2857075)CaDiCaL version: 2.1.3 % 64.44/9.62 % (2857075)Termination reason: Instruction limit % 64.44/9.62 % (2857075)Termination phase: Saturation % 64.44/9.62 % (2857075)Time elapsed: 0.553 s % 64.44/9.62 % (2857075)Peak memory usage: 17 MB % 64.44/9.62 % (2857075)Instructions burned: 684 (million) % 64.44/9.62 % (2857094)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=977630008:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi) % 64.44/9.62 % (2857095)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2716862020:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 64.44/9.62 % (2857091)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.44/9.62 % Exception at run slice level % 64.44/9.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.44/9.62 % (2857098)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3457657538:i=5131_2991 on theBenchmark for (2991ds/5131Mi) % 64.44/9.62 % (2857098)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 64.44/9.62 % Exception at run slice level % 64.44/9.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.44/9.62 % Exception at run slice level % 64.44/9.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.44/9.62 % (2857102)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2815744203:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi) % 64.44/9.62 % (2857105)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1248066506:i=6324_2989 on theBenchmark for (2989ds/6324Mi) % 64.44/9.62 % (2857102)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.44/9.62 % (2857083)Instruction limit reached! % 64.44/9.62 % (2857083)------------------------------ % 64.44/9.62 % (2857083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.44/9.62 % (2857083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.44/9.62 % (2857083)CaDiCaL version: 2.1.3 % 64.44/9.62 % (2857083)Termination reason: Instruction limit % 64.44/9.62 % (2857083)Termination phase: Saturation % 64.44/9.62 % (2857083)Time elapsed: 0.913 s % 64.44/9.62 % (2857083)Peak memory usage: 21 MB % 64.44/9.62 % (2857083)Instructions burned: 1180 (million) % 64.44/9.62 % (2857108)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2147448083:fmbsr=2.30978:i=2174_2987 on theBenchmark for (2987ds/2174Mi) % 64.44/9.62 % (2857102)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 64.44/9.62 % Exception at run slice level % 64.44/9.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.44/9.62 % (2857090)Instruction limit reached! % 64.44/9.62 % (2857090)------------------------------ % 64.44/9.62 % (2857090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.44/9.62 % (2857090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.44/9.62 % (2857090)CaDiCaL version: 2.1.3 % 64.44/9.62 % (2857090)Termination reason: Instruction limit % 64.44/9.62 % (2857090)Termination phase: Saturation % 64.44/9.62 % (2857090)Time elapsed: 0.680 s % 64.44/9.62 % (2857090)Peak memory usage: 20 MB % 64.44/9.62 % (2857090)Instructions burned: 879 (million) % 64.44/9.62 % (2857110)ott-2_1_sil=16000:newcnf=on:random_seed=964286298:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2986 on theBenchmark for (2986ds/869Mi) % 64.44/9.62 % (2857112)ott+10_1_sil=32000:tgt=ground:random_seed=3641852898:i=5114:av=off_2986 on theBenchmark for (2986ds/5114Mi) % 64.44/9.62 % (2857110)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 64.44/9.62 % Exception at run slice level % 64.44/9.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.44/9.62 % (2857118)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4247746621:i=54282_2984 on theBenchmark for (2984ds/54282Mi) % 64.44/9.62 % Exception at run slice level % 64.44/9.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 134.64/19.44 % (2857120)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3107604742:i=3512:aac=none_2981 on theBenchmark for (2981ds/3512Mi) % 134.64/19.44 % (2857120)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 134.64/19.44 % (2857110)Instruction limit reached! % 134.64/19.44 % (2857110)------------------------------ % 134.64/19.44 % (2857110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.44 % (2857110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.44 % (2857110)CaDiCaL version: 2.1.3 % 134.64/19.44 % (2857110)Termination reason: Instruction limit % 134.64/19.44 % (2857110)Termination phase: Saturation % 134.64/19.44 % (2857110)Time elapsed: 0.680 s % 134.64/19.44 % (2857110)Peak memory usage: 19 MB % 134.64/19.44 % (2857110)Instructions burned: 869 (million) % 134.64/19.44 % (2857122)dis+21_1_sil=32000:sas=cadical:random_seed=1450060099:i=3773:amm=off_2979 on theBenchmark for (2979ds/3773Mi) % 134.64/19.44 % (2857102)Instruction limit reached! % 134.64/19.44 % (2857102)------------------------------ % 134.64/19.44 % (2857102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.44 % (2857102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.44 % (2857102)CaDiCaL version: 2.1.3 % 134.64/19.44 % (2857102)Termination reason: Instruction limit % 134.64/19.44 % (2857102)Termination phase: Saturation % 134.64/19.44 % (2857102)Time elapsed: 1.214 s % 134.64/19.44 % (2857102)Peak memory usage: 23 MB % 134.64/19.44 % (2857102)Instructions burned: 1473 (million) % 134.64/19.44 % (2857124)ott+11_1_sil=16000:gs=on:random_seed=2913306131:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2976 on theBenchmark for (2976ds/2251Mi) % 134.64/19.44 % (2857124)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 134.64/19.44 % (2857098)Instruction limit reached! % 134.64/19.44 % (2857098)------------------------------ % 134.64/19.44 % (2857098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.44 % (2857098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.44 % (2857098)CaDiCaL version: 2.1.3 % 134.64/19.44 % (2857098)Termination reason: Instruction limit % 134.64/19.44 % (2857098)Termination phase: Saturation % 134.64/19.44 % (2857098)Time elapsed: 2.202 s % 134.64/19.44 % (2857098)Peak memory usage: 43 MB % 134.64/19.44 % (2857098)Instructions burned: 5131 (million) % 134.64/19.44 % (2857132)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3630042358:fmbsr=1.6:i=67534_2968 on theBenchmark for (2968ds/67534Mi) % 134.64/19.44 % Exception at run slice level % 134.64/19.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 134.64/19.44 % (2857134)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3693131639:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2967 on theBenchmark for (2967ds/4591Mi) % 134.64/19.44 % (2857124)Instruction limit reached! % 134.64/19.44 % (2857124)------------------------------ % 134.64/19.44 % (2857124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.44 % (2857124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.44 % (2857124)CaDiCaL version: 2.1.3 % 134.64/19.44 % (2857124)Termination reason: Instruction limit % 134.64/19.44 % (2857124)Termination phase: Saturation % 134.64/19.44 % (2857124)Time elapsed: 1.661 s % 134.64/19.44 % (2857124)Peak memory usage: 29 MB % 134.64/19.44 % (2857124)Instructions burned: 2253 (million) % 134.64/19.44 % (2857138)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1594980521:i=29340_2959 on theBenchmark for (2959ds/29340Mi) % 134.64/19.44 % (2857120)Instruction limit reached! % 134.64/19.44 % (2857120)------------------------------ % 134.64/19.44 % (2857120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 134.64/19.44 % (2857120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.64/19.44 % (2857120)CaDiCaL version: 2.1.3 % 134.64/19.44 % (2857120)Termination reason: Instruction limit % 134.64/19.44 % (2857120)Termination phase: Saturation % 134.64/19.44 % (2857120)Time elapsed: 2.831 s % 134.64/19.44 % (2857120)Peak memory usage: 31 MB % 134.64/19.44 % (2857120)Instructions burned: 3513 (million) % 134.64/19.44 % (2857142)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3449577696:i=5211_2953 on theBenchmark for (2953ds/5211Mi) % 134.64/19.44 % (2857134)Instruction limit reached! % 165.29/23.79 % (2857134)------------------------------ % 165.29/23.79 % (2857134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.79 % (2857134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.79 % (2857134)CaDiCaL version: 2.1.3 % 165.29/23.79 % (2857134)Termination reason: Instruction limit % 165.29/23.79 % (2857134)Termination phase: Saturation % 165.29/23.79 % (2857134)Time elapsed: 1.669 s % 165.29/23.79 % (2857134)Peak memory usage: 25 MB % 165.29/23.79 % (2857134)Instructions burned: 4593 (million) % 165.29/23.79 % (2857144)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2947671034:i=5497:nm=2_2950 on theBenchmark for (2950ds/5497Mi) % 165.29/23.79 % (2857122)Instruction limit reached! % 165.29/23.79 % (2857122)------------------------------ % 165.29/23.79 % (2857122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.79 % (2857122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.79 % (2857122)CaDiCaL version: 2.1.3 % 165.29/23.79 % (2857122)Termination reason: Instruction limit % 165.29/23.79 % (2857122)Termination phase: Saturation % 165.29/23.79 % (2857122)Time elapsed: 2.994 s % 165.29/23.79 % (2857122)Peak memory usage: 35 MB % 165.29/23.79 % (2857122)Instructions burned: 3773 (million) % 165.29/23.79 % (2857146)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1861039528:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi) % 165.29/23.79 % Exception at run slice level % 165.29/23.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.29/23.79 % (2857148)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1880822879:i=14071_2948 on theBenchmark for (2948ds/14071Mi) % 165.29/23.79 % Exception at run slice level % 165.29/23.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.29/23.79 % (2857150)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=226097854:i=22565:add=on:rawr=on_2946 on theBenchmark for (2946ds/22565Mi) % 165.29/23.79 % Exception at run slice level % 165.29/23.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.29/23.79 % (2857152)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=878365920:i=8173:av=off_2946 on theBenchmark for (2946ds/8173Mi) % 165.29/23.79 % (2857112)Instruction limit reached! % 165.29/23.79 % (2857112)------------------------------ % 165.29/23.79 % (2857112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.79 % (2857112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.79 % (2857112)CaDiCaL version: 2.1.3 % 165.29/23.79 % (2857112)Termination reason: Instruction limit % 165.29/23.79 % (2857112)Termination phase: Saturation % 165.29/23.79 % (2857112)Time elapsed: 4.163 s % 165.29/23.79 % (2857112)Peak memory usage: 53 MB % 165.29/23.79 % (2857112)Instructions burned: 5114 (million) % 165.29/23.79 % (2857154)dis+10_16:1_sil=16000:random_seed=2129042720:i=9155:fsr=off_2944 on theBenchmark for (2944ds/9155Mi) % 165.29/23.79 % (2857152)Instruction limit reached! % 165.29/23.79 % (2857152)------------------------------ % 165.29/23.79 % (2857152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.79 % (2857152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.79 % (2857152)CaDiCaL version: 2.1.3 % 165.29/23.79 % (2857152)Termination reason: Instruction limit % 165.29/23.79 % (2857152)Termination phase: Saturation % 165.29/23.79 % (2857152)Time elapsed: 3.334 s % 165.29/23.79 % (2857152)Peak memory usage: 87 MB % 165.29/23.79 % (2857152)Instructions burned: 8175 (million) % 165.29/23.79 % (2857156)ott-3_8_sil=64000:random_seed=3879004743:i=20139:bs=on_2912 on theBenchmark for (2912ds/20139Mi) % 165.29/23.79 % (2857142)Instruction limit reached! % 165.29/23.79 % (2857142)------------------------------ % 165.29/23.79 % (2857142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.29/23.79 % (2857142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.29/23.79 % (2857142)CaDiCaL version: 2.1.3 % 165.29/23.79 % (2857142)Termination reason: Instruction limit % 165.29/23.79 % (2857142)Termination phase: Saturation % 165.29/23.79 % (2857142)Time elapsed: 4.265 s % 165.29/23.79 % (2857142)Peak memory usage: 47 MB % 165.29/23.79 % (2857142)Instructions burned: 5212 (million) % 165.29/23.79 % (2857158)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=701218033:fmbsr=2:i=32576_2910 on theBenchmark for (2910ds/32576Mi) % 165.29/23.79 % Exception at run slice level % 175.46/25.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 175.46/25.17 % (2857160)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1250412446:i=11404_2907 on theBenchmark for (2907ds/11404Mi) % 175.46/25.17 % (2857154)Instruction limit reached! % 175.46/25.17 % (2857154)------------------------------ % 175.46/25.17 % (2857154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.46/25.17 % (2857154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.46/25.17 % (2857154)CaDiCaL version: 2.1.3 % 175.46/25.17 % (2857154)Termination reason: Instruction limit % 175.46/25.17 % (2857154)Termination phase: Saturation % 175.46/25.17 % (2857154)Time elapsed: 7.140 s % 175.46/25.17 % (2857154)Peak memory usage: 65 MB % 175.46/25.17 % (2857154)Instructions burned: 9155 (million) % 175.46/25.17 % (2857205)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2112931639:i=14134_2872 on theBenchmark for (2872ds/14134Mi) % 175.46/25.17 % (2857205)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 175.46/25.17 % (2857156)Instruction limit reached! % 175.46/25.17 % (2857156)------------------------------ % 175.46/25.17 % (2857156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.46/25.17 % (2857156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.46/25.17 % (2857156)CaDiCaL version: 2.1.3 % 175.46/25.17 % (2857156)Termination reason: Instruction limit % 175.46/25.17 % (2857156)Termination phase: Saturation % 175.46/25.17 % (2857156)Time elapsed: 6.379 s % 175.46/25.17 % (2857156)Peak memory usage: 109 MB % 175.46/25.17 % (2857156)Instructions burned: 20143 (million) % 175.46/25.17 % (2857213)dis+33_16_sil=32000:sac=on:random_seed=1687084267:i=15851:nm=0_2848 on theBenchmark for (2848ds/15851Mi) % 175.46/25.17 % (2857160)Instruction limit reached! % 175.46/25.17 % (2857160)------------------------------ % 175.46/25.17 % (2857160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.46/25.17 % (2857160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.46/25.17 % (2857160)CaDiCaL version: 2.1.3 % 175.46/25.17 % (2857160)Termination reason: Instruction limit % 175.46/25.17 % (2857160)Termination phase: Saturation % 175.46/25.17 % (2857160)Time elapsed: 6.576 s % 175.46/25.17 % (2857160)Peak memory usage: 127 MB % 175.46/25.17 % (2857160)Instructions burned: 11406 (million) % 175.46/25.17 % (2857215)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2726078062:avsq=on:i=17627:add=on:amm=off_2841 on theBenchmark for (2841ds/17627Mi) % 175.46/25.17 % (2857150)Instruction limit reached! % 175.46/25.17 % (2857150)------------------------------ % 175.46/25.17 % (2857150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.46/25.17 % (2857150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.46/25.17 % (2857150)CaDiCaL version: 2.1.3 % 175.46/25.17 % (2857150)Termination reason: Instruction limit % 175.46/25.17 % (2857150)Termination phase: Saturation % 175.46/25.17 % (2857150)Time elapsed: 10.585 s % 175.46/25.17 % (2857150)Peak memory usage: 48 MB % 175.46/25.17 % (2857150)Instructions burned: 22566 (million) % 175.46/25.17 % (2857217)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2534718811:s2a=on:i=53295_2840 on theBenchmark for (2840ds/53295Mi) % 175.46/25.17 % (2857213)Instruction limit reached! % 175.46/25.17 % (2857213)------------------------------ % 175.46/25.17 % (2857213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 175.46/25.17 % (2857213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.46/25.17 % (2857213)CaDiCaL version: 2.1.3 % 175.46/25.17 % (2857213)Termination reason: Instruction limit % 175.46/25.17 % (2857213)Termination phase: Saturation % 175.46/25.17 % (2857213)Time elapsed: 3.643 s % 175.46/25.17 % (2857213)Peak memory usage: 68 MB % 175.46/25.17 % (2857213)Instructions burned: 15852 (million) % 175.46/25.17 % (2857219)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3539517202:i=26857:ins=20_2811 on theBenchmark for (2811ds/26857Mi) % 175.46/25.17 % Exception at run slice level % 175.46/25.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 175.46/25.17 % (2857221)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2611607693:i=28120:bs=on:fsr=off_2811 on theBenchmark for (2811ds/28120Mi) % 175.46/25.17 % (2857205)Instruction limit reached! % 175.46/25.17 % (2857205)------------------------------ % 175.46/25.17 % (2857205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.77/26.94 % (2857205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.77/26.94 % (2857205)CaDiCaL version: 2.1.3 % 186.77/26.94 % (2857205)Termination reason: Instruction limit % 186.77/26.94 % (2857205)Termination phase: Saturation % 186.77/26.94 % (2857205)Time elapsed: 6.305 s % 186.77/26.94 % (2857205)Peak memory usage: 136 MB % 186.77/26.94 % (2857205)Instructions burned: 14134 (million) % 186.77/26.94 % (2857223)fmb+10_1_sil=256000:fmbss=7:random_seed=3204096956:fmbsr=1.6:i=182295_2809 on theBenchmark for (2809ds/182295Mi) % 186.77/26.94 % Exception at run slice level % 186.77/26.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.77/26.94 % (2857226)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3967901456:i=44625:gsp=on_2807 on theBenchmark for (2807ds/44625Mi) % 186.77/26.94 % (2857226)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 186.77/26.94 % (2857226)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 186.77/26.94 % Exception at run slice level % 186.77/26.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.77/26.94 % (2857228)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=350767235:i=160505_2806 on theBenchmark for (2806ds/160505Mi) % 186.77/26.94 % Exception at run slice level % 186.77/26.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.77/26.94 % (2857230)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2110268579:fmbsr=1.3:i=225729_2804 on theBenchmark for (2804ds/225729Mi) % 186.77/26.94 % Exception at run slice level % 186.77/26.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.77/26.94 % (2857232)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=148200808:fmbsr=2:i=185024:ins=7_2803 on theBenchmark for (2803ds/185024Mi) % 186.77/26.94 % Exception at run slice level % 186.77/26.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.77/26.94 % (2857234)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1213572254:rtra=on_2801 on theBenchmark for (2801ds/0Mi) % 186.77/26.94 % Exception at run slice level % 186.77/26.94 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 186.77/26.94 % (2857236)% WARNING: option uhcvi not known. % 186.77/26.94 % (2857236)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1487951178:i=271062:add=off:rtra=on:rawr=on_2799 on theBenchmark for (2799ds/271062Mi) % 186.77/26.94 % (2857236)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 186.77/26.94 % (2857236)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 186.77/26.94 % (2857138)Instruction limit reached! % 186.77/26.94 % (2857138)------------------------------ % 186.77/26.94 % (2857138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.77/26.94 % (2857138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.77/26.94 % (2857138)CaDiCaL version: 2.1.3 % 186.77/26.94 % (2857138)Termination reason: Instruction limit % 186.77/26.94 % (2857138)Termination phase: Saturation % 186.77/26.94 % (2857138)Time elapsed: 16.485 s % 186.77/26.94 % (2857138)Peak memory usage: 48 MB % 186.77/26.94 % (2857138)Instructions burned: 29341 (million) % 186.77/26.94 % (2857238)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3768660778:i=176048:add=on:rtra=on:rawr=on_2794 on theBenchmark for (2794ds/176048Mi) % 186.77/26.94 % (2857215)Instruction limit reached! % 186.77/26.94 % (2857215)------------------------------ % 186.77/26.94 % (2857215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 186.77/26.94 % (2857215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.77/26.94 % (2857215)CaDiCaL version: 2.1.3 % 186.77/26.94 % (2857215)Termination reason: Instruction limit % 186.77/26.94 % (2857215)Termination phase: Saturation % 186.77/26.94 % (2857215)Time elapsed: 7.402 s % 186.77/26.94 % (2857215)Peak memory usage: 57 MB % 186.77/26.94 % (2857215)Instructions burned: 17629 (million) % 186.77/26.94 % (2857240)dis+10_1_sil=32000:si=on:sp=arity:random_seed=295174294:i=206:fgj=on:rtra=on_2766 on theBenchmark for (2766ds/206Mi) % 186.77/26.94 % (2857240)Instruction limit reached! % 186.77/26.94 % (2857240)------------------------------ % 186.77/26.94 % (2857240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.62/29.99 % (2857240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.62/29.99 % (2857240)CaDiCaL version: 2.1.3 % 208.62/29.99 % (2857240)Termination reason: Instruction limit % 208.62/29.99 % (2857240)Termination phase: Property scanning % 208.62/29.99 % (2857240)Time elapsed: 0.093 s % 208.62/29.99 % (2857240)Peak memory usage: 15 MB % 208.62/29.99 % (2857240)Instructions burned: 206 (million) % 208.62/29.99 % (2857242)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1577198534:i=232:rtra=on_2765 on theBenchmark for (2765ds/232Mi) % 208.62/29.99 % (2857242)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 208.62/29.99 % (2857242)Instruction limit reached! % 208.62/29.99 % (2857242)------------------------------ % 208.62/29.99 % (2857242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.62/29.99 % (2857242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.62/29.99 % (2857242)CaDiCaL version: 2.1.3 % 208.62/29.99 % (2857242)Termination reason: Instruction limit % 208.62/29.99 % (2857242)Termination phase: Property scanning % 208.62/29.99 % (2857242)Time elapsed: 0.103 s % 208.62/29.99 % (2857242)Peak memory usage: 15 MB % 208.62/29.99 % (2857242)Instructions burned: 233 (million) % 208.62/29.99 % (2857244)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=376292396:i=262:rtra=on_2764 on theBenchmark for (2764ds/262Mi) % 208.62/29.99 % (2857244)Instruction limit reached! % 208.62/29.99 % (2857244)------------------------------ % 208.62/29.99 % (2857244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.62/29.99 % (2857244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.62/29.99 % (2857244)CaDiCaL version: 2.1.3 % 208.62/29.99 % (2857244)Termination reason: Instruction limit % 208.62/29.99 % (2857244)Termination phase: Property scanning % 208.62/29.99 % (2857244)Time elapsed: 0.114 s % 208.62/29.99 % (2857244)Peak memory usage: 15 MB % 208.62/29.99 % (2857244)Instructions burned: 262 (million) % 208.62/29.99 % (2857246)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3923642238:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2763 on theBenchmark for (2763ds/318Mi) % 208.62/29.99 % (2857246)Instruction limit reached! % 208.62/29.99 % (2857246)------------------------------ % 208.62/29.99 % (2857246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.62/29.99 % (2857246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.62/29.99 % (2857246)CaDiCaL version: 2.1.3 % 208.62/29.99 % (2857246)Termination reason: Instruction limit % 208.62/29.99 % (2857246)Termination phase: Property scanning % 208.62/29.99 % (2857246)Time elapsed: 0.138 s % 208.62/29.99 % (2857246)Peak memory usage: 15 MB % 208.62/29.99 % (2857246)Instructions burned: 318 (million) % 208.62/29.99 % (2857248)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3022615558:i=1428:nm=2:rtra=on_2761 on theBenchmark for (2761ds/1428Mi) % 208.62/29.99 % Exception at run slice level % 208.62/29.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.62/29.99 % (2857250)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2329883282:i=262:bd=preordered:rtra=on:fsd=on_2759 on theBenchmark for (2759ds/262Mi) % 208.62/29.99 % (2857250)Instruction limit reached! % 208.62/29.99 % (2857250)------------------------------ % 208.62/29.99 % (2857250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.62/29.99 % (2857250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.62/29.99 % (2857250)CaDiCaL version: 2.1.3 % 208.62/29.99 % (2857250)Termination reason: Instruction limit % 208.62/29.99 % (2857250)Termination phase: Property scanning % 208.62/29.99 % (2857250)Time elapsed: 0.115 s % 208.62/29.99 % (2857250)Peak memory usage: 15 MB % 208.62/29.99 % (2857250)Instructions burned: 265 (million) % 208.62/29.99 % (2857252)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=1078468015:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2758 on theBenchmark for (2758ds/1368Mi) % 208.62/29.99 % (2857252)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 208.62/29.99 % (2857252)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 208.62/29.99 % (2857252)Instruction limit reached! % 208.62/29.99 % (2857252)------------------------------ % 208.62/29.99 % (2857252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.25/33.70 % (2857252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.25/33.70 % (2857252)CaDiCaL version: 2.1.3 % 236.25/33.70 % (2857252)Termination reason: Instruction limit % 236.25/33.70 % (2857252)Termination phase: Saturation % 236.25/33.70 % (2857252)Time elapsed: 0.636 s % 236.25/33.70 % (2857252)Peak memory usage: 19 MB % 236.25/33.70 % (2857252)Instructions burned: 1369 (million) % 236.25/33.70 % (2857254)ott-21_1_sil=16000:si=on:fs=off:random_seed=302190743:i=360:av=off:fsr=off:rtra=on_2751 on theBenchmark for (2751ds/360Mi) % 236.25/33.70 % (2857254)Instruction limit reached! % 236.25/33.70 % (2857254)------------------------------ % 236.25/33.70 % (2857254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.25/33.70 % (2857254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.25/33.70 % (2857254)CaDiCaL version: 2.1.3 % 236.25/33.70 % (2857254)Termination reason: Instruction limit % 236.25/33.70 % (2857254)Termination phase: Saturation % 236.25/33.70 % (2857254)Time elapsed: 0.156 s % 236.25/33.70 % (2857254)Peak memory usage: 16 MB % 236.25/33.70 % (2857254)Instructions burned: 360 (million) % 236.25/33.70 % (2857256)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1480599945:i=954:bd=all:rtra=on_2750 on theBenchmark for (2750ds/954Mi) % 236.25/33.70 % (2857256)Instruction limit reached! % 236.25/33.70 % (2857256)------------------------------ % 236.25/33.70 % (2857256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.25/33.70 % (2857256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.25/33.70 % (2857256)CaDiCaL version: 2.1.3 % 236.25/33.70 % (2857256)Termination reason: Instruction limit % 236.25/33.70 % (2857256)Termination phase: Saturation % 236.25/33.70 % (2857256)Time elapsed: 0.475 s % 236.25/33.70 % (2857256)Peak memory usage: 19 MB % 236.25/33.70 % (2857256)Instructions burned: 956 (million) % 236.25/33.70 % (2857258)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2001782664:fmbsr=1.3:i=1730:ins=25:rtra=on_2745 on theBenchmark for (2745ds/1730Mi) % 236.25/33.70 % Exception at run slice level % 236.25/33.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.25/33.70 % (2857260)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=2085079945:i=2358:rtra=on_2743 on theBenchmark for (2743ds/2358Mi) % 236.25/33.70 % (2857221)Instruction limit reached! % 236.25/33.70 % (2857221)------------------------------ % 236.25/33.70 % (2857221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.25/33.70 % (2857221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.25/33.70 % (2857221)CaDiCaL version: 2.1.3 % 236.25/33.70 % (2857221)Termination reason: Instruction limit % 236.25/33.70 % (2857221)Termination phase: Saturation % 236.25/33.70 % (2857221)Time elapsed: 7.148 s % 236.25/33.70 % (2857221)Peak memory usage: 209 MB % 236.25/33.70 % (2857221)Instructions burned: 28122 (million) % 236.25/33.70 % (2857262)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1827291604:i=1778:ins=1:rtra=on_2739 on theBenchmark for (2739ds/1778Mi) % 236.25/33.70 % Exception at run slice level % 236.25/33.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 236.25/33.70 % (2857264)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=4221779045:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2738 on theBenchmark for (2738ds/1384Mi) % 236.25/33.70 % (2857264)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 236.25/33.70 % (2857264)Instruction limit reached! % 236.25/33.70 % (2857264)------------------------------ % 236.25/33.70 % (2857264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 236.25/33.70 % (2857264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.25/33.70 % (2857264)CaDiCaL version: 2.1.3 % 236.25/33.70 % (2857264)Termination reason: Instruction limit % 236.25/33.70 % (2857264)Termination phase: Saturation % 236.25/33.70 % (2857264)Time elapsed: 0.342 s % 236.25/33.70 % (2857264)Peak memory usage: 23 MB % 236.25/33.70 % (2857264)Instructions burned: 1388 (million) % 236.25/33.70 % (2857266)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1300925787:i=1758:kws=inv_precedence:fsr=off:rtra=on_2734 on theBenchmark for (2734ds/1758Mi) % 236.25/33.70 % (2857266)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 276.00/39.38 % (2857260)Instruction limit reached! % 276.00/39.38 % (2857260)------------------------------ % 276.00/39.38 % (2857260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.00/39.38 % (2857260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.00/39.38 % (2857260)CaDiCaL version: 2.1.3 % 276.00/39.38 % (2857260)Termination reason: Instruction limit % 276.00/39.38 % (2857260)Termination phase: Saturation % 276.00/39.38 % (2857260)Time elapsed: 1.096 s % 276.00/39.38 % (2857260)Peak memory usage: 32 MB % 276.00/39.38 % (2857260)Instructions burned: 2358 (million) % 276.00/39.38 % (2857268)fmb+10_1_sil=64000:si=on:random_seed=1824310252:i=44122:nm=2:rtra=on:gsp=on_2732 on theBenchmark for (2732ds/44122Mi) % 276.00/39.38 % (2857268)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 276.00/39.38 % Exception at run slice level % 276.00/39.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 276.00/39.38 % (2857270)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2987744846:i=19030:nm=5:rtra=on_2730 on theBenchmark for (2730ds/19030Mi) % 276.00/39.38 % (2857266)Instruction limit reached! % 276.00/39.38 % (2857266)------------------------------ % 276.00/39.38 % (2857266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.00/39.38 % (2857266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.00/39.38 % (2857266)CaDiCaL version: 2.1.3 % 276.00/39.38 % (2857266)Termination reason: Instruction limit % 276.00/39.38 % (2857266)Termination phase: Saturation % 276.00/39.38 % (2857266)Time elapsed: 0.450 s % 276.00/39.38 % (2857266)Peak memory usage: 28 MB % 276.00/39.38 % (2857266)Instructions burned: 1761 (million) % 276.00/39.38 % (2857272)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=955005774:fmbsr=1.7:i=1840:rtra=on_2730 on theBenchmark for (2730ds/1840Mi) % 276.00/39.38 % Exception at run slice level % 276.00/39.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 276.00/39.38 % (2857274)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=842764295:i=10262:rtra=on_2729 on theBenchmark for (2729ds/10262Mi) % 276.00/39.38 % Exception at run slice level % 276.00/39.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 276.00/39.38 % (2857276)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3938066512:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2728 on theBenchmark for (2728ds/2944Mi) % 276.00/39.38 % (2857274)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 276.00/39.38 % (2857276)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 276.00/39.38 % (2857276)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 276.00/39.38 % (2857276)Instruction limit reached! % 276.00/39.38 % (2857276)------------------------------ % 276.00/39.38 % (2857276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.00/39.38 % (2857276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.00/39.38 % (2857276)CaDiCaL version: 2.1.3 % 276.00/39.38 % (2857276)Termination reason: Instruction limit % 276.00/39.38 % (2857276)Termination phase: Saturation % 276.00/39.38 % (2857276)Time elapsed: 1.393 s % 276.00/39.38 % (2857276)Peak memory usage: 27 MB % 276.00/39.38 % (2857276)Instructions burned: 2945 (million) % 276.00/39.38 % (2857280)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=418935672:i=12648:rtra=on_2714 on theBenchmark for (2714ds/12648Mi) % 276.00/39.38 % Exception at run slice level % 276.00/39.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 276.00/39.38 % (2857282)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3407901089:fmbsr=2.30978:i=4348:rtra=on_2713 on theBenchmark for (2713ds/4348Mi) % 276.00/39.38 % Exception at run slice level % 276.00/39.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 276.00/39.38 % (2857284)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=4046280245:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2711 on theBenchmark for (2711ds/1738Mi) % 276.00/39.38 % (2857284)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs. % 276.00/39.38 % (2857274)Instruction limit reached! % 300.11/42.74 % (2857274)------------------------------ % 300.11/42.74 % (2857274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.74 % (2857274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.74 % (2857274)CaDiCaL version: 2.1.3 % 300.11/42.74 % (2857274)Termination reason: Instruction limit % 300.11/42.74 % (2857274)Termination phase: Saturation % 300.11/42.74 % (2857274)Time elapsed: 2.522 s % 300.11/42.74 % (2857274)Peak memory usage: 71 MB % 300.11/42.74 % (2857274)Instructions burned: 10263 (million) % 300.11/42.74 % (2857286)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1951034613:i=10228:av=off:rtra=on_2703 on theBenchmark for (2703ds/10228Mi) % 300.11/42.74 % (2857284)Instruction limit reached! % 300.11/42.74 % (2857284)------------------------------ % 300.11/42.74 % (2857284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.74 % (2857284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.74 % (2857284)CaDiCaL version: 2.1.3 % 300.11/42.74 % (2857284)Termination reason: Instruction limit % 300.11/42.74 % (2857284)Termination phase: Saturation % 300.11/42.74 % (2857284)Time elapsed: 0.820 s % 300.11/42.74 % (2857284)Peak memory usage: 28 MB % 300.11/42.74 % (2857284)Instructions burned: 1740 (million) % 300.11/42.74 % (2857288)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3688358510:i=108564:rtra=on_2702 on theBenchmark for (2702ds/108564Mi) % 300.11/42.74 % Exception at run slice level % 300.11/42.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.11/42.74 % (2857290)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3394272684:i=7024:aac=none:rtra=on_2701 on theBenchmark for (2701ds/7024Mi) % 300.11/42.74 % (2857290)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 300.11/42.74 % (2857060)Instruction limit reached! % 300.11/42.74 % (2857060)------------------------------ % 300.11/42.74 % (2857060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.74 % (2857060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.74 % (2857060)CaDiCaL version: 2.1.3 % 300.11/42.74 % (2857060)Termination reason: Instruction limit % 300.11/42.74 % (2857060)Termination phase: Saturation % 300.11/42.74 % (2857060)Time elapsed: 30.446 s % 300.11/42.74 % (2857060)Peak memory usage: 32 MB % 300.11/42.74 % (2857060)Instructions burned: 88025 (million) % 300.11/42.74 % (2857292)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=100939219:i=7546:rtra=on:amm=off_2694 on theBenchmark for (2694ds/7546Mi) % 300.11/42.74 % (2857286)Instruction limit reached! % 300.11/42.74 % (2857286)------------------------------ % 300.11/42.74 % (2857286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.74 % (2857286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.74 % (2857286)CaDiCaL version: 2.1.3 % 300.11/42.74 % (2857286)Termination reason: Instruction limit % 300.11/42.74 % (2857286)Termination phase: Saturation % 300.11/42.74 % (2857286)Time elapsed: 2.574 s % 300.11/42.74 % (2857286)Peak memory usage: 98 MB % 300.11/42.74 % (2857286)Instructions burned: 10229 (million) % 300.11/42.74 % (2857294)ott+11_1_sil=16000:si=on:gs=on:random_seed=3048419968:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2677 on theBenchmark for (2677ds/4502Mi) % 300.11/42.74 % (2857294)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use % 300.11/42.74 % (2857290)Instruction limit reached! % 300.11/42.74 % (2857290)------------------------------ % 300.11/42.74 % (2857290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.11/42.74 % (2857290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.11/42.74 % (2857290)CaDiCaL version: 2.1.3 % 300.11/42.74 % (2857290)Termination reason: Instruction limit % 300.11/42.74 % (2857290)Termination phase: Saturation % 300.11/42.74 % (2857290)Time elapsed: 3.231 s % 300.11/42.74 % (2857290)Peak memory usage: 59 MB % 300.11/42.74 % (2857290)Instructions burned: 7025 (million) % 300.11/42.74 % (2857296)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=2370163090:fmbsr=1.6:i=135068:rtra=on_2668 on theBenchmark for (2668ds/135068Mi) % 300.11/42.74 % Exception at run slice level % 300.11/42.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.11/42.74 % (2857298)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:ran % 300.11/42.74 Terminated % 300.11/42.74 % Vampire exiting %------------------------------------------------------------------------------