%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : NUM261-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n012.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 12:18:10 PM UTC 2026 % Result : Timeout 300.79s 43.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM261-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.04/0.30 % Computer : n012.cluster.edu % 0.04/0.30 % Model : x86_64 x86_64 % 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.04/0.30 % Memory : 8046.5625MB % 0.04/0.30 % OS : Linux 6.8.0-71-generic % 0.04/0.30 % CPULimit : 300 % 0.04/0.30 % WCLimit : 300 % 0.04/0.30 % DateTime : Sun Sep 27 19:22:34 UTC 2026 % 0.04/0.30 % CPUTime : % 0.04/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.04/0.32 Running first-order model finding % 0.04/0.32 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.17/1.67 % (2683665)Will run a generic schedule for satisfiability detection. % 8.17/1.67 % (2683671)% WARNING: option uhcvi not known. % 8.17/1.67 % (2683672)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1513135791:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.17/1.67 % (2683670)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=702304147_2999 on theBenchmark for (2999ds/0Mi) % 8.17/1.67 % (2683676)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3599928415:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.17/1.67 % (2683671)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2847415010:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.17/1.67 % (2683673)dis+10_1_sil=32000:sp=arity:random_seed=2347619097:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.17/1.67 % (2683674)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3711581835:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.17/1.67 % (2683675)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3503998216:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.17/1.67 % (2683674)Instruction limit reached! % 8.17/1.67 % (2683674)------------------------------ % 8.17/1.67 % (2683674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.17/1.67 % (2683674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/1.67 % (2683674)CaDiCaL version: 2.1.3 % 8.17/1.67 % (2683674)Termination reason: Instruction limit % 8.17/1.67 % (2683674)Termination phase: Saturation % 8.17/1.67 % (2683674)Time elapsed: 0.036 s % 8.17/1.67 % (2683674)Peak memory usage: 13 MB % 8.17/1.67 % (2683674)Instructions burned: 119 (million) % 8.17/1.67 % (2683673)Instruction limit reached! % 8.17/1.67 % (2683673)------------------------------ % 8.17/1.67 % (2683673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.17/1.67 % (2683673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/1.67 % (2683673)CaDiCaL version: 2.1.3 % 8.17/1.67 % (2683673)Termination reason: Instruction limit % 8.17/1.67 % (2683673)Termination phase: Saturation % 8.17/1.67 % (2683673)Time elapsed: 0.040 s % 8.17/1.67 % (2683673)Peak memory usage: 13 MB % 8.17/1.67 % (2683673)Instructions burned: 105 (million) % 8.17/1.67 % (2683675)Instruction limit reached! % 8.17/1.67 % (2683675)------------------------------ % 8.17/1.67 % (2683675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.17/1.67 % (2683675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/1.67 % (2683675)CaDiCaL version: 2.1.3 % 8.17/1.67 % (2683675)Termination reason: Instruction limit % 8.17/1.67 % (2683675)Termination phase: Saturation % 8.17/1.67 % (2683675)Time elapsed: 0.046 s % 8.17/1.67 % (2683675)Peak memory usage: 13 MB % 8.17/1.67 % (2683675)Instructions burned: 131 (million) % 8.17/1.67 % (2683684)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1231117804:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.17/1.67 % (2683685)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1015181855:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 8.17/1.67 % (2683686)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=1078580323:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 8.17/1.67 % (2683676)Instruction limit reached! % 8.17/1.67 % (2683676)------------------------------ % 8.17/1.67 % (2683676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.17/1.67 % (2683676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/1.67 % (2683676)CaDiCaL version: 2.1.3 % 8.17/1.67 % (2683676)Termination reason: Instruction limit % 8.17/1.67 % (2683676)Termination phase: Saturation % 8.17/1.67 % (2683676)Time elapsed: 0.064 s % 8.17/1.67 % (2683676)Peak memory usage: 14 MB % 8.17/1.67 % (2683676)Instructions burned: 160 (million) % 8.17/1.67 % (2683690)ott-21_1_sil=16000:fs=off:random_seed=951544436:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 8.17/1.67 % (2683685)Instruction limit reached! % 8.17/1.67 % (2683685)------------------------------ % 8.17/1.67 % (2683685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.17/1.67 % (2683685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/1.67 % (2683685)CaDiCaL version: 2.1.3 % 25.02/3.95 % (2683685)Termination reason: Instruction limit % 25.02/3.95 % (2683685)Termination phase: Saturation % 25.02/3.95 % (2683685)Time elapsed: 0.049 s % 25.02/3.95 % (2683685)Peak memory usage: 13 MB % 25.02/3.95 % (2683685)Instructions burned: 132 (million) % 25.02/3.95 % TRYING [1] % 25.02/3.95 % (2683692)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=660495910:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 25.02/3.95 % TRYING [2] % 25.02/3.95 % TRYING [3] % 25.02/3.95 % (2683690)Instruction limit reached! % 25.02/3.95 % (2683690)------------------------------ % 25.02/3.95 % (2683690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.02/3.95 % (2683690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/3.95 % (2683690)CaDiCaL version: 2.1.3 % 25.02/3.95 % (2683690)Termination reason: Instruction limit % 25.02/3.95 % (2683690)Termination phase: Saturation % 25.02/3.95 % (2683690)Time elapsed: 0.056 s % 25.02/3.95 % (2683690)Peak memory usage: 13 MB % 25.02/3.95 % (2683690)Instructions burned: 183 (million) % 25.02/3.95 % (2683694)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2417748794:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 25.02/3.95 % TRYING [1] % 25.02/3.95 % TRYING [2] % 25.02/3.95 % TRYING [3] % 25.02/3.95 % (2683684)Instruction limit reached! % 25.02/3.95 % (2683684)------------------------------ % 25.02/3.95 % (2683684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.02/3.95 % (2683684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/3.95 % (2683684)CaDiCaL version: 2.1.3 % 25.02/3.95 % (2683684)Termination reason: Instruction limit % 25.02/3.95 % (2683684)Termination phase: Finite model building constraint generation % 25.02/3.95 % (2683684)Time elapsed: 0.178 s % 25.02/3.95 % (2683684)Peak memory usage: 31 MB % 25.02/3.95 % (2683684)Instructions burned: 718 (million) % 25.02/3.95 % TRYING [4] % 25.02/3.95 % (2683696)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4272342908:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 25.02/3.95 % TRYING [1] % 25.02/3.95 % TRYING [2] % 25.02/3.95 % (2683686)Instruction limit reached! % 25.02/3.95 % (2683686)------------------------------ % 25.02/3.95 % (2683686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.02/3.95 % (2683686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/3.95 % (2683686)CaDiCaL version: 2.1.3 % 25.02/3.95 % (2683686)Termination reason: Instruction limit % 25.02/3.95 % (2683686)Termination phase: Saturation % 25.02/3.95 % (2683686)Time elapsed: 0.234 s % 25.02/3.95 % (2683686)Peak memory usage: 18 MB % 25.02/3.95 % (2683686)Instructions burned: 685 (million) % 25.02/3.95 % (2683692)Instruction limit reached! % 25.02/3.95 % (2683692)------------------------------ % 25.02/3.95 % (2683692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.02/3.95 % (2683692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/3.95 % (2683692)CaDiCaL version: 2.1.3 % 25.02/3.95 % (2683692)Termination reason: Instruction limit % 25.02/3.95 % (2683692)Termination phase: Saturation % 25.02/3.95 % (2683692)Time elapsed: 0.189 s % 25.02/3.95 % (2683692)Peak memory usage: 14 MB % 25.02/3.95 % (2683692)Instructions burned: 478 (million) % 25.02/3.95 % (2683698)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2438933344:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi) % 25.02/3.95 % (2683699)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=1470021648:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi) % 25.02/3.95 % TRYING [3] % 25.02/3.95 % (2683694)Instruction limit reached! % 25.02/3.95 % (2683694)------------------------------ % 25.02/3.95 % (2683694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.02/3.95 % (2683694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.02/3.95 % (2683694)CaDiCaL version: 2.1.3 % 25.02/3.95 % (2683694)Termination reason: Instruction limit % 25.02/3.95 % (2683694)Termination phase: Finite model building constraint generation % 25.02/3.95 % (2683694)Time elapsed: 0.217 s % 25.02/3.95 % (2683694)Peak memory usage: 26 MB % 25.02/3.95 % (2683694)Instructions burned: 865 (million) % 25.02/3.95 % (2683702)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1950816114:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 25.02/3.95 % (2683698)Instruction limit reached! % 25.02/3.95 % (2683698)------------------------------ % 25.02/3.95 % (2683698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.21/7.99 % (2683698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.21/7.99 % (2683698)CaDiCaL version: 2.1.3 % 53.21/7.99 % (2683698)Termination reason: Instruction limit % 53.21/7.99 % (2683698)Termination phase: Finite model building constraint generation % 53.21/7.99 % (2683698)Time elapsed: 0.250 s % 53.21/7.99 % (2683698)Peak memory usage: 73 MB % 53.21/7.99 % (2683698)Instructions burned: 890 (million) % 53.21/7.99 % (2683699)Instruction limit reached! % 53.21/7.99 % (2683699)------------------------------ % 53.21/7.99 % (2683699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.21/7.99 % (2683699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.21/7.99 % (2683699)CaDiCaL version: 2.1.3 % 53.21/7.99 % (2683699)Termination reason: Instruction limit % 53.21/7.99 % (2683699)Termination phase: Saturation % 53.21/7.99 % (2683699)Time elapsed: 0.241 s % 53.21/7.99 % (2683699)Peak memory usage: 19 MB % 53.21/7.99 % (2683699)Instructions burned: 693 (million) % 53.21/7.99 % (2683704)fmb+10_1_sil=64000:random_seed=2244532693:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi) % 53.21/7.99 % (2683705)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=330668355:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 53.21/7.99 % (2683702)Instruction limit reached! % 53.21/7.99 % (2683702)------------------------------ % 53.21/7.99 % (2683702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.21/7.99 % (2683702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.21/7.99 % (2683702)CaDiCaL version: 2.1.3 % 53.21/7.99 % (2683702)Termination reason: Instruction limit % 53.21/7.99 % (2683702)Termination phase: Saturation % 53.21/7.99 % (2683702)Time elapsed: 0.266 s % 53.21/7.99 % (2683702)Peak memory usage: 19 MB % 53.21/7.99 % (2683702)Instructions burned: 881 (million) % 53.21/7.99 % (2683696)Instruction limit reached! % 53.21/7.99 % (2683696)------------------------------ % 53.21/7.99 % (2683696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.21/7.99 % (2683696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.21/7.99 % (2683696)CaDiCaL version: 2.1.3 % 53.21/7.99 % (2683696)Termination reason: Instruction limit % 53.21/7.99 % (2683696)Termination phase: Saturation % 53.21/7.99 % (2683696)Time elapsed: 0.409 s % 53.21/7.99 % (2683696)Peak memory usage: 24 MB % 53.21/7.99 % (2683696)Instructions burned: 1180 (million) % 53.21/7.99 % (2683708)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2385778956:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 53.21/7.99 % (2683709)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3058411849:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 53.21/7.99 % TRYING [1] % 53.21/7.99 % TRYING [20] % 53.21/7.99 % TRYING [2] % 53.21/7.99 % TRYING [5] % 53.21/7.99 % TRYING [8] % 53.21/7.99 % TRYING [3] % 53.21/7.99 % (2683708)Instruction limit reached! % 53.21/7.99 % (2683708)------------------------------ % 53.21/7.99 % (2683708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.21/7.99 % (2683708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.21/7.99 % (2683708)CaDiCaL version: 2.1.3 % 53.21/7.99 % (2683708)Termination reason: Instruction limit % 53.21/7.99 % (2683708)Termination phase: Finite model building constraint generation % 53.21/7.99 % (2683708)Time elapsed: 0.207 s % 53.21/7.99 % (2683708)Peak memory usage: 46 MB % 53.21/7.99 % (2683708)Instructions burned: 920 (million) % 53.21/7.99 % (2683712)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1391962730:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 53.21/7.99 % TRYING [4] % 53.21/7.99 % (2683712)Instruction limit reached! % 53.21/7.99 % (2683712)------------------------------ % 53.21/7.99 % (2683712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 53.21/7.99 % (2683712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.21/7.99 % (2683712)CaDiCaL version: 2.1.3 % 53.21/7.99 % (2683712)Termination reason: Instruction limit % 53.21/7.99 % (2683712)Termination phase: Saturation % 53.21/7.99 % (2683712)Time elapsed: 0.315 s % 53.21/7.99 % (2683712)Peak memory usage: 20 MB % 53.21/7.99 % (2683712)Instructions burned: 1474 (million) % 53.21/7.99 % (2683714)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=475321784:i=6324_2987 on theBenchmark for (2987ds/6324Mi) % 53.21/7.99 % (2683714)Cannot represent all propositional literals internally % 53.21/7.99 % (2683714)Refutation not found, incomplete strategy % 135.02/19.56 % (2683714)------------------------------ % 135.02/19.56 % (2683714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.56 % (2683714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.56 % (2683714)CaDiCaL version: 2.1.3 % 135.02/19.56 % (2683714)Termination reason: Refutation not found, incomplete strategy % 135.02/19.56 % (2683714)Time elapsed: 0.111 s % 135.02/19.56 % (2683714)Peak memory usage: 13 MB % 135.02/19.56 % (2683714)Instructions burned: 406 (million) % 135.02/19.56 % (2683714)------------------------------ % 135.02/19.56 % (2683714)------------------------------ % 135.02/19.56 % (2683716)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3212006164:fmbsr=2.30978:i=2174_2986 on theBenchmark for (2986ds/2174Mi) % 135.02/19.56 % (2683716)Cannot represent all propositional literals internally % 135.02/19.56 % (2683716)Refutation not found, incomplete strategy % 135.02/19.56 % (2683716)------------------------------ % 135.02/19.56 % (2683716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.56 % (2683716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.56 % (2683716)CaDiCaL version: 2.1.3 % 135.02/19.56 % (2683716)Termination reason: Refutation not found, incomplete strategy % 135.02/19.56 % (2683716)Time elapsed: 0.590 s % 135.02/19.56 % (2683716)Peak memory usage: 18 MB % 135.02/19.56 % (2683716)Instructions burned: 2059 (million) % 135.02/19.56 % (2683716)------------------------------ % 135.02/19.56 % (2683716)------------------------------ % 135.02/19.56 % (2683718)ott-2_1_sil=16000:newcnf=on:random_seed=3169715103:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi) % 135.02/19.56 % (2683718)Instruction limit reached! % 135.02/19.56 % (2683718)------------------------------ % 135.02/19.56 % (2683718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.56 % (2683718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.56 % (2683718)CaDiCaL version: 2.1.3 % 135.02/19.56 % (2683718)Termination reason: Instruction limit % 135.02/19.56 % (2683718)Termination phase: Saturation % 135.02/19.56 % (2683718)Time elapsed: 0.292 s % 135.02/19.56 % (2683718)Peak memory usage: 19 MB % 135.02/19.56 % (2683718)Instructions burned: 872 (million) % 135.02/19.56 % (2683720)ott+10_1_sil=32000:tgt=ground:random_seed=348739224:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi) % 135.02/19.56 % (2683709)Instruction limit reached! % 135.02/19.56 % (2683709)------------------------------ % 135.02/19.56 % (2683709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.56 % (2683709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.56 % (2683709)CaDiCaL version: 2.1.3 % 135.02/19.56 % (2683709)Termination reason: Instruction limit % 135.02/19.56 % (2683709)Termination phase: Saturation % 135.02/19.56 % (2683709)Time elapsed: 1.622 s % 135.02/19.56 % (2683709)Peak memory usage: 35 MB % 135.02/19.56 % (2683709)Instructions burned: 5133 (million) % 135.02/19.56 % (2683722)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2838203924:i=54282_2976 on theBenchmark for (2976ds/54282Mi) % 135.02/19.56 % TRYING [1] % 135.02/19.56 % TRYING [2] % 135.02/19.56 % (2683705)Instruction limit reached! % 135.02/19.56 % (2683705)------------------------------ % 135.02/19.56 % (2683705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.56 % (2683705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.56 % (2683705)CaDiCaL version: 2.1.3 % 135.02/19.56 % (2683705)Termination reason: Instruction limit % 135.02/19.56 % (2683705)Termination phase: Finite model building constraint generation % 135.02/19.56 % (2683705)Time elapsed: 1.844 s % 135.02/19.56 % (2683705)Peak memory usage: 537 MB % 135.02/19.56 % (2683705)Instructions burned: 9521 (million) % 135.02/19.56 % TRYING [3] % 135.02/19.56 % (2683724)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3618564379:i=3512:aac=none_2975 on theBenchmark for (2975ds/3512Mi) % 135.02/19.56 % TRYING [4] % 135.02/19.56 % TRYING [6] % 135.02/19.56 % TRYING [5] % 135.02/19.56 % TRYING [5] % 135.02/19.56 % (2683724)Instruction limit reached! % 135.02/19.56 % (2683724)------------------------------ % 135.02/19.56 % (2683724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 135.02/19.56 % (2683724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.02/19.56 % (2683724)CaDiCaL version: 2.1.3 % 135.02/19.56 % (2683724)Termination reason: Instruction limit % 135.02/19.56 % (2683724)Termination phase: Saturation % 135.02/19.56 % (2683724)Time elapsed: 1.121 s % 135.02/19.56 % (2683724)Peak memory usage: 35 MB % 135.02/19.56 % (2683724)Instructions burned: 3513 (million) % 183.31/27.39 % (2683727)dis+21_1_sil=32000:sas=cadical:random_seed=3945609985:i=3773:amm=off_2963 on theBenchmark for (2963ds/3773Mi) % 183.31/27.39 % (2683720)Instruction limit reached! % 183.31/27.39 % (2683720)------------------------------ % 183.31/27.39 % (2683720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.31/27.39 % (2683720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.31/27.39 % (2683720)CaDiCaL version: 2.1.3 % 183.31/27.39 % (2683720)Termination reason: Instruction limit % 183.31/27.39 % (2683720)Termination phase: Saturation % 183.31/27.39 % (2683720)Time elapsed: 1.764 s % 183.31/27.39 % (2683720)Peak memory usage: 48 MB % 183.31/27.39 % (2683720)Instructions burned: 5117 (million) % 183.31/27.39 % (2683729)ott+11_1_sil=16000:gs=on:random_seed=1179363959:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2959 on theBenchmark for (2959ds/2251Mi) % 183.31/27.39 % (2683729)Instruction limit reached! % 183.31/27.39 % (2683729)------------------------------ % 183.31/27.39 % (2683729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.31/27.39 % (2683729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.31/27.39 % (2683729)CaDiCaL version: 2.1.3 % 183.31/27.39 % (2683729)Termination reason: Instruction limit % 183.31/27.39 % (2683729)Termination phase: Saturation % 183.31/27.39 % (2683729)Time elapsed: 0.562 s % 183.31/27.39 % (2683729)Peak memory usage: 20 MB % 183.31/27.39 % (2683729)Instructions burned: 2252 (million) % 183.31/27.39 % (2683731)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2777975114:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi) % 183.31/27.39 % (2683727)Instruction limit reached! % 183.31/27.39 % (2683727)------------------------------ % 183.31/27.39 % (2683727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.31/27.39 % (2683727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.31/27.39 % (2683727)CaDiCaL version: 2.1.3 % 183.31/27.39 % (2683727)Termination reason: Instruction limit % 183.31/27.39 % (2683727)Termination phase: Saturation % 183.31/27.39 % (2683727)Time elapsed: 1.234 s % 183.31/27.39 % (2683727)Peak memory usage: 35 MB % 183.31/27.39 % (2683727)Instructions burned: 3773 (million) % 183.31/27.39 % (2683733)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1047550367:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2951 on theBenchmark for (2951ds/4591Mi) % 183.31/27.39 % TRYING [6] % 183.31/27.39 % TRYING [7] % 183.31/27.39 % (2683704)Instruction limit reached! % 183.31/27.39 % (2683704)------------------------------ % 183.31/27.39 % (2683704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.31/27.39 % (2683704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.31/27.39 % (2683704)CaDiCaL version: 2.1.3 % 183.31/27.39 % (2683704)Termination reason: Instruction limit % 183.31/27.39 % (2683704)Termination phase: Finite model building SAT solving % 183.31/27.39 % (2683704)Time elapsed: 5.098 s % 183.31/27.39 % (2683704)Peak memory usage: 437 MB % 183.31/27.39 % (2683704)Instructions burned: 22064 (million) % 183.31/27.39 % (2683735)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=461419005:i=29340_2942 on theBenchmark for (2942ds/29340Mi) % 183.31/27.39 % (2683733)Instruction limit reached! % 183.31/27.39 % (2683733)------------------------------ % 183.31/27.39 % (2683733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.31/27.39 % (2683733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.31/27.39 % (2683733)CaDiCaL version: 2.1.3 % 183.31/27.39 % (2683733)Termination reason: Instruction limit % 183.31/27.39 % (2683733)Termination phase: Saturation % 183.31/27.39 % (2683733)Time elapsed: 1.391 s % 183.31/27.39 % (2683733)Peak memory usage: 64 MB % 183.31/27.39 % (2683733)Instructions burned: 4592 (million) % 183.31/27.39 % (2683737)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4281591261:i=5211_2937 on theBenchmark for (2937ds/5211Mi) % 183.31/27.39 % (2683737)Instruction limit reached! % 183.31/27.39 % (2683737)------------------------------ % 183.31/27.39 % (2683737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 183.31/27.39 % (2683737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.31/27.39 % (2683737)CaDiCaL version: 2.1.3 % 183.31/27.39 % (2683737)Termination reason: Instruction limit % 183.31/27.39 % (2683737)Termination phase: Saturation % 183.31/27.39 % (2683737)Time elapsed: 1.358 s % 183.31/27.39 % (2683737)Peak memory usage: 45 MB % 183.31/27.39 % (2683737)Instructions burned: 5213 (million) % 183.31/27.39 % (2683739)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2787558698:i=5497:nm=2_2923 on theBenchmark for (2923ds/5497Mi) % 278.82/39.95 % TRYING [17] % 278.82/39.95 % (2683739)Instruction limit reached! % 278.82/39.95 % (2683739)------------------------------ % 278.82/39.95 % (2683739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.82/39.95 % (2683739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.82/39.95 % (2683739)CaDiCaL version: 2.1.3 % 278.82/39.95 % (2683739)Termination reason: Instruction limit % 278.82/39.95 % (2683739)Termination phase: Finite model building constraint generation % 278.82/39.95 % (2683739)Time elapsed: 1.055 s % 278.82/39.95 % (2683739)Peak memory usage: 301 MB % 278.82/39.95 % (2683739)Instructions burned: 5501 (million) % 278.82/39.95 % (2683741)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3342455392:fmbsr=2:i=46332_2912 on theBenchmark for (2912ds/46332Mi) % 278.82/39.95 % TRYING [15] % 278.82/39.95 % TRYING [7] % 278.82/39.95 % TRYING [7] % 278.82/39.95 % (2683735)Instruction limit reached! % 278.82/39.95 % (2683735)------------------------------ % 278.82/39.95 % (2683735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.82/39.95 % (2683735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.82/39.95 % (2683735)CaDiCaL version: 2.1.3 % 278.82/39.95 % (2683735)Termination reason: Instruction limit % 278.82/39.95 % (2683735)Termination phase: Saturation % 278.82/39.95 % (2683735)Time elapsed: 7.693 s % 278.82/39.95 % (2683735)Peak memory usage: 230 MB % 278.82/39.95 % (2683735)Instructions burned: 29343 (million) % 278.82/39.95 % (2683743)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=216239933:i=14071_2865 on theBenchmark for (2865ds/14071Mi) % 278.82/39.95 % TRYING [12] % 278.82/39.95 % (2683722)Instruction limit reached! % 278.82/39.95 % (2683722)------------------------------ % 278.82/39.95 % (2683722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.82/39.95 % (2683722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.82/39.95 % (2683722)CaDiCaL version: 2.1.3 % 278.82/39.95 % (2683722)Termination reason: Instruction limit % 278.82/39.95 % (2683722)Termination phase: Finite model building constraint generation % 278.82/39.95 % (2683722)Time elapsed: 11.433 s % 278.82/39.95 % (2683722)Peak memory usage: 1620 MB % 278.82/39.95 % (2683722)Instructions burned: 54285 (million) % 278.82/39.95 % (2683745)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3213549448:i=22565:add=on:rawr=on_2861 on theBenchmark for (2861ds/22565Mi) % 278.82/39.95 % (2683743)Instruction limit reached! % 278.82/39.95 % (2683743)------------------------------ % 278.82/39.95 % (2683743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.82/39.95 % (2683743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.82/39.95 % (2683743)CaDiCaL version: 2.1.3 % 278.82/39.95 % (2683743)Termination reason: Instruction limit % 278.82/39.95 % (2683743)Termination phase: Finite model building constraint generation % 278.82/39.95 % (2683743)Time elapsed: 2.770 s % 278.82/39.95 % (2683743)Peak memory usage: 909 MB % 278.82/39.95 % (2683743)Instructions burned: 14071 (million) % 278.82/39.95 % (2683747)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2658413835:i=8173:av=off_2836 on theBenchmark for (2836ds/8173Mi) % 278.82/39.95 % (2683741)Instruction limit reached! % 278.82/39.95 % (2683741)------------------------------ % 278.82/39.95 % (2683741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.82/39.95 % (2683741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.82/39.95 % (2683741)CaDiCaL version: 2.1.3 % 278.82/39.95 % (2683741)Termination reason: Instruction limit % 278.82/39.95 % (2683741)Termination phase: Finite model building constraint generation % 278.82/39.95 % (2683741)Time elapsed: 8.620 s % 278.82/39.95 % (2683741)Peak memory usage: 2435 MB % 278.82/39.95 % (2683741)Instructions burned: 46334 (million) % 278.82/39.95 % (2683749)dis+10_16:1_sil=16000:random_seed=1570346953:i=9155:fsr=off_2824 on theBenchmark for (2824ds/9155Mi) % 278.82/39.95 % (2683747)Instruction limit reached! % 278.82/39.95 % (2683747)------------------------------ % 278.82/39.95 % (2683747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.82/39.95 % (2683747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.82/39.95 % (2683747)CaDiCaL version: 2.1.3 % 278.82/39.95 % (2683747)Termination reason: Instruction limit % 278.82/39.95 % (2683747)Termination phase: Saturation % 278.82/39.95 % (2683747)Time elapsed: 2.916 s % 278.82/39.95 % (2683747)PeaTerminated % 300.79/43.05 % Vampire exiting % 300.79/43.06 Terminated %------------------------------------------------------------------------------