%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW505_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n018.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:21 PM UTC 2026 % Result : Timeout 300.53s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW505_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n018.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:17:40 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.08/0.22 Running first-order model finding % 0.08/0.22 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 % 7.93/1.45 % (3412624)Will run a generic schedule for satisfiability detection. % 7.93/1.45 % (3412643)dis+10_1_sil=32000:sp=arity:random_seed=431366952:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.93/1.45 % (3412641)% WARNING: option uhcvi not known. % 7.93/1.45 % (3412640)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1086128444_2999 on theBenchmark for (2999ds/0Mi) % 7.93/1.45 % (3412642)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3913011591:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.93/1.45 % (3412644)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=220622013:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.93/1.45 % (3412641)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=218380554:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.93/1.45 % (3412647)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1958899766:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.93/1.45 % (3412645)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3055630015:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.93/1.45 % Exception at run slice level % 7.93/1.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.93/1.45 % (3412664)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2320674949:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.93/1.45 % (3412643)Instruction limit reached! % 7.93/1.45 % (3412643)------------------------------ % 7.93/1.45 % (3412643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.45 % (3412643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.45 % (3412643)CaDiCaL version: 2.1.3 % 7.93/1.45 % (3412643)Termination reason: Instruction limit % 7.93/1.45 % (3412643)Termination phase: Saturation % 7.93/1.45 % (3412643)Time elapsed: 0.036 s % 7.93/1.45 % (3412643)Peak memory usage: 12 MB % 7.93/1.45 % (3412643)Instructions burned: 104 (million) % 7.93/1.45 % Exception at run slice level % 7.93/1.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.93/1.45 % (3412671)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1069552480:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.93/1.45 % (3412672)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=3484990392:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.93/1.45 % (3412644)Instruction limit reached! % 7.93/1.45 % (3412644)------------------------------ % 7.93/1.45 % (3412644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.45 % (3412644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.45 % (3412644)CaDiCaL version: 2.1.3 % 7.93/1.45 % (3412644)Termination reason: Instruction limit % 7.93/1.45 % (3412644)Termination phase: Saturation % 7.93/1.45 % (3412644)Time elapsed: 0.074 s % 7.93/1.45 % (3412644)Peak memory usage: 13 MB % 7.93/1.45 % (3412644)Instructions burned: 119 (million) % 7.93/1.45 % (3412645)Instruction limit reached! % 7.93/1.45 % (3412645)------------------------------ % 7.93/1.45 % (3412645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.45 % (3412645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.45 % (3412645)CaDiCaL version: 2.1.3 % 7.93/1.45 % (3412645)Termination reason: Instruction limit % 7.93/1.45 % (3412645)Termination phase: Saturation % 7.93/1.45 % (3412645)Time elapsed: 0.074 s % 7.93/1.45 % (3412645)Peak memory usage: 12 MB % 7.93/1.45 % (3412645)Instructions burned: 136 (million) % 7.93/1.45 % (3412671)Instruction limit reached! % 7.93/1.45 % (3412671)------------------------------ % 7.93/1.45 % (3412671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.93/1.45 % (3412671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.93/1.45 % (3412671)CaDiCaL version: 2.1.3 % 7.93/1.45 % (3412671)Termination reason: Instruction limit % 7.93/1.45 % (3412671)Termination phase: Saturation % 7.93/1.45 % (3412671)Time elapsed: 0.053 s % 7.93/1.45 % (3412671)Peak memory usage: 13 MB % 7.93/1.45 % (3412671)Instructions burned: 134 (million) % 7.93/1.45 % (3412677)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2435499060:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 19.95/3.13 % (3412676)ott-21_1_sil=16000:fs=off:random_seed=435810783:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 19.95/3.13 % (3412647)Instruction limit reached! % 19.95/3.13 % (3412647)------------------------------ % 19.95/3.13 % (3412647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.13 % (3412647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.13 % (3412647)CaDiCaL version: 2.1.3 % 19.95/3.13 % (3412647)Termination reason: Instruction limit % 19.95/3.13 % (3412647)Termination phase: Saturation % 19.95/3.13 % (3412647)Time elapsed: 0.101 s % 19.95/3.13 % (3412647)Peak memory usage: 13 MB % 19.95/3.13 % (3412647)Instructions burned: 159 (million) % 19.95/3.13 % (3412678)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1649313994:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.95/3.13 % Exception at run slice level % 19.95/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.95/3.13 % (3412683)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=545965817:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.95/3.13 % Exception at run slice level % 19.95/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.95/3.13 % (3412682)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2043417136:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.95/3.13 % (3412685)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=1407501066:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 19.95/3.13 % (3412676)Instruction limit reached! % 19.95/3.13 % (3412676)------------------------------ % 19.95/3.13 % (3412676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.13 % (3412676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.13 % (3412676)CaDiCaL version: 2.1.3 % 19.95/3.13 % (3412676)Termination reason: Instruction limit % 19.95/3.13 % (3412676)Termination phase: Saturation % 19.95/3.13 % (3412676)Time elapsed: 0.096 s % 19.95/3.13 % (3412676)Peak memory usage: 12 MB % 19.95/3.13 % (3412676)Instructions burned: 181 (million) % 19.95/3.13 % (3412688)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=167381:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.95/3.13 % (3412685)Instruction limit reached! % 19.95/3.13 % (3412685)------------------------------ % 19.95/3.13 % (3412685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.13 % (3412685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.13 % (3412685)CaDiCaL version: 2.1.3 % 19.95/3.13 % (3412685)Termination reason: Instruction limit % 19.95/3.13 % (3412685)Termination phase: Saturation % 19.95/3.13 % (3412685)Time elapsed: 0.214 s % 19.95/3.13 % (3412685)Peak memory usage: 20 MB % 19.95/3.13 % (3412685)Instructions burned: 696 (million) % 19.95/3.13 % (3412677)Instruction limit reached! % 19.95/3.13 % (3412677)------------------------------ % 19.95/3.13 % (3412677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.95/3.13 % (3412677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.95/3.13 % (3412677)CaDiCaL version: 2.1.3 % 19.95/3.13 % (3412677)Termination reason: Instruction limit % 19.95/3.13 % (3412677)Termination phase: Saturation % 19.95/3.13 % (3412677)Time elapsed: 0.250 s % 19.95/3.13 % (3412677)Peak memory usage: 15 MB % 19.95/3.13 % (3412677)Instructions burned: 478 (million) % 19.95/3.13 % (3412690)fmb+10_1_sil=64000:random_seed=1694917294:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 19.95/3.13 % (3412690)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.95/3.13 % Exception at run slice level % 19.95/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.95/3.13 % (3412691)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1795593941:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 19.95/3.13 % (3412693)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4236999378:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 19.95/3.13 % Exception at run slice level % 19.95/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.95/3.13 % Exception at run slice level % 19.95/3.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.34/10.70 % (3412696)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3678821461:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 74.34/10.70 % (3412697)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2371746334:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 74.34/10.70 % (3412697)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 74.34/10.70 % (3412672)Instruction limit reached! % 74.34/10.70 % (3412672)------------------------------ % 74.34/10.70 % (3412672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.34/10.70 % (3412672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.34/10.70 % (3412672)CaDiCaL version: 2.1.3 % 74.34/10.70 % (3412672)Termination reason: Instruction limit % 74.34/10.70 % (3412672)Termination phase: Saturation % 74.34/10.70 % (3412672)Time elapsed: 0.370 s % 74.34/10.70 % (3412672)Peak memory usage: 18 MB % 74.34/10.70 % (3412672)Instructions burned: 684 (million) % 74.34/10.70 % (3412700)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=356600008:i=6324_2995 on theBenchmark for (2995ds/6324Mi) % 74.34/10.70 % Exception at run slice level % 74.34/10.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.34/10.70 % (3412702)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=700628950:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi) % 74.34/10.70 % Exception at run slice level % 74.34/10.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.34/10.70 % (3412704)ott-2_1_sil=16000:newcnf=on:random_seed=2054522064:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi) % 74.34/10.70 % (3412688)Instruction limit reached! % 74.34/10.70 % (3412688)------------------------------ % 74.34/10.70 % (3412688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.34/10.70 % (3412688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.34/10.70 % (3412688)CaDiCaL version: 2.1.3 % 74.34/10.70 % (3412688)Termination reason: Instruction limit % 74.34/10.70 % (3412688)Termination phase: Saturation % 74.34/10.70 % (3412688)Time elapsed: 0.501 s % 74.34/10.70 % (3412688)Peak memory usage: 19 MB % 74.34/10.70 % (3412688)Instructions burned: 880 (million) % 74.34/10.70 % (3412706)ott+10_1_sil=32000:tgt=ground:random_seed=3617790737:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 74.34/10.70 % (3412682)Instruction limit reached! % 74.34/10.70 % (3412682)------------------------------ % 74.34/10.70 % (3412682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.34/10.70 % (3412682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.34/10.70 % (3412682)CaDiCaL version: 2.1.3 % 74.34/10.70 % (3412682)Termination reason: Instruction limit % 74.34/10.70 % (3412682)Termination phase: Saturation % 74.34/10.70 % (3412682)Time elapsed: 0.727 s % 74.34/10.70 % (3412682)Peak memory usage: 22 MB % 74.34/10.70 % (3412682)Instructions burned: 1180 (million) % 74.34/10.70 % (3412708)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2402700352:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 74.34/10.70 % Exception at run slice level % 74.34/10.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 74.34/10.70 % (3412710)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3508123117:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi) % 74.34/10.70 % (3412704)Instruction limit reached! % 74.34/10.70 % (3412704)------------------------------ % 74.34/10.70 % (3412704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 74.34/10.70 % (3412704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.34/10.70 % (3412704)CaDiCaL version: 2.1.3 % 74.34/10.70 % (3412704)Termination reason: Instruction limit % 74.34/10.70 % (3412704)Termination phase: Saturation % 74.34/10.70 % (3412704)Time elapsed: 0.523 s % 74.34/10.70 % (3412704)Peak memory usage: 20 MB % 74.34/10.70 % (3412704)Instructions burned: 869 (million) % 74.34/10.70 % (3412712)dis+21_1_sil=32000:sas=cadical:random_seed=4049011811:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 74.34/10.70 % (3412697)Instruction limit reached! % 74.34/10.70 % (3412697)------------------------------ % 74.34/10.70 % (3412697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.64/16.44 % (3412697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.64/16.44 % (3412697)CaDiCaL version: 2.1.3 % 114.64/16.44 % (3412697)Termination reason: Instruction limit % 114.64/16.44 % (3412697)Termination phase: Saturation % 114.64/16.44 % (3412697)Time elapsed: 0.808 s % 114.64/16.44 % (3412697)Peak memory usage: 20 MB % 114.64/16.44 % (3412697)Instructions burned: 1473 (million) % 114.64/16.44 % (3412714)ott+11_1_sil=16000:gs=on:random_seed=3097262916:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 114.64/16.44 % (3412696)Instruction limit reached! % 114.64/16.44 % (3412696)------------------------------ % 114.64/16.44 % (3412696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.64/16.44 % (3412696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.64/16.44 % (3412696)CaDiCaL version: 2.1.3 % 114.64/16.44 % (3412696)Termination reason: Instruction limit % 114.64/16.44 % (3412696)Termination phase: Saturation % 114.64/16.44 % (3412696)Time elapsed: 1.404 s % 114.64/16.44 % (3412696)Peak memory usage: 31 MB % 114.64/16.44 % (3412696)Instructions burned: 5133 (million) % 114.64/16.44 % (3412716)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=777299482:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 114.64/16.44 % Exception at run slice level % 114.64/16.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.64/16.44 % (3412718)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3499661413:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 114.64/16.44 % (3412714)Instruction limit reached! % 114.64/16.44 % (3412714)------------------------------ % 114.64/16.44 % (3412714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.64/16.44 % (3412714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.64/16.44 % (3412714)CaDiCaL version: 2.1.3 % 114.64/16.44 % (3412714)Termination reason: Instruction limit % 114.64/16.44 % (3412714)Termination phase: Saturation % 114.64/16.44 % (3412714)Time elapsed: 1.185 s % 114.64/16.44 % (3412714)Peak memory usage: 26 MB % 114.64/16.44 % (3412714)Instructions burned: 2252 (million) % 114.64/16.44 % (3412720)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=640367622:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 114.64/16.44 % (3412718)Instruction limit reached! % 114.64/16.44 % (3412718)------------------------------ % 114.64/16.44 % (3412718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.64/16.44 % (3412718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.64/16.44 % (3412718)CaDiCaL version: 2.1.3 % 114.64/16.44 % (3412718)Termination reason: Instruction limit % 114.64/16.44 % (3412718)Termination phase: Saturation % 114.64/16.44 % (3412718)Time elapsed: 0.970 s % 114.64/16.44 % (3412718)Peak memory usage: 24 MB % 114.64/16.44 % (3412718)Instructions burned: 4592 (million) % 114.64/16.44 % (3412722)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=165431665:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 114.64/16.44 % (3412710)Instruction limit reached! % 114.64/16.44 % (3412710)------------------------------ % 114.64/16.44 % (3412710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 114.64/16.44 % (3412710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.64/16.44 % (3412710)CaDiCaL version: 2.1.3 % 114.64/16.44 % (3412710)Termination reason: Instruction limit % 114.64/16.44 % (3412710)Termination phase: Saturation % 114.64/16.44 % (3412710)Time elapsed: 1.907 s % 114.64/16.44 % (3412710)Peak memory usage: 28 MB % 114.64/16.44 % (3412710)Instructions burned: 3512 (million) % 114.64/16.44 % (3412724)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3380929811:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi) % 114.64/16.44 % Exception at run slice level % 114.64/16.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.64/16.44 % (3412726)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2873016543:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi) % 114.64/16.44 % Exception at run slice level % 114.64/16.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 114.64/16.44 % (3412728)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3932261765:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 114.64/16.44 % Exception at run slice level % 158.00/22.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 158.00/22.52 % (3412730)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4259104989:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi) % 158.00/22.52 % (3412712)Instruction limit reached! % 158.00/22.52 % (3412712)------------------------------ % 158.00/22.52 % (3412712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.00/22.52 % (3412712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.00/22.52 % (3412712)CaDiCaL version: 2.1.3 % 158.00/22.52 % (3412712)Termination reason: Instruction limit % 158.00/22.52 % (3412712)Termination phase: Saturation % 158.00/22.52 % (3412712)Time elapsed: 2.154 s % 158.00/22.52 % (3412712)Peak memory usage: 39 MB % 158.00/22.52 % (3412712)Instructions burned: 3773 (million) % 158.00/22.52 % (3412733)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2058918376:i=8173:av=off_2967 on theBenchmark for (2967ds/8173Mi) % 158.00/22.52 % (3412706)Instruction limit reached! % 158.00/22.52 % (3412706)------------------------------ % 158.00/22.52 % (3412706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.00/22.52 % (3412706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.00/22.52 % (3412706)CaDiCaL version: 2.1.3 % 158.00/22.52 % (3412706)Termination reason: Instruction limit % 158.00/22.52 % (3412706)Termination phase: Saturation % 158.00/22.52 % (3412706)Time elapsed: 3.196 s % 158.00/22.52 % (3412706)Peak memory usage: 58 MB % 158.00/22.52 % (3412706)Instructions burned: 5114 (million) % 158.00/22.52 % (3412735)dis+10_16:1_sil=16000:random_seed=3005768026:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi) % 158.00/22.52 % (3412722)Instruction limit reached! % 158.00/22.52 % (3412722)------------------------------ % 158.00/22.52 % (3412722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.00/22.52 % (3412722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.00/22.52 % (3412722)CaDiCaL version: 2.1.3 % 158.00/22.52 % (3412722)Termination reason: Instruction limit % 158.00/22.52 % (3412722)Termination phase: Saturation % 158.00/22.52 % (3412722)Time elapsed: 1.348 s % 158.00/22.52 % (3412722)Peak memory usage: 32 MB % 158.00/22.52 % (3412722)Instructions burned: 5212 (million) % 158.00/22.52 % (3412737)ott-3_8_sil=64000:random_seed=1010060596:i=20139:bs=on_2958 on theBenchmark for (2958ds/20139Mi) % 158.00/22.52 % (3412733)Instruction limit reached! % 158.00/22.52 % (3412733)------------------------------ % 158.00/22.52 % (3412733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.00/22.52 % (3412733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.00/22.52 % (3412733)CaDiCaL version: 2.1.3 % 158.00/22.52 % (3412733)Termination reason: Instruction limit % 158.00/22.52 % (3412733)Termination phase: Saturation % 158.00/22.52 % (3412733)Time elapsed: 4.523 s % 158.00/22.52 % (3412733)Peak memory usage: 86 MB % 158.00/22.52 % (3412733)Instructions burned: 8174 (million) % 158.00/22.52 % (3412739)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4021449829:fmbsr=2:i=32576_2922 on theBenchmark for (2922ds/32576Mi) % 158.00/22.52 % Exception at run slice level % 158.00/22.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 158.00/22.52 % (3412741)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=465366874:i=11404_2922 on theBenchmark for (2922ds/11404Mi) % 158.00/22.52 % (3412735)Instruction limit reached! % 158.00/22.52 % (3412735)------------------------------ % 158.00/22.52 % (3412735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.00/22.52 % (3412735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.00/22.52 % (3412735)CaDiCaL version: 2.1.3 % 158.00/22.52 % (3412735)Termination reason: Instruction limit % 158.00/22.52 % (3412735)Termination phase: Saturation % 158.00/22.52 % (3412735)Time elapsed: 4.820 s % 158.00/22.52 % (3412735)Peak memory usage: 57 MB % 158.00/22.52 % (3412735)Instructions burned: 9157 (million) % 158.00/22.52 % (3412743)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3878669225:i=14134_2911 on theBenchmark for (2911ds/14134Mi) % 158.00/22.52 % (3412737)Instruction limit reached! % 158.00/22.52 % (3412737)------------------------------ % 158.00/22.52 % (3412737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.00/22.52 % (3412737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.00/22.52 % (3412737)CaDiCaL version: 2.1.3 % 181.01/25.78 % (3412737)Termination reason: Instruction limit % 181.01/25.78 % (3412737)Termination phase: Saturation % 181.01/25.78 % (3412737)Time elapsed: 6.293 s % 181.01/25.78 % (3412737)Peak memory usage: 42 MB % 181.01/25.78 % (3412737)Instructions burned: 20142 (million) % 181.01/25.78 % (3412745)dis+33_16_sil=32000:sac=on:random_seed=3823187513:i=15851:nm=0_2895 on theBenchmark for (2895ds/15851Mi) % 181.01/25.78 % (3412730)Instruction limit reached! % 181.01/25.78 % (3412730)------------------------------ % 181.01/25.78 % (3412730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.01/25.78 % (3412730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.01/25.78 % (3412730)CaDiCaL version: 2.1.3 % 181.01/25.78 % (3412730)Termination reason: Instruction limit % 181.01/25.78 % (3412730)Termination phase: Saturation % 181.01/25.78 % (3412730)Time elapsed: 9.557 s % 181.01/25.78 % (3412730)Peak memory usage: 62 MB % 181.01/25.78 % (3412730)Instructions burned: 22568 (million) % 181.01/25.78 % (3412747)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3728599162:avsq=on:i=17627:add=on:amm=off_2875 on theBenchmark for (2875ds/17627Mi) % 181.01/25.78 % (3412745)Instruction limit reached! % 181.01/25.78 % (3412745)------------------------------ % 181.01/25.78 % (3412745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.01/25.78 % (3412745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.01/25.78 % (3412745)CaDiCaL version: 2.1.3 % 181.01/25.78 % (3412745)Termination reason: Instruction limit % 181.01/25.78 % (3412745)Termination phase: Saturation % 181.01/25.78 % (3412745)Time elapsed: 3.834 s % 181.01/25.78 % (3412745)Peak memory usage: 138 MB % 181.01/25.78 % (3412745)Instructions burned: 15856 (million) % 181.01/25.78 % (3412865)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=163715510:s2a=on:i=53295_2856 on theBenchmark for (2856ds/53295Mi) % 181.01/25.78 % (3412741)Instruction limit reached! % 181.01/25.78 % (3412741)------------------------------ % 181.01/25.78 % (3412741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.01/25.78 % (3412741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.01/25.78 % (3412741)CaDiCaL version: 2.1.3 % 181.01/25.78 % (3412741)Termination reason: Instruction limit % 181.01/25.78 % (3412741)Termination phase: Saturation % 181.01/25.78 % (3412741)Time elapsed: 8.119 s % 181.01/25.78 % (3412741)Peak memory usage: 117 MB % 181.01/25.78 % (3412741)Instructions burned: 11404 (million) % 181.01/25.78 % (3413049)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1907007980:i=26857:ins=20_2840 on theBenchmark for (2840ds/26857Mi) % 181.01/25.78 % (3412720)Instruction limit reached! % 181.01/25.78 % (3412720)------------------------------ % 181.01/25.78 % (3412720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 181.01/25.78 % (3412720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.01/25.78 % (3412720)CaDiCaL version: 2.1.3 % 181.01/25.78 % (3412720)Termination reason: Instruction limit % 181.01/25.78 % (3412720)Termination phase: Saturation % 181.01/25.78 % (3412720)Time elapsed: 13.526 s % 181.01/25.78 % (3412720)Peak memory usage: 258 MB % 181.01/25.78 % (3412720)Instructions burned: 29340 (million) % 181.01/25.78 % Exception at run slice level % 181.01/25.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.01/25.78 % (3413051)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=313509712:i=28120:bs=on:fsr=off_2840 on theBenchmark for (2840ds/28120Mi) % 181.01/25.78 % (3413053)fmb+10_1_sil=256000:fmbss=7:random_seed=187149726:fmbsr=1.6:i=182295_2839 on theBenchmark for (2839ds/182295Mi) % 181.01/25.78 % Exception at run slice level % 181.01/25.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.01/25.78 % (3413056)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4036916661:i=44625:gsp=on_2839 on theBenchmark for (2839ds/44625Mi) % 181.01/25.78 % (3413056)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 181.01/25.78 % Exception at run slice level % 181.01/25.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.01/25.78 % (3413060)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3146324309:i=160505_2838 on theBenchmark for (2838ds/160505Mi) % 181.01/25.78 % Exception at run slice level % 181.01/25.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 181.01/25.78 % (3413063)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=272538212:fmbsr=1.3:i=225729_2838 on theBenchmark for (2838ds/225729Mi) % 255.71/36.23 % Exception at run slice level % 255.71/36.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.71/36.23 % (3413065)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3252416970:fmbsr=2:i=185024:ins=7_2837 on theBenchmark for (2837ds/185024Mi) % 255.71/36.23 % Exception at run slice level % 255.71/36.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.71/36.23 % (3413067)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=981243691:rtra=on_2837 on theBenchmark for (2837ds/0Mi) % 255.71/36.23 % Exception at run slice level % 255.71/36.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 255.71/36.23 % (3413069)% WARNING: option uhcvi not known. % 255.71/36.23 % (3413069)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3270364362:i=271062:add=off:rtra=on:rawr=on_2837 on theBenchmark for (2837ds/271062Mi) % 255.71/36.23 % (3412743)Instruction limit reached! % 255.71/36.23 % (3412743)------------------------------ % 255.71/36.23 % (3412743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.71/36.23 % (3412743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.71/36.23 % (3412743)CaDiCaL version: 2.1.3 % 255.71/36.23 % (3412743)Termination reason: Instruction limit % 255.71/36.23 % (3412743)Termination phase: Saturation % 255.71/36.23 % (3412743)Time elapsed: 10.951 s % 255.71/36.23 % (3412743)Peak memory usage: 96 MB % 255.71/36.23 % (3412743)Instructions burned: 14134 (million) % 255.71/36.23 % (3413083)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3167403712:i=176048:add=on:rtra=on:rawr=on_2801 on theBenchmark for (2801ds/176048Mi) % 255.71/36.23 % (3412747)Instruction limit reached! % 255.71/36.23 % (3412747)------------------------------ % 255.71/36.23 % (3412747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.71/36.23 % (3412747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.71/36.23 % (3412747)CaDiCaL version: 2.1.3 % 255.71/36.23 % (3412747)Termination reason: Instruction limit % 255.71/36.23 % (3412747)Termination phase: Saturation % 255.71/36.23 % (3412747)Time elapsed: 8.989 s % 255.71/36.23 % (3412747)Peak memory usage: 56 MB % 255.71/36.23 % (3412747)Instructions burned: 17627 (million) % 255.71/36.23 % (3413097)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1388021037:i=206:fgj=on:rtra=on_2784 on theBenchmark for (2784ds/206Mi) % 255.71/36.23 % (3413097)Instruction limit reached! % 255.71/36.23 % (3413097)------------------------------ % 255.71/36.23 % (3413097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.71/36.23 % (3413097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.71/36.23 % (3413097)CaDiCaL version: 2.1.3 % 255.71/36.23 % (3413097)Termination reason: Instruction limit % 255.71/36.23 % (3413097)Termination phase: Saturation % 255.71/36.23 % (3413097)Time elapsed: 0.191 s % 255.71/36.23 % (3413097)Peak memory usage: 14 MB % 255.71/36.23 % (3413097)Instructions burned: 206 (million) % 255.71/36.23 % (3413099)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=4154758840:i=232:rtra=on_2782 on theBenchmark for (2782ds/232Mi) % 255.71/36.23 % (3413099)Instruction limit reached! % 255.71/36.23 % (3413099)------------------------------ % 255.71/36.23 % (3413099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.71/36.23 % (3413099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.71/36.23 % (3413099)CaDiCaL version: 2.1.3 % 255.71/36.23 % (3413099)Termination reason: Instruction limit % 255.71/36.23 % (3413099)Termination phase: Saturation % 255.71/36.23 % (3413099)Time elapsed: 0.237 s % 255.71/36.23 % (3413099)Peak memory usage: 14 MB % 255.71/36.23 % (3413099)Instructions burned: 233 (million) % 255.71/36.23 % (3413101)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3037453449:i=262:rtra=on_2779 on theBenchmark for (2779ds/262Mi) % 255.71/36.23 % (3413101)Instruction limit reached! % 255.71/36.23 % (3413101)------------------------------ % 255.71/36.23 % (3413101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 255.71/36.23 % (3413101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.71/36.23 % (3413101)CaDiCaL version: 2.1.3 % 255.71/36.23 % (3413101)Termination reason: Instruction limit % 255.71/36.23 % (3413101)Termination phase: SaturatTerminated % 300.53/42.54 % Vampire exiting % 300.53/42.54 Terminated %------------------------------------------------------------------------------