%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV775_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:26:23 PM UTC 2026 % Result : Timeout 300.01s 42.53s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV775_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n004.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 12:31:22 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.90/1.65 % (321988)Will run a generic schedule for satisfiability detection. % 8.90/1.65 % (321993)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=84040829_2999 on theBenchmark for (2999ds/0Mi) % 8.90/1.65 % (321994)% WARNING: option uhcvi not known. % 8.90/1.65 % Exception at run slice level % 8.90/1.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.90/1.65 % (321996)dis+10_1_sil=32000:sp=arity:random_seed=362667014:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.90/1.65 % (321994)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1850859111:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.90/1.65 % (321995)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2062597041:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.90/1.65 % (321997)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1942581144:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.90/1.65 % (321998)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4081792935:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.90/1.65 % (321999)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3173483984:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.90/1.65 % (322001)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1886911039:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.90/1.65 % Exception at run slice level % 8.90/1.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 8.90/1.65 % (322009)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3712466404:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.90/1.65 % (321996)Instruction limit reached! % 8.90/1.65 % (321996)------------------------------ % 8.90/1.65 % (321996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.65 % (321996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.65 % (321996)CaDiCaL version: 2.1.3 % 8.90/1.65 % (321996)Termination reason: Instruction limit % 8.90/1.65 % (321996)Termination phase: Saturation % 8.90/1.65 % (321996)Time elapsed: 0.062 s % 8.90/1.65 % (321996)Peak memory usage: 12 MB % 8.90/1.65 % (321996)Instructions burned: 108 (million) % 8.90/1.65 % (322009)Instruction limit reached! % 8.90/1.65 % (322009)------------------------------ % 8.90/1.65 % (322009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.65 % (321997)Instruction limit reached! % 8.90/1.65 % (321997)------------------------------ % 8.90/1.65 % (321997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.65 % (321997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.65 % (321997)CaDiCaL version: 2.1.3 % 8.90/1.65 % (321997)Termination reason: Instruction limit % 8.90/1.65 % (321997)Termination phase: Saturation % 8.90/1.65 % (321997)Time elapsed: 0.063 s % 8.90/1.65 % (321997)Peak memory usage: 12 MB % 8.90/1.65 % (321997)Instructions burned: 116 (million) % 8.90/1.65 % (322009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.65 % (322009)CaDiCaL version: 2.1.3 % 8.90/1.65 % (322009)Termination reason: Instruction limit % 8.90/1.65 % (322009)Termination phase: Saturation % 8.90/1.65 % (322009)Time elapsed: 0.041 s % 8.90/1.65 % (322009)Peak memory usage: 13 MB % 8.90/1.65 % (322009)Instructions burned: 134 (million) % 8.90/1.65 % (321998)Instruction limit reached! % 8.90/1.65 % (321998)------------------------------ % 8.90/1.65 % (321998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.90/1.65 % (321998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.90/1.65 % (321998)CaDiCaL version: 2.1.3 % 8.90/1.65 % (321998)Termination reason: Instruction limit % 8.90/1.65 % (321998)Termination phase: Saturation % 8.90/1.65 % (321998)Time elapsed: 0.070 s % 8.90/1.65 % (321998)Peak memory usage: 13 MB % 8.90/1.65 % (321998)Instructions burned: 131 (million) % 8.90/1.65 % (322013)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=337664510:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 8.90/1.65 % (322011)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=3320442838:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.90/1.65 % (322012)ott-21_1_sil=16000:fs=off:random_seed=247248894:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 21.06/3.29 % (322014)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3386965949:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 21.06/3.29 % (321999)Instruction limit reached! % 21.06/3.29 % (321999)------------------------------ % 21.06/3.29 % (321999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.29 % (321999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.29 % (321999)CaDiCaL version: 2.1.3 % 21.06/3.29 % (321999)Termination reason: Instruction limit % 21.06/3.29 % (321999)Termination phase: Saturation % 21.06/3.29 % (321999)Time elapsed: 0.091 s % 21.06/3.29 % (321999)Peak memory usage: 13 MB % 21.06/3.29 % (321999)Instructions burned: 160 (million) % 21.06/3.29 % Exception at run slice level % 21.06/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.06/3.29 % (322019)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=896233058:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 21.06/3.29 % (322020)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2797741609:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi) % 21.06/3.29 % Exception at run slice level % 21.06/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.06/3.29 % (322023)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=1466427041: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.06/3.29 % (322012)Instruction limit reached! % 21.06/3.29 % (322012)------------------------------ % 21.06/3.29 % (322012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.29 % (322012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.29 % (322012)CaDiCaL version: 2.1.3 % 21.06/3.29 % (322012)Termination reason: Instruction limit % 21.06/3.29 % (322012)Termination phase: Saturation % 21.06/3.29 % (322012)Time elapsed: 0.095 s % 21.06/3.29 % (322012)Peak memory usage: 12 MB % 21.06/3.29 % (322012)Instructions burned: 180 (million) % 21.06/3.29 % (322025)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2340753605:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 21.06/3.29 % (322013)Instruction limit reached! % 21.06/3.29 % (322013)------------------------------ % 21.06/3.29 % (322013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.29 % (322013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.29 % (322013)CaDiCaL version: 2.1.3 % 21.06/3.29 % (322013)Termination reason: Instruction limit % 21.06/3.29 % (322013)Termination phase: Saturation % 21.06/3.29 % (322013)Time elapsed: 0.148 s % 21.06/3.29 % (322013)Peak memory usage: 14 MB % 21.06/3.29 % (322013)Instructions burned: 477 (million) % 21.06/3.29 % (322027)fmb+10_1_sil=64000:random_seed=1072673223:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi) % 21.06/3.29 % (322027)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 21.06/3.29 % Exception at run slice level % 21.06/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.06/3.29 % (322029)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1690625172:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi) % 21.06/3.29 % Exception at run slice level % 21.06/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.06/3.29 % (322031)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1518709118:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi) % 21.06/3.29 % Exception at run slice level % 21.06/3.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 21.06/3.29 % (322033)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3607047370:i=5131_2996 on theBenchmark for (2996ds/5131Mi) % 21.06/3.29 % (322011)Instruction limit reached! % 21.06/3.29 % (322011)------------------------------ % 21.06/3.29 % (322011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 21.06/3.29 % (322011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.06/3.29 % (322011)CaDiCaL version: 2.1.3 % 21.06/3.29 % (322011)Termination reason: Instruction limit % 21.06/3.29 % (322011)Termination phase: Saturation % 57.37/8.43 % (322011)Time elapsed: 0.380 s % 57.37/8.43 % (322011)Peak memory usage: 17 MB % 57.37/8.43 % (322011)Instructions burned: 685 (million) % 57.37/8.43 % (322035)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1576251091:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi) % 57.37/8.43 % (322035)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 57.37/8.43 % (322023)Instruction limit reached! % 57.37/8.43 % (322023)------------------------------ % 57.37/8.43 % (322023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.37/8.43 % (322023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.37/8.43 % (322023)CaDiCaL version: 2.1.3 % 57.37/8.43 % (322023)Termination reason: Instruction limit % 57.37/8.43 % (322023)Termination phase: Saturation % 57.37/8.43 % (322023)Time elapsed: 0.373 s % 57.37/8.43 % (322023)Peak memory usage: 17 MB % 57.37/8.43 % (322023)Instructions burned: 693 (million) % 57.37/8.43 % (322037)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=874525925:i=6324_2994 on theBenchmark for (2994ds/6324Mi) % 57.37/8.43 % Exception at run slice level % 57.37/8.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 57.37/8.43 % (322039)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3135884026:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi) % 57.37/8.43 % Exception at run slice level % 57.37/8.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 57.37/8.43 % (322041)ott-2_1_sil=16000:newcnf=on:random_seed=1857717585:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi) % 57.37/8.43 % (322025)Instruction limit reached! % 57.37/8.43 % (322025)------------------------------ % 57.37/8.43 % (322025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.37/8.43 % (322025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.37/8.43 % (322025)CaDiCaL version: 2.1.3 % 57.37/8.43 % (322025)Termination reason: Instruction limit % 57.37/8.43 % (322025)Termination phase: Saturation % 57.37/8.43 % (322025)Time elapsed: 0.475 s % 57.37/8.43 % (322025)Peak memory usage: 17 MB % 57.37/8.43 % (322025)Instructions burned: 881 (million) % 57.37/8.43 % (322043)ott+10_1_sil=32000:tgt=ground:random_seed=1250505938:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi) % 57.37/8.43 % (322019)Instruction limit reached! % 57.37/8.43 % (322019)------------------------------ % 57.37/8.43 % (322019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.37/8.43 % (322019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.37/8.43 % (322019)CaDiCaL version: 2.1.3 % 57.37/8.43 % (322019)Termination reason: Instruction limit % 57.37/8.43 % (322019)Termination phase: Saturation % 57.37/8.43 % (322019)Time elapsed: 0.662 s % 57.37/8.43 % (322019)Peak memory usage: 20 MB % 57.37/8.43 % (322019)Instructions burned: 1180 (million) % 57.37/8.43 % (322045)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1413447017:i=54282_2991 on theBenchmark for (2991ds/54282Mi) % 57.37/8.43 % Exception at run slice level % 57.37/8.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 57.37/8.43 % (322047)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3318244500:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi) % 57.37/8.43 % (322041)Instruction limit reached! % 57.37/8.43 % (322041)------------------------------ % 57.37/8.43 % (322041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.37/8.43 % (322041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.37/8.43 % (322041)CaDiCaL version: 2.1.3 % 57.37/8.43 % (322041)Termination reason: Instruction limit % 57.37/8.43 % (322041)Termination phase: Saturation % 57.37/8.43 % (322041)Time elapsed: 0.483 s % 57.37/8.43 % (322041)Peak memory usage: 18 MB % 57.37/8.43 % (322041)Instructions burned: 870 (million) % 57.37/8.43 % (322049)dis+21_1_sil=32000:sas=cadical:random_seed=1128073056:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi) % 57.37/8.43 % (322035)Instruction limit reached! % 57.37/8.43 % (322035)------------------------------ % 57.37/8.43 % (322035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 57.37/8.43 % (322035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.37/8.43 % (322035)CaDiCaL version: 2.1.3 % 113.33/16.28 % (322035)Termination reason: Instruction limit % 113.33/16.28 % (322035)Termination phase: Saturation % 113.33/16.28 % (322035)Time elapsed: 0.896 s % 113.33/16.28 % (322035)Peak memory usage: 32 MB % 113.33/16.28 % (322035)Instructions burned: 1473 (million) % 113.33/16.28 % (322051)ott+11_1_sil=16000:gs=on:random_seed=2774026963:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi) % 113.33/16.28 % (322033)Instruction limit reached! % 113.33/16.28 % (322033)------------------------------ % 113.33/16.28 % (322033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.28 % (322033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.28 % (322033)CaDiCaL version: 2.1.3 % 113.33/16.28 % (322033)Termination reason: Instruction limit % 113.33/16.28 % (322033)Termination phase: Saturation % 113.33/16.28 % (322033)Time elapsed: 1.378 s % 113.33/16.28 % (322033)Peak memory usage: 38 MB % 113.33/16.28 % (322033)Instructions burned: 5131 (million) % 113.33/16.28 % (322053)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2787232314:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi) % 113.33/16.28 % Exception at run slice level % 113.33/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.33/16.28 % (322055)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=362053673:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi) % 113.33/16.28 % (322051)Instruction limit reached! % 113.33/16.28 % (322051)------------------------------ % 113.33/16.28 % (322051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.28 % (322051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.28 % (322051)CaDiCaL version: 2.1.3 % 113.33/16.28 % (322051)Termination reason: Instruction limit % 113.33/16.28 % (322051)Termination phase: Saturation % 113.33/16.28 % (322051)Time elapsed: 1.059 s % 113.33/16.28 % (322051)Peak memory usage: 20 MB % 113.33/16.28 % (322051)Instructions burned: 2253 (million) % 113.33/16.28 % (322058)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2530708377:i=29340_2975 on theBenchmark for (2975ds/29340Mi) % 113.33/16.28 % (322047)Instruction limit reached! % 113.33/16.28 % (322047)------------------------------ % 113.33/16.28 % (322047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.28 % (322047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.28 % (322047)CaDiCaL version: 2.1.3 % 113.33/16.28 % (322047)Termination reason: Instruction limit % 113.33/16.28 % (322047)Termination phase: Saturation % 113.33/16.28 % (322047)Time elapsed: 1.838 s % 113.33/16.28 % (322047)Peak memory usage: 29 MB % 113.33/16.28 % (322047)Instructions burned: 3513 (million) % 113.33/16.28 % (322060)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=519002107:i=5211_2972 on theBenchmark for (2972ds/5211Mi) % 113.33/16.28 % (322055)Instruction limit reached! % 113.33/16.28 % (322055)------------------------------ % 113.33/16.28 % (322055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 113.33/16.28 % (322055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.33/16.28 % (322055)CaDiCaL version: 2.1.3 % 113.33/16.28 % (322055)Termination reason: Instruction limit % 113.33/16.28 % (322055)Termination phase: Saturation % 113.33/16.28 % (322055)Time elapsed: 1.278 s % 113.33/16.28 % (322055)Peak memory usage: 66 MB % 113.33/16.28 % (322055)Instructions burned: 4592 (million) % 113.33/16.28 % (322062)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=496586991:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi) % 113.33/16.28 % Exception at run slice level % 113.33/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.33/16.28 % (322064)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1454510715:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi) % 113.33/16.28 % Exception at run slice level % 113.33/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.33/16.28 % (322066)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1376883649:i=14071_2969 on theBenchmark for (2969ds/14071Mi) % 113.33/16.28 % Exception at run slice level % 113.33/16.28 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 113.33/16.28 % (322068)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3657026153:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi) % 124.60/17.90 % (322049)Instruction limit reached! % 124.60/17.90 % (322049)------------------------------ % 124.60/17.90 % (322049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.60/17.90 % (322049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.60/17.90 % (322049)CaDiCaL version: 2.1.3 % 124.60/17.90 % (322049)Termination reason: Instruction limit % 124.60/17.90 % (322049)Termination phase: Saturation % 124.60/17.90 % (322049)Time elapsed: 1.993 s % 124.60/17.90 % (322049)Peak memory usage: 31 MB % 124.60/17.90 % (322049)Instructions burned: 3773 (million) % 124.60/17.90 % (322070)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1471729318:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi) % 124.60/17.90 % (322043)Instruction limit reached! % 124.60/17.90 % (322043)------------------------------ % 124.60/17.90 % (322043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.60/17.90 % (322043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.60/17.90 % (322043)CaDiCaL version: 2.1.3 % 124.60/17.90 % (322043)Termination reason: Instruction limit % 124.60/17.90 % (322043)Termination phase: Saturation % 124.60/17.90 % (322043)Time elapsed: 2.907 s % 124.60/17.90 % (322043)Peak memory usage: 49 MB % 124.60/17.90 % (322043)Instructions burned: 5115 (million) % 124.60/17.90 % (322072)dis+10_16:1_sil=16000:random_seed=738418783:i=9155:fsr=off_2963 on theBenchmark for (2963ds/9155Mi) % 124.60/17.90 % (322060)Instruction limit reached! % 124.60/17.90 % (322060)------------------------------ % 124.60/17.90 % (322060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.60/17.90 % (322060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.60/17.90 % (322060)CaDiCaL version: 2.1.3 % 124.60/17.90 % (322060)Termination reason: Instruction limit % 124.60/17.90 % (322060)Termination phase: Saturation % 124.60/17.90 % (322060)Time elapsed: 2.638 s % 124.60/17.90 % (322060)Peak memory usage: 43 MB % 124.60/17.90 % (322060)Instructions burned: 5212 (million) % 124.60/17.90 % (322074)ott-3_8_sil=64000:random_seed=84524038:i=20139:bs=on_2946 on theBenchmark for (2946ds/20139Mi) % 124.60/17.90 % (322070)Instruction limit reached! % 124.60/17.90 % (322070)------------------------------ % 124.60/17.90 % (322070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.60/17.90 % (322070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.60/17.90 % (322070)CaDiCaL version: 2.1.3 % 124.60/17.90 % (322070)Termination reason: Instruction limit % 124.60/17.90 % (322070)Termination phase: Saturation % 124.60/17.90 % (322070)Time elapsed: 4.648 s % 124.60/17.90 % (322070)Peak memory usage: 73 MB % 124.60/17.90 % (322070)Instructions burned: 8174 (million) % 124.60/17.90 % (322076)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=192667821:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi) % 124.60/17.90 % Exception at run slice level % 124.60/17.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 124.60/17.90 % (322078)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1251380990:i=11404_2921 on theBenchmark for (2921ds/11404Mi) % 124.60/17.90 % (322068)Instruction limit reached! % 124.60/17.90 % (322068)------------------------------ % 124.60/17.90 % (322068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.60/17.90 % (322068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.60/17.90 % (322068)CaDiCaL version: 2.1.3 % 124.60/17.90 % (322068)Termination reason: Instruction limit % 124.60/17.90 % (322068)Termination phase: Saturation % 124.60/17.90 % (322068)Time elapsed: 4.810 s % 124.60/17.90 % (322068)Peak memory usage: 111 MB % 124.60/17.90 % (322068)Instructions burned: 22569 (million) % 124.60/17.90 % (322080)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1045413586:i=14134_2921 on theBenchmark for (2921ds/14134Mi) % 124.60/17.90 % (322072)Instruction limit reached! % 124.60/17.90 % (322072)------------------------------ % 124.60/17.90 % (322072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 124.60/17.90 % (322072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.60/17.90 % (322072)CaDiCaL version: 2.1.3 % 124.60/17.90 % (322072)Termination reason: Instruction limit % 124.60/17.90 % (322072)Termination phase: Saturation % 124.60/17.90 % (322072)Time elapsed: 4.512 s % 124.60/17.90 % (322072)Peak memory usage: 44 MB % 124.60/17.90 % (322072)Instructions burned: 9155 (million) % 124.60/17.90 % (322082)dis+33_16_sil=32000:sac=on:random_seed=1593112236:i=15851:nm=0_2918 on theBenchmark for (2918ds/15851Mi) % 148.81/21.21 % (322080)Instruction limit reached! % 148.81/21.21 % (322080)------------------------------ % 148.81/21.21 % (322080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.81/21.21 % (322080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.81/21.21 % (322080)CaDiCaL version: 2.1.3 % 148.81/21.21 % (322080)Termination reason: Instruction limit % 148.81/21.21 % (322080)Termination phase: Saturation % 148.81/21.21 % (322080)Time elapsed: 4.333 s % 148.81/21.21 % (322080)Peak memory usage: 101 MB % 148.81/21.21 % (322080)Instructions burned: 14136 (million) % 148.81/21.21 % (322084)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=934788122:avsq=on:i=17627:add=on:amm=off_2877 on theBenchmark for (2877ds/17627Mi) % 148.81/21.21 % (322078)Instruction limit reached! % 148.81/21.21 % (322078)------------------------------ % 148.81/21.21 % (322078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.81/21.21 % (322078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.81/21.21 % (322078)CaDiCaL version: 2.1.3 % 148.81/21.21 % (322078)Termination reason: Instruction limit % 148.81/21.21 % (322078)Termination phase: Saturation % 148.81/21.21 % (322078)Time elapsed: 6.593 s % 148.81/21.21 % (322078)Peak memory usage: 91 MB % 148.81/21.21 % (322078)Instructions burned: 11405 (million) % 148.81/21.21 % (322086)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4123704166:s2a=on:i=53295_2855 on theBenchmark for (2855ds/53295Mi) % 148.81/21.21 % (322058)Instruction limit reached! % 148.81/21.21 % (322058)------------------------------ % 148.81/21.21 % (322058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.81/21.21 % (322058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.81/21.21 % (322058)CaDiCaL version: 2.1.3 % 148.81/21.21 % (322058)Termination reason: Instruction limit % 148.81/21.21 % (322058)Termination phase: Saturation % 148.81/21.21 % (322058)Time elapsed: 12.684 s % 148.81/21.21 % (322058)Peak memory usage: 149 MB % 148.81/21.21 % (322058)Instructions burned: 29341 (million) % 148.81/21.21 % (322088)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3419115415:i=26857:ins=20_2847 on theBenchmark for (2847ds/26857Mi) % 148.81/21.21 % Exception at run slice level % 148.81/21.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 148.81/21.21 % (322090)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=8438030:i=28120:bs=on:fsr=off_2847 on theBenchmark for (2847ds/28120Mi) % 148.81/21.21 % (322082)Instruction limit reached! % 148.81/21.21 % (322082)------------------------------ % 148.81/21.21 % (322082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 148.81/21.21 % (322082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.81/21.21 % (322082)CaDiCaL version: 2.1.3 % 148.81/21.21 % (322082)Termination reason: Instruction limit % 148.81/21.21 % (322082)Termination phase: Saturation % 148.81/21.21 % (322082)Time elapsed: 7.706 s % 148.81/21.21 % (322082)Peak memory usage: 119 MB % 148.81/21.21 % (322082)Instructions burned: 15852 (million) % 148.81/21.21 % (322092)fmb+10_1_sil=256000:fmbss=7:random_seed=3929295149:fmbsr=1.6:i=182295_2840 on theBenchmark for (2840ds/182295Mi) % 148.81/21.21 % Exception at run slice level % 148.81/21.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 148.81/21.21 % (322094)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=980866064:i=44625:gsp=on_2840 on theBenchmark for (2840ds/44625Mi) % 148.81/21.21 % (322094)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 148.81/21.21 % Exception at run slice level % 148.81/21.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 148.81/21.21 % (322096)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1274857620:i=160505_2840 on theBenchmark for (2840ds/160505Mi) % 148.81/21.21 % Exception at run slice level % 148.81/21.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 148.81/21.21 % (322098)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3267406752:fmbsr=1.3:i=225729_2839 on theBenchmark for (2839ds/225729Mi) % 148.81/21.21 % Exception at run slice level % 148.81/21.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 148.81/21.21 % (322100)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3676017689:fmbsr=2:i=185024:ins=7_2839 on theBenchmark for (2839ds/185024Mi) % 200.61/28.51 % Exception at run slice level % 200.61/28.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 200.61/28.51 % (322102)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1538443176:rtra=on_2839 on theBenchmark for (2839ds/0Mi) % 200.61/28.51 % (322084)Instruction limit reached! % 200.61/28.51 % (322084)------------------------------ % 200.61/28.51 % (322084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.61/28.51 % (322084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.61/28.51 % (322084)CaDiCaL version: 2.1.3 % 200.61/28.51 % (322084)Termination reason: Instruction limit % 200.61/28.51 % (322084)Termination phase: Saturation % 200.61/28.51 % (322084)Time elapsed: 3.844 s % 200.61/28.51 % (322084)Peak memory usage: 48 MB % 200.61/28.51 % (322084)Instructions burned: 17631 (million) % 200.61/28.51 % Exception at run slice level % 200.61/28.51 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 200.61/28.51 % (322105)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3847639059:i=176048:add=on:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/176048Mi) % 200.61/28.51 % (322104)% WARNING: option uhcvi not known. % 200.61/28.51 % (322104)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=241155656:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi) % 200.61/28.51 % (322074)Instruction limit reached! % 200.61/28.51 % (322074)------------------------------ % 200.61/28.51 % (322074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.61/28.51 % (322074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.61/28.51 % (322074)CaDiCaL version: 2.1.3 % 200.61/28.51 % (322074)Termination reason: Instruction limit % 200.61/28.51 % (322074)Termination phase: Saturation % 200.61/28.51 % (322074)Time elapsed: 11.594 s % 200.61/28.51 % (322074)Peak memory usage: 86 MB % 200.61/28.51 % (322074)Instructions burned: 20140 (million) % 200.61/28.51 % (322108)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3461798042:i=206:fgj=on:rtra=on_2830 on theBenchmark for (2830ds/206Mi) % 200.61/28.51 % (322108)Instruction limit reached! % 200.61/28.51 % (322108)------------------------------ % 200.61/28.51 % (322108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.61/28.51 % (322108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.61/28.51 % (322108)CaDiCaL version: 2.1.3 % 200.61/28.51 % (322108)Termination reason: Instruction limit % 200.61/28.51 % (322108)Termination phase: Saturation % 200.61/28.51 % (322108)Time elapsed: 0.121 s % 200.61/28.51 % (322108)Peak memory usage: 13 MB % 200.61/28.51 % (322108)Instructions burned: 207 (million) % 200.61/28.51 % (322110)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3095096633:i=232:rtra=on_2828 on theBenchmark for (2828ds/232Mi) % 200.61/28.51 % (322110)Instruction limit reached! % 200.61/28.51 % (322110)------------------------------ % 200.61/28.51 % (322110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.61/28.51 % (322110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.61/28.51 % (322110)CaDiCaL version: 2.1.3 % 200.61/28.51 % (322110)Termination reason: Instruction limit % 200.61/28.51 % (322110)Termination phase: Saturation % 200.61/28.51 % (322110)Time elapsed: 0.136 s % 200.61/28.51 % (322110)Peak memory usage: 13 MB % 200.61/28.51 % (322110)Instructions burned: 233 (million) % 200.61/28.51 % (322112)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3311230983:i=262:rtra=on_2827 on theBenchmark for (2827ds/262Mi) % 200.61/28.51 % (322112)Instruction limit reached! % 200.61/28.51 % (322112)------------------------------ % 200.61/28.51 % (322112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.61/28.51 % (322112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.61/28.51 % (322112)CaDiCaL version: 2.1.3 % 200.61/28.51 % (322112)Termination reason: Instruction limit % 200.61/28.51 % (322112)Termination phase: Saturation % 200.61/28.51 % (322112)Time elapsed: 0.153 s % 200.61/28.51 % (322112)Peak memory usage: 14 MB % 200.61/28.51 % (322112)Instructions burned: 262 (million) % 200.61/28.51 % (322114)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2792425134:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2825 on theBenchmark for (2825ds/318Mi) % 200.61/28.51 % (322114)Instruction limit reached! % 200.61/28.51 % (322114)------------------------------ % 200.61/28.51 % (322114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.97/34.01 % (322114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.97/34.01 % (322114)CaDiCaL version: 2.1.3 % 238.97/34.01 % (322114)Termination reason: Instruction limit % 238.97/34.01 % (322114)Termination phase: Saturation % 238.97/34.01 % (322114)Time elapsed: 0.185 s % 238.97/34.01 % (322114)Peak memory usage: 14 MB % 238.97/34.01 % (322114)Instructions burned: 319 (million) % 238.97/34.01 % (322116)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=1540993676:i=1428:nm=2:rtra=on_2823 on theBenchmark for (2823ds/1428Mi) % 238.97/34.01 % Exception at run slice level % 238.97/34.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 238.97/34.01 % (322118)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3905718420:i=262:bd=preordered:rtra=on:fsd=on_2823 on theBenchmark for (2823ds/262Mi) % 238.97/34.01 % (322118)Instruction limit reached! % 238.97/34.01 % (322118)------------------------------ % 238.97/34.01 % (322118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.97/34.01 % (322118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.97/34.01 % (322118)CaDiCaL version: 2.1.3 % 238.97/34.01 % (322118)Termination reason: Instruction limit % 238.97/34.01 % (322118)Termination phase: Saturation % 238.97/34.01 % (322118)Time elapsed: 0.157 s % 238.97/34.01 % (322118)Peak memory usage: 14 MB % 238.97/34.01 % (322118)Instructions burned: 263 (million) % 238.97/34.01 % (322120)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=90251528:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2821 on theBenchmark for (2821ds/1368Mi) % 238.97/34.01 % (322120)Instruction limit reached! % 238.97/34.01 % (322120)------------------------------ % 238.97/34.01 % (322120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.97/34.01 % (322120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.97/34.01 % (322120)CaDiCaL version: 2.1.3 % 238.97/34.01 % (322120)Termination reason: Instruction limit % 238.97/34.01 % (322120)Termination phase: Saturation % 238.97/34.01 % (322120)Time elapsed: 0.787 s % 238.97/34.01 % (322120)Peak memory usage: 21 MB % 238.97/34.01 % (322120)Instructions burned: 1369 (million) % 238.97/34.01 % (322122)ott-21_1_sil=16000:si=on:fs=off:random_seed=240848582:i=360:av=off:fsr=off:rtra=on_2813 on theBenchmark for (2813ds/360Mi) % 238.97/34.01 % (322122)Instruction limit reached! % 238.97/34.01 % (322122)------------------------------ % 238.97/34.01 % (322122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.97/34.01 % (322122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.97/34.01 % (322122)CaDiCaL version: 2.1.3 % 238.97/34.01 % (322122)Termination reason: Instruction limit % 238.97/34.01 % (322122)Termination phase: Saturation % 238.97/34.01 % (322122)Time elapsed: 0.190 s % 238.97/34.01 % (322122)Peak memory usage: 14 MB % 238.97/34.01 % (322122)Instructions burned: 361 (million) % 238.97/34.01 % (322124)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=571659666:i=954:bd=all:rtra=on_2811 on theBenchmark for (2811ds/954Mi) % 238.97/34.01 % (322124)Instruction limit reached! % 238.97/34.01 % (322124)------------------------------ % 238.97/34.01 % (322124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.97/34.01 % (322124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.97/34.01 % (322124)CaDiCaL version: 2.1.3 % 238.97/34.01 % (322124)Termination reason: Instruction limit % 238.97/34.01 % (322124)Termination phase: Saturation % 238.97/34.01 % (322124)Time elapsed: 0.566 s % 238.97/34.01 % (322124)Peak memory usage: 15 MB % 238.97/34.01 % (322124)Instructions burned: 955 (million) % 238.97/34.01 % (322126)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=1479196569:fmbsr=1.3:i=1730:ins=25:rtra=on_2805 on theBenchmark for (2805ds/1730Mi) % 238.97/34.01 % Exception at run slice level % 238.97/34.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 238.97/34.01 % (322128)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3368817260:i=2358:rtra=on_2804 on theBenchmark for (2804ds/2358Mi) % 238.97/34.01 % (322128)Instruction limit reached! % 238.97/34.01 % (322128)------------------------------ % 238.97/34.01 % (322128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 238.97/34.01 % (322128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.38 % (322128)CaDiCaL version: 2.1.3 % 270.20/38.38 % (322128)Termination reason: Instruction limit % 270.20/38.38 % (322128)Termination phase: Saturation % 270.20/38.38 % (322128)Time elapsed: 1.450 s % 270.20/38.38 % (322128)Peak memory usage: 26 MB % 270.20/38.38 % (322128)Instructions burned: 2358 (million) % 270.20/38.38 % (322130)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1686888646:i=1778:ins=1:rtra=on_2790 on theBenchmark for (2790ds/1778Mi) % 270.20/38.38 % Exception at run slice level % 270.20/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 270.20/38.38 % (322132)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=1301978249:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2789 on theBenchmark for (2789ds/1384Mi) % 270.20/38.38 % (322132)Instruction limit reached! % 270.20/38.38 % (322132)------------------------------ % 270.20/38.38 % (322132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.38 % (322132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.38 % (322132)CaDiCaL version: 2.1.3 % 270.20/38.38 % (322132)Termination reason: Instruction limit % 270.20/38.38 % (322132)Termination phase: Saturation % 270.20/38.38 % (322132)Time elapsed: 0.800 s % 270.20/38.38 % (322132)Peak memory usage: 21 MB % 270.20/38.38 % (322132)Instructions burned: 1386 (million) % 270.20/38.38 % (322134)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=442057117:i=1758:kws=inv_precedence:fsr=off:rtra=on_2781 on theBenchmark for (2781ds/1758Mi) % 270.20/38.38 % (322134)Instruction limit reached! % 270.20/38.38 % (322134)------------------------------ % 270.20/38.38 % (322134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.38 % (322134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.38 % (322134)CaDiCaL version: 2.1.3 % 270.20/38.38 % (322134)Termination reason: Instruction limit % 270.20/38.38 % (322134)Termination phase: Saturation % 270.20/38.38 % (322134)Time elapsed: 0.946 s % 270.20/38.38 % (322134)Peak memory usage: 22 MB % 270.20/38.38 % (322134)Instructions burned: 1758 (million) % 270.20/38.38 % (322136)fmb+10_1_sil=64000:si=on:random_seed=2381884279:i=44122:nm=2:rtra=on:gsp=on_2772 on theBenchmark for (2772ds/44122Mi) % 270.20/38.38 % (322136)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 270.20/38.38 % Exception at run slice level % 270.20/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 270.20/38.38 % (322138)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1084536894:i=19030:nm=5:rtra=on_2771 on theBenchmark for (2771ds/19030Mi) % 270.20/38.38 % Exception at run slice level % 270.20/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 270.20/38.38 % (322140)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=4135568927:fmbsr=1.7:i=1840:rtra=on_2771 on theBenchmark for (2771ds/1840Mi) % 270.20/38.38 % Exception at run slice level % 270.20/38.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 270.20/38.38 % (322142)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3752734488:i=10262:rtra=on_2771 on theBenchmark for (2771ds/10262Mi) % 270.20/38.38 % (322090)Instruction limit reached! % 270.20/38.38 % (322090)------------------------------ % 270.20/38.38 % (322090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 270.20/38.38 % (322090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.20/38.38 % (322090)CaDiCaL version: 2.1.3 % 270.20/38.38 % (322090)Termination reason: Instruction limit % 270.20/38.38 % (322090)Termination phase: Saturation % 270.20/38.38 % (322090)Time elapsed: 11.369 s % 270.20/38.38 % (322090)Peak memory usage: 43 MB % 270.20/38.38 % (322090)Instructions burned: 28121 (million) % 270.20/38.38 % (322144)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3934325890:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2733 on theBenchmark for (2733ds/2944Mi) % 270.20/38.38 % (322144)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 270.20/38.38 % (322144)Instruction limit reached! % 270.20/38.38 % (322144)------------------------------ % 270.20/38.38 % (322144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (322144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (322144)CaDiCaL version: 2.1.3 % 300.01/42.53 % (322144)Termination reason: Instruction limit % 300.01/42.53 % (322144)Termination phase: Saturation % 300.01/42.53 % (322144)Time elapsed: 1.606 s % 300.01/42.53 % (322144)Peak memory usage: 39 MB % 300.01/42.53 % (322144)Instructions burned: 2944 (million) % 300.01/42.53 % (322146)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=3296966174:i=12648:rtra=on_2717 on theBenchmark for (2717ds/12648Mi) % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (322148)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=3520849964:fmbsr=2.30978:i=4348:rtra=on_2716 on theBenchmark for (2716ds/4348Mi) % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (322150)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=500272722:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2716 on theBenchmark for (2716ds/1738Mi) % 300.01/42.53 % (321995)Instruction limit reached! % 300.01/42.53 % (321995)------------------------------ % 300.01/42.53 % (321995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (321995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (321995)CaDiCaL version: 2.1.3 % 300.01/42.53 % (321995)Termination reason: Instruction limit % 300.01/42.53 % (321995)Termination phase: Saturation % 300.01/42.53 % (321995)Time elapsed: 28.441 s % 300.01/42.53 % (321995)Peak memory usage: 152 MB % 300.01/42.53 % (321995)Instructions burned: 88025 (million) % 300.01/42.53 % (322152)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1680039040:i=10228:av=off:rtra=on_2715 on theBenchmark for (2715ds/10228Mi) % 300.01/42.53 % (322142)Instruction limit reached! % 300.01/42.53 % (322142)------------------------------ % 300.01/42.53 % (322142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (322142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (322142)CaDiCaL version: 2.1.3 % 300.01/42.53 % (322142)Termination reason: Instruction limit % 300.01/42.53 % (322142)Termination phase: Saturation % 300.01/42.53 % (322142)Time elapsed: 5.619 s % 300.01/42.53 % (322142)Peak memory usage: 52 MB % 300.01/42.53 % (322142)Instructions burned: 10263 (million) % 300.01/42.53 % (322154)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=2433304471:i=108564:rtra=on_2714 on theBenchmark for (2714ds/108564Mi) % 300.01/42.53 % Exception at run slice level % 300.01/42.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 300.01/42.53 % (322156)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3828774194:i=7024:aac=none:rtra=on_2714 on theBenchmark for (2714ds/7024Mi) % 300.01/42.53 % (322150)Instruction limit reached! % 300.01/42.53 % (322150)------------------------------ % 300.01/42.53 % (322150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (322150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (322150)CaDiCaL version: 2.1.3 % 300.01/42.53 % (322150)Termination reason: Instruction limit % 300.01/42.53 % (322150)Termination phase: Saturation % 300.01/42.53 % (322150)Time elapsed: 1.046 s % 300.01/42.53 % (322150)Peak memory usage: 22 MB % 300.01/42.53 % (322150)Instructions burned: 1739 (million) % 300.01/42.53 % (322158)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=4209853437:i=7546:rtra=on:amm=off_2705 on theBenchmark for (2705ds/7546Mi) % 300.01/42.53 % (322156)Instruction limit reached! % 300.01/42.53 % (322156)------------------------------ % 300.01/42.53 % (322156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.01/42.53 % (322156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.01/42.53 % (322156)CaDiCaL version: 2.1.3 % 300.01/42.53 % (322156)Termination reason: Instruction limit % 300.01/42.53 % (322156)Termination phase: Saturation % 300.01/42.53 % (322156)Time elapsed: 3.949 s % 300.01/42.53 % (322156)Peak memory usage: 41 MB % 300.01/42.53 % (322156)Instructions burned: 7024 (million) % 300.01/42.53 % (322160)ott+11_1_sil=16000:si=on:gs=on:random_seed=1176498256:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2674 on theBenchmark for (2674ds/4502Mi) % 300.01/42.53 % (322158)Instruction limit reached! % 300.01/42.53 % (322158)------------------- % 300.01/42.54 Terminated % 300.01/42.54 % Vampire exiting %------------------------------------------------------------------------------