%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV585_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 : n012.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:26:04 PM UTC 2026 % Result : Timeout 300.09s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWV585_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.00/0.11 % Computer : n012.cluster.edu % 0.00/0.11 % Model : x86_64 x86_64 % 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.00/0.11 % Memory : 8046.5625MB % 0.00/0.11 % OS : Linux 6.8.0-71-generic % 0.00/0.11 % CPULimit : 300 % 0.00/0.11 % WCLimit : 300 % 0.00/0.11 % DateTime : Mon Sep 28 11:56:49 UTC 2026 % 0.00/0.11 % CPUTime : % 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.13 Running first-order model finding % 0.08/0.13 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 % 3.61/0.73 % (3334608)Will run a generic schedule for satisfiability detection. % 3.61/0.73 % (3334614)% WARNING: option uhcvi not known. % 3.61/0.73 % (3334613)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1775452650_2999 on theBenchmark for (2999ds/0Mi) % 3.61/0.73 % (3334614)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3572078855:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 3.61/0.73 % (3334615)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4172674178:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 3.61/0.73 % (3334616)dis+10_1_sil=32000:sp=arity:random_seed=2377081744:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 3.61/0.73 % (3334619)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=656647102:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 3.61/0.73 % (3334617)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4211005850:i=116_2999 on theBenchmark for (2999ds/116Mi) % 3.61/0.73 % (3334618)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3388733779:i=131_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.73 % Exception at run slice level % 3.61/0.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 3.61/0.73 % (3334627)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2706702134:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 3.61/0.73 % Exception at run slice level % 3.61/0.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 3.61/0.73 % (3334629)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=836475961:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 3.61/0.73 % (3334616)Instruction limit reached! % 3.61/0.73 % (3334616)------------------------------ % 3.61/0.73 % (3334616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.73 % (3334616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.73 % (3334616)CaDiCaL version: 2.1.3 % 3.61/0.73 % (3334616)Termination reason: Instruction limit % 3.61/0.73 % (3334616)Termination phase: Saturation % 3.61/0.73 % (3334616)Time elapsed: 0.032 s % 3.61/0.73 % (3334616)Peak memory usage: 12 MB % 3.61/0.73 % (3334616)Instructions burned: 107 (million) % 3.61/0.73 % (3334617)Instruction limit reached! % 3.61/0.73 % (3334617)------------------------------ % 3.61/0.73 % (3334617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.73 % (3334617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.73 % (3334617)CaDiCaL version: 2.1.3 % 3.61/0.73 % (3334617)Termination reason: Instruction limit % 3.61/0.73 % (3334617)Termination phase: Saturation % 3.61/0.73 % (3334617)Time elapsed: 0.036 s % 3.61/0.73 % (3334617)Peak memory usage: 12 MB % 3.61/0.73 % (3334617)Instructions burned: 116 (million) % 3.61/0.73 % (3334618)Instruction limit reached! % 3.61/0.73 % (3334618)------------------------------ % 3.61/0.73 % (3334618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.73 % (3334618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.73 % (3334618)CaDiCaL version: 2.1.3 % 3.61/0.73 % (3334618)Termination reason: Instruction limit % 3.61/0.73 % (3334618)Termination phase: Saturation % 3.61/0.73 % (3334618)Time elapsed: 0.042 s % 3.61/0.73 % (3334618)Peak memory usage: 12 MB % 3.61/0.73 % (3334618)Instructions burned: 132 (million) % 3.61/0.73 % (3334631)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=140153889:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 3.61/0.73 % (3334632)ott-21_1_sil=16000:fs=off:random_seed=3071844893:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 3.61/0.73 % (3334633)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1806008088:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 3.61/0.73 % (3334619)Instruction limit reached! % 3.61/0.73 % (3334619)------------------------------ % 3.61/0.73 % (3334619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 3.61/0.73 % (3334619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.61/0.73 % (3334619)CaDiCaL version: 2.1.3 % 3.61/0.73 % (3334619)Termination reason: Instruction limit % 3.61/0.73 % (3334619)Termination phase: Saturation % 11.04/1.86 % (3334619)Time elapsed: 0.054 s % 11.04/1.86 % (3334619)Peak memory usage: 13 MB % 11.04/1.86 % (3334619)Instructions burned: 170 (million) % 11.04/1.86 % (3334637)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3012924826:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi) % 11.04/1.86 % (3334629)Instruction limit reached! % 11.04/1.86 % (3334629)------------------------------ % 11.04/1.86 % (3334629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.04/1.86 % (3334629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/1.86 % (3334629)CaDiCaL version: 2.1.3 % 11.04/1.86 % (3334629)Termination reason: Instruction limit % 11.04/1.86 % (3334629)Termination phase: Saturation % 11.04/1.86 % (3334629)Time elapsed: 0.041 s % 11.04/1.86 % (3334629)Peak memory usage: 12 MB % 11.04/1.86 % (3334629)Instructions burned: 131 (million) % 11.04/1.86 % Exception at run slice level % 11.04/1.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.04/1.86 % (3334639)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=906823728:i=1179_2999 on theBenchmark for (2999ds/1179Mi) % 11.04/1.86 % (3334640)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2021703460:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi) % 11.04/1.86 % Exception at run slice level % 11.04/1.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.04/1.86 % (3334643)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=2330540271: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) % 11.04/1.86 % (3334632)Instruction limit reached! % 11.04/1.86 % (3334632)------------------------------ % 11.04/1.86 % (3334632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.04/1.86 % (3334632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/1.86 % (3334632)CaDiCaL version: 2.1.3 % 11.04/1.86 % (3334632)Termination reason: Instruction limit % 11.04/1.86 % (3334632)Termination phase: Saturation % 11.04/1.86 % (3334632)Time elapsed: 0.046 s % 11.04/1.86 % (3334632)Peak memory usage: 12 MB % 11.04/1.86 % (3334632)Instructions burned: 182 (million) % 11.04/1.86 % (3334645)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2846417226:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi) % 11.04/1.86 % (3334633)Instruction limit reached! % 11.04/1.86 % (3334633)------------------------------ % 11.04/1.86 % (3334633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.04/1.86 % (3334633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/1.86 % (3334633)CaDiCaL version: 2.1.3 % 11.04/1.86 % (3334633)Termination reason: Instruction limit % 11.04/1.86 % (3334633)Termination phase: Saturation % 11.04/1.86 % (3334633)Time elapsed: 0.144 s % 11.04/1.86 % (3334633)Peak memory usage: 15 MB % 11.04/1.86 % (3334633)Instructions burned: 480 (million) % 11.04/1.86 % (3334647)fmb+10_1_sil=64000:random_seed=3594681067:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 11.04/1.86 % (3334647)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.04/1.86 % Exception at run slice level % 11.04/1.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.04/1.86 % (3334649)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2121648010:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 11.04/1.86 % Exception at run slice level % 11.04/1.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 11.04/1.86 % (3334631)Instruction limit reached! % 11.04/1.86 % (3334631)------------------------------ % 11.04/1.86 % (3334631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 11.04/1.86 % (3334631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.04/1.86 % (3334631)CaDiCaL version: 2.1.3 % 11.04/1.86 % (3334631)Termination reason: Instruction limit % 11.04/1.86 % (3334631)Termination phase: Saturation % 11.04/1.86 % (3334631)Time elapsed: 0.181 s % 11.04/1.86 % (3334631)Peak memory usage: 16 MB % 11.04/1.86 % (3334631)Instructions burned: 685 (million) % 11.04/1.86 % (3334651)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2482992149:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 11.04/1.86 % Exception at run slice level % 46.84/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 46.84/6.85 % (3334652)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=591354486:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 46.84/6.85 % (3334654)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2752052007:i=1472:ins=7:fdi=8:gsp=on_2997 on theBenchmark for (2997ds/1472Mi) % 46.84/6.85 % (3334654)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 46.84/6.85 % (3334643)Instruction limit reached! % 46.84/6.85 % (3334643)------------------------------ % 46.84/6.85 % (3334643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.84/6.85 % (3334643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.84/6.85 % (3334643)CaDiCaL version: 2.1.3 % 46.84/6.85 % (3334643)Termination reason: Instruction limit % 46.84/6.85 % (3334643)Termination phase: Saturation % 46.84/6.85 % (3334643)Time elapsed: 0.183 s % 46.84/6.85 % (3334643)Peak memory usage: 15 MB % 46.84/6.85 % (3334643)Instructions burned: 695 (million) % 46.84/6.85 % (3334657)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3312154389:i=6324_2996 on theBenchmark for (2996ds/6324Mi) % 46.84/6.85 % Exception at run slice level % 46.84/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 46.84/6.85 % (3334659)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1312901011:fmbsr=2.30978:i=2174_2996 on theBenchmark for (2996ds/2174Mi) % 46.84/6.85 % Exception at run slice level % 46.84/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 46.84/6.85 % (3334661)ott-2_1_sil=16000:newcnf=on:random_seed=319856801:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2996 on theBenchmark for (2996ds/869Mi) % 46.84/6.85 % (3334645)Instruction limit reached! % 46.84/6.85 % (3334645)------------------------------ % 46.84/6.85 % (3334645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.84/6.85 % (3334645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.84/6.85 % (3334645)CaDiCaL version: 2.1.3 % 46.84/6.85 % (3334645)Termination reason: Instruction limit % 46.84/6.85 % (3334645)Termination phase: Saturation % 46.84/6.85 % (3334645)Time elapsed: 0.265 s % 46.84/6.85 % (3334645)Peak memory usage: 18 MB % 46.84/6.85 % (3334645)Instructions burned: 880 (million) % 46.84/6.85 % (3334663)ott+10_1_sil=32000:tgt=ground:random_seed=4241275368:i=5114:av=off_2995 on theBenchmark for (2995ds/5114Mi) % 46.84/6.85 % (3334639)Instruction limit reached! % 46.84/6.85 % (3334639)------------------------------ % 46.84/6.85 % (3334639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.84/6.85 % (3334639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.84/6.85 % (3334639)CaDiCaL version: 2.1.3 % 46.84/6.85 % (3334639)Termination reason: Instruction limit % 46.84/6.85 % (3334639)Termination phase: Saturation % 46.84/6.85 % (3334639)Time elapsed: 0.361 s % 46.84/6.85 % (3334639)Peak memory usage: 19 MB % 46.84/6.85 % (3334639)Instructions burned: 1181 (million) % 46.84/6.85 % (3334665)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2550874659:i=54282_2995 on theBenchmark for (2995ds/54282Mi) % 46.84/6.85 % Exception at run slice level % 46.84/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 46.84/6.85 % (3334667)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3481703425:i=3512:aac=none_2995 on theBenchmark for (2995ds/3512Mi) % 46.84/6.85 % (3334661)Instruction limit reached! % 46.84/6.85 % (3334661)------------------------------ % 46.84/6.85 % (3334661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 46.84/6.85 % (3334661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.84/6.85 % (3334661)CaDiCaL version: 2.1.3 % 46.84/6.85 % (3334661)Termination reason: Instruction limit % 46.84/6.85 % (3334661)Termination phase: Saturation % 46.84/6.85 % (3334661)Time elapsed: 0.244 s % 46.84/6.85 % (3334661)Peak memory usage: 16 MB % 46.84/6.85 % (3334661)Instructions burned: 872 (million) % 46.84/6.85 % (3334669)dis+21_1_sil=32000:sas=cadical:random_seed=659902102:i=3773:amm=off_2994 on theBenchmark for (2994ds/3773Mi) % 46.84/6.85 % (3334654)Instruction limit reached! % 46.84/6.85 % (3334654)------------------------------ % 46.84/6.85 % (3334654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.27/9.69 % (3334654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.27/9.69 % (3334654)CaDiCaL version: 2.1.3 % 66.27/9.69 % (3334654)Termination reason: Instruction limit % 66.27/9.69 % (3334654)Termination phase: Saturation % 66.27/9.69 % (3334654)Time elapsed: 0.324 s % 66.27/9.69 % (3334654)Peak memory usage: 20 MB % 66.27/9.69 % (3334654)Instructions burned: 1472 (million) % 66.27/9.69 % (3334671)ott+11_1_sil=16000:gs=on:random_seed=461653894:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2993 on theBenchmark for (2993ds/2251Mi) % 66.27/9.69 % (3334671)Instruction limit reached! % 66.27/9.69 % (3334671)------------------------------ % 66.27/9.69 % (3334671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.27/9.69 % (3334671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.27/9.69 % (3334671)CaDiCaL version: 2.1.3 % 66.27/9.69 % (3334671)Termination reason: Instruction limit % 66.27/9.69 % (3334671)Termination phase: Saturation % 66.27/9.69 % (3334671)Time elapsed: 0.635 s % 66.27/9.69 % (3334671)Peak memory usage: 18 MB % 66.27/9.69 % (3334671)Instructions burned: 2255 (million) % 66.27/9.69 % (3334673)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1918273464:fmbsr=1.6:i=67534_2987 on theBenchmark for (2987ds/67534Mi) % 66.27/9.69 % Exception at run slice level % 66.27/9.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 66.27/9.69 % (3334675)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=704651391:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2987 on theBenchmark for (2987ds/4591Mi) % 66.27/9.69 % (3334667)Instruction limit reached! % 66.27/9.69 % (3334667)------------------------------ % 66.27/9.69 % (3334667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.27/9.69 % (3334667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.27/9.69 % (3334667)CaDiCaL version: 2.1.3 % 66.27/9.69 % (3334667)Termination reason: Instruction limit % 66.27/9.69 % (3334667)Termination phase: Saturation % 66.27/9.69 % (3334667)Time elapsed: 1.002 s % 66.27/9.69 % (3334667)Peak memory usage: 29 MB % 66.27/9.69 % (3334667)Instructions burned: 3513 (million) % 66.27/9.69 % (3334677)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=694194677:i=29340_2985 on theBenchmark for (2985ds/29340Mi) % 66.27/9.69 % (3334652)Instruction limit reached! % 66.27/9.69 % (3334652)------------------------------ % 66.27/9.69 % (3334652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.27/9.69 % (3334652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.27/9.69 % (3334652)CaDiCaL version: 2.1.3 % 66.27/9.69 % (3334652)Termination reason: Instruction limit % 66.27/9.69 % (3334652)Termination phase: Saturation % 66.27/9.69 % (3334652)Time elapsed: 1.404 s % 66.27/9.69 % (3334652)Peak memory usage: 27 MB % 66.27/9.69 % (3334652)Instructions burned: 5133 (million) % 66.27/9.69 % (3334679)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3396184965:i=5211_2983 on theBenchmark for (2983ds/5211Mi) % 66.27/9.69 % (3334669)Instruction limit reached! % 66.27/9.69 % (3334669)------------------------------ % 66.27/9.69 % (3334669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 66.27/9.69 % (3334669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.27/9.69 % (3334669)CaDiCaL version: 2.1.3 % 66.27/9.69 % (3334669)Termination reason: Instruction limit % 66.27/9.69 % (3334669)Termination phase: Saturation % 66.27/9.69 % (3334669)Time elapsed: 1.097 s % 66.27/9.69 % (3334669)Peak memory usage: 28 MB % 66.27/9.69 % (3334669)Instructions burned: 3776 (million) % 66.27/9.69 % (3334681)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3197109322:i=5497:nm=2_2983 on theBenchmark for (2983ds/5497Mi) % 66.27/9.69 % Exception at run slice level % 66.27/9.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 66.27/9.69 % (3334683)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2153913619:fmbsr=2:i=46332_2982 on theBenchmark for (2982ds/46332Mi) % 66.27/9.69 % Exception at run slice level % 66.27/9.69 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 66.27/9.69 % (3334685)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3904269207:i=14071_2982 on theBenchmark for (2982ds/14071Mi) % 66.27/9.69 % Exception at run slice level % 99.77/14.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 99.77/14.37 % (3334687)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=611510763:i=22565:add=on:rawr=on_2982 on theBenchmark for (2982ds/22565Mi) % 99.77/14.37 % (3334663)Instruction limit reached! % 99.77/14.37 % (3334663)------------------------------ % 99.77/14.37 % (3334663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.77/14.37 % (3334663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.77/14.37 % (3334663)CaDiCaL version: 2.1.3 % 99.77/14.37 % (3334663)Termination reason: Instruction limit % 99.77/14.37 % (3334663)Termination phase: Saturation % 99.77/14.37 % (3334663)Time elapsed: 1.464 s % 99.77/14.37 % (3334663)Peak memory usage: 29 MB % 99.77/14.37 % (3334663)Instructions burned: 5114 (million) % 99.77/14.37 % (3334689)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=267389438:i=8173:av=off_2981 on theBenchmark for (2981ds/8173Mi) % 99.77/14.37 % (3334675)Instruction limit reached! % 99.77/14.37 % (3334675)------------------------------ % 99.77/14.37 % (3334675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.77/14.37 % (3334675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.77/14.37 % (3334675)CaDiCaL version: 2.1.3 % 99.77/14.37 % (3334675)Termination reason: Instruction limit % 99.77/14.37 % (3334675)Termination phase: Saturation % 99.77/14.37 % (3334675)Time elapsed: 0.900 s % 99.77/14.37 % (3334675)Peak memory usage: 26 MB % 99.77/14.37 % (3334675)Instructions burned: 4593 (million) % 99.77/14.37 % (3334691)dis+10_16:1_sil=16000:random_seed=4067400036:i=9155:fsr=off_2978 on theBenchmark for (2978ds/9155Mi) % 99.77/14.37 % (3334679)Instruction limit reached! % 99.77/14.37 % (3334679)------------------------------ % 99.77/14.37 % (3334679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.77/14.37 % (3334679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.77/14.37 % (3334679)CaDiCaL version: 2.1.3 % 99.77/14.37 % (3334679)Termination reason: Instruction limit % 99.77/14.37 % (3334679)Termination phase: Saturation % 99.77/14.37 % (3334679)Time elapsed: 1.469 s % 99.77/14.37 % (3334679)Peak memory usage: 47 MB % 99.77/14.37 % (3334679)Instructions burned: 5213 (million) % 99.77/14.37 % (3334694)ott-3_8_sil=64000:random_seed=1704755163:i=20139:bs=on_2968 on theBenchmark for (2968ds/20139Mi) % 99.77/14.37 % (3334689)Instruction limit reached! % 99.77/14.37 % (3334689)------------------------------ % 99.77/14.37 % (3334689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.77/14.37 % (3334689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.77/14.37 % (3334689)CaDiCaL version: 2.1.3 % 99.77/14.37 % (3334689)Termination reason: Instruction limit % 99.77/14.37 % (3334689)Termination phase: Saturation % 99.77/14.37 % (3334689)Time elapsed: 2.408 s % 99.77/14.37 % (3334689)Peak memory usage: 45 MB % 99.77/14.37 % (3334689)Instructions burned: 8173 (million) % 99.77/14.37 % (3334696)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3824584045:fmbsr=2:i=32576_2957 on theBenchmark for (2957ds/32576Mi) % 99.77/14.37 % Exception at run slice level % 99.77/14.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 99.77/14.37 % (3334698)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=855805452:i=11404_2956 on theBenchmark for (2956ds/11404Mi) % 99.77/14.37 % (3334691)Instruction limit reached! % 99.77/14.37 % (3334691)------------------------------ % 99.77/14.37 % (3334691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.77/14.37 % (3334691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.77/14.37 % (3334691)CaDiCaL version: 2.1.3 % 99.77/14.37 % (3334691)Termination reason: Instruction limit % 99.77/14.37 % (3334691)Termination phase: Saturation % 99.77/14.37 % (3334691)Time elapsed: 2.431 s % 99.77/14.37 % (3334691)Peak memory usage: 47 MB % 99.77/14.37 % (3334691)Instructions burned: 9157 (million) % 99.77/14.37 % (3334700)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3170591037:i=14134_2953 on theBenchmark for (2953ds/14134Mi) % 99.77/14.37 % (3334687)Instruction limit reached! % 99.77/14.37 % (3334687)------------------------------ % 99.77/14.37 % (3334687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 99.77/14.37 % (3334687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.77/14.37 % (3334687)CaDiCaL version: 2.1.3 % 107.51/15.40 % (3334687)Termination reason: Instruction limit % 107.51/15.40 % (3334687)Termination phase: Saturation % 107.51/15.40 % (3334687)Time elapsed: 4.970 s % 107.51/15.40 % (3334687)Peak memory usage: 33 MB % 107.51/15.40 % (3334687)Instructions burned: 22567 (million) % 107.51/15.40 % (3334702)dis+33_16_sil=32000:sac=on:random_seed=3471052511:i=15851:nm=0_2932 on theBenchmark for (2932ds/15851Mi) % 107.51/15.40 % (3334698)Instruction limit reached! % 107.51/15.40 % (3334698)------------------------------ % 107.51/15.40 % (3334698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.51/15.40 % (3334698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.51/15.40 % (3334698)CaDiCaL version: 2.1.3 % 107.51/15.40 % (3334698)Termination reason: Instruction limit % 107.51/15.40 % (3334698)Termination phase: Saturation % 107.51/15.40 % (3334698)Time elapsed: 3.729 s % 107.51/15.40 % (3334698)Peak memory usage: 54 MB % 107.51/15.40 % (3334698)Instructions burned: 11404 (million) % 107.51/15.40 % (3334704)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=923422736:avsq=on:i=17627:add=on:amm=off_2919 on theBenchmark for (2919ds/17627Mi) % 107.51/15.40 % (3334700)Instruction limit reached! % 107.51/15.40 % (3334700)------------------------------ % 107.51/15.40 % (3334700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.51/15.40 % (3334700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.51/15.40 % (3334700)CaDiCaL version: 2.1.3 % 107.51/15.40 % (3334700)Termination reason: Instruction limit % 107.51/15.40 % (3334700)Termination phase: Saturation % 107.51/15.40 % (3334700)Time elapsed: 4.625 s % 107.51/15.40 % (3334700)Peak memory usage: 44 MB % 107.51/15.40 % (3334700)Instructions burned: 14136 (million) % 107.51/15.40 % (3334706)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2750248319:s2a=on:i=53295_2907 on theBenchmark for (2907ds/53295Mi) % 107.51/15.40 % (3334677)Instruction limit reached! % 107.51/15.40 % (3334677)------------------------------ % 107.51/15.40 % (3334677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.51/15.40 % (3334677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.51/15.40 % (3334677)CaDiCaL version: 2.1.3 % 107.51/15.40 % (3334677)Termination reason: Instruction limit % 107.51/15.40 % (3334677)Termination phase: Saturation % 107.51/15.40 % (3334677)Time elapsed: 7.781 s % 107.51/15.40 % (3334677)Peak memory usage: 45 MB % 107.51/15.40 % (3334677)Instructions burned: 29343 (million) % 107.51/15.40 % (3334708)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4263961468:i=26857:ins=20_2907 on theBenchmark for (2907ds/26857Mi) % 107.51/15.40 % Exception at run slice level % 107.51/15.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.51/15.40 % (3334710)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1243072984:i=28120:bs=on:fsr=off_2906 on theBenchmark for (2906ds/28120Mi) % 107.51/15.40 % (3334694)Instruction limit reached! % 107.51/15.40 % (3334694)------------------------------ % 107.51/15.40 % (3334694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.51/15.40 % (3334694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.51/15.40 % (3334694)CaDiCaL version: 2.1.3 % 107.51/15.40 % (3334694)Termination reason: Instruction limit % 107.51/15.40 % (3334694)Termination phase: Saturation % 107.51/15.40 % (3334694)Time elapsed: 6.339 s % 107.51/15.40 % (3334694)Peak memory usage: 60 MB % 107.51/15.40 % (3334694)Instructions burned: 20141 (million) % 107.51/15.40 % (3334712)fmb+10_1_sil=256000:fmbss=7:random_seed=2912304431:fmbsr=1.6:i=182295_2904 on theBenchmark for (2904ds/182295Mi) % 107.51/15.40 % Exception at run slice level % 107.51/15.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.51/15.40 % (3334714)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1806312991:i=44625:gsp=on_2904 on theBenchmark for (2904ds/44625Mi) % 107.51/15.40 % (3334714)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 107.51/15.40 % Exception at run slice level % 107.51/15.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.51/15.40 % (3334716)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2619039655:i=160505_2904 on theBenchmark for (2904ds/160505Mi) % 107.51/15.40 % Exception at run slice level % 107.51/15.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.51/15.40 % (3334718)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=699798187:fmbsr=1.3:i=225729_2904 on theBenchmark for (2904ds/225729Mi) % 115.97/16.78 % Exception at run slice level % 115.97/16.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.97/16.78 % (3334720)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1347551226:fmbsr=2:i=185024:ins=7_2904 on theBenchmark for (2904ds/185024Mi) % 115.97/16.78 % Exception at run slice level % 115.97/16.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.97/16.78 % (3334722)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1137639282:rtra=on_2904 on theBenchmark for (2904ds/0Mi) % 115.97/16.78 % Exception at run slice level % 115.97/16.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 115.97/16.78 % (3334724)% WARNING: option uhcvi not known. % 115.97/16.78 % (3334724)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=52015186:i=271062:add=off:rtra=on:rawr=on_2904 on theBenchmark for (2904ds/271062Mi) % 115.97/16.78 % (3334702)Instruction limit reached! % 115.97/16.78 % (3334702)------------------------------ % 115.97/16.78 % (3334702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.97/16.78 % (3334702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.97/16.78 % (3334702)CaDiCaL version: 2.1.3 % 115.97/16.78 % (3334702)Termination reason: Instruction limit % 115.97/16.78 % (3334702)Termination phase: Saturation % 115.97/16.78 % (3334702)Time elapsed: 4.102 s % 115.97/16.78 % (3334702)Peak memory usage: 57 MB % 115.97/16.78 % (3334702)Instructions burned: 15853 (million) % 115.97/16.78 % (3334726)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3908159574:i=176048:add=on:rtra=on:rawr=on_2891 on theBenchmark for (2891ds/176048Mi) % 115.97/16.78 % (3334704)Instruction limit reached! % 115.97/16.78 % (3334704)------------------------------ % 115.97/16.78 % (3334704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.97/16.78 % (3334704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.97/16.78 % (3334704)CaDiCaL version: 2.1.3 % 115.97/16.78 % (3334704)Termination reason: Instruction limit % 115.97/16.78 % (3334704)Termination phase: Saturation % 115.97/16.78 % (3334704)Time elapsed: 5.890 s % 115.97/16.78 % (3334704)Peak memory usage: 277 MB % 115.97/16.78 % (3334704)Instructions burned: 17627 (million) % 115.97/16.78 % (3334728)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2216154640:i=206:fgj=on:rtra=on_2860 on theBenchmark for (2860ds/206Mi) % 115.97/16.78 % (3334728)Instruction limit reached! % 115.97/16.78 % (3334728)------------------------------ % 115.97/16.78 % (3334728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.97/16.78 % (3334728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.97/16.78 % (3334728)CaDiCaL version: 2.1.3 % 115.97/16.78 % (3334728)Termination reason: Instruction limit % 115.97/16.78 % (3334728)Termination phase: Saturation % 115.97/16.78 % (3334728)Time elapsed: 0.064 s % 115.97/16.78 % (3334728)Peak memory usage: 13 MB % 115.97/16.78 % (3334728)Instructions burned: 209 (million) % 115.97/16.78 % (3334730)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=561054238:i=232:rtra=on_2859 on theBenchmark for (2859ds/232Mi) % 115.97/16.78 % (3334730)Instruction limit reached! % 115.97/16.78 % (3334730)------------------------------ % 115.97/16.78 % (3334730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.97/16.78 % (3334730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.97/16.78 % (3334730)CaDiCaL version: 2.1.3 % 115.97/16.78 % (3334730)Termination reason: Instruction limit % 115.97/16.78 % (3334730)Termination phase: Saturation % 115.97/16.78 % (3334730)Time elapsed: 0.076 s % 115.97/16.78 % (3334730)Peak memory usage: 13 MB % 115.97/16.78 % (3334730)Instructions burned: 232 (million) % 115.97/16.78 % (3334732)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=694055532:i=262:rtra=on_2858 on theBenchmark for (2858ds/262Mi) % 115.97/16.78 % (3334732)Instruction limit reached! % 115.97/16.78 % (3334732)------------------------------ % 115.97/16.78 % (3334732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 115.97/16.78 % (3334732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.97/16.78 % (3334732)CaDiCaL version: 2.1.3 % 115.97/16.78 % (3334732)Termination reason: Instruction limit % 115.97/16.78 % (3334732)Termination phase: Saturation % 150.36/21.54 % (3334732)Time elapsed: 0.082 s % 150.36/21.54 % (3334732)Peak memory usage: 13 MB % 150.36/21.54 % (3334732)Instructions burned: 265 (million) % 150.36/21.54 % (3334734)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2448601824:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2857 on theBenchmark for (2857ds/318Mi) % 150.36/21.54 % (3334734)Instruction limit reached! % 150.36/21.54 % (3334734)------------------------------ % 150.36/21.54 % (3334734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.36/21.54 % (3334734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.36/21.54 % (3334734)CaDiCaL version: 2.1.3 % 150.36/21.54 % (3334734)Termination reason: Instruction limit % 150.36/21.54 % (3334734)Termination phase: Saturation % 150.36/21.54 % (3334734)Time elapsed: 0.102 s % 150.36/21.54 % (3334734)Peak memory usage: 14 MB % 150.36/21.54 % (3334734)Instructions burned: 321 (million) % 150.36/21.54 % (3334736)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3061125958:i=1428:nm=2:rtra=on_2856 on theBenchmark for (2856ds/1428Mi) % 150.36/21.54 % Exception at run slice level % 150.36/21.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 150.36/21.54 % (3334738)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3247103470:i=262:bd=preordered:rtra=on:fsd=on_2856 on theBenchmark for (2856ds/262Mi) % 150.36/21.54 % (3334738)Instruction limit reached! % 150.36/21.54 % (3334738)------------------------------ % 150.36/21.54 % (3334738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.36/21.54 % (3334738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.36/21.54 % (3334738)CaDiCaL version: 2.1.3 % 150.36/21.54 % (3334738)Termination reason: Instruction limit % 150.36/21.54 % (3334738)Termination phase: Saturation % 150.36/21.54 % (3334738)Time elapsed: 0.085 s % 150.36/21.54 % (3334738)Peak memory usage: 13 MB % 150.36/21.54 % (3334738)Instructions burned: 265 (million) % 150.36/21.54 % (3334740)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=3711630321:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2855 on theBenchmark for (2855ds/1368Mi) % 150.36/21.54 % (3334740)Instruction limit reached! % 150.36/21.54 % (3334740)------------------------------ % 150.36/21.54 % (3334740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.36/21.54 % (3334740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.36/21.54 % (3334740)CaDiCaL version: 2.1.3 % 150.36/21.54 % (3334740)Termination reason: Instruction limit % 150.36/21.54 % (3334740)Termination phase: Saturation % 150.36/21.54 % (3334740)Time elapsed: 0.355 s % 150.36/21.54 % (3334740)Peak memory usage: 18 MB % 150.36/21.54 % (3334740)Instructions burned: 1369 (million) % 150.36/21.54 % (3334742)ott-21_1_sil=16000:si=on:fs=off:random_seed=1899551081:i=360:av=off:fsr=off:rtra=on_2851 on theBenchmark for (2851ds/360Mi) % 150.36/21.54 % (3334742)Instruction limit reached! % 150.36/21.54 % (3334742)------------------------------ % 150.36/21.54 % (3334742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.36/21.54 % (3334742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.36/21.54 % (3334742)CaDiCaL version: 2.1.3 % 150.36/21.54 % (3334742)Termination reason: Instruction limit % 150.36/21.54 % (3334742)Termination phase: Saturation % 150.36/21.54 % (3334742)Time elapsed: 0.089 s % 150.36/21.54 % (3334742)Peak memory usage: 13 MB % 150.36/21.54 % (3334742)Instructions burned: 361 (million) % 150.36/21.54 % (3334744)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4046394349:i=954:bd=all:rtra=on_2850 on theBenchmark for (2850ds/954Mi) % 150.36/21.54 % (3334744)Instruction limit reached! % 150.36/21.54 % (3334744)------------------------------ % 150.36/21.54 % (3334744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 150.36/21.54 % (3334744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.36/21.54 % (3334744)CaDiCaL version: 2.1.3 % 150.36/21.54 % (3334744)Termination reason: Instruction limit % 150.36/21.54 % (3334744)Termination phase: Saturation % 150.36/21.54 % (3334744)Time elapsed: 0.307 s % 150.36/21.54 % (3334744)Peak memory usage: 17 MB % 150.36/21.54 % (3334744)Instructions burned: 956 (million) % 150.36/21.54 % (3334746)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2428779215:fmbsr=1.3:i=1730:ins=25:rtra=on_2847 on theBenchmark for (2847ds/1730Mi) % 150.36/21.54 % Exception at run slice level % 150.36/21.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.37/23.63 % (3334748)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3937774938:i=2358:rtra=on_2847 on theBenchmark for (2847ds/2358Mi) % 165.37/23.63 % (3334710)Instruction limit reached! % 165.37/23.63 % (3334710)------------------------------ % 165.37/23.63 % (3334710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.37/23.63 % (3334710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.37/23.63 % (3334710)CaDiCaL version: 2.1.3 % 165.37/23.63 % (3334710)Termination reason: Instruction limit % 165.37/23.63 % (3334710)Termination phase: Saturation % 165.37/23.63 % (3334710)Time elapsed: 6.462 s % 165.37/23.63 % (3334710)Peak memory usage: 51 MB % 165.37/23.63 % (3334710)Instructions burned: 28120 (million) % 165.37/23.63 % (3334750)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1423303535:i=1778:ins=1:rtra=on_2842 on theBenchmark for (2842ds/1778Mi) % 165.37/23.63 % Exception at run slice level % 165.37/23.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.37/23.63 % (3334752)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=3586357127:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2841 on theBenchmark for (2841ds/1384Mi) % 165.37/23.63 % (3334748)Instruction limit reached! % 165.37/23.63 % (3334748)------------------------------ % 165.37/23.63 % (3334748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.37/23.63 % (3334748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.37/23.63 % (3334748)CaDiCaL version: 2.1.3 % 165.37/23.63 % (3334748)Termination reason: Instruction limit % 165.37/23.63 % (3334748)Termination phase: Saturation % 165.37/23.63 % (3334748)Time elapsed: 0.830 s % 165.37/23.63 % (3334748)Peak memory usage: 23 MB % 165.37/23.63 % (3334748)Instructions burned: 2358 (million) % 165.37/23.63 % (3334754)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=821993491:i=1758:kws=inv_precedence:fsr=off:rtra=on_2838 on theBenchmark for (2838ds/1758Mi) % 165.37/23.63 % (3334752)Instruction limit reached! % 165.37/23.63 % (3334752)------------------------------ % 165.37/23.63 % (3334752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.37/23.63 % (3334752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.37/23.63 % (3334752)CaDiCaL version: 2.1.3 % 165.37/23.63 % (3334752)Termination reason: Instruction limit % 165.37/23.63 % (3334752)Termination phase: Saturation % 165.37/23.63 % (3334752)Time elapsed: 0.445 s % 165.37/23.63 % (3334752)Peak memory usage: 20 MB % 165.37/23.63 % (3334752)Instructions burned: 1386 (million) % 165.37/23.63 % (3334756)fmb+10_1_sil=64000:si=on:random_seed=3739585779:i=44122:nm=2:rtra=on:gsp=on_2837 on theBenchmark for (2837ds/44122Mi) % 165.37/23.63 % (3334756)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 165.37/23.63 % Exception at run slice level % 165.37/23.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.37/23.63 % (3334758)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2917517363:i=19030:nm=5:rtra=on_2837 on theBenchmark for (2837ds/19030Mi) % 165.37/23.63 % Exception at run slice level % 165.37/23.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.37/23.63 % (3334760)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4269406342:fmbsr=1.7:i=1840:rtra=on_2837 on theBenchmark for (2837ds/1840Mi) % 165.37/23.63 % Exception at run slice level % 165.37/23.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 165.37/23.63 % (3334762)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3464557739:i=10262:rtra=on_2837 on theBenchmark for (2837ds/10262Mi) % 165.37/23.63 % (3334754)Instruction limit reached! % 165.37/23.63 % (3334754)------------------------------ % 165.37/23.63 % (3334754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 165.37/23.63 % (3334754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.37/23.63 % (3334754)CaDiCaL version: 2.1.3 % 165.37/23.63 % (3334754)Termination reason: Instruction limit % 165.37/23.63 % (3334754)Termination phase: Saturation % 165.37/23.63 % (3334754)Time elapsed: 0.529 s % 165.37/23.63 % (3334754)Peak memory usage: 23 MB % 165.37/23.63 % (3334754)Instructions burned: 1761 (million) % 260.70/37.18 % (3334764)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=927467468:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2833 on theBenchmark for (2833ds/2944Mi) % 260.70/37.18 % (3334764)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 260.70/37.18 % (3334764)Instruction limit reached! % 260.70/37.18 % (3334764)------------------------------ % 260.70/37.18 % (3334764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.70/37.18 % (3334764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.70/37.18 % (3334764)CaDiCaL version: 2.1.3 % 260.70/37.18 % (3334764)Termination reason: Instruction limit % 260.70/37.18 % (3334764)Termination phase: Saturation % 260.70/37.18 % (3334764)Time elapsed: 0.667 s % 260.70/37.18 % (3334764)Peak memory usage: 27 MB % 260.70/37.18 % (3334764)Instructions burned: 2946 (million) % 260.70/37.18 % (3334766)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=179856809:i=12648:rtra=on_2826 on theBenchmark for (2826ds/12648Mi) % 260.70/37.18 % Exception at run slice level % 260.70/37.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 260.70/37.18 % (3334768)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2892839438:fmbsr=2.30978:i=4348:rtra=on_2826 on theBenchmark for (2826ds/4348Mi) % 260.70/37.18 % Exception at run slice level % 260.70/37.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 260.70/37.18 % (3334770)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1385993500:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2826 on theBenchmark for (2826ds/1738Mi) % 260.70/37.18 % (3334770)Instruction limit reached! % 260.70/37.18 % (3334770)------------------------------ % 260.70/37.18 % (3334770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.70/37.18 % (3334770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.70/37.18 % (3334770)CaDiCaL version: 2.1.3 % 260.70/37.18 % (3334770)Termination reason: Instruction limit % 260.70/37.18 % (3334770)Termination phase: Saturation % 260.70/37.18 % (3334770)Time elapsed: 0.514 s % 260.70/37.18 % (3334770)Peak memory usage: 17 MB % 260.70/37.18 % (3334770)Instructions burned: 1738 (million) % 260.70/37.18 % (3334772)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3930226234:i=10228:av=off:rtra=on_2821 on theBenchmark for (2821ds/10228Mi) % 260.70/37.18 % (3334762)Instruction limit reached! % 260.70/37.18 % (3334762)------------------------------ % 260.70/37.18 % (3334762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.70/37.18 % (3334762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.70/37.18 % (3334762)CaDiCaL version: 2.1.3 % 260.70/37.18 % (3334762)Termination reason: Instruction limit % 260.70/37.18 % (3334762)Termination phase: Saturation % 260.70/37.18 % (3334762)Time elapsed: 2.972 s % 260.70/37.18 % (3334762)Peak memory usage: 43 MB % 260.70/37.18 % (3334762)Instructions burned: 10266 (million) % 260.70/37.18 % (3334774)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3887642187:i=108564:rtra=on_2807 on theBenchmark for (2807ds/108564Mi) % 260.70/37.18 % Exception at run slice level % 260.70/37.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 260.70/37.18 % (3334776)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3909235019:i=7024:aac=none:rtra=on_2806 on theBenchmark for (2806ds/7024Mi) % 260.70/37.18 % (3334772)Instruction limit reached! % 260.70/37.18 % (3334772)------------------------------ % 260.70/37.18 % (3334772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.70/37.18 % (3334772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.70/37.18 % (3334772)CaDiCaL version: 2.1.3 % 260.70/37.18 % (3334772)Termination reason: Instruction limit % 260.70/37.18 % (3334772)Termination phase: Saturation % 260.70/37.18 % (3334772)Time elapsed: 3.259 s % 260.70/37.18 % (3334772)Peak memory usage: 41 MB % 260.70/37.18 % (3334772)Instructions burned: 10229 (million) % 260.70/37.18 % (3334778)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3076098084:i=7546:rtra=on:amm=off_2788 on theBenchmark for (2788ds/7546Mi) % 260.70/37.18 % (3334776)Instruction limit reached! % 260.70/37.18 % (3334776)------------------------------ % 260.70/37.18 % (3334776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 260.70/37.18 % (3334776)Linked with Z3 4.14.0.0 3cTerminated % 300.09/42.74 % Vampire exiting % 300.09/42.74 Terminated %------------------------------------------------------------------------------