%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW471_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 : n008.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:07 PM UTC 2026 % Result : Timeout 300.07s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW471_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.08/0.19 % Computer : n008.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % 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 14:04:39 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.22 Running first-order model finding % 0.08/0.22 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 % 7.37/1.33 % (2264636)Will run a generic schedule for satisfiability detection. % 7.37/1.33 % (2264647)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3433263929:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.37/1.33 % (2264642)% WARNING: option uhcvi not known. % 7.37/1.33 % (2264644)dis+10_1_sil=32000:sp=arity:random_seed=4154163821:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.37/1.33 % (2264641)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1694234079_2999 on theBenchmark for (2999ds/0Mi) % 7.37/1.33 % (2264643)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2759519504:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.37/1.33 % (2264642)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3895917210:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.37/1.33 % (2264645)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2824754263:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.37/1.33 % (2264646)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3005529278:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.37/1.33 % Exception at run slice level % 7.37/1.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.37/1.33 % (2264655)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4031548370:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.37/1.33 % Exception at run slice level % 7.37/1.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 7.37/1.33 % (2264647)Instruction limit reached! % 7.37/1.33 % (2264647)------------------------------ % 7.37/1.33 % (2264647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.33 % (2264647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.33 % (2264647)CaDiCaL version: 2.1.3 % 7.37/1.33 % (2264647)Termination reason: Instruction limit % 7.37/1.33 % (2264647)Termination phase: Saturation % 7.37/1.33 % (2264647)Time elapsed: 0.049 s % 7.37/1.33 % (2264647)Peak memory usage: 13 MB % 7.37/1.33 % (2264647)Instructions burned: 160 (million) % 7.37/1.33 % (2264658)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=2265650767:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.37/1.33 % (2264644)Instruction limit reached! % 7.37/1.33 % (2264644)------------------------------ % 7.37/1.33 % (2264644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.33 % (2264644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.33 % (2264644)CaDiCaL version: 2.1.3 % 7.37/1.33 % (2264644)Termination reason: Instruction limit % 7.37/1.33 % (2264644)Termination phase: Saturation % 7.37/1.33 % (2264644)Time elapsed: 0.057 s % 7.37/1.33 % (2264644)Peak memory usage: 12 MB % 7.37/1.33 % (2264644)Instructions burned: 103 (million) % 7.37/1.33 % (2264657)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3103410791:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.37/1.33 % (2264645)Instruction limit reached! % 7.37/1.33 % (2264645)------------------------------ % 7.37/1.33 % (2264645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.33 % (2264645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.33 % (2264645)CaDiCaL version: 2.1.3 % 7.37/1.33 % (2264645)Termination reason: Instruction limit % 7.37/1.33 % (2264645)Termination phase: Saturation % 7.37/1.33 % (2264645)Time elapsed: 0.063 s % 7.37/1.33 % (2264645)Peak memory usage: 12 MB % 7.37/1.33 % (2264645)Instructions burned: 116 (million) % 7.37/1.33 % (2264661)ott-21_1_sil=16000:fs=off:random_seed=2213070066:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.37/1.33 % (2264646)Instruction limit reached! % 7.37/1.33 % (2264646)------------------------------ % 7.37/1.33 % (2264646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.37/1.33 % (2264646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/1.33 % (2264646)CaDiCaL version: 2.1.3 % 7.37/1.33 % (2264646)Termination reason: Instruction limit % 7.37/1.33 % (2264646)Termination phase: Saturation % 7.37/1.33 % (2264646)Time elapsed: 0.079 s % 7.37/1.33 % (2264646)Peak memory usage: 12 MB % 7.37/1.33 % (2264646)Instructions burned: 131 (million) % 7.37/1.33 % (2264662)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3476520942:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi) % 19.88/3.07 % (2264664)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3847147248:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 19.88/3.07 % Exception at run slice level % 19.88/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.88/3.07 % (2264667)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3474373382:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 19.88/3.07 % (2264657)Instruction limit reached! % 19.88/3.07 % (2264657)------------------------------ % 19.88/3.07 % (2264657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.88/3.07 % (2264657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.88/3.07 % (2264657)CaDiCaL version: 2.1.3 % 19.88/3.07 % (2264657)Termination reason: Instruction limit % 19.88/3.07 % (2264657)Termination phase: Saturation % 19.88/3.07 % (2264657)Time elapsed: 0.080 s % 19.88/3.07 % (2264657)Peak memory usage: 13 MB % 19.88/3.07 % (2264657)Instructions burned: 131 (million) % 19.88/3.07 % (2264669)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2625590262:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 19.88/3.07 % Exception at run slice level % 19.88/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.88/3.07 % (2264661)Instruction limit reached! % 19.88/3.07 % (2264661)------------------------------ % 19.88/3.07 % (2264661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.88/3.07 % (2264661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.88/3.07 % (2264661)CaDiCaL version: 2.1.3 % 19.88/3.07 % (2264661)Termination reason: Instruction limit % 19.88/3.07 % (2264661)Termination phase: Saturation % 19.88/3.07 % (2264661)Time elapsed: 0.094 s % 19.88/3.07 % (2264661)Peak memory usage: 12 MB % 19.88/3.07 % (2264661)Instructions burned: 181 (million) % 19.88/3.07 % (2264671)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=3346261705:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi) % 19.88/3.07 % (2264672)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=38964940:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 19.88/3.07 % (2264658)Instruction limit reached! % 19.88/3.07 % (2264658)------------------------------ % 19.88/3.07 % (2264658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.88/3.07 % (2264658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.88/3.07 % (2264658)CaDiCaL version: 2.1.3 % 19.88/3.07 % (2264658)Termination reason: Instruction limit % 19.88/3.07 % (2264658)Termination phase: Saturation % 19.88/3.07 % (2264658)Time elapsed: 0.179 s % 19.88/3.07 % (2264658)Peak memory usage: 15 MB % 19.88/3.07 % (2264658)Instructions burned: 685 (million) % 19.88/3.07 % (2264675)fmb+10_1_sil=64000:random_seed=3131249438:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 19.88/3.07 % (2264675)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 19.88/3.07 % Exception at run slice level % 19.88/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.88/3.07 % (2264677)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3625790613:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 19.88/3.07 % Exception at run slice level % 19.88/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.88/3.07 % (2264679)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3023636791:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 19.88/3.07 % Exception at run slice level % 19.88/3.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 19.88/3.07 % (2264681)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3212832706:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 19.88/3.07 % (2264662)Instruction limit reached! % 19.88/3.07 % (2264662)------------------------------ % 19.88/3.07 % (2264662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 19.88/3.07 % (2264662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.39/9.37 % (2264662)CaDiCaL version: 2.1.3 % 64.39/9.37 % (2264662)Termination reason: Instruction limit % 64.39/9.37 % (2264662)Termination phase: Saturation % 64.39/9.37 % (2264662)Time elapsed: 0.270 s % 64.39/9.37 % (2264662)Peak memory usage: 13 MB % 64.39/9.37 % (2264662)Instructions burned: 478 (million) % 64.39/9.37 % (2264683)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2511030328:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi) % 64.39/9.37 % (2264683)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 64.39/9.37 % (2264671)Instruction limit reached! % 64.39/9.37 % (2264671)------------------------------ % 64.39/9.37 % (2264671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.39/9.37 % (2264671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.39/9.37 % (2264671)CaDiCaL version: 2.1.3 % 64.39/9.37 % (2264671)Termination reason: Instruction limit % 64.39/9.37 % (2264671)Termination phase: Saturation % 64.39/9.37 % (2264671)Time elapsed: 0.391 s % 64.39/9.37 % (2264671)Peak memory usage: 16 MB % 64.39/9.37 % (2264671)Instructions burned: 693 (million) % 64.39/9.37 % (2264685)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=772218975:i=6324_2993 on theBenchmark for (2993ds/6324Mi) % 64.39/9.37 % Exception at run slice level % 64.39/9.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.39/9.37 % (2264687)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=386508936:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi) % 64.39/9.37 % Exception at run slice level % 64.39/9.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.39/9.37 % (2264689)ott-2_1_sil=16000:newcnf=on:random_seed=1533031016:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 64.39/9.37 % (2264672)Instruction limit reached! % 64.39/9.37 % (2264672)------------------------------ % 64.39/9.37 % (2264672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.39/9.37 % (2264672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.39/9.37 % (2264672)CaDiCaL version: 2.1.3 % 64.39/9.37 % (2264672)Termination reason: Instruction limit % 64.39/9.37 % (2264672)Termination phase: Saturation % 64.39/9.37 % (2264672)Time elapsed: 0.500 s % 64.39/9.37 % (2264672)Peak memory usage: 19 MB % 64.39/9.37 % (2264672)Instructions burned: 879 (million) % 64.39/9.37 % (2264691)ott+10_1_sil=32000:tgt=ground:random_seed=407308498:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 64.39/9.37 % (2264667)Instruction limit reached! % 64.39/9.37 % (2264667)------------------------------ % 64.39/9.37 % (2264667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.39/9.37 % (2264667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.39/9.37 % (2264667)CaDiCaL version: 2.1.3 % 64.39/9.37 % (2264667)Termination reason: Instruction limit % 64.39/9.37 % (2264667)Termination phase: Saturation % 64.39/9.37 % (2264667)Time elapsed: 0.614 s % 64.39/9.37 % (2264667)Peak memory usage: 17 MB % 64.39/9.37 % (2264667)Instructions burned: 1182 (million) % 64.39/9.37 % (2264693)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2691941964:i=54282_2992 on theBenchmark for (2992ds/54282Mi) % 64.39/9.37 % Exception at run slice level % 64.39/9.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 64.39/9.37 % (2264695)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1552603635:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 64.39/9.37 % (2264689)Instruction limit reached! % 64.39/9.37 % (2264689)------------------------------ % 64.39/9.37 % (2264689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 64.39/9.37 % (2264689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.39/9.37 % (2264689)CaDiCaL version: 2.1.3 % 64.39/9.37 % (2264689)Termination reason: Instruction limit % 64.39/9.37 % (2264689)Termination phase: Saturation % 64.39/9.37 % (2264689)Time elapsed: 0.392 s % 64.39/9.37 % (2264689)Peak memory usage: 13 MB % 64.39/9.37 % (2264689)Instructions burned: 870 (million) % 64.39/9.37 % (2264697)dis+21_1_sil=32000:sas=cadical:random_seed=3377548358:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 64.39/9.37 % (2264683)Instruction limit reached! % 64.39/9.37 % (2264683)------------------------------ % 64.39/9.37 % (2264683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.67/15.45 % (2264683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.67/15.45 % (2264683)CaDiCaL version: 2.1.3 % 107.67/15.45 % (2264683)Termination reason: Instruction limit % 107.67/15.45 % (2264683)Termination phase: Saturation % 107.67/15.45 % (2264683)Time elapsed: 0.696 s % 107.67/15.45 % (2264683)Peak memory usage: 17 MB % 107.67/15.45 % (2264683)Instructions burned: 1473 (million) % 107.67/15.45 % (2264699)ott+11_1_sil=16000:gs=on:random_seed=198984722:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 107.67/15.45 % (2264681)Instruction limit reached! % 107.67/15.45 % (2264681)------------------------------ % 107.67/15.45 % (2264681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.67/15.45 % (2264681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.67/15.45 % (2264681)CaDiCaL version: 2.1.3 % 107.67/15.45 % (2264681)Termination reason: Instruction limit % 107.67/15.45 % (2264681)Termination phase: Saturation % 107.67/15.45 % (2264681)Time elapsed: 1.327 s % 107.67/15.45 % (2264681)Peak memory usage: 27 MB % 107.67/15.45 % (2264681)Instructions burned: 5134 (million) % 107.67/15.45 % (2264702)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1823556045:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 107.67/15.45 % Exception at run slice level % 107.67/15.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.67/15.45 % (2264704)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=550022335: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.67/15.45 % (2264699)Instruction limit reached! % 107.67/15.45 % (2264699)------------------------------ % 107.67/15.45 % (2264699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.67/15.45 % (2264699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.67/15.45 % (2264699)CaDiCaL version: 2.1.3 % 107.67/15.45 % (2264699)Termination reason: Instruction limit % 107.67/15.45 % (2264699)Termination phase: Saturation % 107.67/15.45 % (2264699)Time elapsed: 1.152 s % 107.67/15.45 % (2264699)Peak memory usage: 22 MB % 107.67/15.45 % (2264699)Instructions burned: 2253 (million) % 107.67/15.45 % (2264706)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3000650082:i=29340_2977 on theBenchmark for (2977ds/29340Mi) % 107.67/15.45 % (2264695)Instruction limit reached! % 107.67/15.45 % (2264695)------------------------------ % 107.67/15.45 % (2264695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.67/15.45 % (2264695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.67/15.45 % (2264695)CaDiCaL version: 2.1.3 % 107.67/15.45 % (2264695)Termination reason: Instruction limit % 107.67/15.45 % (2264695)Termination phase: Saturation % 107.67/15.45 % (2264695)Time elapsed: 1.878 s % 107.67/15.45 % (2264695)Peak memory usage: 31 MB % 107.67/15.45 % (2264695)Instructions burned: 3514 (million) % 107.67/15.45 % (2264708)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=464755285:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 107.67/15.45 % (2264704)Instruction limit reached! % 107.67/15.45 % (2264704)------------------------------ % 107.67/15.45 % (2264704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 107.67/15.45 % (2264704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.67/15.45 % (2264704)CaDiCaL version: 2.1.3 % 107.67/15.45 % (2264704)Termination reason: Instruction limit % 107.67/15.45 % (2264704)Termination phase: Saturation % 107.67/15.45 % (2264704)Time elapsed: 1.064 s % 107.67/15.45 % (2264704)Peak memory usage: 41 MB % 107.67/15.45 % (2264704)Instructions burned: 4594 (million) % 107.67/15.45 % (2264710)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2466300682:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi) % 107.67/15.45 % Exception at run slice level % 107.67/15.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.67/15.45 % (2264712)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3757152358:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi) % 107.67/15.45 % Exception at run slice level % 107.67/15.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 107.67/15.45 % (2264714)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1567395566:i=14071_2971 on theBenchmark for (2971ds/14071Mi) % 107.67/15.45 % Exception at run slice level % 124.00/17.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.00/17.75 % (2264716)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1699690164:i=22565:add=on:rawr=on_2971 on theBenchmark for (2971ds/22565Mi) % 124.00/17.75 % (2264697)Instruction limit reached! % 124.00/17.75 % (2264697)------------------------------ % 124.00/17.75 % (2264697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.00/17.75 % (2264697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/17.75 % (2264697)CaDiCaL version: 2.1.3 % 124.00/17.75 % (2264697)Termination reason: Instruction limit % 124.00/17.75 % (2264697)Termination phase: Saturation % 124.00/17.75 % (2264697)Time elapsed: 2.068 s % 124.00/17.75 % (2264697)Peak memory usage: 30 MB % 124.00/17.75 % (2264697)Instructions burned: 3774 (million) % 124.00/17.75 % (2264718)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3320423264:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 124.00/17.75 % (2264691)Instruction limit reached! % 124.00/17.75 % (2264691)------------------------------ % 124.00/17.75 % (2264691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.00/17.75 % (2264691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/17.75 % (2264691)CaDiCaL version: 2.1.3 % 124.00/17.75 % (2264691)Termination reason: Instruction limit % 124.00/17.75 % (2264691)Termination phase: Saturation % 124.00/17.75 % (2264691)Time elapsed: 2.508 s % 124.00/17.75 % (2264691)Peak memory usage: 17 MB % 124.00/17.75 % (2264691)Instructions burned: 5114 (million) % 124.00/17.75 % (2264720)dis+10_16:1_sil=16000:random_seed=565323705:i=9155:fsr=off_2967 on theBenchmark for (2967ds/9155Mi) % 124.00/17.75 % (2264708)Instruction limit reached! % 124.00/17.75 % (2264708)------------------------------ % 124.00/17.75 % (2264708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.00/17.75 % (2264708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/17.75 % (2264708)CaDiCaL version: 2.1.3 % 124.00/17.75 % (2264708)Termination reason: Instruction limit % 124.00/17.75 % (2264708)Termination phase: Saturation % 124.00/17.75 % (2264708)Time elapsed: 1.496 s % 124.00/17.75 % (2264708)Peak memory usage: 45 MB % 124.00/17.75 % (2264708)Instructions burned: 5214 (million) % 124.00/17.75 % (2264722)ott-3_8_sil=64000:random_seed=3269980057:i=20139:bs=on_2957 on theBenchmark for (2957ds/20139Mi) % 124.00/17.75 % (2264718)Instruction limit reached! % 124.00/17.75 % (2264718)------------------------------ % 124.00/17.75 % (2264718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.00/17.75 % (2264718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/17.75 % (2264718)CaDiCaL version: 2.1.3 % 124.00/17.75 % (2264718)Termination reason: Instruction limit % 124.00/17.75 % (2264718)Termination phase: Saturation % 124.00/17.75 % (2264718)Time elapsed: 3.661 s % 124.00/17.75 % (2264718)Peak memory usage: 19 MB % 124.00/17.75 % (2264718)Instructions burned: 8174 (million) % 124.00/17.75 % (2264724)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=662124593:fmbsr=2:i=32576_2931 on theBenchmark for (2931ds/32576Mi) % 124.00/17.75 % Exception at run slice level % 124.00/17.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.00/17.75 % (2264726)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1490284389:i=11404_2931 on theBenchmark for (2931ds/11404Mi) % 124.00/17.75 % (2264720)Instruction limit reached! % 124.00/17.75 % (2264720)------------------------------ % 124.00/17.75 % (2264720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.00/17.75 % (2264720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/17.75 % (2264720)CaDiCaL version: 2.1.3 % 124.00/17.75 % (2264720)Termination reason: Instruction limit % 124.00/17.75 % (2264720)Termination phase: Saturation % 124.00/17.75 % (2264720)Time elapsed: 4.843 s % 124.00/17.75 % (2264720)Peak memory usage: 55 MB % 124.00/17.75 % (2264720)Instructions burned: 9155 (million) % 124.00/17.75 % (2264728)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=627254402:i=14134_2918 on theBenchmark for (2918ds/14134Mi) % 124.00/17.75 % (2264722)Instruction limit reached! % 124.00/17.75 % (2264722)------------------------------ % 124.00/17.75 % (2264722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.00/17.75 % (2264722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.00/17.75 % (2264722)CaDiCaL version: 2.1.3 % 131.84/18.81 % (2264722)Termination reason: Instruction limit % 131.84/18.81 % (2264722)Termination phase: Saturation % 131.84/18.81 % (2264722)Time elapsed: 4.909 s % 131.84/18.81 % (2264722)Peak memory usage: 32 MB % 131.84/18.81 % (2264722)Instructions burned: 20141 (million) % 131.84/18.81 % (2264730)dis+33_16_sil=32000:sac=on:random_seed=2890069772:i=15851:nm=0_2908 on theBenchmark for (2908ds/15851Mi) % 131.84/18.81 % (2264730)Instruction limit reached! % 131.84/18.81 % (2264730)------------------------------ % 131.84/18.81 % (2264730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.84/18.81 % (2264730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.84/18.81 % (2264730)CaDiCaL version: 2.1.3 % 131.84/18.81 % (2264730)Termination reason: Instruction limit % 131.84/18.81 % (2264730)Termination phase: Saturation % 131.84/18.81 % (2264730)Time elapsed: 3.791 s % 131.84/18.81 % (2264730)Peak memory usage: 29 MB % 131.84/18.81 % (2264730)Instructions burned: 15855 (million) % 131.84/18.81 % (2264732)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=693281504:avsq=on:i=17627:add=on:amm=off_2870 on theBenchmark for (2870ds/17627Mi) % 131.84/18.81 % (2264716)Instruction limit reached! % 131.84/18.81 % (2264716)------------------------------ % 131.84/18.81 % (2264716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.84/18.81 % (2264716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.84/18.81 % (2264716)CaDiCaL version: 2.1.3 % 131.84/18.81 % (2264716)Termination reason: Instruction limit % 131.84/18.81 % (2264716)Termination phase: Saturation % 131.84/18.81 % (2264716)Time elapsed: 10.304 s % 131.84/18.81 % (2264716)Peak memory usage: 34 MB % 131.84/18.81 % (2264716)Instructions burned: 22566 (million) % 131.84/18.81 % (2264734)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2291422555:s2a=on:i=53295_2868 on theBenchmark for (2868ds/53295Mi) % 131.84/18.81 % (2264726)Instruction limit reached! % 131.84/18.81 % (2264726)------------------------------ % 131.84/18.81 % (2264726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.84/18.81 % (2264726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.84/18.81 % (2264726)CaDiCaL version: 2.1.3 % 131.84/18.81 % (2264726)Termination reason: Instruction limit % 131.84/18.81 % (2264726)Termination phase: Saturation % 131.84/18.81 % (2264726)Time elapsed: 7.227 s % 131.84/18.81 % (2264726)Peak memory usage: 113 MB % 131.84/18.81 % (2264726)Instructions burned: 11405 (million) % 131.84/18.81 % (2264736)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1468912884:i=26857:ins=20_2858 on theBenchmark for (2858ds/26857Mi) % 131.84/18.81 % Exception at run slice level % 131.84/18.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.84/18.81 % (2264738)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3502036173:i=28120:bs=on:fsr=off_2858 on theBenchmark for (2858ds/28120Mi) % 131.84/18.81 % (2264706)Instruction limit reached! % 131.84/18.81 % (2264706)------------------------------ % 131.84/18.81 % (2264706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.84/18.81 % (2264706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.84/18.81 % (2264706)CaDiCaL version: 2.1.3 % 131.84/18.81 % (2264706)Termination reason: Instruction limit % 131.84/18.81 % (2264706)Termination phase: Saturation % 131.84/18.81 % (2264706)Time elapsed: 12.821 s % 131.84/18.81 % (2264706)Peak memory usage: 74 MB % 131.84/18.81 % (2264706)Instructions burned: 29340 (million) % 131.84/18.81 % (2264740)fmb+10_1_sil=256000:fmbss=7:random_seed=2513153798:fmbsr=1.6:i=182295_2848 on theBenchmark for (2848ds/182295Mi) % 131.84/18.81 % Exception at run slice level % 131.84/18.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.84/18.81 % (2264742)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=774006371:i=44625:gsp=on_2848 on theBenchmark for (2848ds/44625Mi) % 131.84/18.81 % (2264742)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 131.84/18.81 % Exception at run slice level % 131.84/18.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.84/18.81 % (2264744)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=704075634:i=160505_2848 on theBenchmark for (2848ds/160505Mi) % 131.84/18.81 % Exception at run slice level % 131.84/18.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.84/18.81 % (2264746)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3632571879:fmbsr=1.3:i=225729_2847 on theBenchmark for (2847ds/225729Mi) % 160.21/22.83 % Exception at run slice level % 160.21/22.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 160.21/22.83 % (2264748)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=748163132:fmbsr=2:i=185024:ins=7_2847 on theBenchmark for (2847ds/185024Mi) % 160.21/22.83 % Exception at run slice level % 160.21/22.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 160.21/22.83 % (2264750)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2670214478:rtra=on_2847 on theBenchmark for (2847ds/0Mi) % 160.21/22.83 % Exception at run slice level % 160.21/22.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 160.21/22.83 % (2264752)% WARNING: option uhcvi not known. % 160.21/22.83 % (2264752)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3590749836:i=271062:add=off:rtra=on:rawr=on_2847 on theBenchmark for (2847ds/271062Mi) % 160.21/22.83 % (2264728)Instruction limit reached! % 160.21/22.83 % (2264728)------------------------------ % 160.21/22.83 % (2264728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.21/22.83 % (2264728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.21/22.83 % (2264728)CaDiCaL version: 2.1.3 % 160.21/22.83 % (2264728)Termination reason: Instruction limit % 160.21/22.83 % (2264728)Termination phase: Saturation % 160.21/22.83 % (2264728)Time elapsed: 7.760 s % 160.21/22.83 % (2264728)Peak memory usage: 53 MB % 160.21/22.83 % (2264728)Instructions burned: 14135 (million) % 160.21/22.83 % (2264754)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2938848833:i=176048:add=on:rtra=on:rawr=on_2840 on theBenchmark for (2840ds/176048Mi) % 160.21/22.83 % (2264732)Instruction limit reached! % 160.21/22.83 % (2264732)------------------------------ % 160.21/22.83 % (2264732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.21/22.83 % (2264732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.21/22.83 % (2264732)CaDiCaL version: 2.1.3 % 160.21/22.83 % (2264732)Termination reason: Instruction limit % 160.21/22.83 % (2264732)Termination phase: Saturation % 160.21/22.83 % (2264732)Time elapsed: 4.307 s % 160.21/22.83 % (2264732)Peak memory usage: 30 MB % 160.21/22.83 % (2264732)Instructions burned: 17629 (million) % 160.21/22.83 % (2264756)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2622090678:i=206:fgj=on:rtra=on_2827 on theBenchmark for (2827ds/206Mi) % 160.21/22.83 % (2264756)Instruction limit reached! % 160.21/22.83 % (2264756)------------------------------ % 160.21/22.83 % (2264756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.21/22.83 % (2264756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.21/22.83 % (2264756)CaDiCaL version: 2.1.3 % 160.21/22.83 % (2264756)Termination reason: Instruction limit % 160.21/22.83 % (2264756)Termination phase: Saturation % 160.21/22.83 % (2264756)Time elapsed: 0.061 s % 160.21/22.83 % (2264756)Peak memory usage: 13 MB % 160.21/22.83 % (2264756)Instructions burned: 210 (million) % 160.21/22.83 % (2264758)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3497032896:i=232:rtra=on_2826 on theBenchmark for (2826ds/232Mi) % 160.21/22.83 % (2264758)Instruction limit reached! % 160.21/22.83 % (2264758)------------------------------ % 160.21/22.83 % (2264758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.21/22.83 % (2264758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.21/22.83 % (2264758)CaDiCaL version: 2.1.3 % 160.21/22.83 % (2264758)Termination reason: Instruction limit % 160.21/22.83 % (2264758)Termination phase: Saturation % 160.21/22.83 % (2264758)Time elapsed: 0.073 s % 160.21/22.83 % (2264758)Peak memory usage: 13 MB % 160.21/22.83 % (2264758)Instructions burned: 234 (million) % 160.21/22.83 % (2264760)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1728912461:i=262:rtra=on_2825 on theBenchmark for (2825ds/262Mi) % 160.21/22.83 % (2264760)Instruction limit reached! % 160.21/22.83 % (2264760)------------------------------ % 160.21/22.83 % (2264760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 160.21/22.83 % (2264760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.21/22.83 % (2264760)CaDiCaL version: 2.1.3 % 160.21/22.83 % (2264760)Termination reason: Instruction limit % 160.21/22.83 % (2264760)Termination phase: Saturation % 198.53/28.29 % (2264760)Time elapsed: 0.086 s % 198.53/28.29 % (2264760)Peak memory usage: 14 MB % 198.53/28.29 % (2264760)Instructions burned: 265 (million) % 198.53/28.29 % (2264762)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=808928748:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2824 on theBenchmark for (2824ds/318Mi) % 198.53/28.29 % (2264762)Instruction limit reached! % 198.53/28.29 % (2264762)------------------------------ % 198.53/28.29 % (2264762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.53/28.29 % (2264762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.53/28.29 % (2264762)CaDiCaL version: 2.1.3 % 198.53/28.29 % (2264762)Termination reason: Instruction limit % 198.53/28.29 % (2264762)Termination phase: Saturation % 198.53/28.29 % (2264762)Time elapsed: 0.103 s % 198.53/28.29 % (2264762)Peak memory usage: 13 MB % 198.53/28.29 % (2264762)Instructions burned: 319 (million) % 198.53/28.29 % (2264764)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3736244926:i=1428:nm=2:rtra=on_2823 on theBenchmark for (2823ds/1428Mi) % 198.53/28.29 % Exception at run slice level % 198.53/28.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 198.53/28.29 % (2264766)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=718738427:i=262:bd=preordered:rtra=on:fsd=on_2823 on theBenchmark for (2823ds/262Mi) % 198.53/28.29 % (2264766)Instruction limit reached! % 198.53/28.29 % (2264766)------------------------------ % 198.53/28.29 % (2264766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.53/28.29 % (2264766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.53/28.29 % (2264766)CaDiCaL version: 2.1.3 % 198.53/28.29 % (2264766)Termination reason: Instruction limit % 198.53/28.29 % (2264766)Termination phase: Saturation % 198.53/28.29 % (2264766)Time elapsed: 0.085 s % 198.53/28.29 % (2264766)Peak memory usage: 13 MB % 198.53/28.29 % (2264766)Instructions burned: 266 (million) % 198.53/28.29 % (2264768)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=1797439356:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/1368Mi) % 198.53/28.29 % (2264768)Instruction limit reached! % 198.53/28.29 % (2264768)------------------------------ % 198.53/28.29 % (2264768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.53/28.29 % (2264768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.53/28.29 % (2264768)CaDiCaL version: 2.1.3 % 198.53/28.29 % (2264768)Termination reason: Instruction limit % 198.53/28.29 % (2264768)Termination phase: Saturation % 198.53/28.29 % (2264768)Time elapsed: 0.376 s % 198.53/28.29 % (2264768)Peak memory usage: 17 MB % 198.53/28.29 % (2264768)Instructions burned: 1370 (million) % 198.53/28.29 % (2264770)ott-21_1_sil=16000:si=on:fs=off:random_seed=427052104:i=360:av=off:fsr=off:rtra=on_2818 on theBenchmark for (2818ds/360Mi) % 198.53/28.29 % (2264770)Instruction limit reached! % 198.53/28.29 % (2264770)------------------------------ % 198.53/28.29 % (2264770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.53/28.29 % (2264770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.53/28.29 % (2264770)CaDiCaL version: 2.1.3 % 198.53/28.29 % (2264770)Termination reason: Instruction limit % 198.53/28.29 % (2264770)Termination phase: Saturation % 198.53/28.29 % (2264770)Time elapsed: 0.102 s % 198.53/28.29 % (2264770)Peak memory usage: 14 MB % 198.53/28.29 % (2264770)Instructions burned: 363 (million) % 198.53/28.29 % (2264772)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3082170689:i=954:bd=all:rtra=on_2817 on theBenchmark for (2817ds/954Mi) % 198.53/28.29 % (2264772)Instruction limit reached! % 198.53/28.29 % (2264772)------------------------------ % 198.53/28.29 % (2264772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 198.53/28.29 % (2264772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.53/28.29 % (2264772)CaDiCaL version: 2.1.3 % 198.53/28.29 % (2264772)Termination reason: Instruction limit % 198.53/28.29 % (2264772)Termination phase: Saturation % 198.53/28.29 % (2264772)Time elapsed: 0.293 s % 198.53/28.29 % (2264772)Peak memory usage: 15 MB % 198.53/28.29 % (2264772)Instructions burned: 956 (million) % 198.53/28.29 % (2264774)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1291152514:fmbsr=1.3:i=1730:ins=25:rtra=on_2814 on theBenchmark for (2814ds/1730Mi) % 198.53/28.29 % Exception at run slice level % 198.53/28.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.11/34.91 % (2264776)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3211957815:i=2358:rtra=on_2814 on theBenchmark for (2814ds/2358Mi) % 246.11/34.91 % (2264776)Instruction limit reached! % 246.11/34.91 % (2264776)------------------------------ % 246.11/34.91 % (2264776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.11/34.91 % (2264776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.11/34.91 % (2264776)CaDiCaL version: 2.1.3 % 246.11/34.91 % (2264776)Termination reason: Instruction limit % 246.11/34.91 % (2264776)Termination phase: Saturation % 246.11/34.91 % (2264776)Time elapsed: 0.754 s % 246.11/34.91 % (2264776)Peak memory usage: 23 MB % 246.11/34.91 % (2264776)Instructions burned: 2361 (million) % 246.11/34.91 % (2264778)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2536701553:i=1778:ins=1:rtra=on_2806 on theBenchmark for (2806ds/1778Mi) % 246.11/34.91 % Exception at run slice level % 246.11/34.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.11/34.91 % (2264780)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=4201380823:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2806 on theBenchmark for (2806ds/1384Mi) % 246.11/34.91 % (2264780)Instruction limit reached! % 246.11/34.91 % (2264780)------------------------------ % 246.11/34.91 % (2264780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.11/34.91 % (2264780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.11/34.91 % (2264780)CaDiCaL version: 2.1.3 % 246.11/34.91 % (2264780)Termination reason: Instruction limit % 246.11/34.91 % (2264780)Termination phase: Saturation % 246.11/34.91 % (2264780)Time elapsed: 0.412 s % 246.11/34.91 % (2264780)Peak memory usage: 18 MB % 246.11/34.91 % (2264780)Instructions burned: 1385 (million) % 246.11/34.91 % (2264782)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=707083795:i=1758:kws=inv_precedence:fsr=off:rtra=on_2802 on theBenchmark for (2802ds/1758Mi) % 246.11/34.91 % (2264782)Instruction limit reached! % 246.11/34.91 % (2264782)------------------------------ % 246.11/34.91 % (2264782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.11/34.91 % (2264782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.11/34.91 % (2264782)CaDiCaL version: 2.1.3 % 246.11/34.91 % (2264782)Termination reason: Instruction limit % 246.11/34.91 % (2264782)Termination phase: Saturation % 246.11/34.91 % (2264782)Time elapsed: 0.528 s % 246.11/34.91 % (2264782)Peak memory usage: 23 MB % 246.11/34.91 % (2264782)Instructions burned: 1760 (million) % 246.11/34.91 % (2264784)fmb+10_1_sil=64000:si=on:random_seed=2819686018:i=44122:nm=2:rtra=on:gsp=on_2796 on theBenchmark for (2796ds/44122Mi) % 246.11/34.91 % (2264784)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 246.11/34.91 % Exception at run slice level % 246.11/34.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.11/34.91 % (2264786)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2239314618:i=19030:nm=5:rtra=on_2796 on theBenchmark for (2796ds/19030Mi) % 246.11/34.91 % Exception at run slice level % 246.11/34.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.11/34.91 % (2264788)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1924963906:fmbsr=1.7:i=1840:rtra=on_2796 on theBenchmark for (2796ds/1840Mi) % 246.11/34.91 % Exception at run slice level % 246.11/34.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 246.11/34.91 % (2264790)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3801856145:i=10262:rtra=on_2796 on theBenchmark for (2796ds/10262Mi) % 246.11/34.91 % (2264738)Instruction limit reached! % 246.11/34.91 % (2264738)------------------------------ % 246.11/34.91 % (2264738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 246.11/34.91 % (2264738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.11/34.91 % (2264738)CaDiCaL version: 2.1.3 % 246.11/34.91 % (2264738)Termination reason: Instruction limit % 246.11/34.91 % (2264738)Termination phase: Saturation % 246.11/34.91 % (2264738)Time elapsed: 8.413 s % 246.11/34.91 % (2264738)Peak memory usage: 16 MB % 246.11/34.91 % (2264738)Instructions burned: 28122 (million) % 300.07/42.53 % (2264792)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3267709895:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2774 on theBenchmark for (2774ds/2944Mi) % 300.07/42.53 % (2264792)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.07/42.53 % (2264790)Instruction limit reached! % 300.07/42.53 % (2264790)------------------------------ % 300.07/42.53 % (2264790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.53 % (2264790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.53 % (2264790)CaDiCaL version: 2.1.3 % 300.07/42.53 % (2264790)Termination reason: Instruction limit % 300.07/42.53 % (2264790)Termination phase: Saturation % 300.07/42.53 % (2264790)Time elapsed: 2.987 s % 300.07/42.53 % (2264790)Peak memory usage: 43 MB % 300.07/42.53 % (2264790)Instructions burned: 10263 (million) % 300.07/42.53 % (2264794)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=2177737791:i=12648:rtra=on_2766 on theBenchmark for (2766ds/12648Mi) % 300.07/42.53 % Exception at run slice level % 300.07/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.07/42.53 % (2264796)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=528818189:fmbsr=2.30978:i=4348:rtra=on_2766 on theBenchmark for (2766ds/4348Mi) % 300.07/42.53 % Exception at run slice level % 300.07/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.07/42.53 % (2264798)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=652021768:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2765 on theBenchmark for (2765ds/1738Mi) % 300.07/42.53 % (2264798)Instruction limit reached! % 300.07/42.53 % (2264798)------------------------------ % 300.07/42.53 % (2264798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.53 % (2264798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.53 % (2264798)CaDiCaL version: 2.1.3 % 300.07/42.53 % (2264798)Termination reason: Instruction limit % 300.07/42.53 % (2264798)Termination phase: Saturation % 300.07/42.53 % (2264798)Time elapsed: 0.435 s % 300.07/42.54 % (2264798)Peak memory usage: 14 MB % 300.07/42.54 % (2264798)Instructions burned: 1743 (million) % 300.07/42.54 % (2264800)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=997095203:i=10228:av=off:rtra=on_2761 on theBenchmark for (2761ds/10228Mi) % 300.07/42.54 % (2264792)Instruction limit reached! % 300.07/42.54 % (2264792)------------------------------ % 300.07/42.54 % (2264792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.54 % (2264792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.54 % (2264792)CaDiCaL version: 2.1.3 % 300.07/42.54 % (2264792)Termination reason: Instruction limit % 300.07/42.54 % (2264792)Termination phase: Saturation % 300.07/42.54 % (2264792)Time elapsed: 1.273 s % 300.07/42.54 % (2264792)Peak memory usage: 17 MB % 300.07/42.54 % (2264792)Instructions burned: 2944 (million) % 300.07/42.54 % (2264802)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=4027343194:i=108564:rtra=on_2761 on theBenchmark for (2761ds/108564Mi) % 300.07/42.54 % Exception at run slice level % 300.07/42.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.07/42.54 % (2264804)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1386236198:i=7024:aac=none:rtra=on_2760 on theBenchmark for (2760ds/7024Mi) % 300.07/42.54 % (2264800)Instruction limit reached! % 300.07/42.54 % (2264800)------------------------------ % 300.07/42.54 % (2264800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.54 % (2264800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.07/42.54 % (2264800)CaDiCaL version: 2.1.3 % 300.07/42.54 % (2264800)Termination reason: Instruction limit % 300.07/42.54 % (2264800)Termination phase: Saturation % 300.07/42.54 % (2264800)Time elapsed: 2.864 s % 300.07/42.54 % (2264800)Peak memory usage: 21 MB % 300.07/42.54 % (2264800)Instructions burned: 10230 (million) % 300.07/42.54 % (2264806)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=4005437250:i=7546:rtra=on:amm=off_2732 on theBenchmark for (2732ds/7546Mi) % 300.07/42.54 % (2264804)Instruction limit reached! % 300.07/42.54 % (2264804)------------------------------ % 300.07/42.54 % (2264804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.07/42.54 % (2264804)Linked with Z3 4.14.0.0 % 300.07/42.54 Terminated % 300.07/42.54 % Vampire exiting % 300.07/42.54 Terminated %------------------------------------------------------------------------------