%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : COM075_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 : n002.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 09:40:15 AM UTC 2026 % Result : Timeout 290.37s 41.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : COM075_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.23 % Computer : n002.cluster.edu % 0.11/0.23 % Model : x86_64 x86_64 % 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.23 % Memory : 8046.5625MB % 0.11/0.23 % OS : Linux 6.8.0-71-generic % 0.11/0.23 % CPULimit : 300 % 0.11/0.23 % WCLimit : 300 % 0.11/0.23 % DateTime : Mon Sep 28 21:55:23 UTC 2026 % 0.11/0.23 % CPUTime : % 0.11/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.24/0.29 Running first-order model finding % 0.24/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.48/2.29 % (812515)Will run a generic schedule for satisfiability detection. % 13.48/2.29 % (812523)dis+10_1_sil=32000:sp=arity:random_seed=3612266693:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.48/2.29 % (812520)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3507253153_2999 on theBenchmark for (2999ds/0Mi) % 13.48/2.29 % (812521)% WARNING: option uhcvi not known. % 13.48/2.29 % (812521)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=324943394:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.48/2.29 % (812524)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3180731047:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.48/2.29 % (812525)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3321540981:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.48/2.29 % (812522)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=714522728:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.48/2.29 % (812526)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3308445748:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.48/2.29 % Exception at run slice level % 13.48/2.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 13.48/2.29 % (812523)Instruction limit reached! % 13.48/2.29 % (812523)------------------------------ % 13.48/2.29 % (812523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.48/2.29 % (812523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.29 % (812523)CaDiCaL version: 2.1.3 % 13.48/2.29 % (812523)Termination reason: Instruction limit % 13.48/2.29 % (812523)Termination phase: Saturation % 13.48/2.29 % (812523)Time elapsed: 0.047 s % 13.48/2.29 % (812523)Peak memory usage: 12 MB % 13.48/2.29 % (812523)Instructions burned: 104 (million) % 13.48/2.29 % (812534)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1756257126:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 13.48/2.29 % Exception at run slice level % 13.48/2.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 13.48/2.29 % (812537)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=110119276:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 13.48/2.29 % (812541)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=26168084:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 13.48/2.29 % (812524)Instruction limit reached! % 13.48/2.29 % (812524)------------------------------ % 13.48/2.29 % (812524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.48/2.29 % (812524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.29 % (812524)CaDiCaL version: 2.1.3 % 13.48/2.29 % (812524)Termination reason: Instruction limit % 13.48/2.29 % (812524)Termination phase: Saturation % 13.48/2.29 % (812524)Time elapsed: 0.098 s % 13.48/2.29 % (812524)Peak memory usage: 12 MB % 13.48/2.29 % (812524)Instructions burned: 117 (million) % 13.48/2.29 % (812537)Instruction limit reached! % 13.48/2.29 % (812537)------------------------------ % 13.48/2.29 % (812537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.48/2.29 % (812537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.29 % (812537)CaDiCaL version: 2.1.3 % 13.48/2.29 % (812537)Termination reason: Instruction limit % 13.48/2.29 % (812537)Termination phase: Saturation % 13.48/2.29 % (812537)Time elapsed: 0.074 s % 13.48/2.29 % (812537)Peak memory usage: 13 MB % 13.48/2.29 % (812537)Instructions burned: 139 (million) % 13.48/2.29 % (812525)Instruction limit reached! % 13.48/2.29 % (812525)------------------------------ % 13.48/2.29 % (812525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.48/2.29 % (812525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.48/2.29 % (812525)CaDiCaL version: 2.1.3 % 13.48/2.29 % (812525)Termination reason: Instruction limit % 13.48/2.29 % (812525)Termination phase: Saturation % 13.48/2.29 % (812525)Time elapsed: 0.128 s % 13.48/2.29 % (812525)Peak memory usage: 13 MB % 13.48/2.29 % (812525)Instructions burned: 132 (million) % 13.48/2.29 % (812526)Instruction limit reached! % 13.48/2.29 % (812526)------------------------------ % 13.48/2.29 % (812526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.48/2.29 % (812526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.50/5.38 % (812526)CaDiCaL version: 2.1.3 % 35.50/5.38 % (812526)Termination reason: Instruction limit % 35.50/5.38 % (812526)Termination phase: Saturation % 35.50/5.38 % (812526)Time elapsed: 0.136 s % 35.50/5.38 % (812526)Peak memory usage: 12 MB % 35.50/5.38 % (812526)Instructions burned: 159 (million) % 35.50/5.38 % (812544)ott-21_1_sil=16000:fs=off:random_seed=1609484505:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 35.50/5.38 % (812549)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=513667027:i=1179_2998 on theBenchmark for (2998ds/1179Mi) % 35.50/5.38 % (812546)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4140747788:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 35.50/5.38 % (812547)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2162709094:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 35.50/5.38 % Exception at run slice level % 35.50/5.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.50/5.38 % (812554)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3385856609:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 35.50/5.38 % Exception at run slice level % 35.50/5.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.50/5.38 % (812556)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=2997011797:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi) % 35.50/5.38 % (812544)Instruction limit reached! % 35.50/5.38 % (812544)------------------------------ % 35.50/5.38 % (812544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.50/5.38 % (812544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.50/5.38 % (812544)CaDiCaL version: 2.1.3 % 35.50/5.38 % (812544)Termination reason: Instruction limit % 35.50/5.38 % (812544)Termination phase: Saturation % 35.50/5.38 % (812544)Time elapsed: 0.099 s % 35.50/5.38 % (812544)Peak memory usage: 11 MB % 35.50/5.38 % (812544)Instructions burned: 180 (million) % 35.50/5.38 % (812558)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1924419593:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi) % 35.50/5.38 % (812546)Instruction limit reached! % 35.50/5.38 % (812546)------------------------------ % 35.50/5.38 % (812546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.50/5.38 % (812546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.50/5.38 % (812546)CaDiCaL version: 2.1.3 % 35.50/5.38 % (812546)Termination reason: Instruction limit % 35.50/5.38 % (812546)Termination phase: Saturation % 35.50/5.38 % (812546)Time elapsed: 0.410 s % 35.50/5.38 % (812546)Peak memory usage: 13 MB % 35.50/5.38 % (812546)Instructions burned: 478 (million) % 35.50/5.38 % (812560)fmb+10_1_sil=64000:random_seed=213563795:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 35.50/5.38 % (812560)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 35.50/5.38 % Exception at run slice level % 35.50/5.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.50/5.38 % (812562)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2454307637:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi) % 35.50/5.38 % Exception at run slice level % 35.50/5.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 35.50/5.38 % (812541)Instruction limit reached! % 35.50/5.38 % (812541)------------------------------ % 35.50/5.38 % (812541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 35.50/5.38 % (812541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.50/5.38 % (812541)CaDiCaL version: 2.1.3 % 35.50/5.38 % (812541)Termination reason: Instruction limit % 35.50/5.38 % (812541)Termination phase: Saturation % 35.50/5.38 % (812541)Time elapsed: 0.562 s % 35.50/5.38 % (812541)Peak memory usage: 15 MB % 35.50/5.38 % (812541)Instructions burned: 685 (million) % 35.50/5.38 % (812564)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2741215293:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 35.50/5.38 % Exception at run slice level % 35.50/5.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 106.63/15.32 % (812565)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=11701211:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 106.63/15.32 % (812549)Instruction limit reached! % 106.63/15.32 % (812549)------------------------------ % 106.63/15.32 % (812549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.63/15.32 % (812549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.63/15.32 % (812549)CaDiCaL version: 2.1.3 % 106.63/15.32 % (812549)Termination reason: Instruction limit % 106.63/15.32 % (812549)Termination phase: Saturation % 106.63/15.32 % (812549)Time elapsed: 0.527 s % 106.63/15.32 % (812549)Peak memory usage: 16 MB % 106.63/15.32 % (812549)Instructions burned: 1180 (million) % 106.63/15.32 % (812568)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1005459470:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi) % 106.63/15.32 % (812570)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=755328319:i=6324_2992 on theBenchmark for (2992ds/6324Mi) % 106.63/15.32 % (812568)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 106.63/15.32 % Exception at run slice level % 106.63/15.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 106.63/15.32 % (812574)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2605278573:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi) % 106.63/15.32 % Exception at run slice level % 106.63/15.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 106.63/15.32 % (812576)ott-2_1_sil=16000:newcnf=on:random_seed=1882199337:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi) % 106.63/15.32 % (812556)Instruction limit reached! % 106.63/15.32 % (812556)------------------------------ % 106.63/15.32 % (812556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.63/15.32 % (812556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.63/15.32 % (812556)CaDiCaL version: 2.1.3 % 106.63/15.32 % (812556)Termination reason: Instruction limit % 106.63/15.32 % (812556)Termination phase: Saturation % 106.63/15.32 % (812556)Time elapsed: 0.644 s % 106.63/15.32 % (812556)Peak memory usage: 16 MB % 106.63/15.32 % (812556)Instructions burned: 692 (million) % 106.63/15.32 % (812578)ott+10_1_sil=32000:tgt=ground:random_seed=2431721276:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi) % 106.63/15.32 % (812558)Instruction limit reached! % 106.63/15.32 % (812558)------------------------------ % 106.63/15.32 % (812558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.63/15.32 % (812558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.63/15.32 % (812558)CaDiCaL version: 2.1.3 % 106.63/15.32 % (812558)Termination reason: Instruction limit % 106.63/15.32 % (812558)Termination phase: Saturation % 106.63/15.32 % (812558)Time elapsed: 0.840 s % 106.63/15.32 % (812558)Peak memory usage: 19 MB % 106.63/15.32 % (812558)Instructions burned: 879 (million) % 106.63/15.32 % (812576)Instruction limit reached! % 106.63/15.32 % (812576)------------------------------ % 106.63/15.32 % (812576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.63/15.32 % (812576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.63/15.32 % (812576)CaDiCaL version: 2.1.3 % 106.63/15.32 % (812576)Termination reason: Instruction limit % 106.63/15.32 % (812576)Termination phase: Saturation % 106.63/15.32 % (812576)Time elapsed: 0.356 s % 106.63/15.32 % (812576)Peak memory usage: 13 MB % 106.63/15.32 % (812576)Instructions burned: 872 (million) % 106.63/15.32 % (812580)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2690362744:i=54282_2988 on theBenchmark for (2988ds/54282Mi) % 106.63/15.32 % Exception at run slice level % 106.63/15.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 106.63/15.32 % (812581)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1214348539:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi) % 106.63/15.32 % (812583)dis+21_1_sil=32000:sas=cadical:random_seed=69700963:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi) % 106.63/15.32 % (812568)Instruction limit reached! % 106.63/15.32 % (812568)------------------------------ % 106.63/15.32 % (812568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 106.63/15.32 % (812568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.63/15.32 % (812568)CaDiCaL version: 2.1.3 % 174.23/24.81 % (812568)Termination reason: Instruction limit % 174.23/24.81 % (812568)Termination phase: Saturation % 174.23/24.81 % (812568)Time elapsed: 1.239 s % 174.23/24.81 % (812568)Peak memory usage: 18 MB % 174.23/24.81 % (812568)Instructions burned: 1472 (million) % 174.23/24.81 % (812590)ott+11_1_sil=16000:gs=on:random_seed=1447709445:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi) % 174.23/24.81 % (812583)Instruction limit reached! % 174.23/24.81 % (812583)------------------------------ % 174.23/24.81 % (812583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.23/24.81 % (812583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.23/24.81 % (812583)CaDiCaL version: 2.1.3 % 174.23/24.81 % (812583)Termination reason: Instruction limit % 174.23/24.81 % (812583)Termination phase: Saturation % 174.23/24.81 % (812583)Time elapsed: 1.603 s % 174.23/24.81 % (812583)Peak memory usage: 26 MB % 174.23/24.81 % (812583)Instructions burned: 3774 (million) % 174.23/24.81 % (812595)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2493402469:fmbsr=1.6:i=67534_2971 on theBenchmark for (2971ds/67534Mi) % 174.23/24.81 % Exception at run slice level % 174.23/24.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.23/24.81 % (812597)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=627929179:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2971 on theBenchmark for (2971ds/4591Mi) % 174.23/24.81 % (812590)Instruction limit reached! % 174.23/24.81 % (812590)------------------------------ % 174.23/24.81 % (812590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.23/24.81 % (812590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.23/24.81 % (812590)CaDiCaL version: 2.1.3 % 174.23/24.81 % (812590)Termination reason: Instruction limit % 174.23/24.81 % (812590)Termination phase: Saturation % 174.23/24.81 % (812590)Time elapsed: 1.353 s % 174.23/24.81 % (812590)Peak memory usage: 19 MB % 174.23/24.81 % (812590)Instructions burned: 2252 (million) % 174.23/24.81 % (812599)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1274789407:i=29340_2966 on theBenchmark for (2966ds/29340Mi) % 174.23/24.81 % (812581)Instruction limit reached! % 174.23/24.81 % (812581)------------------------------ % 174.23/24.81 % (812581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.23/24.81 % (812581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.23/24.81 % (812581)CaDiCaL version: 2.1.3 % 174.23/24.81 % (812581)Termination reason: Instruction limit % 174.23/24.81 % (812581)Termination phase: Saturation % 174.23/24.81 % (812581)Time elapsed: 3.056 s % 174.23/24.81 % (812581)Peak memory usage: 25 MB % 174.23/24.81 % (812581)Instructions burned: 3513 (million) % 174.23/24.81 % (812615)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2445092695:i=5211_2957 on theBenchmark for (2957ds/5211Mi) % 174.23/24.81 % (812565)Instruction limit reached! % 174.23/24.81 % (812565)------------------------------ % 174.23/24.81 % (812565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.23/24.81 % (812565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.23/24.81 % (812565)CaDiCaL version: 2.1.3 % 174.23/24.81 % (812565)Termination reason: Instruction limit % 174.23/24.81 % (812565)Termination phase: Saturation % 174.23/24.81 % (812565)Time elapsed: 4.278 s % 174.23/24.81 % (812565)Peak memory usage: 23 MB % 174.23/24.81 % (812565)Instructions burned: 5131 (million) % 174.23/24.81 % (812617)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3529662598:i=5497:nm=2_2950 on theBenchmark for (2950ds/5497Mi) % 174.23/24.81 % Exception at run slice level % 174.23/24.81 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 174.23/24.81 % (812619)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=881955801:fmbsr=2:i=46332_2949 on theBenchmark for (2949ds/46332Mi) % 174.23/24.81 % (812578)Instruction limit reached! % 174.23/24.81 % (812578)------------------------------ % 174.23/24.81 % (812578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 174.23/24.81 % (812578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.23/24.81 % (812578)CaDiCaL version: 2.1.3 % 174.23/24.81 % (812578)Termination reason: Instruction limit % 174.23/24.81 % (812578)Termination phase: Saturation % 174.23/24.81 % (812578)Time elapsed: 4.124 s % 174.23/24.81 % (812578)Peak memory usage: 18 MB % 174.23/24.81 % (812578)Instructions burned: 5114 (million) % 200.35/28.54 % Exception at run slice level % 200.35/28.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 200.35/28.54 % (812622)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1142814192:i=22565:add=on:rawr=on_2949 on theBenchmark for (2949ds/22565Mi) % 200.35/28.54 % (812621)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1432617694:i=14071_2949 on theBenchmark for (2949ds/14071Mi) % 200.35/28.54 % Exception at run slice level % 200.35/28.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 200.35/28.54 % (812625)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1328422065:i=8173:av=off_2948 on theBenchmark for (2948ds/8173Mi) % 200.35/28.54 % (812597)Instruction limit reached! % 200.35/28.54 % (812597)------------------------------ % 200.35/28.54 % (812597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.35/28.54 % (812597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.35/28.54 % (812597)CaDiCaL version: 2.1.3 % 200.35/28.54 % (812597)Termination reason: Instruction limit % 200.35/28.54 % (812597)Termination phase: Saturation % 200.35/28.54 % (812597)Time elapsed: 3.670 s % 200.35/28.54 % (812597)Peak memory usage: 21 MB % 200.35/28.54 % (812597)Instructions burned: 4591 (million) % 200.35/28.54 % (812629)dis+10_16:1_sil=16000:random_seed=750317957:i=9155:fsr=off_2934 on theBenchmark for (2934ds/9155Mi) % 200.35/28.54 % (812615)Instruction limit reached! % 200.35/28.54 % (812615)------------------------------ % 200.35/28.54 % (812615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.35/28.54 % (812615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.35/28.54 % (812615)CaDiCaL version: 2.1.3 % 200.35/28.54 % (812615)Termination reason: Instruction limit % 200.35/28.54 % (812615)Termination phase: Saturation % 200.35/28.54 % (812615)Time elapsed: 4.646 s % 200.35/28.54 % (812615)Peak memory usage: 44 MB % 200.35/28.54 % (812615)Instructions burned: 5211 (million) % 200.35/28.54 % (812631)ott-3_8_sil=64000:random_seed=3355601642:i=20139:bs=on_2910 on theBenchmark for (2910ds/20139Mi) % 200.35/28.54 % (812625)Instruction limit reached! % 200.35/28.54 % (812625)------------------------------ % 200.35/28.54 % (812625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.35/28.54 % (812625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.35/28.54 % (812625)CaDiCaL version: 2.1.3 % 200.35/28.54 % (812625)Termination reason: Instruction limit % 200.35/28.54 % (812625)Termination phase: Saturation % 200.35/28.54 % (812625)Time elapsed: 6.047 s % 200.35/28.54 % (812625)Peak memory usage: 20 MB % 200.35/28.54 % (812625)Instructions burned: 8174 (million) % 200.35/28.54 % (812637)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1446019689:fmbsr=2:i=32576_2887 on theBenchmark for (2887ds/32576Mi) % 200.35/28.54 % Exception at run slice level % 200.35/28.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 200.35/28.54 % (812639)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2111760232:i=11404_2887 on theBenchmark for (2887ds/11404Mi) % 200.35/28.54 % (812599)Instruction limit reached! % 200.35/28.54 % (812599)------------------------------ % 200.35/28.54 % (812599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.35/28.54 % (812599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.35/28.54 % (812599)CaDiCaL version: 2.1.3 % 200.35/28.54 % (812599)Termination reason: Instruction limit % 200.35/28.54 % (812599)Termination phase: Saturation % 200.35/28.54 % (812599)Time elapsed: 11.092 s % 200.35/28.54 % (812599)Peak memory usage: 32 MB % 200.35/28.54 % (812599)Instructions burned: 29342 (million) % 200.35/28.54 % (812645)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4247023995:i=14134_2855 on theBenchmark for (2855ds/14134Mi) % 200.35/28.54 % (812629)Instruction limit reached! % 200.35/28.54 % (812629)------------------------------ % 200.35/28.54 % (812629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 200.35/28.54 % (812629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.35/28.54 % (812629)CaDiCaL version: 2.1.3 % 200.35/28.54 % (812629)Termination reason: Instruction limit % 200.35/28.54 % (812629)Termination phase: Saturation % 200.35/28.54 % (812629)Time elapsed: 8.384 s % 200.35/28.54 % (812629)Peak memory usage: 53 MB % 200.35/28.54 % (812629)Instructions burned: 9156 (million) % 200.35/28.54 % (812647)dis+33_16_sil=32000:sac=on:random_seed=366549742:i=15851:nm=0_2850 on theBenchmark for (2850ds/15851Mi) % 219.63/31.22 % (812645)Instruction limit reached! % 219.63/31.22 % (812645)------------------------------ % 219.63/31.22 % (812645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.63/31.22 % (812645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.63/31.22 % (812645)CaDiCaL version: 2.1.3 % 219.63/31.22 % (812645)Termination reason: Instruction limit % 219.63/31.22 % (812645)Termination phase: Saturation % 219.63/31.22 % (812645)Time elapsed: 5.568 s % 219.63/31.22 % (812645)Peak memory usage: 26 MB % 219.63/31.22 % (812645)Instructions burned: 14135 (million) % 219.63/31.22 % (812653)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3456648151:avsq=on:i=17627:add=on:amm=off_2799 on theBenchmark for (2799ds/17627Mi) % 219.63/31.22 % (812622)Instruction limit reached! % 219.63/31.22 % (812622)------------------------------ % 219.63/31.22 % (812622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.63/31.22 % (812622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.63/31.22 % (812622)CaDiCaL version: 2.1.3 % 219.63/31.22 % (812622)Termination reason: Instruction limit % 219.63/31.22 % (812622)Termination phase: Saturation % 219.63/31.22 % (812622)Time elapsed: 15.496 s % 219.63/31.22 % (812622)Peak memory usage: 28 MB % 219.63/31.22 % (812622)Instructions burned: 22567 (million) % 219.63/31.22 % (812655)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=863986560:s2a=on:i=53295_2793 on theBenchmark for (2793ds/53295Mi) % 219.63/31.22 % (812639)Instruction limit reached! % 219.63/31.22 % (812639)------------------------------ % 219.63/31.22 % (812639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.63/31.22 % (812639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.63/31.22 % (812639)CaDiCaL version: 2.1.3 % 219.63/31.22 % (812639)Termination reason: Instruction limit % 219.63/31.22 % (812639)Termination phase: Saturation % 219.63/31.22 % (812639)Time elapsed: 11.373 s % 219.63/31.22 % (812639)Peak memory usage: 142 MB % 219.63/31.22 % (812639)Instructions burned: 11404 (million) % 219.63/31.22 % (812661)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1057989520:i=26857:ins=20_2773 on theBenchmark for (2773ds/26857Mi) % 219.63/31.22 % Exception at run slice level % 219.63/31.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.63/31.22 % (812663)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1737982544:i=28120:bs=on:fsr=off_2772 on theBenchmark for (2772ds/28120Mi) % 219.63/31.22 % (812631)Instruction limit reached! % 219.63/31.22 % (812631)------------------------------ % 219.63/31.22 % (812631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 219.63/31.22 % (812631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.63/31.22 % (812631)CaDiCaL version: 2.1.3 % 219.63/31.22 % (812631)Termination reason: Instruction limit % 219.63/31.22 % (812631)Termination phase: Saturation % 219.63/31.22 % (812631)Time elapsed: 15.396 s % 219.63/31.22 % (812631)Peak memory usage: 24 MB % 219.63/31.22 % (812631)Instructions burned: 20139 (million) % 219.63/31.22 % (812679)fmb+10_1_sil=256000:fmbss=7:random_seed=2804025445:fmbsr=1.6:i=182295_2756 on theBenchmark for (2756ds/182295Mi) % 219.63/31.22 % Exception at run slice level % 219.63/31.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.63/31.22 % (812681)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=679674847:i=44625:gsp=on_2755 on theBenchmark for (2755ds/44625Mi) % 219.63/31.22 % (812681)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 219.63/31.22 % Exception at run slice level % 219.63/31.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.63/31.22 % (812683)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=4208187888:i=160505_2755 on theBenchmark for (2755ds/160505Mi) % 219.63/31.22 % Exception at run slice level % 219.63/31.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.63/31.22 % (812685)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2698305060:fmbsr=1.3:i=225729_2755 on theBenchmark for (2755ds/225729Mi) % 219.63/31.22 % Exception at run slice level % 219.63/31.22 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 219.63/31.22 % (812687)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=852040248:fmbsr=2:i=185024:ins=7_2755 on theBenchmark for (2755ds/185024Mi) % 290.37/41.17 % Exception at run slice level % 290.37/41.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 290.37/41.17 % (812689)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=644491344:rtra=on_2754 on theBenchmark for (2754ds/0Mi) % 290.37/41.17 % Exception at run slice level % 290.37/41.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs % 290.37/41.17 % (812691)% WARNING: option uhcvi not known. % 290.37/41.17 % (812691)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2701582005:i=271062:add=off:rtra=on:rawr=on_2754 on theBenchmark for (2754ds/271062Mi) % 290.37/41.17 % (812647)Instruction limit reached! % 290.37/41.17 % (812647)------------------------------ % 290.37/41.17 % (812647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.37/41.17 % (812647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.37/41.17 % (812647)CaDiCaL version: 2.1.3 % 290.37/41.17 % (812647)Termination reason: Instruction limit % 290.37/41.17 % (812647)Termination phase: Saturation % 290.37/41.17 % (812647)Time elapsed: 11.651 s % 290.37/41.17 % (812647)Peak memory usage: 24 MB % 290.37/41.17 % (812647)Instructions burned: 15852 (million) % 290.37/41.17 % (812695)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3103444191:i=176048:add=on:rtra=on:rawr=on_2733 on theBenchmark for (2733ds/176048Mi) % 290.37/41.17 % (812653)Instruction limit reached! % 290.37/41.17 % (812653)------------------------------ % 290.37/41.17 % (812653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.37/41.17 % (812653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.37/41.17 % (812653)CaDiCaL version: 2.1.3 % 290.37/41.17 % (812653)Termination reason: Instruction limit % 290.37/41.17 % (812653)Termination phase: Saturation % 290.37/41.17 % (812653)Time elapsed: 7.499 s % 290.37/41.17 % (812653)Peak memory usage: 38 MB % 290.37/41.17 % (812653)Instructions burned: 17629 (million) % 290.37/41.17 % (812697)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3276533988:i=206:fgj=on:rtra=on_2723 on theBenchmark for (2723ds/206Mi) % 290.37/41.17 % (812697)Instruction limit reached! % 290.37/41.17 % (812697)------------------------------ % 290.37/41.17 % (812697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.37/41.17 % (812697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.37/41.17 % (812697)CaDiCaL version: 2.1.3 % 290.37/41.17 % (812697)Termination reason: Instruction limit % 290.37/41.17 % (812697)Termination phase: Saturation % 290.37/41.17 % (812697)Time elapsed: 0.134 s % 290.37/41.17 % (812697)Peak memory usage: 12 MB % 290.37/41.17 % (812697)Instructions burned: 207 (million) % 290.37/41.17 % (812699)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1025435840:i=232:rtra=on_2722 on theBenchmark for (2722ds/232Mi) % 290.37/41.17 % (812699)Instruction limit reached! % 290.37/41.17 % (812699)------------------------------ % 290.37/41.17 % (812699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.37/41.17 % (812699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.37/41.17 % (812699)CaDiCaL version: 2.1.3 % 290.37/41.17 % (812699)Termination reason: Instruction limit % 290.37/41.17 % (812699)Termination phase: Saturation % 290.37/41.17 % (812699)Time elapsed: 0.116 s % 290.37/41.17 % (812699)Peak memory usage: 13 MB % 290.37/41.17 % (812699)Instructions burned: 232 (million) % 290.37/41.17 % (812701)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3837445160:i=262:rtra=on_2720 on theBenchmark for (2720ds/262Mi) % 290.37/41.17 % (812701)Instruction limit reached! % 290.37/41.17 % (812701)------------------------------ % 290.37/41.17 % (812701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 290.37/41.17 % (812701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.37/41.17 % (812701)CaDiCaL version: 2.1.3 % 290.37/41.17 % (812701)Termination reason: Instruction limit % 290.37/41.17 % (812701)Termination phase: Saturation % 290.37/41.17 % (812701)Time elapsed: 0.122 s % 290.37/41.17 % (812701)Peak memory usage: 12 MB % 290.37/41.17 % (812701)Instructions burned: 264 (million) % 290.37/41.17 % (812703)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=3103470962:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2719 on theBenchmark for (2719ds/318Mi) % 290.37/41.17 % (812703)Instruction limit reached! % 290.37/41.17 % (812703)------------------------------ % 290.37/41.17 % (812703Terminated % 300.37/42.63 % Vampire exiting % 300.37/42.64 Terminated %------------------------------------------------------------------------------