%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV767_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 : n010.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:22 PM UTC 2026 % Result : Timeout 300.69s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV767_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.18 % Computer : n010.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.19 % WCLimit : 300 % 0.08/0.19 % DateTime : Mon Sep 28 12:30:32 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.21 Running first-order model finding % 0.08/0.21 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 % 8.02/1.44 % (1893862)Will run a generic schedule for satisfiability detection. % 8.02/1.44 % (1893873)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4112138629:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.02/1.44 % (1893868)% WARNING: option uhcvi not known. % 8.02/1.44 % (1893867)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2155567257_2999 on theBenchmark for (2999ds/0Mi) % 8.02/1.44 % (1893871)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3875146866:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.02/1.44 % (1893872)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=320073774:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.02/1.44 % (1893870)dis+10_1_sil=32000:sp=arity:random_seed=757324539:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.02/1.44 % (1893869)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=111885678:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.02/1.44 % (1893868)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=454346404:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.02/1.44 % Exception at run slice level % 8.02/1.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.02/1.44 % (1893881)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3888754293:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.02/1.44 % Exception at run slice level % 8.02/1.44 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.02/1.44 % (1893873)Instruction limit reached! % 8.02/1.44 % (1893873)------------------------------ % 8.02/1.44 % (1893873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.02/1.44 % (1893873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.02/1.44 % (1893873)CaDiCaL version: 2.1.3 % 8.02/1.44 % (1893873)Termination reason: Instruction limit % 8.02/1.44 % (1893873)Termination phase: Saturation % 8.02/1.44 % (1893873)Time elapsed: 0.046 s % 8.02/1.44 % (1893873)Peak memory usage: 13 MB % 8.02/1.44 % (1893873)Instructions burned: 160 (million) % 8.02/1.44 % (1893883)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3008245617:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.02/1.44 % (1893884)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=2481256091:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.02/1.44 % (1893870)Instruction limit reached! % 8.02/1.44 % (1893870)------------------------------ % 8.02/1.44 % (1893870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.02/1.44 % (1893870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.02/1.44 % (1893870)CaDiCaL version: 2.1.3 % 8.02/1.44 % (1893870)Termination reason: Instruction limit % 8.02/1.44 % (1893870)Termination phase: Saturation % 8.02/1.44 % (1893870)Time elapsed: 0.061 s % 8.02/1.44 % (1893870)Peak memory usage: 12 MB % 8.02/1.44 % (1893870)Instructions burned: 103 (million) % 8.02/1.44 % (1893871)Instruction limit reached! % 8.02/1.44 % (1893871)------------------------------ % 8.02/1.44 % (1893871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.02/1.44 % (1893871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.02/1.44 % (1893871)CaDiCaL version: 2.1.3 % 8.02/1.44 % (1893871)Termination reason: Instruction limit % 8.02/1.44 % (1893871)Termination phase: Saturation % 8.02/1.44 % (1893871)Time elapsed: 0.071 s % 8.02/1.44 % (1893871)Peak memory usage: 12 MB % 8.02/1.44 % (1893871)Instructions burned: 117 (million) % 8.02/1.44 % (1893872)Instruction limit reached! % 8.02/1.44 % (1893872)------------------------------ % 8.02/1.44 % (1893872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.02/1.44 % (1893872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.02/1.44 % (1893872)CaDiCaL version: 2.1.3 % 8.02/1.44 % (1893872)Termination reason: Instruction limit % 8.02/1.44 % (1893872)Termination phase: Saturation % 8.02/1.44 % (1893872)Time elapsed: 0.074 s % 8.02/1.44 % (1893872)Peak memory usage: 12 MB % 8.02/1.44 % (1893872)Instructions burned: 131 (million) % 8.02/1.44 % (1893887)ott-21_1_sil=16000:fs=off:random_seed=374630084:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 8.02/1.44 % (1893888)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=770378940:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 21.10/3.29 % (1893889)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=646165235:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.10/3.29 % Exception at run slice level % 21.10/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.29 % (1893893)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2961636495:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.10/3.29 % (1893883)Instruction limit reached! % 21.10/3.29 % (1893883)------------------------------ % 21.10/3.29 % (1893883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.29 % (1893883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.29 % (1893883)CaDiCaL version: 2.1.3 % 21.10/3.29 % (1893883)Termination reason: Instruction limit % 21.10/3.29 % (1893883)Termination phase: Saturation % 21.10/3.29 % (1893883)Time elapsed: 0.074 s % 21.10/3.29 % (1893883)Peak memory usage: 13 MB % 21.10/3.29 % (1893883)Instructions burned: 132 (million) % 21.10/3.29 % (1893895)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4125983676:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.10/3.29 % Exception at run slice level % 21.10/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.29 % (1893897)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=1499482174: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) % 21.10/3.29 % (1893887)Instruction limit reached! % 21.10/3.29 % (1893887)------------------------------ % 21.10/3.29 % (1893887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.29 % (1893887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.29 % (1893887)CaDiCaL version: 2.1.3 % 21.10/3.29 % (1893887)Termination reason: Instruction limit % 21.10/3.29 % (1893887)Termination phase: Saturation % 21.10/3.29 % (1893887)Time elapsed: 0.087 s % 21.10/3.29 % (1893887)Peak memory usage: 12 MB % 21.10/3.29 % (1893887)Instructions burned: 182 (million) % 21.10/3.29 % (1893899)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2475984575:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.10/3.29 % (1893884)Instruction limit reached! % 21.10/3.29 % (1893884)------------------------------ % 21.10/3.29 % (1893884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.29 % (1893884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.29 % (1893884)CaDiCaL version: 2.1.3 % 21.10/3.29 % (1893884)Termination reason: Instruction limit % 21.10/3.29 % (1893884)Termination phase: Saturation % 21.10/3.29 % (1893884)Time elapsed: 0.178 s % 21.10/3.29 % (1893884)Peak memory usage: 16 MB % 21.10/3.29 % (1893884)Instructions burned: 686 (million) % 21.10/3.29 % (1893901)fmb+10_1_sil=64000:random_seed=3601976910:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.10/3.29 % (1893901)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.10/3.29 % Exception at run slice level % 21.10/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.29 % (1893903)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1938613408:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.10/3.29 % Exception at run slice level % 21.10/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.29 % (1893905)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1340936496:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 21.10/3.29 % Exception at run slice level % 21.10/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.10/3.29 % (1893907)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1228221599:i=5131_2997 on theBenchmark for (2997ds/5131Mi) % 21.10/3.29 % (1893888)Instruction limit reached! % 21.10/3.29 % (1893888)------------------------------ % 21.10/3.29 % (1893888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.10/3.29 % (1893888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.19/12.89 % (1893888)CaDiCaL version: 2.1.3 % 89.19/12.89 % (1893888)Termination reason: Instruction limit % 89.19/12.89 % (1893888)Termination phase: Saturation % 89.19/12.89 % (1893888)Time elapsed: 0.271 s % 89.19/12.89 % (1893888)Peak memory usage: 13 MB % 89.19/12.89 % (1893888)Instructions burned: 477 (million) % 89.19/12.89 % (1893909)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1015875582:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 89.19/12.89 % (1893909)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 89.19/12.89 % (1893897)Instruction limit reached! % 89.19/12.89 % (1893897)------------------------------ % 89.19/12.89 % (1893897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.19/12.89 % (1893897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.19/12.89 % (1893897)CaDiCaL version: 2.1.3 % 89.19/12.89 % (1893897)Termination reason: Instruction limit % 89.19/12.89 % (1893897)Termination phase: Saturation % 89.19/12.89 % (1893897)Time elapsed: 0.417 s % 89.19/12.89 % (1893897)Peak memory usage: 18 MB % 89.19/12.89 % (1893897)Instructions burned: 693 (million) % 89.19/12.89 % (1893911)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2825836923:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 89.19/12.89 % Exception at run slice level % 89.19/12.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 89.19/12.89 % (1893913)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1718503232:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 89.19/12.89 % (1893899)Instruction limit reached! % 89.19/12.89 % (1893899)------------------------------ % 89.19/12.89 % (1893899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.19/12.89 % (1893899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.19/12.89 % (1893899)CaDiCaL version: 2.1.3 % 89.19/12.89 % (1893899)Termination reason: Instruction limit % 89.19/12.89 % (1893899)Termination phase: Saturation % 89.19/12.89 % (1893899)Time elapsed: 0.453 s % 89.19/12.89 % (1893899)Peak memory usage: 18 MB % 89.19/12.89 % (1893899)Instructions burned: 880 (million) % 89.19/12.89 % Exception at run slice level % 89.19/12.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 89.19/12.89 % (1893916)ott+10_1_sil=32000:tgt=ground:random_seed=2508447069:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi) % 89.19/12.89 % (1893915)ott-2_1_sil=16000:newcnf=on:random_seed=475766:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 89.19/12.89 % (1893893)Instruction limit reached! % 89.19/12.89 % (1893893)------------------------------ % 89.19/12.89 % (1893893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.19/12.89 % (1893893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.19/12.89 % (1893893)CaDiCaL version: 2.1.3 % 89.19/12.89 % (1893893)Termination reason: Instruction limit % 89.19/12.89 % (1893893)Termination phase: Saturation % 89.19/12.89 % (1893893)Time elapsed: 0.677 s % 89.19/12.89 % (1893893)Peak memory usage: 23 MB % 89.19/12.89 % (1893893)Instructions burned: 1179 (million) % 89.19/12.89 % (1893919)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=603672870:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 89.19/12.89 % Exception at run slice level % 89.19/12.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 89.19/12.89 % (1893921)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3853920255:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 89.19/12.89 % (1893915)Instruction limit reached! % 89.19/12.89 % (1893915)------------------------------ % 89.19/12.89 % (1893915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.19/12.89 % (1893915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.19/12.89 % (1893915)CaDiCaL version: 2.1.3 % 89.19/12.89 % (1893915)Termination reason: Instruction limit % 89.19/12.89 % (1893915)Termination phase: Saturation % 89.19/12.89 % (1893915)Time elapsed: 0.501 s % 89.19/12.89 % (1893915)Peak memory usage: 17 MB % 89.19/12.89 % (1893915)Instructions burned: 869 (million) % 89.19/12.89 % (1893909)Instruction limit reached! % 89.19/12.89 % (1893909)------------------------------ % 89.19/12.89 % (1893909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 89.19/12.89 % (1893909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.88/15.59 % (1893909)CaDiCaL version: 2.1.3 % 107.88/15.59 % (1893909)Termination reason: Instruction limit % 107.88/15.59 % (1893909)Termination phase: Saturation % 107.88/15.59 % (1893909)Time elapsed: 0.801 s % 107.88/15.59 % (1893909)Peak memory usage: 31 MB % 107.88/15.59 % (1893909)Instructions burned: 1472 (million) % 107.88/15.59 % (1893923)dis+21_1_sil=32000:sas=cadical:random_seed=1299350875:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 107.88/15.59 % (1893925)ott+11_1_sil=16000:gs=on:random_seed=1509702385:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi) % 107.88/15.59 % (1893907)Instruction limit reached! % 107.88/15.59 % (1893907)------------------------------ % 107.88/15.59 % (1893907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.88/15.59 % (1893907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.88/15.59 % (1893907)CaDiCaL version: 2.1.3 % 107.88/15.59 % (1893907)Termination reason: Instruction limit % 107.88/15.59 % (1893907)Termination phase: Saturation % 107.88/15.59 % (1893907)Time elapsed: 1.319 s % 107.88/15.59 % (1893907)Peak memory usage: 29 MB % 107.88/15.59 % (1893907)Instructions burned: 5135 (million) % 107.88/15.59 % (1893927)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=847770161:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 107.88/15.59 % Exception at run slice level % 107.88/15.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.88/15.59 % (1893929)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=399815231:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi) % 107.88/15.59 % (1893925)Instruction limit reached! % 107.88/15.59 % (1893925)------------------------------ % 107.88/15.59 % (1893925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.88/15.59 % (1893925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.88/15.59 % (1893925)CaDiCaL version: 2.1.3 % 107.88/15.59 % (1893925)Termination reason: Instruction limit % 107.88/15.59 % (1893925)Termination phase: Saturation % 107.88/15.59 % (1893925)Time elapsed: 1.187 s % 107.88/15.59 % (1893925)Peak memory usage: 25 MB % 107.88/15.59 % (1893925)Instructions burned: 2253 (million) % 107.88/15.59 % (1893931)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=894743084:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 107.88/15.59 % (1893921)Instruction limit reached! % 107.88/15.59 % (1893921)------------------------------ % 107.88/15.59 % (1893921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.88/15.59 % (1893921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.88/15.59 % (1893921)CaDiCaL version: 2.1.3 % 107.88/15.59 % (1893921)Termination reason: Instruction limit % 107.88/15.59 % (1893921)Termination phase: Saturation % 107.88/15.59 % (1893921)Time elapsed: 1.841 s % 107.88/15.59 % (1893921)Peak memory usage: 27 MB % 107.88/15.59 % (1893921)Instructions burned: 3513 (million) % 107.88/15.59 % (1893933)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3051084133:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 107.88/15.59 % (1893929)Instruction limit reached! % 107.88/15.59 % (1893929)------------------------------ % 107.88/15.59 % (1893929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.88/15.59 % (1893929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.88/15.59 % (1893929)CaDiCaL version: 2.1.3 % 107.88/15.59 % (1893929)Termination reason: Instruction limit % 107.88/15.59 % (1893929)Termination phase: Saturation % 107.88/15.59 % (1893929)Time elapsed: 1.389 s % 107.88/15.59 % (1893929)Peak memory usage: 55 MB % 107.88/15.59 % (1893929)Instructions burned: 4592 (million) % 107.88/15.59 % (1893923)Instruction limit reached! % 107.88/15.59 % (1893923)------------------------------ % 107.88/15.59 % (1893923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.88/15.59 % (1893923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.88/15.59 % (1893923)CaDiCaL version: 2.1.3 % 107.88/15.59 % (1893923)Termination reason: Instruction limit % 107.88/15.59 % (1893923)Termination phase: Saturation % 107.88/15.59 % (1893923)Time elapsed: 1.845 s % 107.88/15.59 % (1893923)Peak memory usage: 30 MB % 107.88/15.59 % (1893923)Instructions burned: 3774 (million) % 107.88/15.59 % (1893935)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2093120901:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 107.88/15.59 % Exception at run slice level % 107.88/15.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 158.66/22.68 % (1893936)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4191435502:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 158.66/22.68 % (1893938)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2454360248:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 158.66/22.68 % Exception at run slice level % 158.66/22.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 158.66/22.68 % Exception at run slice level % 158.66/22.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 158.66/22.68 % (1893942)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1781210742:i=8173:av=off_2969 on theBenchmark for (2969ds/8173Mi) % 158.66/22.68 % (1893941)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1055483090:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 158.66/22.68 % (1893916)Instruction limit reached! % 158.66/22.68 % (1893916)------------------------------ % 158.66/22.68 % (1893916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.66/22.68 % (1893916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.66/22.68 % (1893916)CaDiCaL version: 2.1.3 % 158.66/22.68 % (1893916)Termination reason: Instruction limit % 158.66/22.68 % (1893916)Termination phase: Saturation % 158.66/22.68 % (1893916)Time elapsed: 2.894 s % 158.66/22.68 % (1893916)Peak memory usage: 41 MB % 158.66/22.68 % (1893916)Instructions burned: 5114 (million) % 158.66/22.68 % (1893945)dis+10_16:1_sil=16000:random_seed=1876988509:i=9155:fsr=off_2964 on theBenchmark for (2964ds/9155Mi) % 158.66/22.68 % (1893933)Instruction limit reached! % 158.66/22.68 % (1893933)------------------------------ % 158.66/22.68 % (1893933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.66/22.68 % (1893933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.66/22.68 % (1893933)CaDiCaL version: 2.1.3 % 158.66/22.68 % (1893933)Termination reason: Instruction limit % 158.66/22.68 % (1893933)Termination phase: Saturation % 158.66/22.68 % (1893933)Time elapsed: 2.524 s % 158.66/22.68 % (1893933)Peak memory usage: 38 MB % 158.66/22.68 % (1893933)Instructions burned: 5213 (million) % 158.66/22.68 % (1893947)ott-3_8_sil=64000:random_seed=1006743704:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi) % 158.66/22.68 % (1893942)Instruction limit reached! % 158.66/22.68 % (1893942)------------------------------ % 158.66/22.68 % (1893942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.66/22.68 % (1893942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.66/22.68 % (1893942)CaDiCaL version: 2.1.3 % 158.66/22.68 % (1893942)Termination reason: Instruction limit % 158.66/22.68 % (1893942)Termination phase: Saturation % 158.66/22.68 % (1893942)Time elapsed: 4.344 s % 158.66/22.68 % (1893942)Peak memory usage: 68 MB % 158.66/22.68 % (1893942)Instructions burned: 8175 (million) % 158.66/22.68 % (1893949)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3856759235:fmbsr=2:i=32576_2925 on theBenchmark for (2925ds/32576Mi) % 158.66/22.68 % Exception at run slice level % 158.66/22.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 158.66/22.68 % (1893951)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3413349498:i=11404_2925 on theBenchmark for (2925ds/11404Mi) % 158.66/22.68 % (1893945)Instruction limit reached! % 158.66/22.68 % (1893945)------------------------------ % 158.66/22.68 % (1893945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.66/22.68 % (1893945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.66/22.68 % (1893945)CaDiCaL version: 2.1.3 % 158.66/22.68 % (1893945)Termination reason: Instruction limit % 158.66/22.68 % (1893945)Termination phase: Saturation % 158.66/22.68 % (1893945)Time elapsed: 4.324 s % 158.66/22.68 % (1893945)Peak memory usage: 44 MB % 158.66/22.68 % (1893945)Instructions burned: 9155 (million) % 158.66/22.68 % (1893953)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=672581286:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 158.66/22.68 % (1893941)Instruction limit reached! % 158.66/22.68 % (1893941)------------------------------ % 158.66/22.68 % (1893941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 158.66/22.68 % (1893941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.66/22.68 % (1893941)CaDiCaL version: 2.1.3 % 158.66/22.68 % (1893941)Termination reason: Instruction limit % 172.23/24.56 % (1893941)Termination phase: Saturation % 172.23/24.56 % (1893941)Time elapsed: 9.559 s % 172.23/24.56 % (1893941)Peak memory usage: 157 MB % 172.23/24.56 % (1893941)Instructions burned: 22566 (million) % 172.23/24.56 % (1893955)dis+33_16_sil=32000:sac=on:random_seed=2804355844:i=15851:nm=0_2873 on theBenchmark for (2873ds/15851Mi) % 172.23/24.56 % (1893951)Instruction limit reached! % 172.23/24.56 % (1893951)------------------------------ % 172.23/24.56 % (1893951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.23/24.56 % (1893951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.23/24.56 % (1893951)CaDiCaL version: 2.1.3 % 172.23/24.56 % (1893951)Termination reason: Instruction limit % 172.23/24.56 % (1893951)Termination phase: Saturation % 172.23/24.56 % (1893951)Time elapsed: 5.709 s % 172.23/24.56 % (1893951)Peak memory usage: 54 MB % 172.23/24.56 % (1893951)Instructions burned: 11406 (million) % 172.23/24.56 % (1893957)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=146057166:avsq=on:i=17627:add=on:amm=off_2867 on theBenchmark for (2867ds/17627Mi) % 172.23/24.56 % (1893931)Instruction limit reached! % 172.23/24.56 % (1893931)------------------------------ % 172.23/24.56 % (1893931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.23/24.56 % (1893931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.23/24.56 % (1893931)CaDiCaL version: 2.1.3 % 172.23/24.56 % (1893931)Termination reason: Instruction limit % 172.23/24.56 % (1893931)Termination phase: Saturation % 172.23/24.56 % (1893931)Time elapsed: 11.174 s % 172.23/24.56 % (1893931)Peak memory usage: 172 MB % 172.23/24.56 % (1893931)Instructions burned: 29343 (million) % 172.23/24.56 % (1893959)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3771559832:s2a=on:i=53295_2863 on theBenchmark for (2863ds/53295Mi) % 172.23/24.56 % (1893947)Instruction limit reached! % 172.23/24.56 % (1893947)------------------------------ % 172.23/24.56 % (1893947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.23/24.56 % (1893947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.23/24.56 % (1893947)CaDiCaL version: 2.1.3 % 172.23/24.56 % (1893947)Termination reason: Instruction limit % 172.23/24.56 % (1893947)Termination phase: Saturation % 172.23/24.56 % (1893947)Time elapsed: 9.490 s % 172.23/24.56 % (1893947)Peak memory usage: 66 MB % 172.23/24.56 % (1893947)Instructions burned: 20139 (million) % 172.23/24.56 % (1893961)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=484157537:i=26857:ins=20_2852 on theBenchmark for (2852ds/26857Mi) % 172.23/24.56 % Exception at run slice level % 172.23/24.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 172.23/24.56 % (1893963)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2445110174:i=28120:bs=on:fsr=off_2851 on theBenchmark for (2851ds/28120Mi) % 172.23/24.56 % (1893953)Instruction limit reached! % 172.23/24.56 % (1893953)------------------------------ % 172.23/24.56 % (1893953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 172.23/24.56 % (1893953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.23/24.56 % (1893953)CaDiCaL version: 2.1.3 % 172.23/24.56 % (1893953)Termination reason: Instruction limit % 172.23/24.56 % (1893953)Termination phase: Saturation % 172.23/24.56 % (1893953)Time elapsed: 7.297 s % 172.23/24.56 % (1893953)Peak memory usage: 90 MB % 172.23/24.56 % (1893953)Instructions burned: 14135 (million) % 172.23/24.56 % (1893965)fmb+10_1_sil=256000:fmbss=7:random_seed=3619327239:fmbsr=1.6:i=182295_2847 on theBenchmark for (2847ds/182295Mi) % 172.23/24.56 % Exception at run slice level % 172.23/24.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 172.23/24.56 % (1893967)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=251620412:i=44625:gsp=on_2847 on theBenchmark for (2847ds/44625Mi) % 172.23/24.56 % (1893967)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 172.23/24.56 % Exception at run slice level % 172.23/24.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 172.23/24.56 % (1893969)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=566479835:i=160505_2846 on theBenchmark for (2846ds/160505Mi) % 172.23/24.56 % Exception at run slice level % 172.23/24.56 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 172.23/24.56 % (1893971)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2993852454:fmbsr=1.3:i=225729_2846 on theBenchmark for (2846ds/225729Mi) % 208.43/29.68 % Exception at run slice level % 208.43/29.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.43/29.68 % (1893973)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2196739056:fmbsr=2:i=185024:ins=7_2846 on theBenchmark for (2846ds/185024Mi) % 208.43/29.68 % Exception at run slice level % 208.43/29.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.43/29.68 % (1893975)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2998356407:rtra=on_2845 on theBenchmark for (2845ds/0Mi) % 208.43/29.68 % Exception at run slice level % 208.43/29.68 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 208.43/29.68 % (1893977)% WARNING: option uhcvi not known. % 208.43/29.68 % (1893977)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1198303534:i=271062:add=off:rtra=on:rawr=on_2845 on theBenchmark for (2845ds/271062Mi) % 208.43/29.68 % (1893955)Instruction limit reached! % 208.43/29.68 % (1893955)------------------------------ % 208.43/29.68 % (1893955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.43/29.68 % (1893955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.43/29.68 % (1893955)CaDiCaL version: 2.1.3 % 208.43/29.68 % (1893955)Termination reason: Instruction limit % 208.43/29.68 % (1893955)Termination phase: Saturation % 208.43/29.68 % (1893955)Time elapsed: 8.068 s % 208.43/29.68 % (1893955)Peak memory usage: 99 MB % 208.43/29.68 % (1893955)Instructions burned: 15857 (million) % 208.43/29.68 % (1893979)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1445024139:i=176048:add=on:rtra=on:rawr=on_2792 on theBenchmark for (2792ds/176048Mi) % 208.43/29.68 % (1893957)Instruction limit reached! % 208.43/29.68 % (1893957)------------------------------ % 208.43/29.68 % (1893957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.43/29.68 % (1893957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.43/29.68 % (1893957)CaDiCaL version: 2.1.3 % 208.43/29.68 % (1893957)Termination reason: Instruction limit % 208.43/29.68 % (1893957)Termination phase: Saturation % 208.43/29.68 % (1893957)Time elapsed: 8.727 s % 208.43/29.68 % (1893957)Peak memory usage: 97 MB % 208.43/29.68 % (1893957)Instructions burned: 17628 (million) % 208.43/29.68 % (1893981)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2799173284:i=206:fgj=on:rtra=on_2780 on theBenchmark for (2780ds/206Mi) % 208.43/29.68 % (1893981)Instruction limit reached! % 208.43/29.68 % (1893981)------------------------------ % 208.43/29.68 % (1893981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.43/29.68 % (1893981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.43/29.68 % (1893981)CaDiCaL version: 2.1.3 % 208.43/29.68 % (1893981)Termination reason: Instruction limit % 208.43/29.68 % (1893981)Termination phase: Saturation % 208.43/29.68 % (1893981)Time elapsed: 0.120 s % 208.43/29.68 % (1893981)Peak memory usage: 13 MB % 208.43/29.68 % (1893981)Instructions burned: 206 (million) % 208.43/29.68 % (1893983)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3327154987:i=232:rtra=on_2778 on theBenchmark for (2778ds/232Mi) % 208.43/29.68 % (1893983)Instruction limit reached! % 208.43/29.68 % (1893983)------------------------------ % 208.43/29.68 % (1893983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.43/29.68 % (1893983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.43/29.68 % (1893983)CaDiCaL version: 2.1.3 % 208.43/29.68 % (1893983)Termination reason: Instruction limit % 208.43/29.68 % (1893983)Termination phase: Saturation % 208.43/29.68 % (1893983)Time elapsed: 0.142 s % 208.43/29.68 % (1893983)Peak memory usage: 13 MB % 208.43/29.68 % (1893983)Instructions burned: 233 (million) % 208.43/29.68 % (1893985)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1275498813:i=262:rtra=on_2777 on theBenchmark for (2777ds/262Mi) % 208.43/29.68 % (1893985)Instruction limit reached! % 208.43/29.68 % (1893985)------------------------------ % 208.43/29.68 % (1893985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 208.43/29.68 % (1893985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.43/29.68 % (1893985)CaDiCaL version: 2.1.3 % 208.43/29.68 % (1893985)Termination reason: Instruction limit % 208.43/29.68 % (1893985)Termination phase: Saturation % 235.87/33.50 % (1893985)Time elapsed: 0.149 s % 235.87/33.50 % (1893985)Peak memory usage: 14 MB % 235.87/33.50 % (1893985)Instructions burned: 262 (million) % 235.87/33.50 % (1893987)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2731980527:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2775 on theBenchmark for (2775ds/318Mi) % 235.87/33.50 % (1893987)Instruction limit reached! % 235.87/33.50 % (1893987)------------------------------ % 235.87/33.50 % (1893987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.87/33.50 % (1893987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.87/33.50 % (1893987)CaDiCaL version: 2.1.3 % 235.87/33.50 % (1893987)Termination reason: Instruction limit % 235.87/33.50 % (1893987)Termination phase: Saturation % 235.87/33.50 % (1893987)Time elapsed: 0.149 s % 235.87/33.50 % (1893987)Peak memory usage: 12 MB % 235.87/33.50 % (1893987)Instructions burned: 319 (million) % 235.87/33.50 % (1893989)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2460248863:i=1428:nm=2:rtra=on_2773 on theBenchmark for (2773ds/1428Mi) % 235.87/33.50 % Exception at run slice level % 235.87/33.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 235.87/33.50 % (1893991)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2467581989:i=262:bd=preordered:rtra=on:fsd=on_2773 on theBenchmark for (2773ds/262Mi) % 235.87/33.50 % (1893991)Instruction limit reached! % 235.87/33.50 % (1893991)------------------------------ % 235.87/33.50 % (1893991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.87/33.50 % (1893991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.87/33.50 % (1893991)CaDiCaL version: 2.1.3 % 235.87/33.50 % (1893991)Termination reason: Instruction limit % 235.87/33.50 % (1893991)Termination phase: Saturation % 235.87/33.50 % (1893991)Time elapsed: 0.156 s % 235.87/33.50 % (1893991)Peak memory usage: 15 MB % 235.87/33.50 % (1893991)Instructions burned: 263 (million) % 235.87/33.50 % (1893993)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=1701349260:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2771 on theBenchmark for (2771ds/1368Mi) % 235.87/33.50 % (1893993)Instruction limit reached! % 235.87/33.50 % (1893993)------------------------------ % 235.87/33.50 % (1893993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.87/33.50 % (1893993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.87/33.50 % (1893993)CaDiCaL version: 2.1.3 % 235.87/33.50 % (1893993)Termination reason: Instruction limit % 235.87/33.50 % (1893993)Termination phase: Saturation % 235.87/33.50 % (1893993)Time elapsed: 0.680 s % 235.87/33.50 % (1893993)Peak memory usage: 20 MB % 235.87/33.50 % (1893993)Instructions burned: 1368 (million) % 235.87/33.50 % (1893995)ott-21_1_sil=16000:si=on:fs=off:random_seed=2339499405:i=360:av=off:fsr=off:rtra=on_2764 on theBenchmark for (2764ds/360Mi) % 235.87/33.50 % (1893995)Instruction limit reached! % 235.87/33.50 % (1893995)------------------------------ % 235.87/33.50 % (1893995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.87/33.50 % (1893995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.87/33.50 % (1893995)CaDiCaL version: 2.1.3 % 235.87/33.50 % (1893995)Termination reason: Instruction limit % 235.87/33.50 % (1893995)Termination phase: Saturation % 235.87/33.50 % (1893995)Time elapsed: 0.160 s % 235.87/33.50 % (1893995)Peak memory usage: 13 MB % 235.87/33.50 % (1893995)Instructions burned: 362 (million) % 235.87/33.50 % (1893997)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3396884245:i=954:bd=all:rtra=on_2762 on theBenchmark for (2762ds/954Mi) % 235.87/33.50 % (1893997)Instruction limit reached! % 235.87/33.50 % (1893997)------------------------------ % 235.87/33.50 % (1893997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.87/33.50 % (1893997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.87/33.50 % (1893997)CaDiCaL version: 2.1.3 % 235.87/33.50 % (1893997)Termination reason: Instruction limit % 235.87/33.50 % (1893997)Termination phase: Saturation % 235.87/33.50 % (1893997)Time elapsed: 0.562 s % 235.87/33.50 % (1893997)Peak memory usage: 15 MB % 235.87/33.50 % (1893997)Instructions burned: 956 (million) % 235.87/33.50 % (1893999)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=554737242:fmbsr=1.3:i=1730:ins=25:rtra=on_2756 on theBenchmark for (2756ds/1730Mi) % 235.87/33.50 % Exception at run slice level % 235.87/33.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.17/37.76 % (1894001)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=632331107:i=2358:rtra=on_2756 on theBenchmark for (2756ds/2358Mi) % 265.17/37.76 % (1894001)Instruction limit reached! % 265.17/37.76 % (1894001)------------------------------ % 265.17/37.76 % (1894001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.76 % (1894001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.76 % (1894001)CaDiCaL version: 2.1.3 % 265.17/37.76 % (1894001)Termination reason: Instruction limit % 265.17/37.76 % (1894001)Termination phase: Saturation % 265.17/37.76 % (1894001)Time elapsed: 1.406 s % 265.17/37.76 % (1894001)Peak memory usage: 34 MB % 265.17/37.76 % (1894001)Instructions burned: 2358 (million) % 265.17/37.76 % (1894003)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2462702311:i=1778:ins=1:rtra=on_2742 on theBenchmark for (2742ds/1778Mi) % 265.17/37.76 % Exception at run slice level % 265.17/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.17/37.76 % (1894005)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=1950539264:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2742 on theBenchmark for (2742ds/1384Mi) % 265.17/37.76 % (1894005)Instruction limit reached! % 265.17/37.76 % (1894005)------------------------------ % 265.17/37.76 % (1894005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.76 % (1894005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.76 % (1894005)CaDiCaL version: 2.1.3 % 265.17/37.76 % (1894005)Termination reason: Instruction limit % 265.17/37.76 % (1894005)Termination phase: Saturation % 265.17/37.76 % (1894005)Time elapsed: 0.761 s % 265.17/37.76 % (1894005)Peak memory usage: 23 MB % 265.17/37.76 % (1894005)Instructions burned: 1385 (million) % 265.17/37.76 % (1894007)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2266184678:i=1758:kws=inv_precedence:fsr=off:rtra=on_2734 on theBenchmark for (2734ds/1758Mi) % 265.17/37.76 % (1894007)Instruction limit reached! % 265.17/37.76 % (1894007)------------------------------ % 265.17/37.76 % (1894007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.76 % (1894007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.76 % (1894007)CaDiCaL version: 2.1.3 % 265.17/37.76 % (1894007)Termination reason: Instruction limit % 265.17/37.76 % (1894007)Termination phase: Saturation % 265.17/37.76 % (1894007)Time elapsed: 0.942 s % 265.17/37.76 % (1894007)Peak memory usage: 22 MB % 265.17/37.76 % (1894007)Instructions burned: 1759 (million) % 265.17/37.76 % (1894009)fmb+10_1_sil=64000:si=on:random_seed=1567299452:i=44122:nm=2:rtra=on:gsp=on_2724 on theBenchmark for (2724ds/44122Mi) % 265.17/37.76 % (1894009)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 265.17/37.76 % Exception at run slice level % 265.17/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.17/37.76 % (1894011)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=924046099:i=19030:nm=5:rtra=on_2724 on theBenchmark for (2724ds/19030Mi) % 265.17/37.76 % Exception at run slice level % 265.17/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.17/37.76 % (1894013)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2902411527:fmbsr=1.7:i=1840:rtra=on_2723 on theBenchmark for (2723ds/1840Mi) % 265.17/37.76 % Exception at run slice level % 265.17/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 265.17/37.76 % (1894015)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2965827083:i=10262:rtra=on_2723 on theBenchmark for (2723ds/10262Mi) % 265.17/37.76 % (1893963)Instruction limit reached! % 265.17/37.76 % (1893963)------------------------------ % 265.17/37.76 % (1893963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 265.17/37.76 % (1893963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.17/37.76 % (1893963)CaDiCaL version: 2.1.3 % 265.17/37.76 % (1893963)Termination reason: Instruction limit % 265.17/37.76 % (1893963)Termination phase: Saturation % 265.17/37.76 % (1893963)Time elapsed: 14.632 s % 265.17/37.76 % (1893963)Peak memory usage: 142 MB % 265.17/37.76 % (1893Terminated % 300.69/42.64 % Vampire exiting % 300.69/42.64 Terminated %------------------------------------------------------------------------------