%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW532_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 : n009.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:24 PM UTC 2026 % Result : Timeout 300.51s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW532_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.09/0.20 % Computer : n009.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 14:17:45 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 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.75/1.41 % (3053434)Will run a generic schedule for satisfiability detection. % 7.75/1.41 % (3053439)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=997200693_2999 on theBenchmark for (2999ds/0Mi) % 7.75/1.41 % Exception at run slice level % 7.75/1.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.75/1.41 % (3053440)% WARNING: option uhcvi not known. % 7.75/1.41 % (3053440)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1625834667:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.75/1.41 % (3053441)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4066692103:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.75/1.41 % (3053442)dis+10_1_sil=32000:sp=arity:random_seed=3004188798:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.75/1.41 % (3053443)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3593923028:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.75/1.41 % (3053444)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2574708187:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.75/1.41 % (3053445)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1111366716:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.75/1.41 % (3053447)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2817287056:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.75/1.41 % Exception at run slice level % 7.75/1.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.75/1.41 % (3053455)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=253588218:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.75/1.41 % (3053455)Instruction limit reached! % 7.75/1.41 % (3053455)------------------------------ % 7.75/1.41 % (3053455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.75/1.41 % (3053455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.41 % (3053455)CaDiCaL version: 2.1.3 % 7.75/1.41 % (3053455)Termination reason: Instruction limit % 7.75/1.41 % (3053455)Termination phase: Saturation % 7.75/1.41 % (3053455)Time elapsed: 0.043 s % 7.75/1.41 % (3053455)Peak memory usage: 13 MB % 7.75/1.41 % (3053455)Instructions burned: 131 (million) % 7.75/1.41 % (3053442)Instruction limit reached! % 7.75/1.41 % (3053442)------------------------------ % 7.75/1.41 % (3053442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.75/1.41 % (3053442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.41 % (3053442)CaDiCaL version: 2.1.3 % 7.75/1.41 % (3053442)Termination reason: Instruction limit % 7.75/1.41 % (3053442)Termination phase: Saturation % 7.75/1.41 % (3053442)Time elapsed: 0.061 s % 7.75/1.41 % (3053442)Peak memory usage: 12 MB % 7.75/1.41 % (3053442)Instructions burned: 105 (million) % 7.75/1.41 % (3053443)Instruction limit reached! % 7.75/1.41 % (3053443)------------------------------ % 7.75/1.41 % (3053443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.75/1.41 % (3053443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.41 % (3053443)CaDiCaL version: 2.1.3 % 7.75/1.41 % (3053443)Termination reason: Instruction limit % 7.75/1.41 % (3053443)Termination phase: Saturation % 7.75/1.41 % (3053443)Time elapsed: 0.068 s % 7.75/1.41 % (3053443)Peak memory usage: 13 MB % 7.75/1.41 % (3053443)Instructions burned: 116 (million) % 7.75/1.41 % (3053457)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=1153732231:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 7.75/1.41 % (3053458)ott-21_1_sil=16000:fs=off:random_seed=1802166615:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 7.75/1.41 % (3053444)Instruction limit reached! % 7.75/1.41 % (3053444)------------------------------ % 7.75/1.41 % (3053444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.75/1.41 % (3053444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.75/1.41 % (3053444)CaDiCaL version: 2.1.3 % 7.75/1.41 % (3053444)Termination reason: Instruction limit % 7.75/1.41 % (3053444)Termination phase: Saturation % 7.75/1.41 % (3053444)Time elapsed: 0.083 s % 7.75/1.41 % (3053444)Peak memory usage: 12 MB % 7.75/1.41 % (3053444)Instructions burned: 131 (million) % 7.75/1.41 % (3053459)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3964912619:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 18.30/3.01 % (3053445)Instruction limit reached! % 18.30/3.01 % (3053445)------------------------------ % 18.30/3.01 % (3053445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.30/3.01 % (3053445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.01 % (3053445)CaDiCaL version: 2.1.3 % 18.30/3.01 % (3053445)Termination reason: Instruction limit % 18.30/3.01 % (3053445)Termination phase: Saturation % 18.30/3.01 % (3053445)Time elapsed: 0.094 s % 18.30/3.01 % (3053445)Peak memory usage: 12 MB % 18.30/3.01 % (3053445)Instructions burned: 159 (million) % 18.30/3.01 % (3053462)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2332164371:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 18.30/3.01 % Exception at run slice level % 18.30/3.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.30/3.01 % (3053464)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3795660216:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 18.30/3.01 % (3053466)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=320437270:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 18.30/3.01 % Exception at run slice level % 18.30/3.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.30/3.01 % (3053469)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=3239480126: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) % 18.30/3.01 % (3053458)Instruction limit reached! % 18.30/3.01 % (3053458)------------------------------ % 18.30/3.01 % (3053458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.30/3.01 % (3053458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.01 % (3053458)CaDiCaL version: 2.1.3 % 18.30/3.01 % (3053458)Termination reason: Instruction limit % 18.30/3.01 % (3053458)Termination phase: Saturation % 18.30/3.01 % (3053458)Time elapsed: 0.091 s % 18.30/3.01 % (3053458)Peak memory usage: 13 MB % 18.30/3.01 % (3053458)Instructions burned: 182 (million) % 18.30/3.01 % (3053471)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2049235482:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 18.30/3.01 % (3053457)Instruction limit reached! % 18.30/3.01 % (3053457)------------------------------ % 18.30/3.01 % (3053457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.30/3.01 % (3053457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.30/3.01 % (3053457)CaDiCaL version: 2.1.3 % 18.30/3.01 % (3053457)Termination reason: Instruction limit % 18.30/3.01 % (3053457)Termination phase: Saturation % 18.30/3.01 % (3053457)Time elapsed: 0.166 s % 18.30/3.01 % (3053457)Peak memory usage: 14 MB % 18.30/3.01 % (3053457)Instructions burned: 685 (million) % 18.30/3.01 % (3053473)fmb+10_1_sil=64000:random_seed=3487136545:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 18.30/3.01 % (3053473)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.30/3.01 % Exception at run slice level % 18.30/3.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.30/3.01 % (3053475)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1039276047:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 18.30/3.01 % Exception at run slice level % 18.30/3.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.30/3.01 % (3053477)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2790369481:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 18.30/3.01 % Exception at run slice level % 18.30/3.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 18.30/3.01 % (3053479)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3502969935:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 18.30/3.01 % (3053459)Instruction limit reached! % 18.30/3.01 % (3053459)------------------------------ % 18.30/3.01 % (3053459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 18.30/3.01 % (3053459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.21/9.38 % (3053459)CaDiCaL version: 2.1.3 % 64.21/9.38 % (3053459)Termination reason: Instruction limit % 64.21/9.38 % (3053459)Termination phase: Saturation % 64.21/9.38 % (3053459)Time elapsed: 0.288 s % 64.21/9.38 % (3053459)Peak memory usage: 14 MB % 64.21/9.38 % (3053459)Instructions burned: 478 (million) % 64.21/9.38 % (3053481)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2976468753:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 64.21/9.38 % (3053481)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.21/9.38 % (3053469)Instruction limit reached! % 64.21/9.38 % (3053469)------------------------------ % 64.21/9.38 % (3053469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.21/9.38 % (3053469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.21/9.38 % (3053469)CaDiCaL version: 2.1.3 % 64.21/9.38 % (3053469)Termination reason: Instruction limit % 64.21/9.38 % (3053469)Termination phase: Saturation % 64.21/9.38 % (3053469)Time elapsed: 0.412 s % 64.21/9.38 % (3053469)Peak memory usage: 15 MB % 64.21/9.38 % (3053469)Instructions burned: 693 (million) % 64.21/9.38 % (3053483)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=828634180:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 64.21/9.38 % Exception at run slice level % 64.21/9.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.21/9.38 % (3053485)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=839273535:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 64.21/9.38 % Exception at run slice level % 64.21/9.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.21/9.38 % (3053487)ott-2_1_sil=16000:newcnf=on:random_seed=2461065820:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 64.21/9.38 % (3053471)Instruction limit reached! % 64.21/9.38 % (3053471)------------------------------ % 64.21/9.38 % (3053471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.21/9.38 % (3053471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.21/9.38 % (3053471)CaDiCaL version: 2.1.3 % 64.21/9.38 % (3053471)Termination reason: Instruction limit % 64.21/9.38 % (3053471)Termination phase: Saturation % 64.21/9.38 % (3053471)Time elapsed: 0.506 s % 64.21/9.38 % (3053471)Peak memory usage: 19 MB % 64.21/9.38 % (3053471)Instructions burned: 880 (million) % 64.21/9.38 % (3053489)ott+10_1_sil=32000:tgt=ground:random_seed=611983480:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 64.21/9.38 % (3053464)Instruction limit reached! % 64.21/9.38 % (3053464)------------------------------ % 64.21/9.38 % (3053464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.21/9.38 % (3053464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.21/9.38 % (3053464)CaDiCaL version: 2.1.3 % 64.21/9.38 % (3053464)Termination reason: Instruction limit % 64.21/9.38 % (3053464)Termination phase: Saturation % 64.21/9.38 % (3053464)Time elapsed: 0.632 s % 64.21/9.38 % (3053464)Peak memory usage: 17 MB % 64.21/9.38 % (3053464)Instructions burned: 1181 (million) % 64.21/9.38 % (3053491)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3112572476:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 64.21/9.38 % Exception at run slice level % 64.21/9.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.21/9.38 % (3053493)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2498271921:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 64.21/9.38 % (3053487)Instruction limit reached! % 64.21/9.38 % (3053487)------------------------------ % 64.21/9.38 % (3053487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.21/9.38 % (3053487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.21/9.38 % (3053487)CaDiCaL version: 2.1.3 % 64.21/9.38 % (3053487)Termination reason: Instruction limit % 64.21/9.38 % (3053487)Termination phase: Saturation % 64.21/9.38 % (3053487)Time elapsed: 0.464 s % 64.21/9.38 % (3053487)Peak memory usage: 15 MB % 64.21/9.38 % (3053487)Instructions burned: 869 (million) % 64.21/9.38 % (3053495)dis+21_1_sil=32000:sas=cadical:random_seed=342349152:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 64.21/9.38 % (3053481)Instruction limit reached! % 64.21/9.38 % (3053481)------------------------------ % 64.21/9.38 % (3053481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.25/14.49 % (3053481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.25/14.49 % (3053481)CaDiCaL version: 2.1.3 % 100.25/14.49 % (3053481)Termination reason: Instruction limit % 100.25/14.49 % (3053481)Termination phase: Saturation % 100.25/14.49 % (3053481)Time elapsed: 0.725 s % 100.25/14.49 % (3053481)Peak memory usage: 17 MB % 100.25/14.49 % (3053481)Instructions burned: 1473 (million) % 100.25/14.49 % (3053497)ott+11_1_sil=16000:gs=on:random_seed=3371268573:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 100.25/14.49 % (3053479)Instruction limit reached! % 100.25/14.49 % (3053479)------------------------------ % 100.25/14.49 % (3053479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.25/14.49 % (3053479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.25/14.49 % (3053479)CaDiCaL version: 2.1.3 % 100.25/14.49 % (3053479)Termination reason: Instruction limit % 100.25/14.49 % (3053479)Termination phase: Saturation % 100.25/14.49 % (3053479)Time elapsed: 1.312 s % 100.25/14.49 % (3053479)Peak memory usage: 21 MB % 100.25/14.49 % (3053479)Instructions burned: 5132 (million) % 100.25/14.49 % (3053499)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2650273840:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 100.25/14.49 % Exception at run slice level % 100.25/14.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.25/14.49 % (3053501)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=970287478:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 100.25/14.49 % (3053497)Instruction limit reached! % 100.25/14.49 % (3053497)------------------------------ % 100.25/14.49 % (3053497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.25/14.49 % (3053497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.25/14.49 % (3053497)CaDiCaL version: 2.1.3 % 100.25/14.49 % (3053497)Termination reason: Instruction limit % 100.25/14.49 % (3053497)Termination phase: Saturation % 100.25/14.49 % (3053497)Time elapsed: 1.080 s % 100.25/14.49 % (3053497)Peak memory usage: 18 MB % 100.25/14.49 % (3053497)Instructions burned: 2252 (million) % 100.25/14.49 % (3053503)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2584375882:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 100.25/14.49 % (3053493)Instruction limit reached! % 100.25/14.49 % (3053493)------------------------------ % 100.25/14.49 % (3053493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.25/14.49 % (3053493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.25/14.49 % (3053493)CaDiCaL version: 2.1.3 % 100.25/14.49 % (3053493)Termination reason: Instruction limit % 100.25/14.49 % (3053493)Termination phase: Saturation % 100.25/14.49 % (3053493)Time elapsed: 1.711 s % 100.25/14.49 % (3053493)Peak memory usage: 21 MB % 100.25/14.49 % (3053493)Instructions burned: 3513 (million) % 100.25/14.49 % (3053505)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=218166317:i=5211_2974 on theBenchmark for (2974ds/5211Mi) % 100.25/14.49 % (3053501)Instruction limit reached! % 100.25/14.49 % (3053501)------------------------------ % 100.25/14.49 % (3053501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 100.25/14.49 % (3053501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.25/14.49 % (3053501)CaDiCaL version: 2.1.3 % 100.25/14.49 % (3053501)Termination reason: Instruction limit % 100.25/14.49 % (3053501)Termination phase: Saturation % 100.25/14.49 % (3053501)Time elapsed: 1.068 s % 100.25/14.49 % (3053501)Peak memory usage: 18 MB % 100.25/14.49 % (3053501)Instructions burned: 4594 (million) % 100.25/14.49 % (3053507)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=881667499:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 100.25/14.49 % Exception at run slice level % 100.25/14.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.25/14.49 % (3053509)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1604488178:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 100.25/14.49 % Exception at run slice level % 100.25/14.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 100.25/14.49 % (3053511)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2438061212:i=14071_2972 on theBenchmark for (2972ds/14071Mi) % 100.25/14.49 % Exception at run slice level % 123.04/17.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 123.04/17.61 % (3053513)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2346435555:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi) % 123.04/17.61 % (3053495)Instruction limit reached! % 123.04/17.61 % (3053495)------------------------------ % 123.04/17.61 % (3053495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.04/17.61 % (3053495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.04/17.61 % (3053495)CaDiCaL version: 2.1.3 % 123.04/17.61 % (3053495)Termination reason: Instruction limit % 123.04/17.61 % (3053495)Termination phase: Saturation % 123.04/17.61 % (3053495)Time elapsed: 1.901 s % 123.04/17.61 % (3053495)Peak memory usage: 25 MB % 123.04/17.61 % (3053495)Instructions burned: 3774 (million) % 123.04/17.61 % (3053489)Instruction limit reached! % 123.04/17.61 % (3053489)------------------------------ % 123.04/17.61 % (3053489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.04/17.61 % (3053489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.04/17.61 % (3053489)CaDiCaL version: 2.1.3 % 123.04/17.61 % (3053489)Termination reason: Instruction limit % 123.04/17.61 % (3053489)Termination phase: Saturation % 123.04/17.61 % (3053489)Time elapsed: 2.299 s % 123.04/17.61 % (3053489)Peak memory usage: 16 MB % 123.04/17.61 % (3053489)Instructions burned: 5115 (million) % 123.04/17.61 % (3053515)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3701200100:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 123.04/17.61 % (3053516)dis+10_16:1_sil=16000:random_seed=2228730282:i=9155:fsr=off_2969 on theBenchmark for (2969ds/9155Mi) % 123.04/17.61 % (3053505)Instruction limit reached! % 123.04/17.61 % (3053505)------------------------------ % 123.04/17.61 % (3053505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.04/17.61 % (3053505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.04/17.61 % (3053505)CaDiCaL version: 2.1.3 % 123.04/17.61 % (3053505)Termination reason: Instruction limit % 123.04/17.61 % (3053505)Termination phase: Saturation % 123.04/17.61 % (3053505)Time elapsed: 2.802 s % 123.04/17.61 % (3053505)Peak memory usage: 43 MB % 123.04/17.61 % (3053505)Instructions burned: 5213 (million) % 123.04/17.61 % (3053519)ott-3_8_sil=64000:random_seed=2012412195:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 123.04/17.61 % (3053515)Instruction limit reached! % 123.04/17.61 % (3053515)------------------------------ % 123.04/17.61 % (3053515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.04/17.61 % (3053515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.04/17.61 % (3053515)CaDiCaL version: 2.1.3 % 123.04/17.61 % (3053515)Termination reason: Instruction limit % 123.04/17.61 % (3053515)Termination phase: Saturation % 123.04/17.61 % (3053515)Time elapsed: 3.636 s % 123.04/17.61 % (3053515)Peak memory usage: 17 MB % 123.04/17.61 % (3053515)Instructions burned: 8175 (million) % 123.04/17.61 % (3053521)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2282950229:fmbsr=2:i=32576_2932 on theBenchmark for (2932ds/32576Mi) % 123.04/17.61 % Exception at run slice level % 123.04/17.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 123.04/17.61 % (3053523)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3104484125:i=11404_2932 on theBenchmark for (2932ds/11404Mi) % 123.04/17.61 % (3053516)Instruction limit reached! % 123.04/17.61 % (3053516)------------------------------ % 123.04/17.61 % (3053516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.04/17.61 % (3053516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.04/17.61 % (3053516)CaDiCaL version: 2.1.3 % 123.04/17.61 % (3053516)Termination reason: Instruction limit % 123.04/17.61 % (3053516)Termination phase: Saturation % 123.04/17.61 % (3053516)Time elapsed: 4.774 s % 123.04/17.61 % (3053516)Peak memory usage: 68 MB % 123.04/17.61 % (3053516)Instructions burned: 9156 (million) % 123.04/17.61 % (3053525)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4258775558:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 123.04/17.61 % (3053513)Instruction limit reached! % 123.04/17.61 % (3053513)------------------------------ % 123.04/17.61 % (3053513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 123.04/17.61 % (3053513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.04/17.61 % (3053513)CaDiCaL version: 2.1.3 % 129.93/18.64 % (3053513)Termination reason: Instruction limit % 129.93/18.64 % (3053513)Termination phase: Saturation % 129.93/18.64 % (3053513)Time elapsed: 6.359 s % 129.93/18.64 % (3053513)Peak memory usage: 99 MB % 129.93/18.64 % (3053513)Instructions burned: 22566 (million) % 129.93/18.64 % (3053527)dis+33_16_sil=32000:sac=on:random_seed=2021586147:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi) % 129.93/18.64 % (3053527)Instruction limit reached! % 129.93/18.64 % (3053527)------------------------------ % 129.93/18.64 % (3053527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.93/18.64 % (3053527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.93/18.64 % (3053527)CaDiCaL version: 2.1.3 % 129.93/18.64 % (3053527)Termination reason: Instruction limit % 129.93/18.64 % (3053527)Termination phase: Saturation % 129.93/18.64 % (3053527)Time elapsed: 3.575 s % 129.93/18.64 % (3053527)Peak memory usage: 22 MB % 129.93/18.64 % (3053527)Instructions burned: 15855 (million) % 129.93/18.64 % (3053529)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2300132275:avsq=on:i=17627:add=on:amm=off_2872 on theBenchmark for (2872ds/17627Mi) % 129.93/18.64 % (3053523)Instruction limit reached! % 129.93/18.64 % (3053523)------------------------------ % 129.93/18.64 % (3053523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.93/18.64 % (3053523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.93/18.64 % (3053523)CaDiCaL version: 2.1.3 % 129.93/18.64 % (3053523)Termination reason: Instruction limit % 129.93/18.64 % (3053523)Termination phase: Saturation % 129.93/18.64 % (3053523)Time elapsed: 6.461 s % 129.93/18.64 % (3053523)Peak memory usage: 41 MB % 129.93/18.64 % (3053523)Instructions burned: 11405 (million) % 129.93/18.64 % (3053531)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1659721189:s2a=on:i=53295_2867 on theBenchmark for (2867ds/53295Mi) % 129.93/18.64 % (3053503)Instruction limit reached! % 129.93/18.64 % (3053503)------------------------------ % 129.93/18.64 % (3053503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.93/18.64 % (3053503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.93/18.64 % (3053503)CaDiCaL version: 2.1.3 % 129.93/18.64 % (3053503)Termination reason: Instruction limit % 129.93/18.64 % (3053503)Termination phase: Saturation % 129.93/18.64 % (3053503)Time elapsed: 11.702 s % 129.93/18.64 % (3053503)Peak memory usage: 26 MB % 129.93/18.64 % (3053503)Instructions burned: 29341 (million) % 129.93/18.64 % (3053533)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3448524668:i=26857:ins=20_2860 on theBenchmark for (2860ds/26857Mi) % 129.93/18.64 % Exception at run slice level % 129.93/18.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.93/18.64 % (3053535)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2305634112:i=28120:bs=on:fsr=off_2859 on theBenchmark for (2859ds/28120Mi) % 129.93/18.64 % (3053519)Instruction limit reached! % 129.93/18.64 % (3053519)------------------------------ % 129.93/18.64 % (3053519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 129.93/18.64 % (3053519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.93/18.64 % (3053519)CaDiCaL version: 2.1.3 % 129.93/18.64 % (3053519)Termination reason: Instruction limit % 129.93/18.64 % (3053519)Termination phase: Saturation % 129.93/18.64 % (3053519)Time elapsed: 8.764 s % 129.93/18.64 % (3053519)Peak memory usage: 22 MB % 129.93/18.64 % (3053519)Instructions burned: 20139 (million) % 129.93/18.64 % (3053537)fmb+10_1_sil=256000:fmbss=7:random_seed=3210014865:fmbsr=1.6:i=182295_2858 on theBenchmark for (2858ds/182295Mi) % 129.93/18.64 % Exception at run slice level % 129.93/18.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.93/18.64 % (3053539)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2515479413:i=44625:gsp=on_2858 on theBenchmark for (2858ds/44625Mi) % 129.93/18.64 % (3053539)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 129.93/18.64 % Exception at run slice level % 129.93/18.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.93/18.64 % (3053541)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1861001653:i=160505_2857 on theBenchmark for (2857ds/160505Mi) % 129.93/18.64 % Exception at run slice level % 129.93/18.64 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 129.93/18.64 % (3053543)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2141622436:fmbsr=1.3:i=225729_2857 on theBenchmark for (2857ds/225729Mi) % 164.28/23.42 % Exception at run slice level % 164.28/23.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 164.28/23.42 % (3053545)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3186567934:fmbsr=2:i=185024:ins=7_2857 on theBenchmark for (2857ds/185024Mi) % 164.28/23.42 % Exception at run slice level % 164.28/23.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 164.28/23.42 % (3053547)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1627411859:rtra=on_2857 on theBenchmark for (2857ds/0Mi) % 164.28/23.42 % Exception at run slice level % 164.28/23.42 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 164.28/23.42 % (3053549)% WARNING: option uhcvi not known. % 164.28/23.42 % (3053549)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2468128725:i=271062:add=off:rtra=on:rawr=on_2856 on theBenchmark for (2856ds/271062Mi) % 164.28/23.42 % (3053525)Instruction limit reached! % 164.28/23.42 % (3053525)------------------------------ % 164.28/23.42 % (3053525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.28/23.42 % (3053525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.28/23.42 % (3053525)CaDiCaL version: 2.1.3 % 164.28/23.42 % (3053525)Termination reason: Instruction limit % 164.28/23.42 % (3053525)Termination phase: Saturation % 164.28/23.42 % (3053525)Time elapsed: 6.609 s % 164.28/23.42 % (3053525)Peak memory usage: 24 MB % 164.28/23.42 % (3053525)Instructions burned: 14134 (million) % 164.28/23.42 % (3053551)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3489404053:i=176048:add=on:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/176048Mi) % 164.28/23.42 % (3053529)Instruction limit reached! % 164.28/23.42 % (3053529)------------------------------ % 164.28/23.42 % (3053529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.28/23.42 % (3053529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.28/23.42 % (3053529)CaDiCaL version: 2.1.3 % 164.28/23.42 % (3053529)Termination reason: Instruction limit % 164.28/23.42 % (3053529)Termination phase: Saturation % 164.28/23.42 % (3053529)Time elapsed: 4.327 s % 164.28/23.42 % (3053529)Peak memory usage: 37 MB % 164.28/23.42 % (3053529)Instructions burned: 17630 (million) % 164.28/23.42 % (3053706)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3341838057:i=206:fgj=on:rtra=on_2829 on theBenchmark for (2829ds/206Mi) % 164.28/23.42 % (3053706)Instruction limit reached! % 164.28/23.42 % (3053706)------------------------------ % 164.28/23.42 % (3053706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.28/23.42 % (3053706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.28/23.42 % (3053706)CaDiCaL version: 2.1.3 % 164.28/23.42 % (3053706)Termination reason: Instruction limit % 164.28/23.42 % (3053706)Termination phase: Saturation % 164.28/23.42 % (3053706)Time elapsed: 0.091 s % 164.28/23.42 % (3053706)Peak memory usage: 12 MB % 164.28/23.42 % (3053706)Instructions burned: 208 (million) % 164.28/23.42 % (3053708)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=500302308:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi) % 164.28/23.42 % (3053708)Instruction limit reached! % 164.28/23.42 % (3053708)------------------------------ % 164.28/23.42 % (3053708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.28/23.42 % (3053708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.28/23.42 % (3053708)CaDiCaL version: 2.1.3 % 164.28/23.42 % (3053708)Termination reason: Instruction limit % 164.28/23.42 % (3053708)Termination phase: Saturation % 164.28/23.42 % (3053708)Time elapsed: 0.076 s % 164.28/23.42 % (3053708)Peak memory usage: 13 MB % 164.28/23.42 % (3053708)Instructions burned: 235 (million) % 164.28/23.42 % (3053710)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1116109465:i=262:rtra=on_2827 on theBenchmark for (2827ds/262Mi) % 164.28/23.42 % (3053710)Instruction limit reached! % 164.28/23.42 % (3053710)------------------------------ % 164.28/23.42 % (3053710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 164.28/23.42 % (3053710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.28/23.42 % (3053710)CaDiCaL version: 2.1.3 % 164.28/23.42 % (3053710)Termination reason: Instruction limit % 164.28/23.42 % (3053710)Termination phase: Saturation % 208.99/29.74 % (3053710)Time elapsed: 0.084 s % 208.99/29.74 % (3053710)Peak memory usage: 13 MB % 208.99/29.74 % (3053710)Instructions burned: 265 (million) % 208.99/29.74 % (3053712)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2240186068:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2826 on theBenchmark for (2826ds/318Mi) % 208.99/29.74 % (3053712)Instruction limit reached! % 208.99/29.74 % (3053712)------------------------------ % 208.99/29.74 % (3053712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.99/29.74 % (3053712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.99/29.74 % (3053712)CaDiCaL version: 2.1.3 % 208.99/29.74 % (3053712)Termination reason: Instruction limit % 208.99/29.74 % (3053712)Termination phase: Saturation % 208.99/29.74 % (3053712)Time elapsed: 0.097 s % 208.99/29.74 % (3053712)Peak memory usage: 13 MB % 208.99/29.74 % (3053712)Instructions burned: 319 (million) % 208.99/29.74 % (3053714)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2357484133:i=1428:nm=2:rtra=on_2825 on theBenchmark for (2825ds/1428Mi) % 208.99/29.74 % Exception at run slice level % 208.99/29.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.99/29.74 % (3053716)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1870656289:i=262:bd=preordered:rtra=on:fsd=on_2825 on theBenchmark for (2825ds/262Mi) % 208.99/29.74 % (3053716)Instruction limit reached! % 208.99/29.74 % (3053716)------------------------------ % 208.99/29.74 % (3053716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.99/29.74 % (3053716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.99/29.74 % (3053716)CaDiCaL version: 2.1.3 % 208.99/29.74 % (3053716)Termination reason: Instruction limit % 208.99/29.74 % (3053716)Termination phase: Saturation % 208.99/29.74 % (3053716)Time elapsed: 0.087 s % 208.99/29.74 % (3053716)Peak memory usage: 14 MB % 208.99/29.74 % (3053716)Instructions burned: 263 (million) % 208.99/29.74 % (3053718)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=899366259:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2824 on theBenchmark for (2824ds/1368Mi) % 208.99/29.74 % (3053718)Instruction limit reached! % 208.99/29.74 % (3053718)------------------------------ % 208.99/29.74 % (3053718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.99/29.74 % (3053718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.99/29.74 % (3053718)CaDiCaL version: 2.1.3 % 208.99/29.74 % (3053718)Termination reason: Instruction limit % 208.99/29.74 % (3053718)Termination phase: Saturation % 208.99/29.74 % (3053718)Time elapsed: 0.352 s % 208.99/29.74 % (3053718)Peak memory usage: 16 MB % 208.99/29.74 % (3053718)Instructions burned: 1376 (million) % 208.99/29.74 % (3053720)ott-21_1_sil=16000:si=on:fs=off:random_seed=1850230640:i=360:av=off:fsr=off:rtra=on_2820 on theBenchmark for (2820ds/360Mi) % 208.99/29.74 % (3053720)Instruction limit reached! % 208.99/29.74 % (3053720)------------------------------ % 208.99/29.74 % (3053720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.99/29.74 % (3053720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.99/29.74 % (3053720)CaDiCaL version: 2.1.3 % 208.99/29.74 % (3053720)Termination reason: Instruction limit % 208.99/29.74 % (3053720)Termination phase: Saturation % 208.99/29.74 % (3053720)Time elapsed: 0.091 s % 208.99/29.74 % (3053720)Peak memory usage: 13 MB % 208.99/29.74 % (3053720)Instructions burned: 364 (million) % 208.99/29.74 % (3053722)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1500096074:i=954:bd=all:rtra=on_2819 on theBenchmark for (2819ds/954Mi) % 208.99/29.74 % (3053722)Instruction limit reached! % 208.99/29.74 % (3053722)------------------------------ % 208.99/29.74 % (3053722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.99/29.74 % (3053722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.99/29.74 % (3053722)CaDiCaL version: 2.1.3 % 208.99/29.74 % (3053722)Termination reason: Instruction limit % 208.99/29.74 % (3053722)Termination phase: Saturation % 208.99/29.74 % (3053722)Time elapsed: 0.313 s % 208.99/29.74 % (3053722)Peak memory usage: 16 MB % 208.99/29.74 % (3053722)Instructions burned: 954 (million) % 208.99/29.74 % (3053724)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1865957283:fmbsr=1.3:i=1730:ins=25:rtra=on_2816 on theBenchmark for (2816ds/1730Mi) % 208.99/29.74 % Exception at run slice level % 208.99/29.74 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.92/36.11 % (3053726)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1609119842:i=2358:rtra=on_2815 on theBenchmark for (2815ds/2358Mi) % 253.92/36.11 % (3053726)Instruction limit reached! % 253.92/36.11 % (3053726)------------------------------ % 253.92/36.11 % (3053726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.92/36.11 % (3053726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.92/36.11 % (3053726)CaDiCaL version: 2.1.3 % 253.92/36.11 % (3053726)Termination reason: Instruction limit % 253.92/36.11 % (3053726)Termination phase: Saturation % 253.92/36.11 % (3053726)Time elapsed: 0.646 s % 253.92/36.11 % (3053726)Peak memory usage: 16 MB % 253.92/36.11 % (3053726)Instructions burned: 2363 (million) % 253.92/36.11 % (3053728)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4220355030:i=1778:ins=1:rtra=on_2809 on theBenchmark for (2809ds/1778Mi) % 253.92/36.11 % Exception at run slice level % 253.92/36.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.92/36.11 % (3053730)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=610044982:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/1384Mi) % 253.92/36.11 % (3053730)Instruction limit reached! % 253.92/36.11 % (3053730)------------------------------ % 253.92/36.11 % (3053730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.92/36.11 % (3053730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.92/36.11 % (3053730)CaDiCaL version: 2.1.3 % 253.92/36.11 % (3053730)Termination reason: Instruction limit % 253.92/36.11 % (3053730)Termination phase: Saturation % 253.92/36.11 % (3053730)Time elapsed: 0.491 s % 253.92/36.11 % (3053730)Peak memory usage: 17 MB % 253.92/36.11 % (3053730)Instructions burned: 1387 (million) % 253.92/36.11 % (3053732)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4128921519:i=1758:kws=inv_precedence:fsr=off:rtra=on_2804 on theBenchmark for (2804ds/1758Mi) % 253.92/36.11 % (3053732)Instruction limit reached! % 253.92/36.11 % (3053732)------------------------------ % 253.92/36.11 % (3053732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.92/36.11 % (3053732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.92/36.11 % (3053732)CaDiCaL version: 2.1.3 % 253.92/36.11 % (3053732)Termination reason: Instruction limit % 253.92/36.11 % (3053732)Termination phase: Saturation % 253.92/36.11 % (3053732)Time elapsed: 0.574 s % 253.92/36.11 % (3053732)Peak memory usage: 24 MB % 253.92/36.11 % (3053732)Instructions burned: 1759 (million) % 253.92/36.11 % (3053734)fmb+10_1_sil=64000:si=on:random_seed=542836577:i=44122:nm=2:rtra=on:gsp=on_2798 on theBenchmark for (2798ds/44122Mi) % 253.92/36.11 % (3053734)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 253.92/36.11 % Exception at run slice level % 253.92/36.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.92/36.11 % (3053736)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=81140140:i=19030:nm=5:rtra=on_2798 on theBenchmark for (2798ds/19030Mi) % 253.92/36.11 % Exception at run slice level % 253.92/36.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.92/36.11 % (3053738)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2014012489:fmbsr=1.7:i=1840:rtra=on_2797 on theBenchmark for (2797ds/1840Mi) % 253.92/36.11 % Exception at run slice level % 253.92/36.11 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 253.92/36.11 % (3053740)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=4262521329:i=10262:rtra=on_2797 on theBenchmark for (2797ds/10262Mi) % 253.92/36.11 % (3053740)Instruction limit reached! % 253.92/36.11 % (3053740)------------------------------ % 253.92/36.11 % (3053740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 253.92/36.11 % (3053740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.92/36.11 % (3053740)CaDiCaL version: 2.1.3 % 253.92/36.11 % (3053740)Termination reason: Instruction limit % 253.92/36.11 % (3053740)Termination phase: Saturation % 253.92/36.11 % (3053740)Time elapsed: 2.945 s % 253.92/36.11 % (3053740)Peak memory usage: 29 MB % 253.92/36.11 % (3Terminated % 300.51/42.64 % Vampire exiting %------------------------------------------------------------------------------