%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW502_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 : n001.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:20 PM UTC 2026 % Result : Timeout 300.02s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW502_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.10/0.19 % Computer : n001.cluster.edu % 0.10/0.19 % Model : x86_64 x86_64 % 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.19 % Memory : 8046.5625MB % 0.10/0.19 % OS : Linux 6.8.0-71-generic % 0.10/0.19 % CPULimit : 300 % 0.10/0.19 % WCLimit : 300 % 0.10/0.19 % DateTime : Mon Sep 28 14:21:03 UTC 2026 % 0.10/0.19 % CPUTime : % 0.10/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.10/0.22 Running first-order model finding % 0.10/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 % 6.91/1.38 % (371075)Will run a generic schedule for satisfiability detection. % 6.91/1.38 % (371086)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1345080337:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 6.91/1.38 % (371081)% WARNING: option uhcvi not known. % 6.91/1.38 % (371082)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1892438463:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 6.91/1.38 % (371080)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1481368650_2999 on theBenchmark for (2999ds/0Mi) % 6.91/1.38 % (371084)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2755391636:i=116_2999 on theBenchmark for (2999ds/116Mi) % 6.91/1.38 % (371081)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2958194984:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 6.91/1.38 % (371083)dis+10_1_sil=32000:sp=arity:random_seed=822803121:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 6.91/1.38 % (371085)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=603532889:i=131_2999 on theBenchmark for (2999ds/131Mi) % 6.91/1.38 % Exception at run slice level % 6.91/1.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.91/1.38 % (371094)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3813769385:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 6.91/1.38 % Exception at run slice level % 6.91/1.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 6.91/1.38 % (371096)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2094838501:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 6.91/1.38 % (371086)Instruction limit reached! % 6.91/1.38 % (371086)------------------------------ % 6.91/1.38 % (371086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.38 % (371086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.38 % (371086)CaDiCaL version: 2.1.3 % 6.91/1.38 % (371086)Termination reason: Instruction limit % 6.91/1.38 % (371086)Termination phase: Saturation % 6.91/1.38 % (371086)Time elapsed: 0.055 s % 6.91/1.38 % (371086)Peak memory usage: 14 MB % 6.91/1.38 % (371086)Instructions burned: 162 (million) % 6.91/1.38 % (371098)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=1668918303:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 6.91/1.38 % (371083)Instruction limit reached! % 6.91/1.38 % (371083)------------------------------ % 6.91/1.38 % (371083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.38 % (371083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.38 % (371083)CaDiCaL version: 2.1.3 % 6.91/1.38 % (371083)Termination reason: Instruction limit % 6.91/1.38 % (371083)Termination phase: Saturation % 6.91/1.38 % (371083)Time elapsed: 0.063 s % 6.91/1.38 % (371083)Peak memory usage: 13 MB % 6.91/1.38 % (371083)Instructions burned: 104 (million) % 6.91/1.38 % (371084)Instruction limit reached! % 6.91/1.38 % (371084)------------------------------ % 6.91/1.38 % (371084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.38 % (371084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.38 % (371084)CaDiCaL version: 2.1.3 % 6.91/1.38 % (371084)Termination reason: Instruction limit % 6.91/1.38 % (371084)Termination phase: Saturation % 6.91/1.38 % (371084)Time elapsed: 0.072 s % 6.91/1.38 % (371084)Peak memory usage: 13 MB % 6.91/1.38 % (371084)Instructions burned: 116 (million) % 6.91/1.38 % (371085)Instruction limit reached! % 6.91/1.38 % (371085)------------------------------ % 6.91/1.38 % (371085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 6.91/1.38 % (371085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.91/1.38 % (371085)CaDiCaL version: 2.1.3 % 6.91/1.38 % (371085)Termination reason: Instruction limit % 6.91/1.38 % (371085)Termination phase: Saturation % 6.91/1.38 % (371085)Time elapsed: 0.078 s % 6.91/1.38 % (371085)Peak memory usage: 13 MB % 6.91/1.38 % (371085)Instructions burned: 132 (million) % 6.91/1.38 % (371100)ott-21_1_sil=16000:fs=off:random_seed=3866607110:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 6.91/1.38 % (371101)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3915674849:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 21.60/3.33 % (371102)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4188826596:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.60/3.33 % Exception at run slice level % 21.60/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.60/3.33 % (371106)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1893512606:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.60/3.33 % (371096)Instruction limit reached! % 21.60/3.33 % (371096)------------------------------ % 21.60/3.33 % (371096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (371096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (371096)CaDiCaL version: 2.1.3 % 21.60/3.33 % (371096)Termination reason: Instruction limit % 21.60/3.33 % (371096)Termination phase: Saturation % 21.60/3.33 % (371096)Time elapsed: 0.082 s % 21.60/3.33 % (371096)Peak memory usage: 13 MB % 21.60/3.33 % (371096)Instructions burned: 132 (million) % 21.60/3.33 % (371108)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=496098397:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.60/3.33 % Exception at run slice level % 21.60/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.60/3.33 % (371110)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=2754880191: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.60/3.33 % (371100)Instruction limit reached! % 21.60/3.33 % (371100)------------------------------ % 21.60/3.33 % (371100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (371100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (371100)CaDiCaL version: 2.1.3 % 21.60/3.33 % (371100)Termination reason: Instruction limit % 21.60/3.33 % (371100)Termination phase: Saturation % 21.60/3.33 % (371100)Time elapsed: 0.094 s % 21.60/3.33 % (371100)Peak memory usage: 13 MB % 21.60/3.33 % (371100)Instructions burned: 180 (million) % 21.60/3.33 % (371112)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2774554651:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.60/3.33 % (371098)Instruction limit reached! % 21.60/3.33 % (371098)------------------------------ % 21.60/3.33 % (371098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (371098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (371098)CaDiCaL version: 2.1.3 % 21.60/3.33 % (371098)Termination reason: Instruction limit % 21.60/3.33 % (371098)Termination phase: Saturation % 21.60/3.33 % (371098)Time elapsed: 0.175 s % 21.60/3.33 % (371098)Peak memory usage: 15 MB % 21.60/3.33 % (371098)Instructions burned: 686 (million) % 21.60/3.33 % (371114)fmb+10_1_sil=64000:random_seed=652500699:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.60/3.33 % (371114)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.60/3.33 % Exception at run slice level % 21.60/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.60/3.33 % (371116)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=114694368:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.60/3.33 % Exception at run slice level % 21.60/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.60/3.33 % (371118)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3189961028:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 21.60/3.33 % Exception at run slice level % 21.60/3.33 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.60/3.33 % (371120)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3407973308:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.60/3.33 % (371101)Instruction limit reached! % 21.60/3.33 % (371101)------------------------------ % 21.60/3.33 % (371101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.60/3.33 % (371101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.60/3.33 % (371101)CaDiCaL version: 2.1.3 % 21.60/3.33 % (371101)Termination reason: Instruction limit % 21.60/3.33 % (371101)Termination phase: Saturation % 60.82/8.90 % (371101)Time elapsed: 0.298 s % 60.82/8.90 % (371101)Peak memory usage: 14 MB % 60.82/8.90 % (371101)Instructions burned: 478 (million) % 60.82/8.90 % (371122)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=695943197:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 60.82/8.90 % (371122)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 60.82/8.90 % (371110)Instruction limit reached! % 60.82/8.90 % (371110)------------------------------ % 60.82/8.90 % (371110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.82/8.90 % (371110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.82/8.90 % (371110)CaDiCaL version: 2.1.3 % 60.82/8.90 % (371110)Termination reason: Instruction limit % 60.82/8.90 % (371110)Termination phase: Saturation % 60.82/8.90 % (371110)Time elapsed: 0.313 s % 60.82/8.90 % (371110)Peak memory usage: 15 MB % 60.82/8.90 % (371110)Instructions burned: 692 (million) % 60.82/8.90 % (371124)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3530530865:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 60.82/8.90 % Exception at run slice level % 60.82/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.82/8.90 % (371126)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3639778557:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 60.82/8.90 % Exception at run slice level % 60.82/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.82/8.90 % (371128)ott-2_1_sil=16000:newcnf=on:random_seed=3856011178:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi) % 60.82/8.90 % (371112)Instruction limit reached! % 60.82/8.90 % (371112)------------------------------ % 60.82/8.90 % (371112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.82/8.90 % (371112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.82/8.90 % (371112)CaDiCaL version: 2.1.3 % 60.82/8.90 % (371112)Termination reason: Instruction limit % 60.82/8.90 % (371112)Termination phase: Saturation % 60.82/8.90 % (371112)Time elapsed: 0.503 s % 60.82/8.90 % (371112)Peak memory usage: 20 MB % 60.82/8.90 % (371112)Instructions burned: 880 (million) % 60.82/8.90 % (371130)ott+10_1_sil=32000:tgt=ground:random_seed=1145214423:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 60.82/8.90 % (371106)Instruction limit reached! % 60.82/8.90 % (371106)------------------------------ % 60.82/8.90 % (371106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.82/8.90 % (371106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.82/8.90 % (371106)CaDiCaL version: 2.1.3 % 60.82/8.90 % (371106)Termination reason: Instruction limit % 60.82/8.90 % (371106)Termination phase: Saturation % 60.82/8.90 % (371106)Time elapsed: 0.686 s % 60.82/8.90 % (371106)Peak memory usage: 22 MB % 60.82/8.90 % (371106)Instructions burned: 1180 (million) % 60.82/8.90 % (371132)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2417441933:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 60.82/8.90 % Exception at run slice level % 60.82/8.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 60.82/8.90 % (371134)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1264460249:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 60.82/8.90 % (371128)Instruction limit reached! % 60.82/8.90 % (371128)------------------------------ % 60.82/8.90 % (371128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.82/8.90 % (371128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.82/8.90 % (371128)CaDiCaL version: 2.1.3 % 60.82/8.90 % (371128)Termination reason: Instruction limit % 60.82/8.90 % (371128)Termination phase: Saturation % 60.82/8.90 % (371128)Time elapsed: 0.480 s % 60.82/8.90 % (371128)Peak memory usage: 18 MB % 60.82/8.90 % (371128)Instructions burned: 869 (million) % 60.82/8.90 % (371136)dis+21_1_sil=32000:sas=cadical:random_seed=2121826274:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi) % 60.82/8.90 % (371122)Instruction limit reached! % 60.82/8.90 % (371122)------------------------------ % 60.82/8.90 % (371122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 60.82/8.90 % (371122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.82/8.90 % (371122)CaDiCaL version: 2.1.3 % 120.35/17.26 % (371122)Termination reason: Instruction limit % 120.35/17.26 % (371122)Termination phase: Saturation % 120.35/17.26 % (371122)Time elapsed: 0.711 s % 120.35/17.26 % (371122)Peak memory usage: 26 MB % 120.35/17.26 % (371122)Instructions burned: 1472 (million) % 120.35/17.26 % (371138)ott+11_1_sil=16000:gs=on:random_seed=2652920312:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi) % 120.35/17.26 % (371120)Instruction limit reached! % 120.35/17.26 % (371120)------------------------------ % 120.35/17.26 % (371120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.35/17.26 % (371120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.35/17.26 % (371120)CaDiCaL version: 2.1.3 % 120.35/17.26 % (371120)Termination reason: Instruction limit % 120.35/17.26 % (371120)Termination phase: Saturation % 120.35/17.26 % (371120)Time elapsed: 1.499 s % 120.35/17.26 % (371120)Peak memory usage: 34 MB % 120.35/17.26 % (371120)Instructions burned: 5131 (million) % 120.35/17.26 % (371140)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3438973887:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi) % 120.35/17.26 % Exception at run slice level % 120.35/17.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 120.35/17.26 % (371142)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3766716516:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi) % 120.35/17.26 % (371138)Instruction limit reached! % 120.35/17.26 % (371138)------------------------------ % 120.35/17.26 % (371138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.35/17.26 % (371138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.35/17.26 % (371138)CaDiCaL version: 2.1.3 % 120.35/17.26 % (371138)Termination reason: Instruction limit % 120.35/17.26 % (371138)Termination phase: Saturation % 120.35/17.26 % (371138)Time elapsed: 1.291 s % 120.35/17.26 % (371138)Peak memory usage: 30 MB % 120.35/17.26 % (371138)Instructions burned: 2252 (million) % 120.35/17.26 % (371144)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=512982819:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 120.35/17.26 % (371134)Instruction limit reached! % 120.35/17.26 % (371134)------------------------------ % 120.35/17.26 % (371134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.35/17.26 % (371134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.35/17.26 % (371134)CaDiCaL version: 2.1.3 % 120.35/17.26 % (371134)Termination reason: Instruction limit % 120.35/17.26 % (371134)Termination phase: Saturation % 120.35/17.26 % (371134)Time elapsed: 1.976 s % 120.35/17.26 % (371134)Peak memory usage: 31 MB % 120.35/17.26 % (371134)Instructions burned: 3512 (million) % 120.35/17.26 % (371146)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2149246533:i=5211_2971 on theBenchmark for (2971ds/5211Mi) % 120.35/17.26 % (371142)Instruction limit reached! % 120.35/17.26 % (371142)------------------------------ % 120.35/17.26 % (371142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 120.35/17.26 % (371142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.35/17.26 % (371142)CaDiCaL version: 2.1.3 % 120.35/17.26 % (371142)Termination reason: Instruction limit % 120.35/17.26 % (371142)Termination phase: Saturation % 120.35/17.26 % (371142)Time elapsed: 1.203 s % 120.35/17.26 % (371142)Peak memory usage: 42 MB % 120.35/17.26 % (371142)Instructions burned: 4593 (million) % 120.35/17.26 % (371148)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1033688208:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 120.35/17.26 % Exception at run slice level % 120.35/17.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 120.35/17.26 % (371150)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=34607251:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 120.35/17.26 % Exception at run slice level % 120.35/17.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 120.35/17.26 % (371152)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1571899686:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 120.35/17.26 % Exception at run slice level % 120.35/17.26 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 120.35/17.26 % (371154)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2099975850:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 131.58/18.80 % (371136)Instruction limit reached! % 131.58/18.80 % (371136)------------------------------ % 131.58/18.80 % (371136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.58/18.80 % (371136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.58/18.80 % (371136)CaDiCaL version: 2.1.3 % 131.58/18.80 % (371136)Termination reason: Instruction limit % 131.58/18.80 % (371136)Termination phase: Saturation % 131.58/18.80 % (371136)Time elapsed: 2.096 s % 131.58/18.80 % (371136)Peak memory usage: 33 MB % 131.58/18.80 % (371136)Instructions burned: 3774 (million) % 131.58/18.80 % (371156)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3197594620:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 131.58/18.80 % (371130)Instruction limit reached! % 131.58/18.80 % (371130)------------------------------ % 131.58/18.80 % (371130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.58/18.80 % (371130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.58/18.80 % (371130)CaDiCaL version: 2.1.3 % 131.58/18.80 % (371130)Termination reason: Instruction limit % 131.58/18.80 % (371130)Termination phase: Saturation % 131.58/18.80 % (371130)Time elapsed: 3.059 s % 131.58/18.80 % (371130)Peak memory usage: 46 MB % 131.58/18.80 % (371130)Instructions burned: 5115 (million) % 131.58/18.80 % (371158)dis+10_16:1_sil=16000:random_seed=3943376331:i=9155:fsr=off_2961 on theBenchmark for (2961ds/9155Mi) % 131.58/18.80 % (371146)Instruction limit reached! % 131.58/18.80 % (371146)------------------------------ % 131.58/18.80 % (371146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.58/18.80 % (371146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.58/18.80 % (371146)CaDiCaL version: 2.1.3 % 131.58/18.80 % (371146)Termination reason: Instruction limit % 131.58/18.80 % (371146)Termination phase: Saturation % 131.58/18.80 % (371146)Time elapsed: 2.685 s % 131.58/18.80 % (371146)Peak memory usage: 41 MB % 131.58/18.80 % (371146)Instructions burned: 5212 (million) % 131.58/18.80 % (371160)ott-3_8_sil=64000:random_seed=2115068554:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi) % 131.58/18.80 % (371154)Instruction limit reached! % 131.58/18.80 % (371154)------------------------------ % 131.58/18.80 % (371154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.58/18.80 % (371154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.58/18.80 % (371154)CaDiCaL version: 2.1.3 % 131.58/18.80 % (371154)Termination reason: Instruction limit % 131.58/18.80 % (371154)Termination phase: Saturation % 131.58/18.80 % (371154)Time elapsed: 4.232 s % 131.58/18.80 % (371154)Peak memory usage: 30 MB % 131.58/18.80 % (371154)Instructions burned: 22568 (million) % 131.58/18.80 % (371162)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2653352722:fmbsr=2:i=32576_2926 on theBenchmark for (2926ds/32576Mi) % 131.58/18.80 % Exception at run slice level % 131.58/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 131.58/18.80 % (371164)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4095912679:i=11404_2926 on theBenchmark for (2926ds/11404Mi) % 131.58/18.80 % (371156)Instruction limit reached! % 131.58/18.80 % (371156)------------------------------ % 131.58/18.80 % (371156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.58/18.80 % (371156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.58/18.80 % (371156)CaDiCaL version: 2.1.3 % 131.58/18.80 % (371156)Termination reason: Instruction limit % 131.58/18.80 % (371156)Termination phase: Saturation % 131.58/18.80 % (371156)Time elapsed: 4.733 s % 131.58/18.80 % (371156)Peak memory usage: 73 MB % 131.58/18.80 % (371156)Instructions burned: 8174 (million) % 131.58/18.80 % (371166)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2728634205:i=14134_2920 on theBenchmark for (2920ds/14134Mi) % 131.58/18.80 % (371158)Instruction limit reached! % 131.58/18.80 % (371158)------------------------------ % 131.58/18.80 % (371158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 131.58/18.80 % (371158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.58/18.80 % (371158)CaDiCaL version: 2.1.3 % 131.58/18.80 % (371158)Termination reason: Instruction limit % 131.58/18.80 % (371158)Termination phase: Saturation % 131.58/18.80 % (371158)Time elapsed: 4.809 s % 131.58/18.80 % (371158)Peak memory usage: 73 MB % 131.58/18.80 % (371158)Instructions burned: 9156 (million) % 131.58/18.80 % (371168)dis+33_16_sil=32000:sac=on:random_seed=602383962:i=15851:nm=0_2913 on theBenchmark for (2913ds/15851Mi) % 153.80/21.93 % (371164)Instruction limit reached! % 153.80/21.93 % (371164)------------------------------ % 153.80/21.93 % (371164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.80/21.93 % (371164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.80/21.93 % (371164)CaDiCaL version: 2.1.3 % 153.80/21.93 % (371164)Termination reason: Instruction limit % 153.80/21.93 % (371164)Termination phase: Saturation % 153.80/21.93 % (371164)Time elapsed: 3.870 s % 153.80/21.93 % (371164)Peak memory usage: 94 MB % 153.80/21.93 % (371164)Instructions burned: 11406 (million) % 153.80/21.93 % (371170)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2839406666:avsq=on:i=17627:add=on:amm=off_2887 on theBenchmark for (2887ds/17627Mi) % 153.80/21.93 % (371144)Instruction limit reached! % 153.80/21.93 % (371144)------------------------------ % 153.80/21.93 % (371144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.80/21.93 % (371144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.80/21.93 % (371144)CaDiCaL version: 2.1.3 % 153.80/21.93 % (371144)Termination reason: Instruction limit % 153.80/21.93 % (371144)Termination phase: Saturation % 153.80/21.93 % (371144)Time elapsed: 13.241 s % 153.80/21.93 % (371144)Peak memory usage: 151 MB % 153.80/21.93 % (371144)Instructions burned: 29341 (million) % 153.80/21.93 % (371532)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1387852446:s2a=on:i=53295_2842 on theBenchmark for (2842ds/53295Mi) % 153.80/21.93 % (371170)Instruction limit reached! % 153.80/21.93 % (371170)------------------------------ % 153.80/21.93 % (371170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.80/21.93 % (371170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.80/21.93 % (371170)CaDiCaL version: 2.1.3 % 153.80/21.93 % (371170)Termination reason: Instruction limit % 153.80/21.93 % (371170)Termination phase: Saturation % 153.80/21.93 % (371170)Time elapsed: 5.559 s % 153.80/21.93 % (371170)Peak memory usage: 181 MB % 153.80/21.93 % (371170)Instructions burned: 17630 (million) % 153.80/21.93 % (371534)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=242315631:i=26857:ins=20_2831 on theBenchmark for (2831ds/26857Mi) % 153.80/21.93 % Exception at run slice level % 153.80/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.80/21.93 % (371536)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1582323025:i=28120:bs=on:fsr=off_2831 on theBenchmark for (2831ds/28120Mi) % 153.80/21.93 % (371168)Instruction limit reached! % 153.80/21.93 % (371168)------------------------------ % 153.80/21.93 % (371168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 153.80/21.93 % (371168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.80/21.93 % (371168)CaDiCaL version: 2.1.3 % 153.80/21.93 % (371168)Termination reason: Instruction limit % 153.80/21.93 % (371168)Termination phase: Saturation % 153.80/21.93 % (371168)Time elapsed: 8.235 s % 153.80/21.93 % (371168)Peak memory usage: 69 MB % 153.80/21.93 % (371168)Instructions burned: 15853 (million) % 153.80/21.93 % (371538)fmb+10_1_sil=256000:fmbss=7:random_seed=2879443608:fmbsr=1.6:i=182295_2830 on theBenchmark for (2830ds/182295Mi) % 153.80/21.93 % Exception at run slice level % 153.80/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.80/21.93 % (371540)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=884122922:i=44625:gsp=on_2830 on theBenchmark for (2830ds/44625Mi) % 153.80/21.93 % (371540)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 153.80/21.93 % Exception at run slice level % 153.80/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.80/21.93 % (371542)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3027597615:i=160505_2830 on theBenchmark for (2830ds/160505Mi) % 153.80/21.93 % Exception at run slice level % 153.80/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.80/21.93 % (371544)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2079080742:fmbsr=1.3:i=225729_2830 on theBenchmark for (2830ds/225729Mi) % 153.80/21.93 % Exception at run slice level % 153.80/21.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 153.80/21.93 % (371546)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=688350594:fmbsr=2:i=185024:ins=7_2829 on theBenchmark for (2829ds/185024Mi) % 195.50/27.98 % Exception at run slice level % 195.50/27.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.50/27.98 % (371548)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1818477308:rtra=on_2829 on theBenchmark for (2829ds/0Mi) % 195.50/27.98 % Exception at run slice level % 195.50/27.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 195.50/27.98 % (371550)% WARNING: option uhcvi not known. % 195.50/27.98 % (371550)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3765922453:i=271062:add=off:rtra=on:rawr=on_2829 on theBenchmark for (2829ds/271062Mi) % 195.50/27.98 % (371166)Instruction limit reached! % 195.50/27.98 % (371166)------------------------------ % 195.50/27.98 % (371166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.50/27.98 % (371166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.50/27.98 % (371166)CaDiCaL version: 2.1.3 % 195.50/27.98 % (371166)Termination reason: Instruction limit % 195.50/27.98 % (371166)Termination phase: Saturation % 195.50/27.98 % (371166)Time elapsed: 9.222 s % 195.50/27.98 % (371166)Peak memory usage: 91 MB % 195.50/27.98 % (371166)Instructions burned: 14135 (million) % 195.50/27.98 % (371552)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1232601464:i=176048:add=on:rtra=on:rawr=on_2827 on theBenchmark for (2827ds/176048Mi) % 195.50/27.98 % (371160)Instruction limit reached! % 195.50/27.98 % (371160)------------------------------ % 195.50/27.98 % (371160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.50/27.98 % (371160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.50/27.98 % (371160)CaDiCaL version: 2.1.3 % 195.50/27.98 % (371160)Termination reason: Instruction limit % 195.50/27.98 % (371160)Termination phase: Saturation % 195.50/27.98 % (371160)Time elapsed: 12.260 s % 195.50/27.98 % (371160)Peak memory usage: 60 MB % 195.50/27.98 % (371160)Instructions burned: 20141 (million) % 195.50/27.98 % (371554)dis+10_1_sil=32000:si=on:sp=arity:random_seed=1039573616:i=206:fgj=on:rtra=on_2821 on theBenchmark for (2821ds/206Mi) % 195.50/27.98 % (371554)Instruction limit reached! % 195.50/27.98 % (371554)------------------------------ % 195.50/27.98 % (371554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.50/27.98 % (371554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.50/27.98 % (371554)CaDiCaL version: 2.1.3 % 195.50/27.98 % (371554)Termination reason: Instruction limit % 195.50/27.98 % (371554)Termination phase: Saturation % 195.50/27.98 % (371554)Time elapsed: 0.122 s % 195.50/27.98 % (371554)Peak memory usage: 13 MB % 195.50/27.98 % (371554)Instructions burned: 208 (million) % 195.50/27.98 % (371556)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=100775375:i=232:rtra=on_2819 on theBenchmark for (2819ds/232Mi) % 195.50/27.98 % (371556)Instruction limit reached! % 195.50/27.98 % (371556)------------------------------ % 195.50/27.98 % (371556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.50/27.98 % (371556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.50/27.98 % (371556)CaDiCaL version: 2.1.3 % 195.50/27.98 % (371556)Termination reason: Instruction limit % 195.50/27.98 % (371556)Termination phase: Saturation % 195.50/27.98 % (371556)Time elapsed: 0.148 s % 195.50/27.98 % (371556)Peak memory usage: 14 MB % 195.50/27.98 % (371556)Instructions burned: 232 (million) % 195.50/27.98 % (371558)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2334120899:i=262:rtra=on_2818 on theBenchmark for (2818ds/262Mi) % 195.50/27.98 % (371558)Instruction limit reached! % 195.50/27.98 % (371558)------------------------------ % 195.50/27.98 % (371558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 195.50/27.98 % (371558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.50/27.98 % (371558)CaDiCaL version: 2.1.3 % 195.50/27.98 % (371558)Termination reason: Instruction limit % 195.50/27.98 % (371558)Termination phase: Saturation % 195.50/27.98 % (371558)Time elapsed: 0.155 s % 195.50/27.98 % (371558)Peak memory usage: 14 MB % 195.50/27.98 % (371558)Instructions burned: 262 (million) % 195.50/27.98 % (371560)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3534376218:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2816 on theBenchmark for (2816ds/318Mi) % 195.50/27.98 % (371560)Instruction limit reached! % 195.50/27.98 % (371560)------------------------------ % 195.50/27.98 % (371560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.43/33.46 % (371560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.43/33.46 % (371560)CaDiCaL version: 2.1.3 % 235.43/33.46 % (371560)Termination reason: Instruction limit % 235.43/33.46 % (371560)Termination phase: Saturation % 235.43/33.46 % (371560)Time elapsed: 0.204 s % 235.43/33.46 % (371560)Peak memory usage: 15 MB % 235.43/33.46 % (371560)Instructions burned: 319 (million) % 235.43/33.46 % (371562)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4113003457:i=1428:nm=2:rtra=on_2814 on theBenchmark for (2814ds/1428Mi) % 235.43/33.46 % Exception at run slice level % 235.43/33.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 235.43/33.46 % (371564)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=1237521177:i=262:bd=preordered:rtra=on:fsd=on_2813 on theBenchmark for (2813ds/262Mi) % 235.43/33.46 % (371564)Instruction limit reached! % 235.43/33.46 % (371564)------------------------------ % 235.43/33.46 % (371564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.43/33.46 % (371564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.43/33.46 % (371564)CaDiCaL version: 2.1.3 % 235.43/33.46 % (371564)Termination reason: Instruction limit % 235.43/33.46 % (371564)Termination phase: Saturation % 235.43/33.46 % (371564)Time elapsed: 0.162 s % 235.43/33.46 % (371564)Peak memory usage: 15 MB % 235.43/33.46 % (371564)Instructions burned: 262 (million) % 235.43/33.46 % (371566)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=2833769438:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2812 on theBenchmark for (2812ds/1368Mi) % 235.43/33.46 % (371566)Instruction limit reached! % 235.43/33.46 % (371566)------------------------------ % 235.43/33.46 % (371566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.43/33.46 % (371566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.43/33.46 % (371566)CaDiCaL version: 2.1.3 % 235.43/33.46 % (371566)Termination reason: Instruction limit % 235.43/33.46 % (371566)Termination phase: Saturation % 235.43/33.46 % (371566)Time elapsed: 0.548 s % 235.43/33.46 % (371566)Peak memory usage: 17 MB % 235.43/33.46 % (371566)Instructions burned: 1369 (million) % 235.43/33.46 % (371568)ott-21_1_sil=16000:si=on:fs=off:random_seed=2332372896:i=360:av=off:fsr=off:rtra=on_2806 on theBenchmark for (2806ds/360Mi) % 235.43/33.46 % (371568)Instruction limit reached! % 235.43/33.46 % (371568)------------------------------ % 235.43/33.46 % (371568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.43/33.46 % (371568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.43/33.46 % (371568)CaDiCaL version: 2.1.3 % 235.43/33.46 % (371568)Termination reason: Instruction limit % 235.43/33.46 % (371568)Termination phase: Saturation % 235.43/33.46 % (371568)Time elapsed: 0.179 s % 235.43/33.46 % (371568)Peak memory usage: 15 MB % 235.43/33.46 % (371568)Instructions burned: 361 (million) % 235.43/33.46 % (371570)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1258671487:i=954:bd=all:rtra=on_2804 on theBenchmark for (2804ds/954Mi) % 235.43/33.46 % (371570)Instruction limit reached! % 235.43/33.46 % (371570)------------------------------ % 235.43/33.46 % (371570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.43/33.46 % (371570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.43/33.46 % (371570)CaDiCaL version: 2.1.3 % 235.43/33.46 % (371570)Termination reason: Instruction limit % 235.43/33.46 % (371570)Termination phase: Saturation % 235.43/33.46 % (371570)Time elapsed: 0.628 s % 235.43/33.46 % (371570)Peak memory usage: 16 MB % 235.43/33.46 % (371570)Instructions burned: 954 (million) % 235.43/33.46 % (371572)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3607140101:fmbsr=1.3:i=1730:ins=25:rtra=on_2797 on theBenchmark for (2797ds/1730Mi) % 235.43/33.46 % Exception at run slice level % 235.43/33.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 235.43/33.46 % (371574)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3746174202:i=2358:rtra=on_2797 on theBenchmark for (2797ds/2358Mi) % 235.43/33.46 % (371574)Instruction limit reached! % 235.43/33.46 % (371574)------------------------------ % 235.43/33.46 % (371574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 235.43/33.46 % (371574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.45/39.67 % (371574)CaDiCaL version: 2.1.3 % 279.45/39.67 % (371574)Termination reason: Instruction limit % 279.45/39.67 % (371574)Termination phase: Saturation % 279.45/39.67 % (371574)Time elapsed: 1.458 s % 279.45/39.67 % (371574)Peak memory usage: 31 MB % 279.45/39.67 % (371574)Instructions burned: 2358 (million) % 279.45/39.67 % (371576)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2778871614:i=1778:ins=1:rtra=on_2782 on theBenchmark for (2782ds/1778Mi) % 279.45/39.67 % Exception at run slice level % 279.45/39.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 279.45/39.67 % (371578)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=432711143:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/1384Mi) % 279.45/39.67 % (371578)Instruction limit reached! % 279.45/39.67 % (371578)------------------------------ % 279.45/39.67 % (371578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.45/39.67 % (371578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.45/39.67 % (371578)CaDiCaL version: 2.1.3 % 279.45/39.67 % (371578)Termination reason: Instruction limit % 279.45/39.67 % (371578)Termination phase: Saturation % 279.45/39.67 % (371578)Time elapsed: 0.660 s % 279.45/39.67 % (371578)Peak memory usage: 22 MB % 279.45/39.67 % (371578)Instructions burned: 1385 (million) % 279.45/39.67 % (371580)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3009729052:i=1758:kws=inv_precedence:fsr=off:rtra=on_2775 on theBenchmark for (2775ds/1758Mi) % 279.45/39.67 % (371580)Instruction limit reached! % 279.45/39.67 % (371580)------------------------------ % 279.45/39.67 % (371580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.45/39.67 % (371580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.45/39.67 % (371580)CaDiCaL version: 2.1.3 % 279.45/39.67 % (371580)Termination reason: Instruction limit % 279.45/39.67 % (371580)Termination phase: Saturation % 279.45/39.67 % (371580)Time elapsed: 0.987 s % 279.45/39.67 % (371580)Peak memory usage: 24 MB % 279.45/39.67 % (371580)Instructions burned: 1758 (million) % 279.45/39.67 % (371582)fmb+10_1_sil=64000:si=on:random_seed=3286063507:i=44122:nm=2:rtra=on:gsp=on_2765 on theBenchmark for (2765ds/44122Mi) % 279.45/39.67 % (371582)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 279.45/39.67 % Exception at run slice level % 279.45/39.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 279.45/39.67 % (371584)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=108255265:i=19030:nm=5:rtra=on_2765 on theBenchmark for (2765ds/19030Mi) % 279.45/39.67 % Exception at run slice level % 279.45/39.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 279.45/39.67 % (371586)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1861025492:fmbsr=1.7:i=1840:rtra=on_2765 on theBenchmark for (2765ds/1840Mi) % 279.45/39.67 % Exception at run slice level % 279.45/39.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 279.45/39.67 % (371588)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=441393308:i=10262:rtra=on_2765 on theBenchmark for (2765ds/10262Mi) % 279.45/39.67 % (371536)Instruction limit reached! % 279.45/39.67 % (371536)------------------------------ % 279.45/39.67 % (371536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 279.45/39.67 % (371536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.45/39.67 % (371536)CaDiCaL version: 2.1.3 % 279.45/39.67 % (371536)Termination reason: Instruction limit % 279.45/39.67 % (371536)Termination phase: Saturation % 279.45/39.67 % (371536)Time elapsed: 9.890 s % 279.45/39.67 % (371536)Peak memory usage: 383 MB % 279.45/39.67 % (371536)Instructions burned: 28120 (million) % 279.45/39.67 % (371590)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1330451563:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2732 on theBenchmark for (2732ds/2944Mi) % 279.45/39.67 % (371590)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 279.45/39.67 % (371590)Instruction limit reached! % 279.45/39.67 % (371590)------------------------------ % 279.45/39.67 % (371590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.53 % (371590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.53 % (371590)CaDiCaL version: 2.1.3 % 300.02/42.53 % (371590)Termination reason: Instruction limit % 300.02/42.53 % (371590)Termination phase: Saturation % 300.02/42.53 % (371590)Time elapsed: 0.965 s % 300.02/42.53 % (371590)Peak memory usage: 49 MB % 300.02/42.53 % (371590)Instructions burned: 2948 (million) % 300.02/42.53 % (371592)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=406991090:i=12648:rtra=on_2722 on theBenchmark for (2722ds/12648Mi) % 300.02/42.53 % Exception at run slice level % 300.02/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.02/42.53 % (371594)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1637673052:fmbsr=2.30978:i=4348:rtra=on_2722 on theBenchmark for (2722ds/4348Mi) % 300.02/42.53 % Exception at run slice level % 300.02/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.02/42.53 % (371596)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1389786558:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2722 on theBenchmark for (2722ds/1738Mi) % 300.02/42.53 % (371596)Instruction limit reached! % 300.02/42.53 % (371596)------------------------------ % 300.02/42.53 % (371596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.53 % (371596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.53 % (371596)CaDiCaL version: 2.1.3 % 300.02/42.53 % (371596)Termination reason: Instruction limit % 300.02/42.53 % (371596)Termination phase: Saturation % 300.02/42.53 % (371596)Time elapsed: 0.452 s % 300.02/42.53 % (371596)Peak memory usage: 20 MB % 300.02/42.53 % (371596)Instructions burned: 1741 (million) % 300.02/42.53 % (371598)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=2026352690:i=10228:av=off:rtra=on_2717 on theBenchmark for (2717ds/10228Mi) % 300.02/42.53 % (371082)Instruction limit reached! % 300.02/42.53 % (371082)------------------------------ % 300.02/42.53 % (371082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.53 % (371082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.53 % (371082)CaDiCaL version: 2.1.3 % 300.02/42.53 % (371082)Termination reason: Instruction limit % 300.02/42.53 % (371082)Termination phase: Saturation % 300.02/42.53 % (371082)Time elapsed: 29.439 s % 300.02/42.53 % (371082)Peak memory usage: 42 MB % 300.02/42.53 % (371082)Instructions burned: 88025 (million) % 300.02/42.53 % (371744)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=933181609:i=108564:rtra=on_2705 on theBenchmark for (2705ds/108564Mi) % 300.02/42.53 % Exception at run slice level % 300.02/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.02/42.53 % (371751)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=4038544153:i=7024:aac=none:rtra=on_2704 on theBenchmark for (2704ds/7024Mi) % 300.02/42.53 % (371588)Instruction limit reached! % 300.02/42.53 % (371588)------------------------------ % 300.02/42.53 % (371588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.53 % (371588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.53 % (371588)CaDiCaL version: 2.1.3 % 300.02/42.53 % (371588)Termination reason: Instruction limit % 300.02/42.53 % (371588)Termination phase: Saturation % 300.02/42.54 % (371588)Time elapsed: 6.180 s % 300.02/42.54 % (371588)Peak memory usage: 53 MB % 300.02/42.54 % (371588)Instructions burned: 10264 (million) % 300.02/42.54 % (371811)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=2866863544:i=7546:rtra=on:amm=off_2702 on theBenchmark for (2702ds/7546Mi) % 300.02/42.54 % (371598)Instruction limit reached! % 300.02/42.54 % (371598)------------------------------ % 300.02/42.54 % (371598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.02/42.54 % (371598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.02/42.54 % (371598)CaDiCaL version: 2.1.3 % 300.02/42.54 % (371598)Termination reason: Instruction limit % 300.02/42.54 % (371598)Termination phase: Saturation % 300.02/42.54 % (371598)Time elapsed: 3.526 s % 300.02/42.54 % (371598)Peak memory usage: 64 MB % 300.02/42.54 % (371598)Instructions burned: 10228 (million) % 300.02/42.54 % (371965)ott+11_1_sil=16000:si=on:gs=on:random_seed=2963591224:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2682 on theBenchmark for (2682ds/4502Mi) % 300.02/42.54 % (371965)Instruction limit reached! % 300.02/42.54 % (371965)-------------- % 300.02/42.54 Terminated % 300.02/42.54 % Vampire exiting %------------------------------------------------------------------------------