%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW892+1 : TPTP v9.3.1. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:45:08 PM UTC 2026 % Result : Timeout 300.39s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW892+1 : TPTP v9.3.1. Released v7.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.19 % Computer : n006.cluster.edu % 0.06/0.19 % Model : x86_64 x86_64 % 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.19 % Memory : 8046.5625MB % 0.06/0.19 % OS : Linux 6.8.0-71-generic % 0.06/0.19 % CPULimit : 300 % 0.06/0.19 % WCLimit : 300 % 0.06/0.19 % DateTime : Mon Sep 28 14:37:25 UTC 2026 % 0.06/0.19 % CPUTime : % 0.06/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.06/0.22 Running first-order model finding % 0.06/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.76/3.64 % (4018858)Will run a generic schedule for satisfiability detection. % 23.76/3.64 % (4018866)dis+10_1_sil=32000:sp=arity:random_seed=3876519585:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 23.76/3.64 % (4018864)% WARNING: option uhcvi not known. % 23.76/3.64 % (4018863)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=940624148_2999 on theBenchmark for (2999ds/0Mi) % 23.76/3.64 % (4018864)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2632732994:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 23.76/3.64 % (4018865)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1588692471:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 23.76/3.64 % (4018867)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3073585140:i=116_2999 on theBenchmark for (2999ds/116Mi) % 23.76/3.64 % (4018868)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=71451461:i=131_2999 on theBenchmark for (2999ds/131Mi) % 23.76/3.64 % (4018869)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2796067554:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 23.76/3.64 % (4018866)Instruction limit reached! % 23.76/3.64 % (4018866)------------------------------ % 23.76/3.64 % (4018866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.76/3.64 % (4018866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.76/3.64 % (4018866)CaDiCaL version: 2.1.3 % 23.76/3.64 % (4018866)Termination reason: Instruction limit % 23.76/3.64 % (4018866)Termination phase: Saturation % 23.76/3.64 % (4018866)Time elapsed: 0.029 s % 23.76/3.64 % (4018866)Peak memory usage: 12 MB % 23.76/3.64 % (4018866)Instructions burned: 103 (million) % 23.76/3.64 % (4018877)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3902298956:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 23.76/3.64 % (4018867)Instruction limit reached! % 23.76/3.64 % (4018867)------------------------------ % 23.76/3.64 % (4018867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.76/3.64 % (4018867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.76/3.64 % (4018867)CaDiCaL version: 2.1.3 % 23.76/3.64 % (4018867)Termination reason: Instruction limit % 23.76/3.64 % (4018867)Termination phase: Saturation % 23.76/3.64 % (4018867)Time elapsed: 0.056 s % 23.76/3.64 % (4018867)Peak memory usage: 13 MB % 23.76/3.64 % (4018867)Instructions burned: 117 (million) % 23.76/3.64 % (4018868)Instruction limit reached! % 23.76/3.64 % (4018868)------------------------------ % 23.76/3.64 % (4018868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.76/3.64 % (4018868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.76/3.64 % (4018868)CaDiCaL version: 2.1.3 % 23.76/3.64 % (4018868)Termination reason: Instruction limit % 23.76/3.64 % (4018868)Termination phase: Saturation % 23.76/3.64 % (4018868)Time elapsed: 0.066 s % 23.76/3.64 % (4018868)Peak memory usage: 13 MB % 23.76/3.64 % (4018868)Instructions burned: 131 (million) % 23.76/3.64 % (4018879)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3833215046:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 23.76/3.64 % (4018880)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=2592426254:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 23.76/3.64 % (4018869)Instruction limit reached! % 23.76/3.64 % (4018869)------------------------------ % 23.76/3.64 % (4018869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.76/3.64 % (4018869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.76/3.64 % (4018869)CaDiCaL version: 2.1.3 % 23.76/3.64 % (4018869)Termination reason: Instruction limit % 23.76/3.64 % (4018869)Termination phase: Saturation % 23.76/3.64 % (4018869)Time elapsed: 0.086 s % 23.76/3.64 % (4018869)Peak memory usage: 13 MB % 23.76/3.64 % (4018869)Instructions burned: 159 (million) % 23.76/3.64 % (4018883)ott-21_1_sil=16000:fs=off:random_seed=2186551197:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 23.76/3.64 % (4018879)Instruction limit reached! % 23.76/3.64 % (4018879)------------------------------ % 23.76/3.64 % (4018879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 23.76/3.64 % (4018879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.76/3.64 % (4018879)CaDiCaL version: 2.1.3 % 44.86/6.64 % (4018879)Termination reason: Instruction limit % 44.86/6.64 % (4018879)Termination phase: Saturation % 44.86/6.64 % (4018879)Time elapsed: 0.065 s % 44.86/6.64 % (4018879)Peak memory usage: 13 MB % 44.86/6.64 % (4018879)Instructions burned: 131 (million) % 44.86/6.64 % (4018885)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2721178650:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi) % 44.86/6.64 % (4018883)Instruction limit reached! % 44.86/6.64 % (4018883)------------------------------ % 44.86/6.64 % (4018883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.86/6.64 % (4018883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.86/6.64 % (4018883)CaDiCaL version: 2.1.3 % 44.86/6.64 % (4018883)Termination reason: Instruction limit % 44.86/6.64 % (4018883)Termination phase: Saturation % 44.86/6.64 % (4018883)Time elapsed: 0.083 s % 44.86/6.64 % (4018883)Peak memory usage: 13 MB % 44.86/6.64 % (4018883)Instructions burned: 180 (million) % 44.86/6.64 % (4018887)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=690877737:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 44.86/6.64 % (4018877)Instruction limit reached! % 44.86/6.64 % (4018877)------------------------------ % 44.86/6.64 % (4018877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.86/6.64 % (4018877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.86/6.64 % (4018877)CaDiCaL version: 2.1.3 % 44.86/6.64 % (4018877)Termination reason: Instruction limit % 44.86/6.64 % (4018877)Termination phase: Finite model building preprocessing % 44.86/6.64 % (4018877)Time elapsed: 0.194 s % 44.86/6.64 % (4018877)Peak memory usage: 14 MB % 44.86/6.64 % (4018877)Instructions burned: 714 (million) % 44.86/6.64 % (4018889)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3025877667:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 44.86/6.64 % (4018885)Instruction limit reached! % 44.86/6.64 % (4018885)------------------------------ % 44.86/6.64 % (4018885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.86/6.64 % (4018885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.86/6.64 % (4018885)CaDiCaL version: 2.1.3 % 44.86/6.64 % (4018885)Termination reason: Instruction limit % 44.86/6.64 % (4018885)Termination phase: Saturation % 44.86/6.64 % (4018885)Time elapsed: 0.263 s % 44.86/6.64 % (4018885)Peak memory usage: 14 MB % 44.86/6.64 % (4018885)Instructions burned: 479 (million) % 44.86/6.64 % (4018880)Instruction limit reached! % 44.86/6.64 % (4018880)------------------------------ % 44.86/6.64 % (4018880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.86/6.64 % (4018880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.86/6.64 % (4018880)CaDiCaL version: 2.1.3 % 44.86/6.64 % (4018880)Termination reason: Instruction limit % 44.86/6.64 % (4018880)Termination phase: Saturation % 44.86/6.64 % (4018880)Time elapsed: 0.351 s % 44.86/6.64 % (4018880)Peak memory usage: 17 MB % 44.86/6.64 % (4018880)Instructions burned: 685 (million) % 44.86/6.64 % (4018891)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3437060202:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 44.86/6.64 % (4018892)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=3811410223:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi) % 44.86/6.64 % (4018889)Instruction limit reached! % 44.86/6.64 % (4018889)------------------------------ % 44.86/6.64 % (4018889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.86/6.64 % (4018889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.86/6.64 % (4018889)CaDiCaL version: 2.1.3 % 44.86/6.64 % (4018889)Termination reason: Instruction limit % 44.86/6.64 % (4018889)Termination phase: Saturation % 44.86/6.64 % (4018889)Time elapsed: 0.313 s % 44.86/6.64 % (4018889)Peak memory usage: 20 MB % 44.86/6.64 % (4018889)Instructions burned: 1183 (million) % 44.86/6.64 % (4018895)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1846611462:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi) % 44.86/6.64 % (4018887)Instruction limit reached! % 44.86/6.64 % (4018887)------------------------------ % 44.86/6.64 % (4018887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 44.86/6.64 % (4018887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018887)CaDiCaL version: 2.1.3 % 108.89/15.68 % (4018887)Termination reason: Instruction limit % 108.89/15.68 % (4018887)Termination phase: Finite model building preprocessing % 108.89/15.68 % (4018887)Time elapsed: 0.442 s % 108.89/15.68 % (4018887)Peak memory usage: 14 MB % 108.89/15.68 % (4018887)Instructions burned: 865 (million) % 108.89/15.68 % (4018897)fmb+10_1_sil=64000:random_seed=2941197964:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 108.89/15.68 % (4018892)Instruction limit reached! % 108.89/15.68 % (4018892)------------------------------ % 108.89/15.68 % (4018892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.89/15.68 % (4018892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018892)CaDiCaL version: 2.1.3 % 108.89/15.68 % (4018892)Termination reason: Instruction limit % 108.89/15.68 % (4018892)Termination phase: Saturation % 108.89/15.68 % (4018892)Time elapsed: 0.353 s % 108.89/15.68 % (4018892)Peak memory usage: 15 MB % 108.89/15.68 % (4018892)Instructions burned: 692 (million) % 108.89/15.68 % (4018895)Instruction limit reached! % 108.89/15.68 % (4018895)------------------------------ % 108.89/15.68 % (4018895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.89/15.68 % (4018895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018895)CaDiCaL version: 2.1.3 % 108.89/15.68 % (4018895)Termination reason: Instruction limit % 108.89/15.68 % (4018895)Termination phase: Saturation % 108.89/15.68 % (4018895)Time elapsed: 0.248 s % 108.89/15.68 % (4018895)Peak memory usage: 20 MB % 108.89/15.68 % (4018895)Instructions burned: 881 (million) % 108.89/15.68 % (4018900)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2521853950:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi) % 108.89/15.68 % (4018899)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2745952533:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi) % 108.89/15.68 % (4018891)Instruction limit reached! % 108.89/15.68 % (4018891)------------------------------ % 108.89/15.68 % (4018891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.89/15.68 % (4018891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018891)CaDiCaL version: 2.1.3 % 108.89/15.68 % (4018891)Termination reason: Instruction limit % 108.89/15.68 % (4018891)Termination phase: Finite model building preprocessing % 108.89/15.68 % (4018891)Time elapsed: 0.455 s % 108.89/15.68 % (4018891)Peak memory usage: 15 MB % 108.89/15.68 % (4018891)Instructions burned: 890 (million) % 108.89/15.68 % (4018903)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=856079303:i=5131_2990 on theBenchmark for (2990ds/5131Mi) % 108.89/15.68 % (4018900)Instruction limit reached! % 108.89/15.68 % (4018900)------------------------------ % 108.89/15.68 % (4018900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.89/15.68 % (4018900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018900)CaDiCaL version: 2.1.3 % 108.89/15.68 % (4018900)Termination reason: Instruction limit % 108.89/15.68 % (4018900)Termination phase: Finite model building preprocessing % 108.89/15.68 % (4018900)Time elapsed: 0.250 s % 108.89/15.68 % (4018900)Peak memory usage: 14 MB % 108.89/15.68 % (4018900)Instructions burned: 921 (million) % 108.89/15.68 % (4018905)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2925867656:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 108.89/15.68 % TRYING [1] % 108.89/15.68 % TRYING [2] % 108.89/15.68 % (4018905)Instruction limit reached! % 108.89/15.68 % (4018905)------------------------------ % 108.89/15.68 % (4018905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.89/15.68 % (4018905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018905)CaDiCaL version: 2.1.3 % 108.89/15.68 % (4018905)Termination reason: Instruction limit % 108.89/15.68 % (4018905)Termination phase: Saturation % 108.89/15.68 % (4018905)Time elapsed: 0.427 s % 108.89/15.68 % (4018905)Peak memory usage: 30 MB % 108.89/15.68 % (4018905)Instructions burned: 1475 (million) % 108.89/15.68 % (4018907)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2567833338:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 108.89/15.68 % TRYING [3] % 108.89/15.68 % TRYING [4] % 108.89/15.68 % (4018907)Instruction limit reached! % 108.89/15.68 % (4018907)------------------------------ % 108.89/15.68 % (4018907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 108.89/15.68 % (4018907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.89/15.68 % (4018907)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018907)Termination reason: Instruction limit % 205.76/33.41 % (4018907)Termination phase: Finite model building preprocessing % 205.76/33.41 % (4018907)Time elapsed: 1.835 s % 205.76/33.41 % (4018907)Peak memory usage: 26 MB % 205.76/33.41 % (4018907)Instructions burned: 6326 (million) % 205.76/33.41 % (4018910)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3028097536:fmbsr=2.30978:i=2174_2965 on theBenchmark for (2965ds/2174Mi) % 205.76/33.41 % (4018903)Instruction limit reached! % 205.76/33.41 % (4018903)------------------------------ % 205.76/33.41 % (4018903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.76/33.41 % (4018903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.76/33.41 % (4018903)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018903)Termination reason: Instruction limit % 205.76/33.41 % (4018903)Termination phase: Saturation % 205.76/33.41 % (4018903)Time elapsed: 2.673 s % 205.76/33.41 % (4018903)Peak memory usage: 32 MB % 205.76/33.41 % (4018903)Instructions burned: 5133 (million) % 205.76/33.41 % (4018912)ott-2_1_sil=16000:newcnf=on:random_seed=4190208311:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2963 on theBenchmark for (2963ds/869Mi) % 205.76/33.41 % (4018910)Instruction limit reached! % 205.76/33.41 % (4018910)------------------------------ % 205.76/33.41 % (4018910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.76/33.41 % (4018910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.76/33.41 % (4018910)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018910)Termination reason: Instruction limit % 205.76/33.41 % (4018910)Termination phase: Finite model building preprocessing % 205.76/33.41 % (4018910)Time elapsed: 0.613 s % 205.76/33.41 % (4018910)Peak memory usage: 18 MB % 205.76/33.41 % (4018910)Instructions burned: 2176 (million) % 205.76/33.41 % (4018914)ott+10_1_sil=32000:tgt=ground:random_seed=3407185359:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi) % 205.76/33.41 % (4018912)Instruction limit reached! % 205.76/33.41 % (4018912)------------------------------ % 205.76/33.41 % (4018912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.76/33.41 % (4018912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.76/33.41 % (4018912)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018912)Termination reason: Instruction limit % 205.76/33.41 % (4018912)Termination phase: Saturation % 205.76/33.41 % (4018912)Time elapsed: 0.456 s % 205.76/33.41 % (4018912)Peak memory usage: 16 MB % 205.76/33.41 % (4018912)Instructions burned: 870 (million) % 205.76/33.41 % (4018916)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=15753933:i=54282_2958 on theBenchmark for (2958ds/54282Mi) % 205.76/33.41 % (4018914)Instruction limit reached! % 205.76/33.41 % (4018914)------------------------------ % 205.76/33.41 % (4018914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.76/33.41 % (4018914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.76/33.41 % (4018914)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018914)Termination reason: Instruction limit % 205.76/33.41 % (4018914)Termination phase: Saturation % 205.76/33.41 % (4018914)Time elapsed: 1.375 s % 205.76/33.41 % (4018914)Peak memory usage: 33 MB % 205.76/33.41 % (4018914)Instructions burned: 5114 (million) % 205.76/33.41 % (4018918)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=727027831:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi) % 205.76/33.41 % (4018899)Instruction limit reached! % 205.76/33.41 % (4018899)------------------------------ % 205.76/33.41 % (4018899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.76/33.41 % (4018899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.76/33.41 % (4018899)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018899)Termination reason: Instruction limit % 205.76/33.41 % (4018899)Termination phase: Finite model building preprocessing % 205.76/33.41 % (4018899)Time elapsed: 5.254 s % 205.76/33.41 % (4018899)Peak memory usage: 31 MB % 205.76/33.41 % (4018899)Instructions burned: 9517 (million) % 205.76/33.41 % (4018920)dis+21_1_sil=32000:sas=cadical:random_seed=3867170330:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi) % 205.76/33.41 % (4018918)Instruction limit reached! % 205.76/33.41 % (4018918)------------------------------ % 205.76/33.41 % (4018918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 205.76/33.41 % (4018918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 205.76/33.41 % (4018918)CaDiCaL version: 2.1.3 % 205.76/33.41 % (4018918)Termination reason: Instruction limit % 205.76/33.41 % (4018918)Termination phase: Saturation % 205.76/33.41 % (401Terminated % 300.39/42.64 % Vampire exiting %------------------------------------------------------------------------------