%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW476_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:40:14 PM UTC 2026 % Result : Timeout 300.12s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW476_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.12/0.26 % Computer : n002.cluster.edu % 0.12/0.26 % Model : x86_64 x86_64 % 0.12/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.26 % Memory : 8046.5625MB % 0.12/0.26 % OS : Linux 6.8.0-71-generic % 0.12/0.27 % CPULimit : 300 % 0.12/0.27 % WCLimit : 300 % 0.12/0.27 % DateTime : Mon Sep 28 14:14:22 UTC 2026 % 0.12/0.27 % CPUTime : % 0.12/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.27/0.31 Running first-order model finding % 0.27/0.31 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 14.14/2.35 % (372702)Will run a generic schedule for satisfiability detection. % 14.14/2.35 % (372707)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2128666075_2999 on theBenchmark for (2999ds/0Mi) % 14.14/2.35 % (372708)% WARNING: option uhcvi not known. % 14.14/2.35 % Exception at run slice level % 14.14/2.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.14/2.35 % (372712)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3240951287:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.14/2.35 % (372711)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1413837005:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.14/2.35 % (372708)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3513804780:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.14/2.35 % (372713)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2095894208:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.14/2.35 % (372710)dis+10_1_sil=32000:sp=arity:random_seed=4044397821:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.14/2.35 % (372709)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3013679298:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.14/2.35 % (372715)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=168839018:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 14.14/2.35 % Exception at run slice level % 14.14/2.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 14.14/2.35 % (372723)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2678000914:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 14.14/2.35 % (372711)Instruction limit reached! % 14.14/2.35 % (372711)------------------------------ % 14.14/2.35 % (372711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.14/2.35 % (372711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.35 % (372711)CaDiCaL version: 2.1.3 % 14.14/2.35 % (372711)Termination reason: Instruction limit % 14.14/2.35 % (372711)Termination phase: Saturation % 14.14/2.35 % (372711)Time elapsed: 0.084 s % 14.14/2.35 % (372711)Peak memory usage: 12 MB % 14.14/2.35 % (372711)Instructions burned: 117 (million) % 14.14/2.35 % (372713)Instruction limit reached! % 14.14/2.35 % (372713)------------------------------ % 14.14/2.35 % (372713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.14/2.35 % (372713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.35 % (372713)CaDiCaL version: 2.1.3 % 14.14/2.35 % (372713)Termination reason: Instruction limit % 14.14/2.35 % (372713)Termination phase: Saturation % 14.14/2.35 % (372713)Time elapsed: 0.098 s % 14.14/2.35 % (372713)Peak memory usage: 12 MB % 14.14/2.35 % (372713)Instructions burned: 159 (million) % 14.14/2.35 % (372710)Instruction limit reached! % 14.14/2.35 % (372710)------------------------------ % 14.14/2.35 % (372710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.14/2.35 % (372710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.35 % (372710)CaDiCaL version: 2.1.3 % 14.14/2.35 % (372710)Termination reason: Instruction limit % 14.14/2.35 % (372710)Termination phase: Saturation % 14.14/2.35 % (372710)Time elapsed: 0.104 s % 14.14/2.35 % (372710)Peak memory usage: 12 MB % 14.14/2.35 % (372710)Instructions burned: 103 (million) % 14.14/2.35 % (372723)Instruction limit reached! % 14.14/2.35 % (372723)------------------------------ % 14.14/2.35 % (372723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.14/2.35 % (372723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.14/2.35 % (372723)CaDiCaL version: 2.1.3 % 14.14/2.35 % (372723)Termination reason: Instruction limit % 14.14/2.35 % (372723)Termination phase: Saturation % 14.14/2.35 % (372723)Time elapsed: 0.074 s % 14.14/2.35 % (372723)Peak memory usage: 13 MB % 14.14/2.35 % (372723)Instructions burned: 132 (million) % 14.14/2.35 % (372725)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=86749776:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.14/2.35 % (372712)Instruction limit reached! % 14.14/2.35 % (372712)------------------------------ % 14.14/2.35 % (372712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.14/2.35 % (372712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.63/4.72 % (372712)CaDiCaL version: 2.1.3 % 30.63/4.72 % (372712)Termination reason: Instruction limit % 30.63/4.72 % (372712)Termination phase: Saturation % 30.63/4.72 % (372712)Time elapsed: 0.125 s % 30.63/4.72 % (372712)Peak memory usage: 13 MB % 30.63/4.72 % (372712)Instructions burned: 131 (million) % 30.63/4.72 % (372726)ott-21_1_sil=16000:fs=off:random_seed=2754301560:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 30.63/4.72 % (372727)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=575237477:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 30.63/4.72 % (372728)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2940875690:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 30.63/4.72 % (372730)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2880078870:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 30.63/4.72 % Exception at run slice level % 30.63/4.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.63/4.72 % (372735)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2875191262:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 30.63/4.72 % Exception at run slice level % 30.63/4.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.63/4.72 % (372737)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=2154051958:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 30.63/4.72 % (372726)Instruction limit reached! % 30.63/4.72 % (372726)------------------------------ % 30.63/4.72 % (372726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.63/4.72 % (372726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.63/4.72 % (372726)CaDiCaL version: 2.1.3 % 30.63/4.72 % (372726)Termination reason: Instruction limit % 30.63/4.72 % (372726)Termination phase: Saturation % 30.63/4.72 % (372726)Time elapsed: 0.164 s % 30.63/4.72 % (372726)Peak memory usage: 12 MB % 30.63/4.72 % (372726)Instructions burned: 180 (million) % 30.63/4.72 % (372739)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2308290934:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 30.63/4.72 % (372730)Instruction limit reached! % 30.63/4.72 % (372730)------------------------------ % 30.63/4.72 % (372730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.63/4.72 % (372730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.63/4.72 % (372730)CaDiCaL version: 2.1.3 % 30.63/4.72 % (372730)Termination reason: Instruction limit % 30.63/4.72 % (372730)Termination phase: Saturation % 30.63/4.72 % (372730)Time elapsed: 0.342 s % 30.63/4.72 % (372730)Peak memory usage: 13 MB % 30.63/4.72 % (372730)Instructions burned: 1181 (million) % 30.63/4.72 % (372741)fmb+10_1_sil=64000:random_seed=709974959:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 30.63/4.72 % (372741)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 30.63/4.72 % Exception at run slice level % 30.63/4.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.63/4.72 % (372743)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=887540605:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 30.63/4.72 % Exception at run slice level % 30.63/4.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.63/4.72 % (372745)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=861102507:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi) % 30.63/4.72 % Exception at run slice level % 30.63/4.72 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 30.63/4.72 % (372747)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2405198828:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 30.63/4.72 % (372727)Instruction limit reached! % 30.63/4.72 % (372727)------------------------------ % 30.63/4.72 % (372727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 30.63/4.72 % (372727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.63/4.72 % (372727)CaDiCaL version: 2.1.3 % 30.63/4.72 % (372727)Termination reason: Instruction limit % 30.63/4.72 % (372727)Termination phase: Saturation % 100.05/14.47 % (372727)Time elapsed: 0.466 s % 100.05/14.47 % (372727)Peak memory usage: 15 MB % 100.05/14.47 % (372727)Instructions burned: 477 (million) % 100.05/14.47 % (372749)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3432601088:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 100.05/14.47 % (372749)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 100.05/14.47 % (372725)Instruction limit reached! % 100.05/14.47 % (372725)------------------------------ % 100.05/14.47 % (372725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.05/14.47 % (372725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.47 % (372725)CaDiCaL version: 2.1.3 % 100.05/14.47 % (372725)Termination reason: Instruction limit % 100.05/14.47 % (372725)Termination phase: Saturation % 100.05/14.47 % (372725)Time elapsed: 0.648 s % 100.05/14.47 % (372725)Peak memory usage: 16 MB % 100.05/14.47 % (372725)Instructions burned: 685 (million) % 100.05/14.47 % (372751)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=610757159:i=6324_2991 on theBenchmark for (2991ds/6324Mi) % 100.05/14.47 % Exception at run slice level % 100.05/14.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.05/14.47 % (372753)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=526431605:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi) % 100.05/14.47 % Exception at run slice level % 100.05/14.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.05/14.47 % (372737)Instruction limit reached! % 100.05/14.47 % (372737)------------------------------ % 100.05/14.47 % (372737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.05/14.47 % (372737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.47 % (372737)CaDiCaL version: 2.1.3 % 100.05/14.47 % (372737)Termination reason: Instruction limit % 100.05/14.47 % (372737)Termination phase: Saturation % 100.05/14.47 % (372737)Time elapsed: 0.667 s % 100.05/14.47 % (372737)Peak memory usage: 18 MB % 100.05/14.47 % (372737)Instructions burned: 692 (million) % 100.05/14.47 % (372755)ott-2_1_sil=16000:newcnf=on:random_seed=634106466:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 100.05/14.47 % (372756)ott+10_1_sil=32000:tgt=ground:random_seed=2328342457:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 100.05/14.47 % (372739)Instruction limit reached! % 100.05/14.47 % (372739)------------------------------ % 100.05/14.47 % (372739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.05/14.47 % (372739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.47 % (372739)CaDiCaL version: 2.1.3 % 100.05/14.47 % (372739)Termination reason: Instruction limit % 100.05/14.47 % (372739)Termination phase: Saturation % 100.05/14.47 % (372739)Time elapsed: 0.791 s % 100.05/14.47 % (372739)Peak memory usage: 20 MB % 100.05/14.47 % (372739)Instructions burned: 879 (million) % 100.05/14.47 % (372759)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1011929649:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 100.05/14.47 % Exception at run slice level % 100.05/14.47 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.05/14.47 % (372761)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1444987772:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 100.05/14.47 % (372755)Instruction limit reached! % 100.05/14.47 % (372755)------------------------------ % 100.05/14.47 % (372755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.05/14.47 % (372755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.47 % (372755)CaDiCaL version: 2.1.3 % 100.05/14.47 % (372755)Termination reason: Instruction limit % 100.05/14.47 % (372755)Termination phase: Saturation % 100.05/14.47 % (372755)Time elapsed: 0.500 s % 100.05/14.47 % (372755)Peak memory usage: 12 MB % 100.05/14.47 % (372755)Instructions burned: 870 (million) % 100.05/14.47 % (372765)dis+21_1_sil=32000:sas=cadical:random_seed=3745293077:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi) % 100.05/14.47 % (372749)Instruction limit reached! % 100.05/14.47 % (372749)------------------------------ % 100.05/14.47 % (372749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.05/14.47 % (372749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.05/14.47 % (372749)CaDiCaL version: 2.1.3 % 116.69/16.91 % (372749)Termination reason: Instruction limit % 116.69/16.91 % (372749)Termination phase: Saturation % 116.69/16.91 % (372749)Time elapsed: 1.345 s % 116.69/16.91 % (372749)Peak memory usage: 30 MB % 116.69/16.91 % (372749)Instructions burned: 1473 (million) % 116.69/16.91 % (372767)ott+11_1_sil=16000:gs=on:random_seed=810513276:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi) % 116.69/16.91 % (372767)Instruction limit reached! % 116.69/16.91 % (372767)------------------------------ % 116.69/16.91 % (372767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.69/16.91 % (372767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.69/16.91 % (372767)CaDiCaL version: 2.1.3 % 116.69/16.91 % (372767)Termination reason: Instruction limit % 116.69/16.91 % (372767)Termination phase: Saturation % 116.69/16.91 % (372767)Time elapsed: 1.252 s % 116.69/16.91 % (372767)Peak memory usage: 22 MB % 116.69/16.91 % (372767)Instructions burned: 2251 (million) % 116.69/16.91 % (372769)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1821646178:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi) % 116.69/16.91 % Exception at run slice level % 116.69/16.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 116.69/16.91 % (372771)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3756221919:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi) % 116.69/16.91 % (372756)Instruction limit reached! % 116.69/16.91 % (372756)------------------------------ % 116.69/16.91 % (372756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.69/16.91 % (372756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.69/16.91 % (372756)CaDiCaL version: 2.1.3 % 116.69/16.91 % (372756)Termination reason: Instruction limit % 116.69/16.91 % (372756)Termination phase: Saturation % 116.69/16.91 % (372756)Time elapsed: 2.596 s % 116.69/16.91 % (372756)Peak memory usage: 38 MB % 116.69/16.91 % (372756)Instructions burned: 5116 (million) % 116.69/16.91 % (372773)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2701362362:i=29340_2964 on theBenchmark for (2964ds/29340Mi) % 116.69/16.91 % (372747)Instruction limit reached! % 116.69/16.91 % (372747)------------------------------ % 116.69/16.91 % (372747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.69/16.91 % (372747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.69/16.91 % (372747)CaDiCaL version: 2.1.3 % 116.69/16.91 % (372747)Termination reason: Instruction limit % 116.69/16.91 % (372747)Termination phase: Saturation % 116.69/16.91 % (372747)Time elapsed: 3.261 s % 116.69/16.91 % (372747)Peak memory usage: 21 MB % 116.69/16.91 % (372747)Instructions burned: 5133 (million) % 116.69/16.91 % (372777)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3010483870:i=5211_2960 on theBenchmark for (2960ds/5211Mi) % 116.69/16.91 % (372761)Instruction limit reached! % 116.69/16.91 % (372761)------------------------------ % 116.69/16.91 % (372761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 116.69/16.91 % (372761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.69/16.91 % (372761)CaDiCaL version: 2.1.3 % 116.69/16.91 % (372761)Termination reason: Instruction limit % 116.69/16.91 % (372761)Termination phase: Saturation % 116.69/16.91 % (372761)Time elapsed: 3.018 s % 116.69/16.91 % (372761)Peak memory usage: 24 MB % 116.69/16.91 % (372761)Instructions burned: 3513 (million) % 116.69/16.91 % (372779)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=795733695:i=5497:nm=2_2957 on theBenchmark for (2957ds/5497Mi) % 116.69/16.91 % Exception at run slice level % 116.69/16.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 116.69/16.91 % (372781)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3018322484:fmbsr=2:i=46332_2956 on theBenchmark for (2956ds/46332Mi) % 116.69/16.91 % Exception at run slice level % 116.69/16.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 116.69/16.91 % (372783)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3200961921:i=14071_2956 on theBenchmark for (2956ds/14071Mi) % 116.69/16.91 % Exception at run slice level % 116.69/16.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 116.69/16.91 % (372785)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3824907683:i=22565:add=on:rawr=on_2956 on theBenchmark for (2956ds/22565Mi) % 206.41/29.40 % (372765)Instruction limit reached! % 206.41/29.40 % (372765)------------------------------ % 206.41/29.40 % (372765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.41/29.40 % (372765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.41/29.40 % (372765)CaDiCaL version: 2.1.3 % 206.41/29.40 % (372765)Termination reason: Instruction limit % 206.41/29.40 % (372765)Termination phase: Saturation % 206.41/29.40 % (372765)Time elapsed: 3.226 s % 206.41/29.40 % (372765)Peak memory usage: 25 MB % 206.41/29.40 % (372765)Instructions burned: 3774 (million) % 206.41/29.40 % (372787)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=468862583:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi) % 206.41/29.40 % (372771)Instruction limit reached! % 206.41/29.40 % (372771)------------------------------ % 206.41/29.40 % (372771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.41/29.40 % (372771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.41/29.40 % (372771)CaDiCaL version: 2.1.3 % 206.41/29.40 % (372771)Termination reason: Instruction limit % 206.41/29.40 % (372771)Termination phase: Saturation % 206.41/29.40 % (372771)Time elapsed: 1.377 s % 206.41/29.40 % (372771)Peak memory usage: 14 MB % 206.41/29.40 % (372771)Instructions burned: 4595 (million) % 206.41/29.40 % (372789)dis+10_16:1_sil=16000:random_seed=4076614279:i=9155:fsr=off_2952 on theBenchmark for (2952ds/9155Mi) % 206.41/29.40 % (372777)Instruction limit reached! % 206.41/29.40 % (372777)------------------------------ % 206.41/29.40 % (372777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.41/29.40 % (372777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.41/29.40 % (372777)CaDiCaL version: 2.1.3 % 206.41/29.40 % (372777)Termination reason: Instruction limit % 206.41/29.40 % (372777)Termination phase: Saturation % 206.41/29.40 % (372777)Time elapsed: 4.931 s % 206.41/29.40 % (372777)Peak memory usage: 49 MB % 206.41/29.40 % (372777)Instructions burned: 5212 (million) % 206.41/29.40 % (372791)ott-3_8_sil=64000:random_seed=3221781732:i=20139:bs=on_2911 on theBenchmark for (2911ds/20139Mi) % 206.41/29.40 % (372789)Instruction limit reached! % 206.41/29.40 % (372789)------------------------------ % 206.41/29.40 % (372789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.41/29.40 % (372789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.41/29.40 % (372789)CaDiCaL version: 2.1.3 % 206.41/29.40 % (372789)Termination reason: Instruction limit % 206.41/29.40 % (372789)Termination phase: Saturation % 206.41/29.40 % (372789)Time elapsed: 4.369 s % 206.41/29.40 % (372789)Peak memory usage: 35 MB % 206.41/29.40 % (372789)Instructions burned: 9157 (million) % 206.41/29.40 % (372793)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2321463273:fmbsr=2:i=32576_2908 on theBenchmark for (2908ds/32576Mi) % 206.41/29.40 % Exception at run slice level % 206.41/29.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 206.41/29.40 % (372795)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1321297965:i=11404_2908 on theBenchmark for (2908ds/11404Mi) % 206.41/29.40 % (372787)Instruction limit reached! % 206.41/29.40 % (372787)------------------------------ % 206.41/29.40 % (372787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.41/29.40 % (372787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.41/29.40 % (372787)CaDiCaL version: 2.1.3 % 206.41/29.40 % (372787)Termination reason: Instruction limit % 206.41/29.40 % (372787)Termination phase: Saturation % 206.41/29.40 % (372787)Time elapsed: 7.532 s % 206.41/29.40 % (372787)Peak memory usage: 68 MB % 206.41/29.40 % (372787)Instructions burned: 8173 (million) % 206.41/29.40 % (372801)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=36168697:i=14134_2877 on theBenchmark for (2877ds/14134Mi) % 206.41/29.40 % (372795)Instruction limit reached! % 206.41/29.40 % (372795)------------------------------ % 206.41/29.40 % (372795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 206.41/29.40 % (372795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.41/29.40 % (372795)CaDiCaL version: 2.1.3 % 206.41/29.40 % (372795)Termination reason: Instruction limit % 206.41/29.40 % (372795)Termination phase: Saturation % 206.41/29.40 % (372795)Time elapsed: 4.950 s % 206.41/29.40 % (372795)Peak memory usage: 66 MB % 206.41/29.40 % (372795)Instructions burned: 11406 (million) % 206.41/29.40 % (372957)dis+33_16_sil=32000:sac=on:random_seed=2337896073:i=15851:nm=0_2858 on theBenchmark for (2858ds/15851Mi) % 233.09/33.17 % (372785)Instruction limit reached! % 233.09/33.17 % (372785)------------------------------ % 233.09/33.17 % (372785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.09/33.17 % (372785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.09/33.17 % (372785)CaDiCaL version: 2.1.3 % 233.09/33.17 % (372785)Termination reason: Instruction limit % 233.09/33.17 % (372785)Termination phase: Saturation % 233.09/33.17 % (372785)Time elapsed: 11.519 s % 233.09/33.17 % (372785)Peak memory usage: 75 MB % 233.09/33.17 % (372785)Instructions burned: 22568 (million) % 233.09/33.17 % (372960)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2436311877:avsq=on:i=17627:add=on:amm=off_2840 on theBenchmark for (2840ds/17627Mi) % 233.09/33.17 % (372791)Instruction limit reached! % 233.09/33.17 % (372791)------------------------------ % 233.09/33.17 % (372791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.09/33.17 % (372791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.09/33.17 % (372791)CaDiCaL version: 2.1.3 % 233.09/33.17 % (372791)Termination reason: Instruction limit % 233.09/33.17 % (372791)Termination phase: Saturation % 233.09/33.17 % (372791)Time elapsed: 7.365 s % 233.09/33.17 % (372791)Peak memory usage: 14 MB % 233.09/33.17 % (372791)Instructions burned: 20139 (million) % 233.09/33.17 % (372962)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2960695115:s2a=on:i=53295_2837 on theBenchmark for (2837ds/53295Mi) % 233.09/33.17 % (372773)Instruction limit reached! % 233.09/33.17 % (372773)------------------------------ % 233.09/33.17 % (372773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.09/33.17 % (372773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.09/33.17 % (372773)CaDiCaL version: 2.1.3 % 233.09/33.17 % (372773)Termination reason: Instruction limit % 233.09/33.17 % (372773)Termination phase: Saturation % 233.09/33.17 % (372773)Time elapsed: 12.795 s % 233.09/33.17 % (372773)Peak memory usage: 13 MB % 233.09/33.17 % (372773)Instructions burned: 29343 (million) % 233.09/33.17 % (372964)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2451292324:i=26857:ins=20_2836 on theBenchmark for (2836ds/26857Mi) % 233.09/33.17 % Exception at run slice level % 233.09/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.09/33.17 % (372966)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1628280509:i=28120:bs=on:fsr=off_2835 on theBenchmark for (2835ds/28120Mi) % 233.09/33.17 % (372801)Instruction limit reached! % 233.09/33.17 % (372801)------------------------------ % 233.09/33.17 % (372801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 233.09/33.17 % (372801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.09/33.17 % (372801)CaDiCaL version: 2.1.3 % 233.09/33.17 % (372801)Termination reason: Instruction limit % 233.09/33.17 % (372801)Termination phase: Saturation % 233.09/33.17 % (372801)Time elapsed: 4.175 s % 233.09/33.17 % (372801)Peak memory usage: 13 MB % 233.09/33.17 % (372801)Instructions burned: 14136 (million) % 233.09/33.17 % (372968)fmb+10_1_sil=256000:fmbss=7:random_seed=364733914:fmbsr=1.6:i=182295_2835 on theBenchmark for (2835ds/182295Mi) % 233.09/33.17 % Exception at run slice level % 233.09/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.09/33.17 % (372970)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=663044520:i=44625:gsp=on_2835 on theBenchmark for (2835ds/44625Mi) % 233.09/33.17 % (372970)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 233.09/33.17 % Exception at run slice level % 233.09/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.09/33.17 % (372972)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3731768521:i=160505_2834 on theBenchmark for (2834ds/160505Mi) % 233.09/33.17 % Exception at run slice level % 233.09/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.09/33.17 % (372974)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2972996194:fmbsr=1.3:i=225729_2834 on theBenchmark for (2834ds/225729Mi) % 233.09/33.17 % Exception at run slice level % 233.09/33.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 233.09/33.17 % (372976)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2855786277:fmbsr=2:i=185024:ins=7_2834 on theBenchmark for (2834ds/185024Mi) % 282.15/40.06 % Exception at run slice level % 282.15/40.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 282.15/40.06 % (372978)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2317552741:rtra=on_2833 on theBenchmark for (2833ds/0Mi) % 282.15/40.06 % Exception at run slice level % 282.15/40.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 282.15/40.06 % (372980)% WARNING: option uhcvi not known. % 282.15/40.06 % (372980)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2478753372:i=271062:add=off:rtra=on:rawr=on_2833 on theBenchmark for (2833ds/271062Mi) % 282.15/40.06 % (372957)Instruction limit reached! % 282.15/40.06 % (372957)------------------------------ % 282.15/40.06 % (372957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.15/40.06 % (372957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.15/40.06 % (372957)CaDiCaL version: 2.1.3 % 282.15/40.06 % (372957)Termination reason: Instruction limit % 282.15/40.06 % (372957)Termination phase: Saturation % 282.15/40.06 % (372957)Time elapsed: 4.397 s % 282.15/40.06 % (372957)Peak memory usage: 58 MB % 282.15/40.06 % (372957)Instructions burned: 15855 (million) % 282.15/40.06 % (372982)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2716222422:i=176048:add=on:rtra=on:rawr=on_2814 on theBenchmark for (2814ds/176048Mi) % 282.15/40.06 % (372960)Instruction limit reached! % 282.15/40.06 % (372960)------------------------------ % 282.15/40.06 % (372960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.15/40.06 % (372960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.15/40.06 % (372960)CaDiCaL version: 2.1.3 % 282.15/40.06 % (372960)Termination reason: Instruction limit % 282.15/40.06 % (372960)Termination phase: Saturation % 282.15/40.06 % (372960)Time elapsed: 12.457 s % 282.15/40.06 % (372960)Peak memory usage: 442 MB % 282.15/40.06 % (372960)Instructions burned: 17628 (million) % 282.15/40.06 % (372984)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1065164884:i=206:fgj=on:rtra=on_2715 on theBenchmark for (2715ds/206Mi) % 282.15/40.06 % (372984)Instruction limit reached! % 282.15/40.06 % (372984)------------------------------ % 282.15/40.06 % (372984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.15/40.06 % (372984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.15/40.06 % (372984)CaDiCaL version: 2.1.3 % 282.15/40.06 % (372984)Termination reason: Instruction limit % 282.15/40.06 % (372984)Termination phase: Saturation % 282.15/40.06 % (372984)Time elapsed: 0.125 s % 282.15/40.06 % (372984)Peak memory usage: 13 MB % 282.15/40.06 % (372984)Instructions burned: 206 (million) % 282.15/40.06 % (372987)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1772610395:i=232:rtra=on_2713 on theBenchmark for (2713ds/232Mi) % 282.15/40.06 % (372987)Instruction limit reached! % 282.15/40.06 % (372987)------------------------------ % 282.15/40.06 % (372987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.15/40.06 % (372987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.15/40.06 % (372987)CaDiCaL version: 2.1.3 % 282.15/40.06 % (372987)Termination reason: Instruction limit % 282.15/40.06 % (372987)Termination phase: Saturation % 282.15/40.06 % (372987)Time elapsed: 0.132 s % 282.15/40.06 % (372987)Peak memory usage: 14 MB % 282.15/40.06 % (372987)Instructions burned: 233 (million) % 282.15/40.06 % (373028)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=759335686:i=262:rtra=on_2712 on theBenchmark for (2712ds/262Mi) % 282.15/40.06 % (373028)Instruction limit reached! % 282.15/40.06 % (373028)------------------------------ % 282.15/40.06 % (373028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 282.15/40.06 % (373028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.15/40.06 % (373028)CaDiCaL version: 2.1.3 % 282.15/40.06 % (373028)Termination reason: Instruction limit % 282.15/40.06 % (373028)Termination phase: Saturation % 282.15/40.06 % (373028)Time elapsed: 0.166 s % 282.15/40.06 % (373028)Peak memory usage: 14 MB % 282.15/40.06 % (373028)Instructions burned: 263 (million) % 282.15/40.06 % (373102)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=117379320:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2710 on theBenchmark for (2710ds/318Mi) % 282.15/40.06 % (373102)Instruction limit reached! % 282.15/40.06 % (373102)------------------------------ % 282.15/40.06 % (373102)Terminated % 300.12/42.63 % Vampire exiting %------------------------------------------------------------------------------