%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW228+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:39:40 PM UTC 2026 % Result : Timeout 286.65s 40.75s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW228+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n004.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 13:19:22 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.23 Running first-order model finding % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 13.14/2.18 % (352992)Will run a generic schedule for satisfiability detection. % 13.14/2.18 % (352999)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=417146654:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 13.14/2.18 % (352998)% WARNING: option uhcvi not known. % 13.14/2.18 % (352997)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2559171841_2999 on theBenchmark for (2999ds/0Mi) % 13.14/2.18 % (352998)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3962113424:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 13.14/2.18 % (353000)dis+10_1_sil=32000:sp=arity:random_seed=3002061910:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 13.14/2.18 % (353001)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1829178237:i=116_2999 on theBenchmark for (2999ds/116Mi) % 13.14/2.18 % (353003)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3681226283:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 13.14/2.18 % (353002)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3633062209:i=131_2999 on theBenchmark for (2999ds/131Mi) % 13.14/2.18 % (353000)Instruction limit reached! % 13.14/2.18 % (353000)------------------------------ % 13.14/2.18 % (353000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.14/2.18 % (353000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.18 % (353000)CaDiCaL version: 2.1.3 % 13.14/2.18 % (353000)Termination reason: Instruction limit % 13.14/2.18 % (353000)Termination phase: Saturation % 13.14/2.18 % (353000)Time elapsed: 0.050 s % 13.14/2.18 % (353000)Peak memory usage: 14 MB % 13.14/2.18 % (353000)Instructions burned: 103 (million) % 13.14/2.18 % (353001)Instruction limit reached! % 13.14/2.18 % (353001)------------------------------ % 13.14/2.18 % (353001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.14/2.18 % (353001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.18 % (353001)CaDiCaL version: 2.1.3 % 13.14/2.18 % (353001)Termination reason: Instruction limit % 13.14/2.18 % (353001)Termination phase: Property scanning % 13.14/2.18 % (353001)Time elapsed: 0.054 s % 13.14/2.18 % (353001)Peak memory usage: 13 MB % 13.14/2.18 % (353001)Instructions burned: 118 (million) % 13.14/2.18 % (353011)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1242934607:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 13.14/2.18 % (353002)Instruction limit reached! % 13.14/2.18 % (353002)------------------------------ % 13.14/2.18 % (353002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.14/2.18 % (353002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.18 % (353002)CaDiCaL version: 2.1.3 % 13.14/2.18 % (353002)Termination reason: Instruction limit % 13.14/2.18 % (353002)Termination phase: Saturation % 13.14/2.18 % (353002)Time elapsed: 0.073 s % 13.14/2.18 % (353002)Peak memory usage: 14 MB % 13.14/2.18 % (353002)Instructions burned: 132 (million) % 13.14/2.18 % (353012)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1490713778:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 13.14/2.18 % (353003)Instruction limit reached! % 13.14/2.18 % (353003)------------------------------ % 13.14/2.18 % (353003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.14/2.18 % (353003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.18 % (353003)CaDiCaL version: 2.1.3 % 13.14/2.18 % (353003)Termination reason: Instruction limit % 13.14/2.18 % (353003)Termination phase: Saturation % 13.14/2.18 % (353003)Time elapsed: 0.087 s % 13.14/2.18 % (353003)Peak memory usage: 15 MB % 13.14/2.18 % (353003)Instructions burned: 161 (million) % 13.14/2.18 % (353015)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=1450240980:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 13.14/2.18 % (353016)ott-21_1_sil=16000:fs=off:random_seed=5865381:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 13.14/2.18 % (353012)Instruction limit reached! % 13.14/2.18 % (353012)------------------------------ % 13.14/2.18 % (353012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 13.14/2.18 % (353012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.14/2.18 % (353012)CaDiCaL version: 2.1.3 % 13.14/2.18 % (353012)Termination reason: Instruction limit % 45.82/6.81 % (353012)Termination phase: Property scanning % 45.82/6.81 % (353012)Time elapsed: 0.060 s % 45.82/6.81 % (353012)Peak memory usage: 13 MB % 45.82/6.81 % (353012)Instructions burned: 133 (million) % 45.82/6.81 % (353019)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2338520826:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 45.82/6.81 % (353016)Instruction limit reached! % 45.82/6.81 % (353016)------------------------------ % 45.82/6.81 % (353016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.82/6.81 % (353016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.82/6.81 % (353016)CaDiCaL version: 2.1.3 % 45.82/6.81 % (353016)Termination reason: Instruction limit % 45.82/6.81 % (353016)Termination phase: Saturation % 45.82/6.81 % (353016)Time elapsed: 0.083 s % 45.82/6.81 % (353016)Peak memory usage: 14 MB % 45.82/6.81 % (353016)Instructions burned: 181 (million) % 45.82/6.81 % (353021)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1365163778:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 45.82/6.81 % TRYING [1] % 45.82/6.81 % TRYING [2] % 45.82/6.81 % TRYING [1] % 45.82/6.81 % TRYING [2] % 45.82/6.81 % (353011)Instruction limit reached! % 45.82/6.81 % (353011)------------------------------ % 45.82/6.81 % (353011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.82/6.81 % (353011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.82/6.81 % (353011)CaDiCaL version: 2.1.3 % 45.82/6.81 % (353011)Termination reason: Instruction limit % 45.82/6.81 % (353011)Termination phase: Finite model building constraint generation % 45.82/6.81 % (353011)Time elapsed: 0.331 s % 45.82/6.81 % (353011)Peak memory usage: 24 MB % 45.82/6.81 % (353011)Instructions burned: 714 (million) % 45.82/6.81 % (353023)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3499771538:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 45.82/6.81 % (353019)Instruction limit reached! % 45.82/6.81 % (353019)------------------------------ % 45.82/6.81 % (353019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.82/6.81 % (353019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.82/6.81 % (353019)CaDiCaL version: 2.1.3 % 45.82/6.81 % (353019)Termination reason: Instruction limit % 45.82/6.81 % (353019)Termination phase: Saturation % 45.82/6.81 % (353019)Time elapsed: 0.297 s % 45.82/6.81 % (353019)Peak memory usage: 16 MB % 45.82/6.81 % (353019)Instructions burned: 478 (million) % 45.82/6.81 % (353025)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1939680517:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi) % 45.82/6.81 % (353015)Instruction limit reached! % 45.82/6.81 % (353015)------------------------------ % 45.82/6.81 % (353015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.82/6.81 % (353015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.82/6.81 % (353015)CaDiCaL version: 2.1.3 % 45.82/6.81 % (353015)Termination reason: Instruction limit % 45.82/6.81 % (353015)Termination phase: Saturation % 45.82/6.81 % (353015)Time elapsed: 0.409 s % 45.82/6.81 % (353015)Peak memory usage: 20 MB % 45.82/6.81 % (353015)Instructions burned: 685 (million) % 45.82/6.81 % TRYING [3] % 45.82/6.81 % (353027)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=496160246:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi) % 45.82/6.81 % TRYING [1] % 45.82/6.81 % TRYING [2] % 45.82/6.81 % (353021)Instruction limit reached! % 45.82/6.81 % (353021)------------------------------ % 45.82/6.81 % (353021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.82/6.81 % (353021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.82/6.81 % (353021)CaDiCaL version: 2.1.3 % 45.82/6.81 % (353021)Termination reason: Instruction limit % 45.82/6.81 % (353021)Termination phase: Finite model building constraint generation % 45.82/6.81 % (353021)Time elapsed: 0.405 s % 45.82/6.81 % (353021)Peak memory usage: 33 MB % 45.82/6.81 % (353021)Instructions burned: 867 (million) % 45.82/6.81 % (353029)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1534996706:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi) % 45.82/6.81 % (353025)Instruction limit reached! % 45.82/6.81 % (353025)------------------------------ % 45.82/6.81 % (353025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 45.82/6.81 % (353025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.39/15.73 % (353025)CaDiCaL version: 2.1.3 % 109.39/15.73 % (353025)Termination reason: Instruction limit % 109.39/15.73 % (353025)Termination phase: Finite model building constraint generation % 109.39/15.73 % (353025)Time elapsed: 0.430 s % 109.39/15.73 % (353025)Peak memory usage: 53 MB % 109.39/15.73 % (353025)Instructions burned: 892 (million) % 109.39/15.73 % (353031)fmb+10_1_sil=64000:random_seed=3170777540:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 109.39/15.73 % (353027)Instruction limit reached! % 109.39/15.73 % (353027)------------------------------ % 109.39/15.73 % (353027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.39/15.73 % (353027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.39/15.73 % (353027)CaDiCaL version: 2.1.3 % 109.39/15.73 % (353027)Termination reason: Instruction limit % 109.39/15.73 % (353027)Termination phase: Saturation % 109.39/15.73 % (353027)Time elapsed: 0.451 s % 109.39/15.73 % (353027)Peak memory usage: 22 MB % 109.39/15.73 % (353027)Instructions burned: 692 (million) % 109.39/15.73 % (353033)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3117798723:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 109.39/15.73 % (353029)Instruction limit reached! % 109.39/15.73 % (353029)------------------------------ % 109.39/15.73 % (353029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.39/15.73 % (353029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.39/15.73 % (353029)CaDiCaL version: 2.1.3 % 109.39/15.73 % (353029)Termination reason: Instruction limit % 109.39/15.73 % (353029)Termination phase: Saturation % 109.39/15.73 % (353029)Time elapsed: 0.450 s % 109.39/15.73 % (353029)Peak memory usage: 20 MB % 109.39/15.73 % (353029)Instructions burned: 880 (million) % 109.39/15.73 % (353035)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3857085477:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 109.39/15.73 % (353023)Instruction limit reached! % 109.39/15.73 % (353023)------------------------------ % 109.39/15.73 % (353023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.39/15.73 % (353023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.39/15.73 % (353023)CaDiCaL version: 2.1.3 % 109.39/15.73 % (353023)Termination reason: Instruction limit % 109.39/15.73 % (353023)Termination phase: Saturation % 109.39/15.73 % (353023)Time elapsed: 0.733 s % 109.39/15.73 % (353023)Peak memory usage: 23 MB % 109.39/15.73 % (353023)Instructions burned: 1180 (million) % 109.39/15.73 % (353037)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2484493286:i=5131_2987 on theBenchmark for (2987ds/5131Mi) % 109.39/15.73 % TRYING [1] % 109.39/15.73 % TRYING [2] % 109.39/15.73 % (353033)Cannot represent all propositional literals internally % 109.39/15.73 % (353033)Refutation not found, incomplete strategy % 109.39/15.73 % (353033)------------------------------ % 109.39/15.73 % (353033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.39/15.73 % (353033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.39/15.73 % (353033)CaDiCaL version: 2.1.3 % 109.39/15.73 % (353033)Termination reason: Refutation not found, incomplete strategy % 109.39/15.73 % (353033)Time elapsed: 0.306 s % 109.39/15.73 % (353033)Peak memory usage: 22 MB % 109.39/15.73 % (353033)Instructions burned: 646 (million) % 109.39/15.73 % (353033)------------------------------ % 109.39/15.73 % (353033)------------------------------ % 109.39/15.73 % (353039)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2555826710:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 109.39/15.73 % TRYING [8] % 109.39/15.73 % (353035)Instruction limit reached! % 109.39/15.73 % (353035)------------------------------ % 109.39/15.73 % (353035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 109.39/15.73 % (353035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.39/15.73 % (353035)CaDiCaL version: 2.1.3 % 109.39/15.73 % (353035)Termination reason: Instruction limit % 109.39/15.73 % (353035)Termination phase: Finite model building constraint generation % 109.39/15.73 % (353035)Time elapsed: 0.401 s % 109.39/15.73 % (353035)Peak memory usage: 39 MB % 109.39/15.73 % (353035)Instructions burned: 922 (million) % 109.39/15.73 % TRYING [4] % 109.39/15.73 % (353041)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=268135048:i=6324_2984 on theBenchmark for (2984ds/6324Mi) % 109.39/15.73 % (353041)Cannot represent all propositional literals internally % 109.39/15.73 % (353041)Refutation not found, incomplete strategy % 109.39/15.73 % (353041)------------------------------ % 109.39/15.73 % (353041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.05/30.64 % (353041)CaDiCaL version: 2.1.3 % 215.05/30.64 % (353041)Termination reason: Refutation not found, incomplete strategy % 215.05/30.64 % (353041)Time elapsed: 0.329 s % 215.05/30.64 % (353041)Peak memory usage: 23 MB % 215.05/30.64 % (353041)Instructions burned: 693 (million) % 215.05/30.64 % (353041)------------------------------ % 215.05/30.64 % (353041)------------------------------ % 215.05/30.64 % (353043)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=108347079:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi) % 215.05/30.64 % (353039)Instruction limit reached! % 215.05/30.64 % (353039)------------------------------ % 215.05/30.64 % (353039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.05/30.64 % (353039)CaDiCaL version: 2.1.3 % 215.05/30.64 % (353039)Termination reason: Instruction limit % 215.05/30.64 % (353039)Termination phase: Saturation % 215.05/30.64 % (353039)Time elapsed: 0.768 s % 215.05/30.64 % (353039)Peak memory usage: 28 MB % 215.05/30.64 % (353039)Instructions burned: 1472 (million) % 215.05/30.64 % (353045)ott-2_1_sil=16000:newcnf=on:random_seed=2173623043:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi) % 215.05/30.64 % TRYING [3] % 215.05/30.64 % (353045)Instruction limit reached! % 215.05/30.64 % (353045)------------------------------ % 215.05/30.64 % (353045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.05/30.64 % (353045)CaDiCaL version: 2.1.3 % 215.05/30.64 % (353045)Termination reason: Instruction limit % 215.05/30.64 % (353045)Termination phase: Saturation % 215.05/30.64 % (353045)Time elapsed: 0.520 s % 215.05/30.64 % (353045)Peak memory usage: 19 MB % 215.05/30.64 % (353045)Instructions burned: 869 (million) % 215.05/30.64 % (353047)ott+10_1_sil=32000:tgt=ground:random_seed=2086124552:i=5114:av=off_2972 on theBenchmark for (2972ds/5114Mi) % 215.05/30.64 % (353043)Instruction limit reached! % 215.05/30.64 % (353043)------------------------------ % 215.05/30.64 % (353043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.05/30.64 % (353043)CaDiCaL version: 2.1.3 % 215.05/30.64 % (353043)Termination reason: Instruction limit % 215.05/30.64 % (353043)Termination phase: Finite model building preprocessing % 215.05/30.64 % (353043)Time elapsed: 1.068 s % 215.05/30.64 % (353043)Peak memory usage: 37 MB % 215.05/30.64 % (353043)Instructions burned: 2175 (million) % 215.05/30.64 % (353049)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=257755517:i=54282_2969 on theBenchmark for (2969ds/54282Mi) % 215.05/30.64 % TRYING [1] % 215.05/30.64 % TRYING [2] % 215.05/30.64 % TRYING [3] % 215.05/30.64 % (353037)Instruction limit reached! % 215.05/30.64 % (353037)------------------------------ % 215.05/30.64 % (353037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.05/30.64 % (353037)CaDiCaL version: 2.1.3 % 215.05/30.64 % (353037)Termination reason: Instruction limit % 215.05/30.64 % (353037)Termination phase: Saturation % 215.05/30.64 % (353037)Time elapsed: 3.118 s % 215.05/30.64 % (353037)Peak memory usage: 38 MB % 215.05/30.64 % (353037)Instructions burned: 5131 (million) % 215.05/30.64 % (353051)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3620143397:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi) % 215.05/30.64 % TRYING [4] % 215.05/30.64 % TRYING [5] % 215.05/30.64 % TRYING [4] % 215.05/30.64 % (353047)Instruction limit reached! % 215.05/30.64 % (353047)------------------------------ % 215.05/30.64 % (353047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.05/30.64 % (353047)CaDiCaL version: 2.1.3 % 215.05/30.64 % (353047)Termination reason: Instruction limit % 215.05/30.64 % (353047)Termination phase: Saturation % 215.05/30.64 % (353047)Time elapsed: 3.368 s % 215.05/30.64 % (353047)Peak memory usage: 40 MB % 215.05/30.64 % (353047)Instructions burned: 5116 (million) % 215.05/30.64 % (353053)dis+21_1_sil=32000:sas=cadical:random_seed=2392361821:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi) % 215.05/30.64 % (353051)Instruction limit reached! % 215.05/30.64 % (353051)------------------------------ % 215.05/30.64 % (353051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 215.05/30.64 % (353051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.65/40.75 % (353051)CaDiCaL version: 2.1.3 % 286.65/40.75 % (353051)Termination reason: Instruction limit % 286.65/40.75 % (353051)Termination phase: Saturation % 286.65/40.75 % (353051)Time elapsed: 2.165 s % 286.65/40.75 % (353051)Peak memory usage: 35 MB % 286.65/40.75 % (353051)Instructions burned: 3512 (million) % 286.65/40.75 % (353055)ott+11_1_sil=16000:gs=on:random_seed=134820820:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi) % 286.65/40.75 % (353055)Instruction limit reached! % 286.65/40.75 % (353055)------------------------------ % 286.65/40.75 % (353055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.65/40.75 % (353055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.65/40.75 % (353055)CaDiCaL version: 2.1.3 % 286.65/40.75 % (353055)Termination reason: Instruction limit % 286.65/40.75 % (353055)Termination phase: Saturation % 286.65/40.75 % (353055)Time elapsed: 1.464 s % 286.65/40.75 % (353055)Peak memory usage: 55 MB % 286.65/40.75 % (353055)Instructions burned: 2252 (million) % 286.65/40.75 % (353057)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4189115686:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi) % 286.65/40.75 % (353053)Instruction limit reached! % 286.65/40.75 % (353053)------------------------------ % 286.65/40.75 % (353053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.65/40.75 % (353053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.65/40.75 % (353053)CaDiCaL version: 2.1.3 % 286.65/40.75 % (353053)Termination reason: Instruction limit % 286.65/40.75 % (353053)Termination phase: Saturation % 286.65/40.75 % (353053)Time elapsed: 2.238 s % 286.65/40.75 % (353053)Peak memory usage: 38 MB % 286.65/40.75 % (353053)Instructions burned: 3774 (million) % 286.65/40.75 % (353059)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2448359720:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi) % 286.65/40.75 % TRYING [5] % 286.65/40.75 % (353031)Instruction limit reached! % 286.65/40.75 % (353031)------------------------------ % 286.65/40.75 % (353031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.65/40.75 % (353031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.65/40.75 % (353031)CaDiCaL version: 2.1.3 % 286.65/40.75 % (353031)Termination reason: Instruction limit % 286.65/40.75 % (353031)Termination phase: Finite model building SAT solving % 286.65/40.75 % (353031)Time elapsed: 9.379 s % 286.65/40.75 % (353031)Peak memory usage: 509 MB % 286.65/40.75 % (353031)Instructions burned: 22062 (million) % 286.65/40.75 % (353062)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3260286691:i=29340_2895 on theBenchmark for (2895ds/29340Mi) % 286.65/40.75 % (353059)Instruction limit reached! % 286.65/40.75 % (353059)------------------------------ % 286.65/40.75 % (353059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.65/40.75 % (353059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.65/40.75 % (353059)CaDiCaL version: 2.1.3 % 286.65/40.75 % (353059)Termination reason: Instruction limit % 286.65/40.75 % (353059)Termination phase: Saturation % 286.65/40.75 % (353059)Time elapsed: 2.428 s % 286.65/40.75 % (353059)Peak memory usage: 55 MB % 286.65/40.75 % (353059)Instructions burned: 4592 (million) % 286.65/40.75 % (353064)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1582899824:i=5211_2891 on theBenchmark for (2891ds/5211Mi) % 286.65/40.75 % TRYING [7] % 286.65/40.75 % (353064)Instruction limit reached! % 286.65/40.75 % (353064)------------------------------ % 286.65/40.75 % (353064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.65/40.75 % (353064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.65/40.75 % (353064)CaDiCaL version: 2.1.3 % 286.65/40.75 % (353064)Termination reason: Instruction limit % 286.65/40.75 % (353064)Termination phase: Saturation % 286.65/40.75 % (353064)Time elapsed: 2.584 s % 286.65/40.75 % (353064)Peak memory usage: 44 MB % 286.65/40.75 % (353064)Instructions burned: 5213 (million) % 286.65/40.75 % (353066)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2286639002:i=5497:nm=2_2865 on theBenchmark for (2865ds/5497Mi) % 286.65/40.75 % TRYING [17] % 286.65/40.75 % (353066)Instruction limit reached! % 286.65/40.75 % (353066)------------------------------ % 286.65/40.75 % (353066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 286.65/40.75 % (353066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (353066)CaDiCaL version: 2.1.3 % 300.15/42.63 % (353066)Termination reason: Instruction limit % 300.15/42.63 % (353066)Termination phase: Finite model building constraint generation % 300.15/42.63 % (353066)Time elapsed: 2.034 s % 300.15/42.63 % (353066)Peak memory usage: 336 MB % 300.15/42.63 % (353066)Instructions burned: 5500 (million) % 300.15/42.63 % (353068)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4257188680:fmbsr=2:i=46332_2844 on theBenchmark for (2844ds/46332Mi) % 300.15/42.63 % TRYING [15] % 300.15/42.63 % TRYING [6] % 300.15/42.63 % TRYING [6] % 300.15/42.63 % (352999)Instruction limit reached! % 300.15/42.63 % (352999)------------------------------ % 300.15/42.63 % (352999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.63 % (352999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (352999)CaDiCaL version: 2.1.3 % 300.15/42.63 % (352999)Termination reason: Instruction limit % 300.15/42.63 % (352999)Termination phase: Saturation % 300.15/42.63 % (352999)Time elapsed: 22.684 s % 300.15/42.63 % (352999)Peak memory usage: 526 MB % 300.15/42.63 % (352999)Instructions burned: 88028 (million) % 300.15/42.63 % (353070)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4256191793:i=14071_2771 on theBenchmark for (2771ds/14071Mi) % 300.15/42.63 % TRYING [12] % 300.15/42.63 % (353049)Instruction limit reached! % 300.15/42.63 % (353049)------------------------------ % 300.15/42.63 % (353049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.63 % (353049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (353049)CaDiCaL version: 2.1.3 % 300.15/42.63 % (353049)Termination reason: Instruction limit % 300.15/42.63 % (353049)Termination phase: Finite model building constraint generation % 300.15/42.63 % (353049)Time elapsed: 20.755 s % 300.15/42.63 % (353049)Peak memory usage: 1838 MB % 300.15/42.63 % (353049)Instructions burned: 54285 (million) % 300.15/42.63 % (353072)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3360102312:i=22565:add=on:rawr=on_2759 on theBenchmark for (2759ds/22565Mi) % 300.15/42.63 % (353062)Instruction limit reached! % 300.15/42.63 % (353062)------------------------------ % 300.15/42.63 % (353062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.63 % (353062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (353062)CaDiCaL version: 2.1.3 % 300.15/42.63 % (353062)Termination reason: Instruction limit % 300.15/42.63 % (353062)Termination phase: Saturation % 300.15/42.63 % (353062)Time elapsed: 14.554 s % 300.15/42.63 % (353062)Peak memory usage: 210 MB % 300.15/42.63 % (353062)Instructions burned: 29340 (million) % 300.15/42.63 % (353074)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1076789840:i=8173:av=off_2749 on theBenchmark for (2749ds/8173Mi) % 300.15/42.63 % (353070)Instruction limit reached! % 300.15/42.63 % (353070)------------------------------ % 300.15/42.63 % (353070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.63 % (353070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (353070)CaDiCaL version: 2.1.3 % 300.15/42.63 % (353070)Termination reason: Instruction limit % 300.15/42.63 % (353070)Termination phase: Finite model building constraint generation % 300.15/42.63 % (353070)Time elapsed: 2.726 s % 300.15/42.63 % (353070)Peak memory usage: 827 MB % 300.15/42.63 % (353070)Instructions burned: 14072 (million) % 300.15/42.63 % (353076)dis+10_16:1_sil=16000:random_seed=2167193738:i=9155:fsr=off_2744 on theBenchmark for (2744ds/9155Mi) % 300.15/42.63 % (353076)Instruction limit reached! % 300.15/42.63 % (353076)------------------------------ % 300.15/42.63 % (353076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.63 % (353076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (353076)CaDiCaL version: 2.1.3 % 300.15/42.63 % (353076)Termination reason: Instruction limit % 300.15/42.63 % (353076)Termination phase: Saturation % 300.15/42.63 % (353076)Time elapsed: 2.508 s % 300.15/42.63 % (353076)Peak memory usage: 76 MB % 300.15/42.63 % (353076)Instructions burned: 9156 (million) % 300.15/42.63 % (353078)ott-3_8_sil=64000:random_seed=3294990940:i=20139:bs=on_2718 on theBenchmark for (2718ds/20139Mi) % 300.15/42.63 % (353074)Instruction limit reached! % 300.15/42.63 % (353074)------------------------------ % 300.15/42.63 % (353074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.63 % (353074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.63 % (353074)CaDiCaL version: 2.1.3 % 300.15/42.63 % (353074) % 300.15/42.63 Terminated % 300.15/42.63 % Vampire exiting % 300.15/42.64 Terminated %------------------------------------------------------------------------------