%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV814-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.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:26:28 PM UTC 2026 % Result : Timeout 300.19s 42.63s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWV814-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.22 % Computer : n011.cluster.edu % 0.11/0.22 % Model : x86_64 x86_64 % 0.11/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.22 % Memory : 8046.5625MB % 0.11/0.22 % OS : Linux 6.8.0-71-generic % 0.11/0.22 % CPULimit : 300 % 0.11/0.22 % WCLimit : 300 % 0.11/0.22 % DateTime : Mon Sep 28 12:38:33 UTC 2026 % 0.11/0.22 % CPUTime : % 0.11/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.25 Running first-order model finding % 0.11/0.25 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 % 9.16/1.88 % (3362175)Will run a generic schedule for satisfiability detection. % 9.16/1.88 % (3362185)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2691682096:i=131_2999 on theBenchmark for (2999ds/131Mi) % 9.16/1.88 % (3362181)% WARNING: option uhcvi not known. % 9.16/1.88 % (3362180)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=185728516_2999 on theBenchmark for (2999ds/0Mi) % 9.16/1.88 % (3362181)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=842278061:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 9.16/1.88 % (3362183)dis+10_1_sil=32000:sp=arity:random_seed=2088137838:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 9.16/1.88 % (3362184)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1622222942:i=116_2999 on theBenchmark for (2999ds/116Mi) % 9.16/1.88 % (3362182)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2919100288:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 9.16/1.88 % (3362186)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=594936204:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 9.16/1.88 % (3362185)Instruction limit reached! % 9.16/1.88 % (3362185)------------------------------ % 9.16/1.88 % (3362185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.16/1.88 % (3362185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.16/1.88 % (3362185)CaDiCaL version: 2.1.3 % 9.16/1.88 % (3362185)Termination reason: Instruction limit % 9.16/1.88 % (3362185)Termination phase: Saturation % 9.16/1.88 % (3362185)Time elapsed: 0.045 s % 9.16/1.88 % (3362185)Peak memory usage: 13 MB % 9.16/1.88 % (3362185)Instructions burned: 131 (million) % 9.16/1.88 % (3362194)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=146644484:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 9.16/1.88 % (3362183)Instruction limit reached! % 9.16/1.88 % (3362183)------------------------------ % 9.16/1.88 % (3362183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.16/1.88 % (3362183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.16/1.88 % (3362183)CaDiCaL version: 2.1.3 % 9.16/1.88 % (3362183)Termination reason: Instruction limit % 9.16/1.88 % (3362183)Termination phase: Saturation % 9.16/1.88 % (3362183)Time elapsed: 0.065 s % 9.16/1.88 % (3362183)Peak memory usage: 12 MB % 9.16/1.88 % (3362183)Instructions burned: 103 (million) % 9.16/1.88 % (3362184)Instruction limit reached! % 9.16/1.88 % (3362184)------------------------------ % 9.16/1.88 % (3362184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.16/1.88 % (3362184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.16/1.88 % (3362184)CaDiCaL version: 2.1.3 % 9.16/1.88 % (3362184)Termination reason: Instruction limit % 9.16/1.88 % (3362184)Termination phase: Saturation % 9.16/1.88 % (3362184)Time elapsed: 0.074 s % 9.16/1.88 % (3362184)Peak memory usage: 13 MB % 9.16/1.88 % (3362184)Instructions burned: 117 (million) % 9.16/1.88 % (3362196)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1840470004:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 9.16/1.88 % (3362186)Instruction limit reached! % 9.16/1.88 % (3362186)------------------------------ % 9.16/1.88 % (3362186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.16/1.88 % (3362186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.16/1.88 % (3362186)CaDiCaL version: 2.1.3 % 9.16/1.88 % (3362186)Termination reason: Instruction limit % 9.16/1.88 % (3362186)Termination phase: Saturation % 9.16/1.88 % (3362186)Time elapsed: 0.088 s % 9.16/1.88 % (3362186)Peak memory usage: 13 MB % 9.16/1.88 % (3362186)Instructions burned: 159 (million) % 9.16/1.88 % (3362197)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=1245136704:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 9.16/1.88 % (3362199)ott-21_1_sil=16000:fs=off:random_seed=1907708113:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 9.16/1.88 % TRYING [1] % 9.16/1.88 % TRYING [2] % 9.16/1.88 % (3362196)Instruction limit reached! % 9.16/1.88 % (3362196)------------------------------ % 9.16/1.88 % (3362196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 9.16/1.88 % (3362196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.91/5.93 % (3362196)CaDiCaL version: 2.1.3 % 39.91/5.93 % (3362196)Termination reason: Instruction limit % 39.91/5.93 % (3362196)Termination phase: Saturation % 39.91/5.93 % (3362196)Time elapsed: 0.084 s % 39.91/5.93 % (3362196)Peak memory usage: 13 MB % 39.91/5.93 % (3362196)Instructions burned: 132 (million) % 39.91/5.93 % (3362199)Instruction limit reached! % 39.91/5.93 % (3362199)------------------------------ % 39.91/5.93 % (3362199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.91/5.93 % (3362199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.91/5.93 % (3362199)CaDiCaL version: 2.1.3 % 39.91/5.93 % (3362199)Termination reason: Instruction limit % 39.91/5.93 % (3362199)Termination phase: Saturation % 39.91/5.93 % (3362199)Time elapsed: 0.070 s % 39.91/5.93 % (3362199)Peak memory usage: 12 MB % 39.91/5.93 % (3362199)Instructions burned: 180 (million) % 39.91/5.93 % TRYING [1] % 39.91/5.93 % (3362202)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=467795950:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 39.91/5.93 % TRYING [3] % 39.91/5.93 % (3362203)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2796512553:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 39.91/5.93 % TRYING [2] % 39.91/5.93 % (3362194)Instruction limit reached! % 39.91/5.93 % (3362194)------------------------------ % 39.91/5.93 % (3362194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.91/5.93 % (3362194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.91/5.93 % (3362194)CaDiCaL version: 2.1.3 % 39.91/5.93 % (3362194)Termination reason: Instruction limit % 39.91/5.93 % (3362194)Termination phase: Finite model building constraint generation % 39.91/5.93 % (3362194)Time elapsed: 0.168 s % 39.91/5.93 % (3362194)Peak memory usage: 29 MB % 39.91/5.93 % (3362194)Instructions burned: 715 (million) % 39.91/5.93 % (3362206)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3067905723:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 39.91/5.93 % TRYING [3] % 39.91/5.93 % TRYING [1] % 39.91/5.93 % TRYING [2] % 39.91/5.93 % (3362203)Instruction limit reached! % 39.91/5.93 % (3362203)------------------------------ % 39.91/5.93 % (3362203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.91/5.93 % (3362203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.91/5.93 % (3362203)CaDiCaL version: 2.1.3 % 39.91/5.93 % (3362203)Termination reason: Instruction limit % 39.91/5.93 % (3362203)Termination phase: Finite model building SAT solving % 39.91/5.93 % (3362203)Time elapsed: 0.238 s % 39.91/5.93 % (3362203)Peak memory usage: 30 MB % 39.91/5.93 % (3362203)Instructions burned: 868 (million) % 39.91/5.93 % (3362208)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3280655206:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 39.91/5.93 % (3362202)Instruction limit reached! % 39.91/5.93 % (3362202)------------------------------ % 39.91/5.93 % (3362202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.91/5.93 % (3362202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.91/5.93 % (3362202)CaDiCaL version: 2.1.3 % 39.91/5.93 % (3362202)Termination reason: Instruction limit % 39.91/5.93 % (3362202)Termination phase: Saturation % 39.91/5.93 % (3362202)Time elapsed: 0.301 s % 39.91/5.93 % (3362202)Peak memory usage: 14 MB % 39.91/5.93 % (3362202)Instructions burned: 478 (million) % 39.91/5.93 % (3362197)Instruction limit reached! % 39.91/5.93 % (3362197)------------------------------ % 39.91/5.93 % (3362197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 39.91/5.93 % (3362197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.91/5.93 % (3362197)CaDiCaL version: 2.1.3 % 39.91/5.93 % (3362197)Termination reason: Instruction limit % 39.91/5.93 % (3362197)Termination phase: Saturation % 39.91/5.93 % (3362197)Time elapsed: 0.415 s % 39.91/5.93 % (3362197)Peak memory usage: 18 MB % 39.91/5.93 % (3362197)Instructions burned: 684 (million) % 39.91/5.93 % (3362210)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=2499891341: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) % 39.91/5.93 % (3362211)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2429487254:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 39.91/5.93 % (3362208)Instruction limit reached! % 39.91/5.93 % (3362208)------------------------------ % 39.91/5.93 % (3362208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.39/10.99 % (3362208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/10.99 % (3362208)CaDiCaL version: 2.1.3 % 75.39/10.99 % (3362208)Termination reason: Instruction limit % 75.39/10.99 % (3362208)Termination phase: Finite model building constraint generation % 75.39/10.99 % (3362208)Time elapsed: 0.259 s % 75.39/10.99 % (3362208)Peak memory usage: 80 MB % 75.39/10.99 % (3362208)Instructions burned: 893 (million) % 75.39/10.99 % (3362214)fmb+10_1_sil=64000:random_seed=1348420835:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 75.39/10.99 % TRYING [4] % 75.39/10.99 % TRYING [1] % 75.39/10.99 % TRYING [2] % 75.39/10.99 % (3362210)Instruction limit reached! % 75.39/10.99 % (3362210)------------------------------ % 75.39/10.99 % (3362210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.39/10.99 % (3362210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/10.99 % (3362210)CaDiCaL version: 2.1.3 % 75.39/10.99 % (3362210)Termination reason: Instruction limit % 75.39/10.99 % (3362210)Termination phase: Saturation % 75.39/10.99 % (3362210)Time elapsed: 0.421 s % 75.39/10.99 % (3362210)Peak memory usage: 19 MB % 75.39/10.99 % (3362210)Instructions burned: 693 (million) % 75.39/10.99 % (3362206)Instruction limit reached! % 75.39/10.99 % (3362206)------------------------------ % 75.39/10.99 % (3362206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.39/10.99 % (3362206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/10.99 % (3362206)CaDiCaL version: 2.1.3 % 75.39/10.99 % (3362206)Termination reason: Instruction limit % 75.39/10.99 % (3362206)Termination phase: Saturation % 75.39/10.99 % (3362206)Time elapsed: 0.713 s % 75.39/10.99 % (3362206)Peak memory usage: 22 MB % 75.39/10.99 % (3362206)Instructions burned: 1180 (million) % 75.39/10.99 % (3362216)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2597718141:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 75.39/10.99 % (3362217)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4051019549:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 75.39/10.99 % TRYING [3] % 75.39/10.99 % (3362211)Instruction limit reached! % 75.39/10.99 % (3362211)------------------------------ % 75.39/10.99 % (3362211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.39/10.99 % (3362211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/10.99 % (3362211)CaDiCaL version: 2.1.3 % 75.39/10.99 % (3362211)Termination reason: Instruction limit % 75.39/10.99 % (3362211)Termination phase: Saturation % 75.39/10.99 % (3362211)Time elapsed: 0.503 s % 75.39/10.99 % (3362211)Peak memory usage: 19 MB % 75.39/10.99 % (3362211)Instructions burned: 881 (million) % 75.39/10.99 % (3362220)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2753849446:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 75.39/10.99 % (3362216)Cannot represent all propositional literals internally % 75.39/10.99 % (3362216)Refutation not found, incomplete strategy % 75.39/10.99 % (3362216)------------------------------ % 75.39/10.99 % (3362216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.39/10.99 % (3362216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/10.99 % (3362216)CaDiCaL version: 2.1.3 % 75.39/10.99 % (3362216)Termination reason: Refutation not found, incomplete strategy % 75.39/10.99 % (3362216)Time elapsed: 0.186 s % 75.39/10.99 % (3362216)Peak memory usage: 17 MB % 75.39/10.99 % (3362216)Instructions burned: 376 (million) % 75.39/10.99 % (3362216)------------------------------ % 75.39/10.99 % (3362216)------------------------------ % 75.39/10.99 % TRYING [8] % 75.39/10.99 % (3362222)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=361354432:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 75.39/10.99 % (3362217)Instruction limit reached! % 75.39/10.99 % (3362217)------------------------------ % 75.39/10.99 % (3362217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 75.39/10.99 % (3362217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.39/10.99 % (3362217)CaDiCaL version: 2.1.3 % 75.39/10.99 % (3362217)Termination reason: Instruction limit % 75.39/10.99 % (3362217)Termination phase: Finite model building constraint generation % 75.39/10.99 % (3362217)Time elapsed: 0.373 s % 75.39/10.99 % (3362217)Peak memory usage: 50 MB % 75.39/10.99 % (3362217)Instructions burned: 923 (million) % 75.39/10.99 % (3362224)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3680114259:i=6324_2985 on theBenchmark for (2985ds/6324Mi) % 75.39/10.99 % (3362224)Cannot represent all propositional literals internally % 202.33/28.86 % (3362224)Refutation not found, incomplete strategy % 202.33/28.86 % (3362224)------------------------------ % 202.33/28.86 % (3362224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.86 % (3362224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.86 % (3362224)CaDiCaL version: 2.1.3 % 202.33/28.86 % (3362224)Termination reason: Refutation not found, incomplete strategy % 202.33/28.86 % (3362224)Time elapsed: 0.191 s % 202.33/28.86 % (3362224)Peak memory usage: 17 MB % 202.33/28.86 % (3362224)Instructions burned: 384 (million) % 202.33/28.86 % (3362224)------------------------------ % 202.33/28.86 % (3362224)------------------------------ % 202.33/28.86 % (3362226)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2919416805:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi) % 202.33/28.86 % TRYING [4] % 202.33/28.86 % (3362222)Instruction limit reached! % 202.33/28.86 % (3362222)------------------------------ % 202.33/28.86 % (3362222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.86 % (3362222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.86 % (3362222)CaDiCaL version: 2.1.3 % 202.33/28.86 % (3362222)Termination reason: Instruction limit % 202.33/28.86 % (3362222)Termination phase: Saturation % 202.33/28.86 % (3362222)Time elapsed: 0.871 s % 202.33/28.86 % (3362222)Peak memory usage: 32 MB % 202.33/28.86 % (3362222)Instructions burned: 1472 (million) % 202.33/28.86 % (3362228)ott-2_1_sil=16000:newcnf=on:random_seed=507371447:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi) % 202.33/28.86 % (3362226)Cannot represent all propositional literals internally % 202.33/28.86 % (3362226)Refutation not found, incomplete strategy % 202.33/28.86 % (3362226)------------------------------ % 202.33/28.86 % (3362226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.86 % (3362226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.86 % (3362226)CaDiCaL version: 2.1.3 % 202.33/28.86 % (3362226)Termination reason: Refutation not found, incomplete strategy % 202.33/28.86 % (3362226)Time elapsed: 0.682 s % 202.33/28.86 % (3362226)Peak memory usage: 26 MB % 202.33/28.86 % (3362226)Instructions burned: 1398 (million) % 202.33/28.86 % (3362226)------------------------------ % 202.33/28.86 % (3362226)------------------------------ % 202.33/28.86 % (3362230)ott+10_1_sil=32000:tgt=ground:random_seed=1561808395:i=5114:av=off_2976 on theBenchmark for (2976ds/5114Mi) % 202.33/28.86 % (3362228)Instruction limit reached! % 202.33/28.86 % (3362228)------------------------------ % 202.33/28.86 % (3362228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.86 % (3362228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.86 % (3362228)CaDiCaL version: 2.1.3 % 202.33/28.86 % (3362228)Termination reason: Instruction limit % 202.33/28.86 % (3362228)Termination phase: Saturation % 202.33/28.86 % (3362228)Time elapsed: 0.483 s % 202.33/28.86 % (3362228)Peak memory usage: 21 MB % 202.33/28.86 % (3362228)Instructions burned: 871 (million) % 202.33/28.86 % (3362232)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3260275477:i=54282_2974 on theBenchmark for (2974ds/54282Mi) % 202.33/28.86 % TRYING [1] % 202.33/28.86 % TRYING [2] % 202.33/28.86 % TRYING [3] % 202.33/28.86 % TRYING [5] % 202.33/28.86 % TRYING [4] % 202.33/28.86 % (3362220)Instruction limit reached! % 202.33/28.86 % (3362220)------------------------------ % 202.33/28.86 % (3362220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.86 % (3362220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.86 % (3362220)CaDiCaL version: 2.1.3 % 202.33/28.86 % (3362220)Termination reason: Instruction limit % 202.33/28.86 % (3362220)Termination phase: Saturation % 202.33/28.86 % (3362220)Time elapsed: 3.057 s % 202.33/28.86 % (3362220)Peak memory usage: 45 MB % 202.33/28.86 % (3362220)Instructions burned: 5132 (million) % 202.33/28.86 % (3362234)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3768331943:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi) % 202.33/28.86 % (3362230)Instruction limit reached! % 202.33/28.86 % (3362230)------------------------------ % 202.33/28.86 % (3362230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.33/28.86 % (3362230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.33/28.86 % (3362230)CaDiCaL version: 2.1.3 % 202.33/28.86 % (3362230)Termination reason: Instruction limit % 202.33/28.86 % (3362230)Termination phase: Saturation % 202.33/28.86 % (3362230)Time elapsed: 3.315 s % 202.33/28.86 % (3362230)Peak memory usage: 54 MB % 278.71/39.61 % (3362230)Instructions burned: 5114 (million) % 278.71/39.61 % TRYING [5] % 278.71/39.61 % (3362236)dis+21_1_sil=32000:sas=cadical:random_seed=3552388013:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi) % 278.71/39.61 % (3362214)Instruction limit reached! % 278.71/39.61 % (3362214)------------------------------ % 278.71/39.61 % (3362214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.71/39.61 % (3362214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.71/39.61 % (3362214)CaDiCaL version: 2.1.3 % 278.71/39.61 % (3362214)Termination reason: Instruction limit % 278.71/39.61 % (3362214)Termination phase: Finite model building SAT solving % 278.71/39.61 % (3362214)Time elapsed: 5.176 s % 278.71/39.61 % (3362214)Peak memory usage: 322 MB % 278.71/39.61 % (3362214)Instructions burned: 22062 (million) % 278.71/39.61 % (3362238)ott+11_1_sil=16000:gs=on:random_seed=1246275804:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2940 on theBenchmark for (2940ds/2251Mi) % 278.71/39.61 % (3362234)Instruction limit reached! % 278.71/39.61 % (3362234)------------------------------ % 278.71/39.61 % (3362234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.71/39.61 % (3362234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.71/39.61 % (3362234)CaDiCaL version: 2.1.3 % 278.71/39.61 % (3362234)Termination reason: Instruction limit % 278.71/39.61 % (3362234)Termination phase: Saturation % 278.71/39.61 % (3362234)Time elapsed: 2.151 s % 278.71/39.61 % (3362234)Peak memory usage: 39 MB % 278.71/39.61 % (3362234)Instructions burned: 3514 (million) % 278.71/39.61 % (3362240)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4035718689:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi) % 278.71/39.61 % (3362238)Instruction limit reached! % 278.71/39.61 % (3362238)------------------------------ % 278.71/39.61 % (3362238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.71/39.61 % (3362238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.71/39.61 % (3362238)CaDiCaL version: 2.1.3 % 278.71/39.61 % (3362238)Termination reason: Instruction limit % 278.71/39.61 % (3362238)Termination phase: Saturation % 278.71/39.61 % (3362238)Time elapsed: 0.745 s % 278.71/39.61 % (3362238)Peak memory usage: 27 MB % 278.71/39.61 % (3362238)Instructions burned: 2253 (million) % 278.71/39.61 % (3362242)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=784217933:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2932 on theBenchmark for (2932ds/4591Mi) % 278.71/39.61 % (3362242)Instruction limit reached! % 278.71/39.61 % (3362242)------------------------------ % 278.71/39.61 % (3362242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.71/39.61 % (3362242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.71/39.61 % (3362242)CaDiCaL version: 2.1.3 % 278.71/39.61 % (3362242)Termination reason: Instruction limit % 278.71/39.61 % (3362242)Termination phase: Saturation % 278.71/39.61 % (3362242)Time elapsed: 1.073 s % 278.71/39.61 % (3362242)Peak memory usage: 42 MB % 278.71/39.61 % (3362242)Instructions burned: 4596 (million) % 278.71/39.61 % (3362244)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3098634391:i=29340_2921 on theBenchmark for (2921ds/29340Mi) % 278.71/39.61 % (3362236)Instruction limit reached! % 278.71/39.61 % (3362236)------------------------------ % 278.71/39.61 % (3362236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.71/39.61 % (3362236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.71/39.61 % (3362236)CaDiCaL version: 2.1.3 % 278.71/39.61 % (3362236)Termination reason: Instruction limit % 278.71/39.61 % (3362236)Termination phase: Saturation % 278.71/39.61 % (3362236)Time elapsed: 2.255 s % 278.71/39.61 % (3362236)Peak memory usage: 43 MB % 278.71/39.61 % (3362236)Instructions burned: 3774 (million) % 278.71/39.61 % (3362246)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3982778079:i=5211_2920 on theBenchmark for (2920ds/5211Mi) % 278.71/39.61 % TRYING [7] % 278.71/39.61 % (3362246)Instruction limit reached! % 278.71/39.61 % (3362246)------------------------------ % 278.71/39.61 % (3362246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 278.71/39.61 % (3362246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.71/39.61 % (3362246)CaDiCaL version: 2.1.3 % 278.71/39.61 % (3362246)Termination reason: Instruction limit % 278.71/39.61 % (3362246)Termination phase: Saturation % 278.71/39.61 % (3362246)Time elapsed: 2.756 s % 278.71/39.61 % (3362246)Peak memory usage: 48 MB % 278.71/39.61 % (3362246)Instructions burned: 5211 (million) % 300.19/42.63 % (3362248)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2383249171:i=5497:nm=2_2892 on theBenchmark for (2892ds/5497Mi) % 300.19/42.63 % TRYING [17] % 300.19/42.63 % TRYING [6] % 300.19/42.63 % (3362248)Instruction limit reached! % 300.19/42.63 % (3362248)------------------------------ % 300.19/42.63 % (3362248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (3362248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (3362248)CaDiCaL version: 2.1.3 % 300.19/42.63 % (3362248)Termination reason: Instruction limit % 300.19/42.63 % (3362248)Termination phase: Finite model building constraint generation % 300.19/42.63 % (3362248)Time elapsed: 2.003 s % 300.19/42.63 % (3362248)Peak memory usage: 346 MB % 300.19/42.63 % (3362248)Instructions burned: 5497 (million) % 300.19/42.63 % (3362250)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2643598379:fmbsr=2:i=46332_2871 on theBenchmark for (2871ds/46332Mi) % 300.19/42.63 % TRYING [15] % 300.19/42.63 % TRYING [6] % 300.19/42.63 % (3362244)Instruction limit reached! % 300.19/42.63 % (3362244)------------------------------ % 300.19/42.63 % (3362244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (3362244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (3362244)CaDiCaL version: 2.1.3 % 300.19/42.63 % (3362244)Termination reason: Instruction limit % 300.19/42.63 % (3362244)Termination phase: Saturation % 300.19/42.63 % (3362244)Time elapsed: 8.178 s % 300.19/42.63 % (3362244)Peak memory usage: 250 MB % 300.19/42.63 % (3362244)Instructions burned: 29341 (million) % 300.19/42.63 % (3362253)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2902636959:i=14071_2839 on theBenchmark for (2839ds/14071Mi) % 300.19/42.63 % TRYING [12] % 300.19/42.63 % (3362253)Instruction limit reached! % 300.19/42.63 % (3362253)------------------------------ % 300.19/42.63 % (3362253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (3362253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (3362253)CaDiCaL version: 2.1.3 % 300.19/42.63 % (3362253)Termination reason: Instruction limit % 300.19/42.63 % (3362253)Termination phase: Finite model building constraint generation % 300.19/42.63 % (3362253)Time elapsed: 2.876 s % 300.19/42.63 % (3362253)Peak memory usage: 900 MB % 300.19/42.63 % (3362253)Instructions burned: 14079 (million) % 300.19/42.63 % (3362255)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4277776092:i=22565:add=on:rawr=on_2809 on theBenchmark for (2809ds/22565Mi) % 300.19/42.63 % (3362232)Instruction limit reached! % 300.19/42.63 % (3362232)------------------------------ % 300.19/42.63 % (3362232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (3362232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (3362232)CaDiCaL version: 2.1.3 % 300.19/42.63 % (3362232)Termination reason: Instruction limit % 300.19/42.63 % (3362232)Termination phase: Finite model building constraint generation % 300.19/42.63 % (3362232)Time elapsed: 20.306 s % 300.19/42.63 % (3362232)Peak memory usage: 1861 MB % 300.19/42.63 % (3362232)Instructions burned: 54284 (million) % 300.19/42.63 % (3362257)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=52095996:i=8173:av=off_2768 on theBenchmark for (2768ds/8173Mi) % 300.19/42.63 % (3362255)Instruction limit reached! % 300.19/42.63 % (3362255)------------------------------ % 300.19/42.63 % (3362255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (3362255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (3362255)CaDiCaL version: 2.1.3 % 300.19/42.63 % (3362255)Termination reason: Instruction limit % 300.19/42.63 % (3362255)Termination phase: Saturation % 300.19/42.63 % (3362255)Time elapsed: 7.955 s % 300.19/42.63 % (3362255)Peak memory usage: 235 MB % 300.19/42.63 % (3362255)Instructions burned: 22566 (million) % 300.19/42.63 % (3362259)dis+10_16:1_sil=16000:random_seed=527263015:i=9155:fsr=off_2730 on theBenchmark for (2730ds/9155Mi) % 300.19/42.63 % (3362257)Instruction limit reached! % 300.19/42.63 % (3362257)------------------------------ % 300.19/42.63 % (3362257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.19/42.63 % (3362257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.19/42.63 % (3362257)CaDiCaL version: 2.1.3 % 300.19/42.63 % (3362257)Termination reason: Instruction limit % 300.19/42.63 % (3362257)Termination phase: Saturation % 300.19/42.63 % (3362257)Time elapsed: 5.412 s % 300.19/42.63 % (3362257)Peak % 300.19/42.64 Terminated % 300.19/42.64 % Vampire exiting %------------------------------------------------------------------------------