%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW548_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 : n004.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:25 PM UTC 2026 % Result : Timeout 300.02s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW548_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 % Computer : n004.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 14:18:37 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.25/0.28 Running first-order model finding % 0.25/0.28 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 % 13.19/2.17 % (376931)Will run a generic schedule for satisfiability detection. % 13.19/2.17 % (376940)dis+10_1_sil=32000:sp=arity:random_seed=3297152673:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.19/2.17 % (376937)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=773478440_2999 on theBenchmark for (2999ds/0Mi) % 13.19/2.17 % (376938)% WARNING: option uhcvi not known. % 13.19/2.17 % Exception at run slice level % 13.19/2.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 13.19/2.17 % (376938)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1920360145:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.19/2.17 % (376939)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2583521925:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.19/2.17 % (376941)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1061375252:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.19/2.17 % (376942)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3289564942:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.19/2.17 % (376943)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1152989532:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.19/2.17 % (376947)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1621911768:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 13.19/2.17 % Exception at run slice level % 13.19/2.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 13.19/2.17 % (376940)Instruction limit reached! % 13.19/2.17 % (376940)------------------------------ % 13.19/2.17 % (376940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.19/2.17 % (376940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.17 % (376940)CaDiCaL version: 2.1.3 % 13.19/2.17 % (376940)Termination reason: Instruction limit % 13.19/2.17 % (376940)Termination phase: Saturation % 13.19/2.17 % (376940)Time elapsed: 0.056 s % 13.19/2.17 % (376940)Peak memory usage: 12 MB % 13.19/2.17 % (376940)Instructions burned: 109 (million) % 13.19/2.17 % (376955)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=2998060945:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 13.19/2.17 % (376954)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1905672916:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 13.19/2.17 % (376941)Instruction limit reached! % 13.19/2.17 % (376941)------------------------------ % 13.19/2.17 % (376941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.19/2.17 % (376941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.17 % (376941)CaDiCaL version: 2.1.3 % 13.19/2.17 % (376941)Termination reason: Instruction limit % 13.19/2.17 % (376941)Termination phase: Saturation % 13.19/2.17 % (376941)Time elapsed: 0.117 s % 13.19/2.17 % (376941)Peak memory usage: 13 MB % 13.19/2.17 % (376941)Instructions burned: 116 (million) % 13.19/2.17 % (376942)Instruction limit reached! % 13.19/2.17 % (376942)------------------------------ % 13.19/2.17 % (376942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.19/2.17 % (376942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.17 % (376942)CaDiCaL version: 2.1.3 % 13.19/2.17 % (376942)Termination reason: Instruction limit % 13.19/2.17 % (376942)Termination phase: Saturation % 13.19/2.17 % (376942)Time elapsed: 0.133 s % 13.19/2.17 % (376942)Peak memory usage: 13 MB % 13.19/2.17 % (376942)Instructions burned: 131 (million) % 13.19/2.17 % (376943)Instruction limit reached! % 13.19/2.17 % (376943)------------------------------ % 13.19/2.17 % (376943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.19/2.17 % (376943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.19/2.17 % (376943)CaDiCaL version: 2.1.3 % 13.19/2.17 % (376943)Termination reason: Instruction limit % 13.19/2.17 % (376943)Termination phase: Saturation % 13.19/2.17 % (376943)Time elapsed: 0.144 s % 13.19/2.17 % (376943)Peak memory usage: 13 MB % 13.19/2.17 % (376943)Instructions burned: 159 (million) % 13.19/2.17 % (376958)ott-21_1_sil=16000:fs=off:random_seed=1495306590:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.19/2.17 % (376959)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1758863128:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 34.60/5.17 % (376960)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1958501556:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 34.60/5.17 % Exception at run slice level % 34.60/5.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.60/5.17 % (376964)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=994912153:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 34.60/5.17 % (376954)Instruction limit reached! % 34.60/5.17 % (376954)------------------------------ % 34.60/5.17 % (376954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.60/5.17 % (376954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.60/5.17 % (376954)CaDiCaL version: 2.1.3 % 34.60/5.17 % (376954)Termination reason: Instruction limit % 34.60/5.17 % (376954)Termination phase: Saturation % 34.60/5.17 % (376954)Time elapsed: 0.141 s % 34.60/5.17 % (376954)Peak memory usage: 13 MB % 34.60/5.17 % (376954)Instructions burned: 132 (million) % 34.60/5.17 % (376966)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1415939628:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 34.60/5.17 % Exception at run slice level % 34.60/5.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.60/5.17 % (376968)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=2934471843:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 34.60/5.17 % (376958)Instruction limit reached! % 34.60/5.17 % (376958)------------------------------ % 34.60/5.17 % (376958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.60/5.17 % (376958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.60/5.17 % (376958)CaDiCaL version: 2.1.3 % 34.60/5.17 % (376958)Termination reason: Instruction limit % 34.60/5.17 % (376958)Termination phase: Saturation % 34.60/5.17 % (376958)Time elapsed: 0.150 s % 34.60/5.17 % (376958)Peak memory usage: 12 MB % 34.60/5.17 % (376958)Instructions burned: 180 (million) % 34.60/5.17 % (376955)Instruction limit reached! % 34.60/5.17 % (376955)------------------------------ % 34.60/5.17 % (376955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.60/5.17 % (376955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.60/5.17 % (376955)CaDiCaL version: 2.1.3 % 34.60/5.17 % (376955)Termination reason: Instruction limit % 34.60/5.17 % (376955)Termination phase: Saturation % 34.60/5.17 % (376955)Time elapsed: 0.251 s % 34.60/5.17 % (376955)Peak memory usage: 16 MB % 34.60/5.17 % (376955)Instructions burned: 685 (million) % 34.60/5.17 % (376971)fmb+10_1_sil=64000:random_seed=745872615:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi) % 34.60/5.17 % (376971)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 34.60/5.17 % Exception at run slice level % 34.60/5.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.60/5.17 % (376973)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3265452876:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi) % 34.60/5.17 % Exception at run slice level % 34.60/5.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.60/5.17 % (376970)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3282748608:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 34.60/5.17 % (376975)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1100258034:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi) % 34.60/5.17 % Exception at run slice level % 34.60/5.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 34.60/5.17 % (376978)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=55625635:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 34.60/5.17 % (376959)Instruction limit reached! % 34.60/5.17 % (376959)------------------------------ % 34.60/5.17 % (376959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 34.60/5.17 % (376959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.60/5.17 % (376959)CaDiCaL version: 2.1.3 % 34.60/5.17 % (376959)Termination reason: Instruction limit % 34.60/5.17 % (376959)Termination phase: Saturation % 101.86/14.61 % (376959)Time elapsed: 0.430 s % 101.86/14.61 % (376959)Peak memory usage: 14 MB % 101.86/14.61 % (376959)Instructions burned: 478 (million) % 101.86/14.61 % (376980)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2092593081:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi) % 101.86/14.61 % (376980)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 101.86/14.61 % (376968)Instruction limit reached! % 101.86/14.61 % (376968)------------------------------ % 101.86/14.61 % (376968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.86/14.61 % (376968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.86/14.61 % (376968)CaDiCaL version: 2.1.3 % 101.86/14.61 % (376968)Termination reason: Instruction limit % 101.86/14.61 % (376968)Termination phase: Saturation % 101.86/14.61 % (376968)Time elapsed: 0.650 s % 101.86/14.61 % (376968)Peak memory usage: 19 MB % 101.86/14.61 % (376968)Instructions burned: 692 (million) % 101.86/14.61 % (376982)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2367490657:i=6324_2990 on theBenchmark for (2990ds/6324Mi) % 101.86/14.61 % Exception at run slice level % 101.86/14.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.86/14.61 % (376984)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1883249883:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi) % 101.86/14.61 % Exception at run slice level % 101.86/14.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.86/14.61 % (376986)ott-2_1_sil=16000:newcnf=on:random_seed=2793932769:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi) % 101.86/14.61 % (376970)Instruction limit reached! % 101.86/14.61 % (376970)------------------------------ % 101.86/14.61 % (376970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.86/14.61 % (376970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.86/14.61 % (376970)CaDiCaL version: 2.1.3 % 101.86/14.61 % (376970)Termination reason: Instruction limit % 101.86/14.61 % (376970)Termination phase: Saturation % 101.86/14.61 % (376970)Time elapsed: 0.859 s % 101.86/14.61 % (376970)Peak memory usage: 19 MB % 101.86/14.61 % (376970)Instructions burned: 879 (million) % 101.86/14.61 % (376964)Instruction limit reached! % 101.86/14.61 % (376964)------------------------------ % 101.86/14.61 % (376964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.86/14.61 % (376964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.86/14.61 % (376964)CaDiCaL version: 2.1.3 % 101.86/14.61 % (376964)Termination reason: Instruction limit % 101.86/14.61 % (376964)Termination phase: Saturation % 101.86/14.61 % (376964)Time elapsed: 1.017 s % 101.86/14.61 % (376964)Peak memory usage: 15 MB % 101.86/14.61 % (376964)Instructions burned: 1180 (million) % 101.86/14.61 % (376988)ott+10_1_sil=32000:tgt=ground:random_seed=1470312626:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi) % 101.86/14.61 % (376989)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1518593578:i=54282_2987 on theBenchmark for (2987ds/54282Mi) % 101.86/14.61 % Exception at run slice level % 101.86/14.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 101.86/14.61 % (376992)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=621917457:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi) % 101.86/14.61 % (376986)Instruction limit reached! % 101.86/14.61 % (376986)------------------------------ % 101.86/14.61 % (376986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.86/14.61 % (376986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.86/14.61 % (376986)CaDiCaL version: 2.1.3 % 101.86/14.61 % (376986)Termination reason: Instruction limit % 101.86/14.61 % (376986)Termination phase: Saturation % 101.86/14.61 % (376986)Time elapsed: 0.577 s % 101.86/14.61 % (376986)Peak memory usage: 13 MB % 101.86/14.61 % (376986)Instructions burned: 869 (million) % 101.86/14.61 % (376995)dis+21_1_sil=32000:sas=cadical:random_seed=2172674250:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi) % 101.86/14.61 % (376980)Instruction limit reached! % 101.86/14.61 % (376980)------------------------------ % 101.86/14.61 % (376980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.86/14.61 % (376980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.86/14.61 % (376980)CaDiCaL version: 2.1.3 % 149.30/21.32 % (376980)Termination reason: Instruction limit % 149.30/21.32 % (376980)Termination phase: Saturation % 149.30/21.32 % (376980)Time elapsed: 1.223 s % 149.30/21.32 % (376980)Peak memory usage: 16 MB % 149.30/21.32 % (376980)Instructions burned: 1472 (million) % 149.30/21.32 % (377000)ott+11_1_sil=16000:gs=on:random_seed=1119305912:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi) % 149.30/21.32 % (376978)Instruction limit reached! % 149.30/21.32 % (376978)------------------------------ % 149.30/21.32 % (376978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.30/21.32 % (376978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.30/21.32 % (376978)CaDiCaL version: 2.1.3 % 149.30/21.32 % (376978)Termination reason: Instruction limit % 149.30/21.32 % (376978)Termination phase: Saturation % 149.30/21.32 % (376978)Time elapsed: 2.393 s % 149.30/21.32 % (376978)Peak memory usage: 39 MB % 149.30/21.32 % (376978)Instructions burned: 5133 (million) % 149.30/21.32 % (377004)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=690670307:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 149.30/21.32 % Exception at run slice level % 149.30/21.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.30/21.32 % (377006)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2477588714:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 149.30/21.32 % (377000)Instruction limit reached! % 149.30/21.32 % (377000)------------------------------ % 149.30/21.32 % (377000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.30/21.32 % (377000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.30/21.32 % (377000)CaDiCaL version: 2.1.3 % 149.30/21.32 % (377000)Termination reason: Instruction limit % 149.30/21.32 % (377000)Termination phase: Saturation % 149.30/21.32 % (377000)Time elapsed: 1.713 s % 149.30/21.32 % (377000)Peak memory usage: 14 MB % 149.30/21.32 % (377000)Instructions burned: 2252 (million) % 149.30/21.32 % (377008)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2174311876:i=29340_2963 on theBenchmark for (2963ds/29340Mi) % 149.30/21.32 % (376992)Instruction limit reached! % 149.30/21.32 % (376992)------------------------------ % 149.30/21.32 % (376992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.30/21.32 % (376992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.30/21.32 % (376992)CaDiCaL version: 2.1.3 % 149.30/21.32 % (376992)Termination reason: Instruction limit % 149.30/21.32 % (376992)Termination phase: Saturation % 149.30/21.32 % (376992)Time elapsed: 3.026 s % 149.30/21.32 % (376992)Peak memory usage: 26 MB % 149.30/21.32 % (376992)Instructions burned: 3512 (million) % 149.30/21.32 % (377012)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1858266629:i=5211_2956 on theBenchmark for (2956ds/5211Mi) % 149.30/21.32 % (377006)Instruction limit reached! % 149.30/21.32 % (377006)------------------------------ % 149.30/21.32 % (377006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 149.30/21.32 % (377006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.30/21.32 % (377006)CaDiCaL version: 2.1.3 % 149.30/21.32 % (377006)Termination reason: Instruction limit % 149.30/21.32 % (377006)Termination phase: Saturation % 149.30/21.32 % (377006)Time elapsed: 1.932 s % 149.30/21.32 % (377006)Peak memory usage: 22 MB % 149.30/21.32 % (377006)Instructions burned: 4591 (million) % 149.30/21.32 % (377014)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2421413305:i=5497:nm=2_2952 on theBenchmark for (2952ds/5497Mi) % 149.30/21.32 % Exception at run slice level % 149.30/21.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.30/21.32 % (377016)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1056808921:fmbsr=2:i=46332_2951 on theBenchmark for (2951ds/46332Mi) % 149.30/21.32 % Exception at run slice level % 149.30/21.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.30/21.32 % (377018)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2008668:i=14071_2951 on theBenchmark for (2951ds/14071Mi) % 149.30/21.32 % Exception at run slice level % 149.30/21.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 149.30/21.32 % (377020)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3451153448:i=22565:add=on:rawr=on_2951 on theBenchmark for (2951ds/22565Mi) % 170.60/24.31 % (376995)Instruction limit reached! % 170.60/24.31 % (376995)------------------------------ % 170.60/24.31 % (376995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.60/24.31 % (376995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.60/24.31 % (376995)CaDiCaL version: 2.1.3 % 170.60/24.31 % (376995)Termination reason: Instruction limit % 170.60/24.31 % (376995)Termination phase: Saturation % 170.60/24.31 % (376995)Time elapsed: 3.437 s % 170.60/24.31 % (376995)Peak memory usage: 31 MB % 170.60/24.31 % (376995)Instructions burned: 3773 (million) % 170.60/24.31 % (377022)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=92148243:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi) % 170.60/24.31 % (376988)Instruction limit reached! % 170.60/24.31 % (376988)------------------------------ % 170.60/24.31 % (376988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.60/24.31 % (376988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.60/24.31 % (376988)CaDiCaL version: 2.1.3 % 170.60/24.31 % (376988)Termination reason: Instruction limit % 170.60/24.31 % (376988)Termination phase: Saturation % 170.60/24.31 % (376988)Time elapsed: 4.246 s % 170.60/24.31 % (376988)Peak memory usage: 17 MB % 170.60/24.31 % (376988)Instructions burned: 5115 (million) % 170.60/24.31 % (377024)dis+10_16:1_sil=16000:random_seed=1604724511:i=9155:fsr=off_2944 on theBenchmark for (2944ds/9155Mi) % 170.60/24.31 % (377012)Instruction limit reached! % 170.60/24.31 % (377012)------------------------------ % 170.60/24.31 % (377012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.60/24.31 % (377012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.60/24.31 % (377012)CaDiCaL version: 2.1.3 % 170.60/24.31 % (377012)Termination reason: Instruction limit % 170.60/24.31 % (377012)Termination phase: Saturation % 170.60/24.31 % (377012)Time elapsed: 4.857 s % 170.60/24.31 % (377012)Peak memory usage: 52 MB % 170.60/24.31 % (377012)Instructions burned: 5211 (million) % 170.60/24.31 % (377027)ott-3_8_sil=64000:random_seed=1017542777:i=20139:bs=on_2907 on theBenchmark for (2907ds/20139Mi) % 170.60/24.31 % (377022)Instruction limit reached! % 170.60/24.31 % (377022)------------------------------ % 170.60/24.31 % (377022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.60/24.31 % (377022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.60/24.31 % (377022)CaDiCaL version: 2.1.3 % 170.60/24.31 % (377022)Termination reason: Instruction limit % 170.60/24.31 % (377022)Termination phase: Saturation % 170.60/24.31 % (377022)Time elapsed: 6.868 s % 170.60/24.31 % (377022)Peak memory usage: 29 MB % 170.60/24.31 % (377022)Instructions burned: 8173 (million) % 170.60/24.31 % (377036)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2181739421:fmbsr=2:i=32576_2879 on theBenchmark for (2879ds/32576Mi) % 170.60/24.31 % Exception at run slice level % 170.60/24.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 170.60/24.31 % (377038)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1399177507:i=11404_2879 on theBenchmark for (2879ds/11404Mi) % 170.60/24.31 % (377024)Instruction limit reached! % 170.60/24.31 % (377024)------------------------------ % 170.60/24.31 % (377024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.60/24.31 % (377024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.60/24.31 % (377024)CaDiCaL version: 2.1.3 % 170.60/24.31 % (377024)Termination reason: Instruction limit % 170.60/24.31 % (377024)Termination phase: Saturation % 170.60/24.31 % (377024)Time elapsed: 7.897 s % 170.60/24.31 % (377024)Peak memory usage: 62 MB % 170.60/24.31 % (377024)Instructions burned: 9155 (million) % 170.60/24.31 % (377194)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2403653101:i=14134_2865 on theBenchmark for (2865ds/14134Mi) % 170.60/24.31 % (377020)Instruction limit reached! % 170.60/24.31 % (377020)------------------------------ % 170.60/24.31 % (377020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 170.60/24.31 % (377020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.60/24.31 % (377020)CaDiCaL version: 2.1.3 % 170.60/24.31 % (377020)Termination reason: Instruction limit % 170.60/24.31 % (377020)Termination phase: Saturation % 170.60/24.31 % (377020)Time elapsed: 9.420 s % 170.60/24.31 % (377020)Peak memory usage: 78 MB % 170.60/24.31 % (377020)Instructions burned: 22568 (million) % 170.60/24.31 % (377196)dis+33_16_sil=32000:sac=on:random_seed=4227804035:i=15851:nm=0_2856 on theBenchmark for (2856ds/15851Mi) % 182.99/26.05 % (377196)Instruction limit reached! % 182.99/26.05 % (377196)------------------------------ % 182.99/26.05 % (377196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.99/26.05 % (377196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.99/26.05 % (377196)CaDiCaL version: 2.1.3 % 182.99/26.05 % (377196)Termination reason: Instruction limit % 182.99/26.05 % (377196)Termination phase: Saturation % 182.99/26.05 % (377196)Time elapsed: 4.723 s % 182.99/26.05 % (377196)Peak memory usage: 281 MB % 182.99/26.05 % (377196)Instructions burned: 15854 (million) % 182.99/26.05 % (377198)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=152340537:avsq=on:i=17627:add=on:amm=off_2809 on theBenchmark for (2809ds/17627Mi) % 182.99/26.05 % (377038)Instruction limit reached! % 182.99/26.05 % (377038)------------------------------ % 182.99/26.05 % (377038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.99/26.05 % (377038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.99/26.05 % (377038)CaDiCaL version: 2.1.3 % 182.99/26.05 % (377038)Termination reason: Instruction limit % 182.99/26.05 % (377038)Termination phase: Saturation % 182.99/26.05 % (377038)Time elapsed: 7.465 s % 182.99/26.05 % (377038)Peak memory usage: 154 MB % 182.99/26.05 % (377038)Instructions burned: 11404 (million) % 182.99/26.05 % (377200)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1692497871:s2a=on:i=53295_2804 on theBenchmark for (2804ds/53295Mi) % 182.99/26.05 % (377194)Instruction limit reached! % 182.99/26.05 % (377194)------------------------------ % 182.99/26.05 % (377194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.99/26.05 % (377194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.99/26.05 % (377194)CaDiCaL version: 2.1.3 % 182.99/26.05 % (377194)Termination reason: Instruction limit % 182.99/26.05 % (377194)Termination phase: Saturation % 182.99/26.05 % (377194)Time elapsed: 7.405 s % 182.99/26.05 % (377194)Peak memory usage: 47 MB % 182.99/26.05 % (377194)Instructions burned: 14134 (million) % 182.99/26.05 % (377027)Instruction limit reached! % 182.99/26.05 % (377027)------------------------------ % 182.99/26.05 % (377027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 182.99/26.05 % (377027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.99/26.05 % (377027)CaDiCaL version: 2.1.3 % 182.99/26.05 % (377027)Termination reason: Instruction limit % 182.99/26.05 % (377027)Termination phase: Saturation % 182.99/26.05 % (377027)Time elapsed: 11.591 s % 182.99/26.05 % (377027)Peak memory usage: 30 MB % 182.99/26.05 % (377027)Instructions burned: 20141 (million) % 182.99/26.05 % (377202)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=4115086962:i=26857:ins=20_2791 on theBenchmark for (2791ds/26857Mi) % 182.99/26.05 % (377203)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2277429651:i=28120:bs=on:fsr=off_2791 on theBenchmark for (2791ds/28120Mi) % 182.99/26.05 % Exception at run slice level % 182.99/26.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.99/26.05 % (377206)fmb+10_1_sil=256000:fmbss=7:random_seed=1755426549:fmbsr=1.6:i=182295_2790 on theBenchmark for (2790ds/182295Mi) % 182.99/26.05 % Exception at run slice level % 182.99/26.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.99/26.05 % (377208)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=4226300987:i=44625:gsp=on_2790 on theBenchmark for (2790ds/44625Mi) % 182.99/26.05 % (377208)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 182.99/26.05 % Exception at run slice level % 182.99/26.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.99/26.05 % (377210)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4177081473:i=160505_2790 on theBenchmark for (2790ds/160505Mi) % 182.99/26.05 % Exception at run slice level % 182.99/26.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.99/26.05 % (377212)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1898957918:fmbsr=1.3:i=225729_2790 on theBenchmark for (2790ds/225729Mi) % 182.99/26.05 % Exception at run slice level % 182.99/26.05 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 182.99/26.05 % (377214)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3618713552:fmbsr=2:i=185024:ins=7_2789 on theBenchmark for (2789ds/185024Mi) % 221.83/31.59 % Exception at run slice level % 221.83/31.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.83/31.59 % (377216)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3791102940:rtra=on_2789 on theBenchmark for (2789ds/0Mi) % 221.83/31.59 % Exception at run slice level % 221.83/31.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 221.83/31.59 % (377218)% WARNING: option uhcvi not known. % 221.83/31.59 % (377218)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3060744943:i=271062:add=off:rtra=on:rawr=on_2789 on theBenchmark for (2789ds/271062Mi) % 221.83/31.59 % (377008)Instruction limit reached! % 221.83/31.59 % (377008)------------------------------ % 221.83/31.59 % (377008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.83/31.59 % (377008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.83/31.59 % (377008)CaDiCaL version: 2.1.3 % 221.83/31.59 % (377008)Termination reason: Instruction limit % 221.83/31.59 % (377008)Termination phase: Saturation % 221.83/31.59 % (377008)Time elapsed: 18.502 s % 221.83/31.59 % (377008)Peak memory usage: 799 MB % 221.83/31.59 % (377008)Instructions burned: 29340 (million) % 221.83/31.59 % (377220)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=900804660:i=176048:add=on:rtra=on:rawr=on_2777 on theBenchmark for (2777ds/176048Mi) % 221.83/31.59 % (377198)Instruction limit reached! % 221.83/31.59 % (377198)------------------------------ % 221.83/31.59 % (377198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.83/31.59 % (377198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.83/31.59 % (377198)CaDiCaL version: 2.1.3 % 221.83/31.59 % (377198)Termination reason: Instruction limit % 221.83/31.59 % (377198)Termination phase: Saturation % 221.83/31.59 % (377198)Time elapsed: 4.555 s % 221.83/31.59 % (377198)Peak memory usage: 44 MB % 221.83/31.59 % (377198)Instructions burned: 17631 (million) % 221.83/31.59 % (377222)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2275002169:i=206:fgj=on:rtra=on_2763 on theBenchmark for (2763ds/206Mi) % 221.83/31.59 % (377222)Instruction limit reached! % 221.83/31.59 % (377222)------------------------------ % 221.83/31.59 % (377222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.83/31.59 % (377222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.83/31.59 % (377222)CaDiCaL version: 2.1.3 % 221.83/31.59 % (377222)Termination reason: Instruction limit % 221.83/31.59 % (377222)Termination phase: Saturation % 221.83/31.59 % (377222)Time elapsed: 0.067 s % 221.83/31.59 % (377222)Peak memory usage: 13 MB % 221.83/31.59 % (377222)Instructions burned: 211 (million) % 221.83/31.59 % (377224)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2813429194:i=232:rtra=on_2762 on theBenchmark for (2762ds/232Mi) % 221.83/31.59 % (377224)Instruction limit reached! % 221.83/31.59 % (377224)------------------------------ % 221.83/31.59 % (377224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.83/31.59 % (377224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.83/31.59 % (377224)CaDiCaL version: 2.1.3 % 221.83/31.59 % (377224)Termination reason: Instruction limit % 221.83/31.59 % (377224)Termination phase: Saturation % 221.83/31.59 % (377224)Time elapsed: 0.078 s % 221.83/31.59 % (377224)Peak memory usage: 14 MB % 221.83/31.59 % (377224)Instructions burned: 234 (million) % 221.83/31.59 % (377226)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1116133618:i=262:rtra=on_2761 on theBenchmark for (2761ds/262Mi) % 221.83/31.59 % (377226)Instruction limit reached! % 221.83/31.59 % (377226)------------------------------ % 221.83/31.59 % (377226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 221.83/31.59 % (377226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.83/31.59 % (377226)CaDiCaL version: 2.1.3 % 221.83/31.59 % (377226)Termination reason: Instruction limit % 221.83/31.59 % (377226)Termination phase: Saturation % 221.83/31.59 % (377226)Time elapsed: 0.086 s % 221.83/31.59 % (377226)Peak memory usage: 17 MB % 221.83/31.59 % (377226)Instructions burned: 265 (million) % 221.83/31.59 % (377228)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=1345624810:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2760 on theBenchmark for (2760ds/318Mi) % 221.83/31.59 % (377228)Instruction limit reached! % 221.83/31.59 % (377228)------------------------------ % 221.83/31.59 % (377228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.40/40.37 % (377228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.40/40.37 % (377228)CaDiCaL version: 2.1.3 % 284.40/40.37 % (377228)Termination reason: Instruction limit % 284.40/40.37 % (377228)Termination phase: Saturation % 284.40/40.37 % (377228)Time elapsed: 0.104 s % 284.40/40.37 % (377228)Peak memory usage: 19 MB % 284.40/40.37 % (377228)Instructions burned: 321 (million) % 284.40/40.37 % (377230)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1452692853:i=1428:nm=2:rtra=on_2759 on theBenchmark for (2759ds/1428Mi) % 284.40/40.37 % Exception at run slice level % 284.40/40.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 284.40/40.37 % (377232)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1141308700:i=262:bd=preordered:rtra=on:fsd=on_2759 on theBenchmark for (2759ds/262Mi) % 284.40/40.37 % (377232)Instruction limit reached! % 284.40/40.37 % (377232)------------------------------ % 284.40/40.37 % (377232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.40/40.37 % (377232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.40/40.37 % (377232)CaDiCaL version: 2.1.3 % 284.40/40.37 % (377232)Termination reason: Instruction limit % 284.40/40.37 % (377232)Termination phase: Saturation % 284.40/40.37 % (377232)Time elapsed: 0.087 s % 284.40/40.37 % (377232)Peak memory usage: 14 MB % 284.40/40.37 % (377232)Instructions burned: 265 (million) % 284.40/40.37 % (377234)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=1190205771:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2758 on theBenchmark for (2758ds/1368Mi) % 284.40/40.37 % (377234)Instruction limit reached! % 284.40/40.37 % (377234)------------------------------ % 284.40/40.37 % (377234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.40/40.37 % (377234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.40/40.37 % (377234)CaDiCaL version: 2.1.3 % 284.40/40.37 % (377234)Termination reason: Instruction limit % 284.40/40.37 % (377234)Termination phase: Saturation % 284.40/40.37 % (377234)Time elapsed: 0.360 s % 284.40/40.37 % (377234)Peak memory usage: 17 MB % 284.40/40.37 % (377234)Instructions burned: 1371 (million) % 284.40/40.37 % (377236)ott-21_1_sil=16000:si=on:fs=off:random_seed=978778530:i=360:av=off:fsr=off:rtra=on_2754 on theBenchmark for (2754ds/360Mi) % 284.40/40.37 % (377236)Instruction limit reached! % 284.40/40.37 % (377236)------------------------------ % 284.40/40.37 % (377236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.40/40.37 % (377236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.40/40.37 % (377236)CaDiCaL version: 2.1.3 % 284.40/40.37 % (377236)Termination reason: Instruction limit % 284.40/40.37 % (377236)Termination phase: Saturation % 284.40/40.37 % (377236)Time elapsed: 0.089 s % 284.40/40.37 % (377236)Peak memory usage: 13 MB % 284.40/40.37 % (377236)Instructions burned: 363 (million) % 284.40/40.37 % (377238)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1283916902:i=954:bd=all:rtra=on_2753 on theBenchmark for (2753ds/954Mi) % 284.40/40.37 % (377238)Instruction limit reached! % 284.40/40.37 % (377238)------------------------------ % 284.40/40.37 % (377238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.40/40.37 % (377238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.40/40.37 % (377238)CaDiCaL version: 2.1.3 % 284.40/40.37 % (377238)Termination reason: Instruction limit % 284.40/40.37 % (377238)Termination phase: Saturation % 284.40/40.37 % (377238)Time elapsed: 0.286 s % 284.40/40.37 % (377238)Peak memory usage: 15 MB % 284.40/40.37 % (377238)Instructions burned: 954 (million) % 284.40/40.37 % (377240)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=596385667:fmbsr=1.3:i=1730:ins=25:rtra=on_2750 on theBenchmark for (2750ds/1730Mi) % 284.40/40.37 % Exception at run slice level % 284.40/40.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 284.40/40.37 % (377242)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1702472634:i=2358:rtra=on_2750 on theBenchmark for (2750ds/2358Mi) % 284.40/40.37 % (377242)Instruction limit reached! % 284.40/40.37 % (377242)------------------------------ % 284.40/40.37 % (377242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.40/40.37 % (377242)Linked with Z3 4.14.0.0 3c47fd96cfTerminated % 300.02/42.54 Terminated %------------------------------------------------------------------------------