%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWC199-1 : TPTP v9.3.1. Released v2.4.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 01:05:04 PM UTC 2026 % Result : Timeout 300.85s 43.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWC199-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.04/0.31 % Computer : n012.cluster.edu % 0.04/0.31 % Model : x86_64 x86_64 % 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.04/0.31 % Memory : 8046.5625MB % 0.04/0.31 % OS : Linux 6.8.0-71-generic % 0.04/0.32 % CPULimit : 300 % 0.04/0.32 % WCLimit : 300 % 0.04/0.32 % DateTime : Mon Sep 28 08:24:34 UTC 2026 % 0.04/0.32 % CPUTime : % 0.04/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.33 Running first-order model finding % 0.07/0.33 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 % 7.73/1.51 % (3234510)Will run a generic schedule for satisfiability detection. % 7.73/1.51 % (3234516)% WARNING: option uhcvi not known. % 7.73/1.51 % (3234515)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2920336102_2999 on theBenchmark for (2999ds/0Mi) % 7.73/1.51 % (3234516)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=962575357:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 7.73/1.51 % (3234517)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2838040067:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 7.73/1.51 % (3234518)dis+10_1_sil=32000:sp=arity:random_seed=2746216340:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 7.73/1.51 % (3234519)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1400057715:i=116_2999 on theBenchmark for (2999ds/116Mi) % 7.73/1.51 % (3234520)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1350104515:i=131_2999 on theBenchmark for (2999ds/131Mi) % 7.73/1.51 % (3234521)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1611811364:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 7.73/1.51 % TRYING [1] % 7.73/1.51 % TRYING [2] % 7.73/1.51 % TRYING [3] % 7.73/1.51 % TRYING [4] % 7.73/1.51 % (3234519)Instruction limit reached! % 7.73/1.51 % (3234519)------------------------------ % 7.73/1.51 % (3234519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.73/1.51 % (3234519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.73/1.51 % (3234519)CaDiCaL version: 2.1.3 % 7.73/1.51 % (3234519)Termination reason: Instruction limit % 7.73/1.51 % (3234519)Termination phase: Saturation % 7.73/1.51 % (3234519)Time elapsed: 0.033 s % 7.73/1.51 % (3234519)Peak memory usage: 13 MB % 7.73/1.51 % (3234519)Instructions burned: 121 (million) % 7.73/1.51 % (3234518)Instruction limit reached! % 7.73/1.51 % (3234518)------------------------------ % 7.73/1.51 % (3234518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.73/1.51 % (3234518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.73/1.51 % (3234518)CaDiCaL version: 2.1.3 % 7.73/1.51 % (3234518)Termination reason: Instruction limit % 7.73/1.51 % (3234518)Termination phase: Saturation % 7.73/1.51 % (3234518)Time elapsed: 0.034 s % 7.73/1.51 % (3234518)Peak memory usage: 13 MB % 7.73/1.51 % (3234518)Instructions burned: 106 (million) % 7.73/1.51 % (3234520)Instruction limit reached! % 7.73/1.51 % (3234520)------------------------------ % 7.73/1.51 % (3234520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.73/1.51 % (3234520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.73/1.51 % (3234520)CaDiCaL version: 2.1.3 % 7.73/1.51 % (3234520)Termination reason: Instruction limit % 7.73/1.51 % (3234520)Termination phase: Saturation % 7.73/1.51 % (3234520)Time elapsed: 0.035 s % 7.73/1.51 % (3234520)Peak memory usage: 14 MB % 7.73/1.51 % (3234520)Instructions burned: 131 (million) % 7.73/1.51 % (3234530)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2261720005:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi) % 7.73/1.51 % (3234529)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1437713202:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 7.73/1.51 % (3234521)Instruction limit reached! % 7.73/1.51 % (3234521)------------------------------ % 7.73/1.51 % (3234521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 7.73/1.51 % (3234521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.73/1.51 % (3234521)CaDiCaL version: 2.1.3 % 7.73/1.51 % (3234521)Termination reason: Instruction limit % 7.73/1.51 % (3234521)Termination phase: Saturation % 7.73/1.51 % (3234521)Time elapsed: 0.046 s % 7.73/1.51 % (3234521)Peak memory usage: 15 MB % 7.73/1.51 % (3234521)Instructions burned: 160 (million) % 7.73/1.51 % (3234531)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=4137558492:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi) % 7.73/1.51 % TRYING [1] % 7.73/1.51 % TRYING [2] % 7.73/1.51 % TRYING [5] % 7.73/1.51 % TRYING [3] % 7.73/1.51 % (3234535)ott-21_1_sil=16000:fs=off:random_seed=478765929:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi) % 7.73/1.51 % TRYING [4] % 7.73/1.51 % (3234530)Instruction limit reached! % 7.73/1.51 % (3234530)------------------------------ % 7.73/1.51 % (3234530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.00/3.99 % (3234530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.00/3.99 % (3234530)CaDiCaL version: 2.1.3 % 25.00/3.99 % (3234530)Termination reason: Instruction limit % 25.00/3.99 % (3234530)Termination phase: Saturation % 25.00/3.99 % (3234530)Time elapsed: 0.040 s % 25.00/3.99 % (3234530)Peak memory usage: 13 MB % 25.00/3.99 % (3234530)Instructions burned: 134 (million) % 25.00/3.99 % (3234537)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3749238215:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 25.00/3.99 % TRYING [5] % 25.00/3.99 % (3234535)Instruction limit reached! % 25.00/3.99 % (3234535)------------------------------ % 25.00/3.99 % (3234535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.00/3.99 % (3234535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.00/3.99 % (3234535)CaDiCaL version: 2.1.3 % 25.00/3.99 % (3234535)Termination reason: Instruction limit % 25.00/3.99 % (3234535)Termination phase: Saturation % 25.00/3.99 % (3234535)Time elapsed: 0.049 s % 25.00/3.99 % (3234535)Peak memory usage: 13 MB % 25.00/3.99 % (3234535)Instructions burned: 180 (million) % 25.00/3.99 % (3234539)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1313683238:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi) % 25.00/3.99 % TRYING [1] % 25.00/3.99 % TRYING [2] % 25.00/3.99 % TRYING [3] % 25.00/3.99 % TRYING [6] % 25.00/3.99 % TRYING [4] % 25.00/3.99 % TRYING [6] % 25.00/3.99 % (3234529)Instruction limit reached! % 25.00/3.99 % (3234529)------------------------------ % 25.00/3.99 % (3234529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.00/3.99 % (3234529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.00/3.99 % (3234529)CaDiCaL version: 2.1.3 % 25.00/3.99 % (3234529)Termination reason: Instruction limit % 25.00/3.99 % (3234529)Termination phase: Finite model building constraint generation % 25.00/3.99 % (3234529)Time elapsed: 0.159 s % 25.00/3.99 % (3234529)Peak memory usage: 36 MB % 25.00/3.99 % (3234529)Instructions burned: 719 (million) % 25.00/3.99 % TRYING [5] % 25.00/3.99 % (3234541)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=534796784:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 25.00/3.99 % (3234531)Instruction limit reached! % 25.00/3.99 % (3234531)------------------------------ % 25.00/3.99 % (3234531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.00/3.99 % (3234531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.00/3.99 % (3234531)CaDiCaL version: 2.1.3 % 25.00/3.99 % (3234531)Termination reason: Instruction limit % 25.00/3.99 % (3234531)Termination phase: Saturation % 25.00/3.99 % (3234531)Time elapsed: 0.207 s % 25.00/3.99 % (3234531)Peak memory usage: 20 MB % 25.00/3.99 % (3234531)Instructions burned: 685 (million) % 25.00/3.99 % (3234543)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2227947990:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi) % 25.00/3.99 % (3234537)Instruction limit reached! % 25.00/3.99 % (3234537)------------------------------ % 25.00/3.99 % (3234537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.00/3.99 % (3234537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.00/3.99 % (3234537)CaDiCaL version: 2.1.3 % 25.00/3.99 % (3234537)Termination reason: Instruction limit % 25.00/3.99 % (3234537)Termination phase: Saturation % 25.00/3.99 % (3234537)Time elapsed: 0.170 s % 25.00/3.99 % (3234537)Peak memory usage: 14 MB % 25.00/3.99 % (3234537)Instructions burned: 479 (million) % 25.00/3.99 % (3234545)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=4070506106: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) % 25.00/3.99 % (3234539)Instruction limit reached! % 25.00/3.99 % (3234539)------------------------------ % 25.00/3.99 % (3234539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 25.00/3.99 % (3234539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.00/3.99 % (3234539)CaDiCaL version: 2.1.3 % 25.00/3.99 % (3234539)Termination reason: Instruction limit % 25.00/3.99 % (3234539)Termination phase: Finite model building SAT solving % 25.00/3.99 % (3234539)Time elapsed: 0.192 s % 25.00/3.99 % (3234539)Peak memory usage: 23 MB % 25.00/3.99 % (3234539)Instructions burned: 871 (million) % 25.00/3.99 % (3234547)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3433298940:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi) % 25.00/3.99 % TRYING [14] % 25.00/3.99 % TRYING [7] % 52.48/7.80 % (3234543)Instruction limit reached! % 52.48/7.80 % (3234543)------------------------------ % 52.48/7.80 % (3234543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 52.48/7.80 % (3234543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.48/7.80 % (3234543)CaDiCaL version: 2.1.3 % 52.48/7.80 % (3234543)Termination reason: Instruction limit % 52.48/7.80 % (3234543)Termination phase: Finite model building constraint generation % 52.48/7.80 % (3234543)Time elapsed: 0.181 s % 52.48/7.80 % (3234543)Peak memory usage: 73 MB % 52.48/7.80 % (3234543)Instructions burned: 892 (million) % 52.48/7.80 % (3234549)fmb+10_1_sil=64000:random_seed=4021850257:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi) % 52.48/7.80 % TRYING [1] % 52.48/7.80 % TRYING [2] % 52.48/7.80 % TRYING [3] % 52.48/7.80 % (3234545)Instruction limit reached! % 52.48/7.80 % (3234545)------------------------------ % 52.48/7.80 % (3234545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 52.48/7.80 % (3234545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.48/7.80 % (3234545)CaDiCaL version: 2.1.3 % 52.48/7.80 % (3234545)Termination reason: Instruction limit % 52.48/7.80 % (3234545)Termination phase: Saturation % 52.48/7.80 % (3234545)Time elapsed: 0.213 s % 52.48/7.80 % (3234545)Peak memory usage: 21 MB % 52.48/7.80 % (3234545)Instructions burned: 695 (million) % 52.48/7.80 % (3234551)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2618100466:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi) % 52.48/7.80 % TRYING [4] % 52.48/7.80 % TRYING [20] % 52.48/7.80 % (3234541)Instruction limit reached! % 52.48/7.80 % (3234541)------------------------------ % 52.48/7.80 % (3234541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 52.48/7.80 % (3234541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.48/7.80 % (3234541)CaDiCaL version: 2.1.3 % 52.48/7.80 % (3234541)Termination reason: Instruction limit % 52.48/7.80 % (3234541)Termination phase: Saturation % 52.48/7.80 % (3234541)Time elapsed: 0.357 s % 52.48/7.80 % (3234541)Peak memory usage: 29 MB % 52.48/7.80 % (3234541)Instructions burned: 1182 (million) % 52.48/7.80 % (3234547)Instruction limit reached! % 52.48/7.80 % (3234547)------------------------------ % 52.48/7.80 % (3234547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 52.48/7.80 % (3234547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.48/7.80 % (3234547)CaDiCaL version: 2.1.3 % 52.48/7.80 % (3234547)Termination reason: Instruction limit % 52.48/7.80 % (3234547)Termination phase: Saturation % 52.48/7.80 % (3234547)Time elapsed: 0.257 s % 52.48/7.80 % (3234547)Peak memory usage: 20 MB % 52.48/7.80 % (3234547)Instructions burned: 879 (million) % 52.48/7.80 % (3234553)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=175375447:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi) % 52.48/7.80 % (3234554)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3655182033:i=5131_2993 on theBenchmark for (2993ds/5131Mi) % 52.48/7.80 % TRYING [8] % 52.48/7.80 % TRYING [5] % 52.48/7.80 % (3234553)Instruction limit reached! % 52.48/7.80 % (3234553)------------------------------ % 52.48/7.80 % (3234553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 52.48/7.80 % (3234553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.48/7.80 % (3234553)CaDiCaL version: 2.1.3 % 52.48/7.80 % (3234553)Termination reason: Instruction limit % 52.48/7.80 % (3234553)Termination phase: Finite model building constraint generation % 52.48/7.80 % (3234553)Time elapsed: 0.183 s % 52.48/7.80 % (3234553)Peak memory usage: 79 MB % 52.48/7.80 % (3234553)Instructions burned: 923 (million) % 52.48/7.80 % (3234557)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=255162388:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi) % 52.48/7.80 % TRYING [6] % 52.48/7.80 % TRYING [8] % 52.48/7.80 % (3234557)Instruction limit reached! % 52.48/7.80 % (3234557)------------------------------ % 52.48/7.80 % (3234557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 52.48/7.80 % (3234557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.48/7.80 % (3234557)CaDiCaL version: 2.1.3 % 52.48/7.80 % (3234557)Termination reason: Instruction limit % 52.48/7.80 % (3234557)Termination phase: Saturation % 52.48/7.80 % (3234557)Time elapsed: 0.346 s % 52.48/7.80 % (3234557)Peak memory usage: 15 MB % 52.48/7.80 % (3234557)Instructions burned: 1484 (million) % 52.48/7.80 % (3234559)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3448593807:i=6324_2988 on theBenchmark for (2988ds/6324Mi) % 139.92/20.26 % TRYING [77] % 139.92/20.26 % TRYING [7] % 139.92/20.26 % (3234554)Instruction limit reached! % 139.92/20.26 % (3234554)------------------------------ % 139.92/20.26 % (3234554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.92/20.26 % (3234554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.92/20.26 % (3234554)CaDiCaL version: 2.1.3 % 139.92/20.26 % (3234554)Termination reason: Instruction limit % 139.92/20.26 % (3234554)Termination phase: Saturation % 139.92/20.26 % (3234554)Time elapsed: 1.403 s % 139.92/20.26 % (3234554)Peak memory usage: 57 MB % 139.92/20.26 % (3234554)Instructions burned: 5134 (million) % 139.92/20.26 % (3234561)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=99744640:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi) % 139.92/20.26 % TRYING [16] % 139.92/20.26 % (3234551)Instruction limit reached! % 139.92/20.26 % (3234551)------------------------------ % 139.92/20.26 % (3234551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.92/20.26 % (3234551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.92/20.26 % (3234551)CaDiCaL version: 2.1.3 % 139.92/20.26 % (3234551)Termination reason: Instruction limit % 139.92/20.26 % (3234551)Termination phase: Finite model building constraint generation % 139.92/20.26 % (3234551)Time elapsed: 1.799 s % 139.92/20.26 % (3234551)Peak memory usage: 589 MB % 139.92/20.26 % (3234551)Instructions burned: 9515 (million) % 139.92/20.26 % (3234563)ott-2_1_sil=16000:newcnf=on:random_seed=3075934402:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2976 on theBenchmark for (2976ds/869Mi) % 139.92/20.26 % (3234559)Instruction limit reached! % 139.92/20.26 % (3234559)------------------------------ % 139.92/20.26 % (3234559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.92/20.26 % (3234559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.92/20.26 % (3234559)CaDiCaL version: 2.1.3 % 139.92/20.26 % (3234559)Termination reason: Instruction limit % 139.92/20.26 % (3234559)Termination phase: Finite model building constraint generation % 139.92/20.26 % (3234559)Time elapsed: 1.245 s % 139.92/20.26 % (3234559)Peak memory usage: 455 MB % 139.92/20.26 % (3234559)Instructions burned: 6330 (million) % 139.92/20.26 % TRYING [8] % 139.92/20.26 % (3234561)Instruction limit reached! % 139.92/20.26 % (3234561)------------------------------ % 139.92/20.26 % (3234561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.92/20.26 % (3234561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.92/20.26 % (3234561)CaDiCaL version: 2.1.3 % 139.92/20.26 % (3234561)Termination reason: Instruction limit % 139.92/20.26 % (3234561)Termination phase: Finite model building constraint generation % 139.92/20.26 % (3234561)Time elapsed: 0.415 s % 139.92/20.26 % (3234561)Peak memory usage: 138 MB % 139.92/20.26 % (3234561)Instructions burned: 2178 (million) % 139.92/20.26 % (3234565)ott+10_1_sil=32000:tgt=ground:random_seed=60136884:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi) % 139.92/20.26 % (3234566)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2674236108:i=54282_2975 on theBenchmark for (2975ds/54282Mi) % 139.92/20.26 % TRYING [1] % 139.92/20.26 % TRYING [2] % 139.92/20.26 % TRYING [3] % 139.92/20.26 % TRYING [4] % 139.92/20.26 % TRYING [5] % 139.92/20.26 % TRYING [6] % 139.92/20.26 % (3234563)Instruction limit reached! % 139.92/20.26 % (3234563)------------------------------ % 139.92/20.26 % (3234563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.92/20.26 % (3234563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.92/20.26 % (3234563)CaDiCaL version: 2.1.3 % 139.92/20.26 % (3234563)Termination reason: Instruction limit % 139.92/20.26 % (3234563)Termination phase: Saturation % 139.92/20.26 % (3234563)Time elapsed: 0.259 s % 139.92/20.26 % (3234563)Peak memory usage: 24 MB % 139.92/20.26 % (3234563)Instructions burned: 871 (million) % 139.92/20.26 % (3234569)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1612492868:i=3512:aac=none_2973 on theBenchmark for (2973ds/3512Mi) % 139.92/20.26 % TRYING [9] % 139.92/20.26 % TRYING [7] % 139.92/20.26 % TRYING [8] % 139.92/20.26 % (3234569)Instruction limit reached! % 139.92/20.26 % (3234569)------------------------------ % 139.92/20.26 % (3234569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 139.92/20.26 % (3234569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.92/20.26 % (3234569)CaDiCaL version: 2.1.3 % 139.92/20.26 % (3234569)Termination reason: Instruction limit % 139.92/20.26 % (3234569)Termination phase: Saturation % 139.92/20.26 % (3234569)Time elapsed: 0.987 s % 139.92/20.26 % (3234569)Peak memory usage: 42 MB % 139.92/20.26 % (3234569)Instructions burned: 3512 (million) % 188.72/27.18 % (3234571)dis+21_1_sil=32000:sas=cadical:random_seed=966366565:i=3773:amm=off_2963 on theBenchmark for (2963ds/3773Mi) % 188.72/27.18 % (3234565)Instruction limit reached! % 188.72/27.18 % (3234565)------------------------------ % 188.72/27.18 % (3234565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.72/27.18 % (3234565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.72/27.18 % (3234565)CaDiCaL version: 2.1.3 % 188.72/27.18 % (3234565)Termination reason: Instruction limit % 188.72/27.18 % (3234565)Termination phase: Saturation % 188.72/27.18 % (3234565)Time elapsed: 1.455 s % 188.72/27.18 % (3234565)Peak memory usage: 65 MB % 188.72/27.18 % (3234565)Instructions burned: 5115 (million) % 188.72/27.18 % (3234573)ott+11_1_sil=16000:gs=on:random_seed=4123589931:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2960 on theBenchmark for (2960ds/2251Mi) % 188.72/27.18 % (3234573)Instruction limit reached! % 188.72/27.18 % (3234573)------------------------------ % 188.72/27.18 % (3234573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.72/27.18 % (3234573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.72/27.18 % (3234573)CaDiCaL version: 2.1.3 % 188.72/27.18 % (3234573)Termination reason: Instruction limit % 188.72/27.18 % (3234573)Termination phase: Saturation % 188.72/27.18 % (3234573)Time elapsed: 0.464 s % 188.72/27.18 % (3234573)Peak memory usage: 13 MB % 188.72/27.18 % (3234573)Instructions burned: 2251 (million) % 188.72/27.18 % (3234575)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=849452925:fmbsr=1.6:i=67534_2956 on theBenchmark for (2956ds/67534Mi) % 188.72/27.18 % TRYING [7] % 188.72/27.18 % TRYING [9] % 188.72/27.18 % (3234571)Instruction limit reached! % 188.72/27.18 % (3234571)------------------------------ % 188.72/27.18 % (3234571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.72/27.18 % (3234571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.72/27.18 % (3234571)CaDiCaL version: 2.1.3 % 188.72/27.18 % (3234571)Termination reason: Instruction limit % 188.72/27.18 % (3234571)Termination phase: Saturation % 188.72/27.18 % (3234571)Time elapsed: 1.130 s % 188.72/27.18 % (3234571)Peak memory usage: 48 MB % 188.72/27.18 % (3234571)Instructions burned: 3775 (million) % 188.72/27.18 % (3234577)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1625190883:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2952 on theBenchmark for (2952ds/4591Mi) % 188.72/27.18 % TRYING [9] % 188.72/27.18 % TRYING [10] % 188.72/27.18 % TRYING [8] % 188.72/27.18 % (3234549)Instruction limit reached! % 188.72/27.18 % (3234549)------------------------------ % 188.72/27.18 % (3234549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.72/27.18 % (3234549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.72/27.18 % (3234549)CaDiCaL version: 2.1.3 % 188.72/27.18 % (3234549)Termination reason: Instruction limit % 188.72/27.18 % (3234549)Termination phase: Finite model building constraint generation % 188.72/27.18 % (3234549)Time elapsed: 5.130 s % 188.72/27.18 % (3234549)Peak memory usage: 245 MB % 188.72/27.18 % (3234549)Instructions burned: 22065 (million) % 188.72/27.18 % (3234579)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2932338239:i=29340_2943 on theBenchmark for (2943ds/29340Mi) % 188.72/27.18 % (3234577)Instruction limit reached! % 188.72/27.18 % (3234577)------------------------------ % 188.72/27.18 % (3234577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.72/27.18 % (3234577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.72/27.18 % (3234577)CaDiCaL version: 2.1.3 % 188.72/27.18 % (3234577)Termination reason: Instruction limit % 188.72/27.18 % (3234577)Termination phase: Saturation % 188.72/27.18 % (3234577)Time elapsed: 1.106 s % 188.72/27.18 % (3234577)Peak memory usage: 53 MB % 188.72/27.18 % (3234577)Instructions burned: 4595 (million) % 188.72/27.18 % (3234581)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2471476160:i=5211_2940 on theBenchmark for (2940ds/5211Mi) % 188.72/27.18 % (3234581)Instruction limit reached! % 188.72/27.18 % (3234581)------------------------------ % 188.72/27.18 % (3234581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 188.72/27.18 % (3234581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.72/27.18 % (3234581)CaDiCaL version: 2.1.3 % 188.72/27.18 % (3234581)Termination reason: Instruction limit % 188.72/27.18 % (3234581)Termination phase: Saturation % 188.72/27.18 % (3234581)Time elapsed: 1.531 s % 188.72/27.18 % (3234581)Peak memory usage: 58 MB % 188.72/27.18 % (3234581)Instructions burned: 5211 (million) % 284.50/40.77 % (3234583)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3544420296:i=5497:nm=2_2925 on theBenchmark for (2925ds/5497Mi) % 284.50/40.77 % TRYING [17] % 284.50/40.77 % TRYING [10] % 284.50/40.77 % TRYING [9] % 284.50/40.77 % (3234583)Instruction limit reached! % 284.50/40.77 % (3234583)------------------------------ % 284.50/40.77 % (3234583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.50/40.77 % (3234583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/40.77 % (3234583)CaDiCaL version: 2.1.3 % 284.50/40.77 % (3234583)Termination reason: Instruction limit % 284.50/40.77 % (3234583)Termination phase: Finite model building constraint generation % 284.50/40.77 % (3234583)Time elapsed: 1.027 s % 284.50/40.77 % (3234583)Peak memory usage: 345 MB % 284.50/40.77 % (3234583)Instructions burned: 5499 (million) % 284.50/40.77 % (3234585)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2361305387:fmbsr=2:i=46332_2914 on theBenchmark for (2914ds/46332Mi) % 284.50/40.77 % TRYING [15] % 284.50/40.77 % TRYING [11] % 284.50/40.77 % TRYING [10] % 284.50/40.77 % (3234579)Instruction limit reached! % 284.50/40.77 % (3234579)------------------------------ % 284.50/40.77 % (3234579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.50/40.77 % (3234579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/40.77 % (3234579)CaDiCaL version: 2.1.3 % 284.50/40.77 % (3234579)Termination reason: Instruction limit % 284.50/40.77 % (3234579)Termination phase: Saturation % 284.50/40.77 % (3234579)Time elapsed: 7.645 s % 284.50/40.77 % (3234579)Peak memory usage: 196 MB % 284.50/40.77 % (3234579)Instructions burned: 29343 (million) % 284.50/40.77 % (3234587)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3019447520:i=14071_2866 on theBenchmark for (2866ds/14071Mi) % 284.50/40.77 % TRYING [12] % 284.50/40.77 % TRYING [11] % 284.50/40.77 % (3234587)Instruction limit reached! % 284.50/40.77 % (3234587)------------------------------ % 284.50/40.77 % (3234587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.50/40.77 % (3234587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/40.77 % (3234587)CaDiCaL version: 2.1.3 % 284.50/40.77 % (3234587)Termination reason: Instruction limit % 284.50/40.77 % (3234587)Termination phase: Finite model building constraint generation % 284.50/40.77 % (3234587)Time elapsed: 2.765 s % 284.50/40.77 % (3234587)Peak memory usage: 897 MB % 284.50/40.77 % (3234587)Instructions burned: 14072 (million) % 284.50/40.77 % (3234589)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1200107617:i=22565:add=on:rawr=on_2838 on theBenchmark for (2838ds/22565Mi) % 284.50/40.77 % (3234585)Instruction limit reached! % 284.50/40.77 % (3234585)------------------------------ % 284.50/40.77 % (3234585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.50/40.77 % (3234585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/40.77 % (3234585)CaDiCaL version: 2.1.3 % 284.50/40.77 % (3234585)Termination reason: Instruction limit % 284.50/40.77 % (3234585)Termination phase: Finite model building constraint generation % 284.50/40.77 % (3234585)Time elapsed: 8.498 s % 284.50/40.77 % (3234585)Peak memory usage: 2196 MB % 284.50/40.77 % (3234585)Instructions burned: 46336 (million) % 284.50/40.77 % (3234591)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=848291230:i=8173:av=off_2827 on theBenchmark for (2827ds/8173Mi) % 284.50/40.77 % (3234591)Instruction limit reached! % 284.50/40.77 % (3234591)------------------------------ % 284.50/40.77 % (3234591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.50/40.77 % (3234591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/40.77 % (3234591)CaDiCaL version: 2.1.3 % 284.50/40.77 % (3234591)Termination reason: Instruction limit % 284.50/40.77 % (3234591)Termination phase: Saturation % 284.50/40.77 % (3234591)Time elapsed: 2.220 s % 284.50/40.77 % (3234591)Peak memory usage: 95 MB % 284.50/40.77 % (3234591)Instructions burned: 8174 (million) % 284.50/40.77 % (3234593)dis+10_16:1_sil=16000:random_seed=2543384815:i=9155:fsr=off_2805 on theBenchmark for (2805ds/9155Mi) % 284.50/40.77 % (3234566)Instruction limit reached! % 284.50/40.77 % (3234566)------------------------------ % 284.50/40.77 % (3234566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 284.50/40.77 % (3234566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/40.77 % (3234566)CaDiCaL version: 2.1.3 % 284.50/40.77 % (3234566)Termination reason: Instruction limit % 284.50/40.77 % (3234566)Termination phase: Finite model builTerminated % 300.85/43.05 % Vampire exiting %------------------------------------------------------------------------------