%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX137_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n019.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:57 PM UTC 2026 % Result : Timeout 300.01s 43.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX137_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.19 % Computer : n019.cluster.edu % 0.12/0.19 % Model : x86_64 x86_64 % 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.19 % Memory : 8046.5625MB % 0.12/0.19 % OS : Linux 6.8.0-71-generic % 0.12/0.19 % CPULimit : 300 % 0.12/0.19 % WCLimit : 300 % 0.12/0.19 % DateTime : Mon Sep 28 15:03:18 UTC 2026 % 0.12/0.19 % CPUTime : % 0.12/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.23 Running first-order theorem proving % 0.12/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.79/1.64 % (4070594)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 4.79/1.64 % (4070749)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=283915928:s2a=on:i=7:rtra=on:inst=on_2998 on theBenchmark for (2998ds/7Mi) % 4.79/1.64 % (4070749)Instruction limit reached! % 4.79/1.64 % (4070749)------------------------------ % 4.79/1.64 % (4070749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.79/1.64 % (4070749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.79/1.64 % (4070749)CaDiCaL version: 2.1.3 % 4.79/1.64 % (4070749)Termination reason: Instruction limit % 4.79/1.64 % (4070749)Termination phase: Property scanning % 4.79/1.64 % (4070749)Time elapsed: 0.003 s % 4.79/1.64 % (4070749)Peak memory usage: 85 MB % 4.79/1.64 % (4070749)Instructions burned: 8 (million) % 4.79/1.64 % (4070746)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1128546093:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2998 on theBenchmark for (2998ds/12Mi) % 4.79/1.64 % (4070746)Instruction limit reached! % 4.79/1.64 % (4070746)------------------------------ % 4.79/1.64 % (4070746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.79/1.64 % (4070746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.79/1.64 % (4070746)CaDiCaL version: 2.1.3 % 4.79/1.64 % (4070746)Termination reason: Instruction limit % 4.79/1.64 % (4070746)Termination phase: Property scanning % 4.79/1.64 % (4070746)Time elapsed: 0.011 s % 4.79/1.64 % (4070746)Peak memory usage: 85 MB % 4.79/1.64 % (4070746)Instructions burned: 13 (million) % 4.79/1.64 % (4070750)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3451677350:i=4:rtra=on_2998 on theBenchmark for (2998ds/4Mi) % 4.79/1.64 % (4070750)Instruction limit reached! % 4.79/1.64 % (4070750)------------------------------ % 4.79/1.64 % (4070750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.79/1.64 % (4070750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.79/1.64 % (4070750)CaDiCaL version: 2.1.3 % 4.79/1.64 % (4070750)Termination reason: Instruction limit % 4.79/1.64 % (4070750)Termination phase: Property scanning % 4.79/1.64 % (4070750)Time elapsed: 0.003 s % 4.79/1.64 % (4070750)Peak memory usage: 85 MB % 4.79/1.64 % (4070750)Instructions burned: 5 (million) % 4.79/1.64 % (4070748)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=425923434:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/201Mi) % 4.79/1.64 % (4070751)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2314277608:i=46:rtra=on_2998 on theBenchmark for (2998ds/46Mi) % 4.79/1.64 % (4070752)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2170501073:i=33:rtra=on_2998 on theBenchmark for (2998ds/33Mi) % 4.79/1.64 % (4070747)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1135383518:i=307:kws=precedence:nm=0:rtra=on_2998 on theBenchmark for (2998ds/307Mi) % 4.79/1.64 % (4070752)Instruction limit reached! % 4.79/1.64 % (4070752)------------------------------ % 4.79/1.64 % (4070752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.79/1.64 % (4070752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.79/1.64 % (4070752)CaDiCaL version: 2.1.3 % 4.79/1.64 % (4070752)Termination reason: Instruction limit % 4.79/1.64 % (4070752)Termination phase: Property scanning % 4.79/1.64 % (4070752)Time elapsed: 0.026 s % 4.79/1.64 % (4070752)Peak memory usage: 85 MB % 4.79/1.64 % (4070752)Instructions burned: 33 (million) % 4.79/1.64 % (4070751)Instruction limit reached! % 4.79/1.64 % (4070751)------------------------------ % 4.79/1.64 % (4070751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.79/1.64 % (4070751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.79/1.64 % (4070751)CaDiCaL version: 2.1.3 % 4.79/1.64 % (4070751)Termination reason: Instruction limit % 4.79/1.64 % (4070751)Termination phase: Property scanning % 4.79/1.64 % (4070751)Time elapsed: 0.035 s % 4.79/1.64 % (4070751)Peak memory usage: 85 MB % 4.79/1.64 % (4070751)Instructions burned: 46 (million) % 4.79/1.64 % (4070756)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=988735409:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2996 on theBenchmark for (2996ds/14Mi) % 4.79/1.64 % (4070756)Instruction limit reached! % 4.79/1.64 % (4070756)------------------------------ % 6.55/1.89 % (4070756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.89 % (4070756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.89 % (4070756)CaDiCaL version: 2.1.3 % 6.55/1.89 % (4070756)Termination reason: Instruction limit % 6.55/1.89 % (4070756)Termination phase: Property scanning % 6.55/1.89 % (4070756)Time elapsed: 0.006 s % 6.55/1.89 % (4070756)Peak memory usage: 85 MB % 6.55/1.89 % (4070756)Instructions burned: 14 (million) % 6.55/1.89 % (4070748)Instruction limit reached! % 6.55/1.89 % (4070748)------------------------------ % 6.55/1.89 % (4070748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.89 % (4070748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.89 % (4070748)CaDiCaL version: 2.1.3 % 6.55/1.89 % (4070748)Termination reason: Instruction limit % 6.55/1.89 % (4070748)Termination phase: Saturation % 6.55/1.89 % (4070748)Time elapsed: 0.183 s % 6.55/1.89 % (4070748)Peak memory usage: 111 MB % 6.55/1.89 % (4070748)Instructions burned: 202 (million) % 6.55/1.89 % (4070758)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3485891753:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/29Mi) % 6.55/1.90 % (4070760)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=114559073:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi) % 6.55/1.90 % (4070758)Instruction limit reached! % 6.55/1.90 % (4070758)------------------------------ % 6.55/1.90 % (4070758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.90 % (4070758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.90 % (4070758)CaDiCaL version: 2.1.3 % 6.55/1.90 % (4070758)Termination reason: Instruction limit % 6.55/1.90 % (4070758)Termination phase: Property scanning % 6.55/1.90 % (4070758)Time elapsed: 0.012 s % 6.55/1.90 % (4070758)Peak memory usage: 85 MB % 6.55/1.90 % (4070758)Instructions burned: 31 (million) % 6.55/1.90 % (4070760)Instruction limit reached! % 6.55/1.90 % (4070760)------------------------------ % 6.55/1.90 % (4070760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.90 % (4070760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.90 % (4070760)CaDiCaL version: 2.1.3 % 6.55/1.90 % (4070760)Termination reason: Instruction limit % 6.55/1.90 % (4070760)Termination phase: Property scanning % 6.55/1.90 % (4070760)Time elapsed: 0.013 s % 6.55/1.90 % (4070760)Peak memory usage: 85 MB % 6.55/1.90 % (4070760)Instructions burned: 16 (million) % 6.55/1.90 % (4070765)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2134800529:i=24:canc=force:rtra=on_2995 on theBenchmark for (2995ds/24Mi) % 6.55/1.90 % (4070765)Instruction limit reached! % 6.55/1.90 % (4070765)------------------------------ % 6.55/1.90 % (4070765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.90 % (4070765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.90 % (4070765)CaDiCaL version: 2.1.3 % 6.55/1.90 % (4070765)Termination reason: Instruction limit % 6.55/1.90 % (4070765)Termination phase: Property scanning % 6.55/1.90 % (4070765)Time elapsed: 0.011 s % 6.55/1.90 % (4070765)Peak memory usage: 85 MB % 6.55/1.90 % (4070765)Instructions burned: 27 (million) % 6.55/1.90 % (4070747)Instruction limit reached! % 6.55/1.90 % (4070747)------------------------------ % 6.55/1.90 % (4070747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.90 % (4070747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.55/1.90 % (4070747)CaDiCaL version: 2.1.3 % 6.55/1.90 % (4070747)Termination reason: Instruction limit % 6.55/1.90 % (4070747)Termination phase: Saturation % 6.55/1.90 % (4070747)Time elapsed: 0.257 s % 6.55/1.90 % (4070747)Peak memory usage: 112 MB % 6.55/1.90 % (4070747)Instructions burned: 308 (million) % 6.55/1.90 % (4070766)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3937145538:i=27:canc=cautious:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/27Mi) % 6.55/1.90 % (4070766)Instruction limit reached! % 6.55/1.90 % (4070766)------------------------------ % 6.55/1.90 % (4070766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.55/1.90 % (4070766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.10 % (4070766)CaDiCaL version: 2.1.3 % 8.95/2.10 % (4070766)Termination reason: Instruction limit % 8.95/2.10 % (4070766)Termination phase: Property scanning % 8.95/2.10 % (4070766)Time elapsed: 0.022 s % 8.95/2.10 % (4070766)Peak memory usage: 85 MB % 8.95/2.10 % (4070766)Instructions burned: 28 (million) % 8.95/2.10 % (4070769)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2157497749:i=85:gtgl=4:rtra=on:gtg=exists_sym_2994 on theBenchmark for (2994ds/85Mi) % 8.95/2.10 % (4070769)Instruction limit reached! % 8.95/2.10 % (4070769)------------------------------ % 8.95/2.10 % (4070769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.10 % (4070769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.10 % (4070769)CaDiCaL version: 2.1.3 % 8.95/2.10 % (4070769)Termination reason: Instruction limit % 8.95/2.10 % (4070769)Termination phase: Property scanning % 8.95/2.10 % (4070769)Time elapsed: 0.035 s % 8.95/2.10 % (4070769)Peak memory usage: 85 MB % 8.95/2.10 % (4070769)Instructions burned: 87 (million) % 8.95/2.10 % (4070775)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1450116919:i=181:rtra=on:ss=axioms:ev=cautious_2993 on theBenchmark for (2993ds/181Mi) % 8.95/2.10 % (4070775)Refutation not found, incomplete strategy % 8.95/2.10 % (4070775)------------------------------ % 8.95/2.10 % (4070775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.10 % (4070775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.10 % (4070775)CaDiCaL version: 2.1.3 % 8.95/2.10 % (4070775)Termination reason: Refutation not found, incomplete strategy % 8.95/2.10 % (4070775)Time elapsed: 0.016 s % 8.95/2.10 % (4070775)Peak memory usage: 87 MB % 8.95/2.10 % (4070775)Instructions burned: 40 (million) % 8.95/2.10 % (4070774)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1458893459:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi) % 8.95/2.10 % (4070774)Instruction limit reached! % 8.95/2.10 % (4070774)------------------------------ % 8.95/2.10 % (4070774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.10 % (4070774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.10 % (4070774)CaDiCaL version: 2.1.3 % 8.95/2.10 % (4070774)Termination reason: Instruction limit % 8.95/2.10 % (4070774)Termination phase: shuffling % 8.95/2.10 % (4070774)Time elapsed: 0.002 s % 8.95/2.10 % (4070774)Peak memory usage: 85 MB % 8.95/2.10 % (4070774)Instructions burned: 3 (million) % 8.95/2.10 % (4070777)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1299891186:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi) % 8.95/2.10 % (4070779)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2966003019:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi) % 8.95/2.10 % (4070777)Instruction limit reached! % 8.95/2.10 % (4070777)------------------------------ % 8.95/2.10 % (4070777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.10 % (4070777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.10 % (4070777)CaDiCaL version: 2.1.3 % 8.95/2.10 % (4070777)Termination reason: Instruction limit % 8.95/2.10 % (4070777)Termination phase: shuffling % 8.95/2.10 % (4070777)Time elapsed: 0.004 s % 8.95/2.10 % (4070777)Peak memory usage: 84 MB % 8.95/2.10 % (4070777)Instructions burned: 5 (million) % 8.95/2.10 % (4070782)lrs+10_1_thi=all:si=on:fd=off:random_seed=3709095028:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi) % 8.95/2.10 % (4070779)Instruction limit reached! % 8.95/2.10 % (4070779)------------------------------ % 8.95/2.10 % (4070779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.95/2.10 % (4070779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.95/2.10 % (4070779)CaDiCaL version: 2.1.3 % 8.95/2.10 % (4070779)Termination reason: Instruction limit % 8.95/2.10 % (4070779)Termination phase: Property scanning % 8.95/2.10 % (4070779)Time elapsed: 0.051 s % 8.95/2.10 % (4070779)Peak memory usage: 85 MB % 8.95/2.10 % (4070779)Instructions burned: 66 (million) % 8.95/2.10 % (4070782)Instruction limit reached! % 8.95/2.10 % (4070782)------------------------------ % 8.95/2.10 % (4070782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.39/2.42 % (4070782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.39/2.42 % (4070782)CaDiCaL version: 2.1.3 % 10.39/2.42 % (4070782)Termination reason: Instruction limit % 10.39/2.42 % (4070782)Termination phase: Property scanning % 10.39/2.42 % (4070782)Time elapsed: 0.041 s % 10.39/2.42 % (4070782)Peak memory usage: 85 MB % 10.39/2.42 % (4070782)Instructions burned: 53 (million) % 10.39/2.42 % (4070787)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=4252168018:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 10.39/2.42 % (4070787)Instruction limit reached! % 10.39/2.42 % (4070787)------------------------------ % 10.39/2.42 % (4070787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.39/2.42 % (4070787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.39/2.42 % (4070787)CaDiCaL version: 2.1.3 % 10.39/2.42 % (4070787)Termination reason: Instruction limit % 10.39/2.42 % (4070787)Termination phase: Property scanning % 10.39/2.42 % (4070787)Time elapsed: 0.007 s % 10.39/2.42 % (4070787)Peak memory usage: 85 MB % 10.39/2.42 % (4070787)Instructions burned: 8 (million) % 10.39/2.42 % (4070791)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1701651816:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 10.39/2.42 % (4070775)------------------------------ % 10.39/2.42 % (4070775)------------------------------ % 10.39/2.42 % (4070791)Instruction limit reached! % 10.39/2.42 % (4070791)------------------------------ % 10.39/2.42 % (4070791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.39/2.42 % (4070791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.39/2.42 % (4070791)CaDiCaL version: 2.1.3 % 10.39/2.42 % (4070791)Termination reason: Instruction limit % 10.39/2.42 % (4070791)Termination phase: shuffling % 10.39/2.42 % (4070791)Time elapsed: 0.002 s % 10.39/2.42 % (4070791)Peak memory usage: 84 MB % 10.39/2.42 % (4070791)Instructions burned: 3 (million) % 10.39/2.42 % (4070795)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3144047:i=2:doe=on:canc=force:asg=cautious:rtra=on_2991 on theBenchmark for (2991ds/2Mi) % 10.39/2.42 % (4070795)Instruction limit reached! % 10.39/2.42 % (4070795)------------------------------ % 10.39/2.42 % (4070795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.39/2.42 % (4070795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.39/2.42 % (4070795)CaDiCaL version: 2.1.3 % 10.39/2.42 % (4070795)Termination reason: Instruction limit % 10.39/2.42 % (4070795)Termination phase: shuffling % 10.39/2.42 % (4070795)Time elapsed: 0.001 s % 10.39/2.42 % (4070795)Peak memory usage: 85 MB % 10.39/2.42 % (4070795)Instructions burned: 2 (million) % 10.39/2.42 % (4070798)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2761979791:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 10.39/2.42 % (4070801)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=776874920:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi) % 10.39/2.42 % (4070801)Instruction limit reached! % 10.39/2.42 % (4070801)------------------------------ % 10.39/2.42 % (4070801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.39/2.42 % (4070801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.39/2.42 % (4070801)CaDiCaL version: 2.1.3 % 10.39/2.42 % (4070801)Termination reason: Instruction limit % 10.39/2.42 % (4070801)Termination phase: Property scanning % 10.39/2.42 % (4070801)Time elapsed: 0.011 s % 10.39/2.42 % (4070801)Peak memory usage: 85 MB % 10.39/2.42 % (4070801)Instructions burned: 26 (million) % 10.39/2.42 % (4070800)dis+10_1_si=on:random_seed=1233635217:i=10:ep=R:rtra=on_2990 on theBenchmark for (2990ds/10Mi) % 10.39/2.42 % (4070800)Instruction limit reached! % 10.39/2.42 % (4070800)------------------------------ % 10.39/2.42 % (4070800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.39/2.42 % (4070800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.39/2.42 % (4070800)CaDiCaL version: 2.1.3 % 10.39/2.42 % (4070800)Termination reason: Instruction limit % 10.39/2.42 % (4070800)Termination phase: Property scanning % 10.39/2.42 % (4070800)Time elapsed: 0.008 s % 10.39/2.42 % (4070800)Peak memory usage: 85 MB % 10.39/2.42 % (4070800)Instructions burned: 10 (million) % 10.39/2.42 % (4070798)Instruction limit reached! % 10.39/2.42 % (4070798)------------------------------ % 10.39/2.42 % (4070798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.12/2.79 % (4070798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.12/2.79 % (4070798)CaDiCaL version: 2.1.3 % 12.12/2.79 % (4070798)Termination reason: Instruction limit % 12.12/2.79 % (4070798)Termination phase: Saturation % 12.12/2.79 % (4070798)Time elapsed: 0.127 s % 12.12/2.79 % (4070798)Peak memory usage: 112 MB % 12.12/2.79 % (4070798)Instructions burned: 128 (million) % 12.12/2.79 % (4070803)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2608612017:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi) % 12.12/2.79 % (4070806)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4176930888:i=2:fsr=off:rtra=on:inst=on_2989 on theBenchmark for (2989ds/2Mi) % 12.12/2.79 % (4070806)Instruction limit reached! % 12.12/2.79 % (4070806)------------------------------ % 12.12/2.79 % (4070806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.12/2.79 % (4070806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.12/2.79 % (4070806)CaDiCaL version: 2.1.3 % 12.12/2.79 % (4070806)Termination reason: Instruction limit % 12.12/2.79 % (4070806)Termination phase: shuffling % 12.12/2.79 % (4070806)Time elapsed: 0.001 s % 12.12/2.79 % (4070806)Peak memory usage: 85 MB % 12.12/2.79 % (4070806)Instructions burned: 2 (million) % 12.12/2.79 % (4070803)Instruction limit reached! % 12.12/2.79 % (4070803)------------------------------ % 12.12/2.79 % (4070803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.12/2.79 % (4070803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.12/2.79 % (4070803)CaDiCaL version: 2.1.3 % 12.12/2.79 % (4070803)Termination reason: Instruction limit % 12.12/2.79 % (4070803)Termination phase: Property scanning % 12.12/2.79 % (4070803)Time elapsed: 0.027 s % 12.12/2.79 % (4070803)Peak memory usage: 85 MB % 12.12/2.79 % (4070803)Instructions burned: 35 (million) % 12.12/2.79 % (4070809)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=779721139:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi) % 12.12/2.79 % (4070807)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4211767260:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi) % 12.12/2.79 % (4070807)Instruction limit reached! % 12.12/2.79 % (4070807)------------------------------ % 12.12/2.79 % (4070807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.12/2.79 % (4070807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.12/2.79 % (4070807)CaDiCaL version: 2.1.3 % 12.12/2.79 % (4070807)Termination reason: Instruction limit % 12.12/2.79 % (4070807)Termination phase: Property scanning % 12.12/2.79 % (4070807)Time elapsed: 0.006 s % 12.12/2.79 % (4070807)Peak memory usage: 85 MB % 12.12/2.79 % (4070807)Instructions burned: 8 (million) % 12.12/2.79 % (4070812)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4222760249:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi) % 12.12/2.79 % (4070812)Instruction limit reached! % 12.12/2.79 % (4070812)------------------------------ % 12.12/2.79 % (4070812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.12/2.79 % (4070812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.12/2.79 % (4070812)CaDiCaL version: 2.1.3 % 12.12/2.79 % (4070812)Termination reason: Instruction limit % 12.12/2.79 % (4070812)Termination phase: Property scanning % 12.12/2.79 % (4070812)Time elapsed: 0.006 s % 12.12/2.79 % (4070812)Peak memory usage: 85 MB % 12.12/2.79 % (4070812)Instructions burned: 15 (million) % 12.12/2.79 % (4070814)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2986371901:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi) % 12.12/2.79 % (4070814)Instruction limit reached! % 12.12/2.79 % (4070814)------------------------------ % 12.12/2.79 % (4070814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.12/2.79 % (4070814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.12/2.79 % (4070814)CaDiCaL version: 2.1.3 % 12.12/2.79 % (4070814)Termination reason: Instruction limit % 12.12/2.79 % (4070814)Termination phase: Property scanning % 12.12/2.79 % (4070814)Time elapsed: 0.005 s % 15.85/3.20 % (4070814)Peak memory usage: 85 MB % 15.85/3.20 % (4070814)Instructions burned: 12 (million) % 15.85/3.20 % (4070813)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=731455950:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi) % 15.85/3.20 % (4070809)Refutation not found, incomplete strategy % 15.85/3.20 % (4070809)------------------------------ % 15.85/3.20 % (4070809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.85/3.20 % (4070809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.85/3.20 % (4070809)CaDiCaL version: 2.1.3 % 15.85/3.20 % (4070809)Termination reason: Refutation not found, incomplete strategy % 15.85/3.20 % (4070809)Time elapsed: 0.121 s % 15.85/3.20 % (4070809)Peak memory usage: 89 MB % 15.85/3.20 % (4070809)Instructions burned: 161 (million) % 15.85/3.20 % (4070817)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1403277182:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi) % 15.85/3.20 % (4070813)Refutation not found, incomplete strategy % 15.85/3.20 % (4070813)------------------------------ % 15.85/3.20 % (4070813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.85/3.20 % (4070813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.85/3.20 % (4070813)CaDiCaL version: 2.1.3 % 15.85/3.20 % (4070813)Termination reason: Refutation not found, incomplete strategy % 15.85/3.20 % (4070813)Time elapsed: 0.086 s % 15.85/3.20 % (4070813)Peak memory usage: 111 MB % 15.85/3.20 % (4070813)Instructions burned: 72 (million) % 15.85/3.20 % (4070818)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=2699480385:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi) % 15.85/3.20 % (4070817)Instruction limit reached! % 15.85/3.20 % (4070817)------------------------------ % 15.85/3.20 % (4070817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.85/3.20 % (4070817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.85/3.20 % (4070817)CaDiCaL version: 2.1.3 % 15.85/3.20 % (4070817)Termination reason: Instruction limit % 15.85/3.20 % (4070817)Termination phase: Property scanning % 15.85/3.20 % (4070817)Time elapsed: 0.055 s % 15.85/3.20 % (4070817)Peak memory usage: 85 MB % 15.85/3.20 % (4070817)Instructions burned: 72 (million) % 15.85/3.20 % (4070818)Instruction limit reached! % 15.85/3.20 % (4070818)------------------------------ % 15.85/3.20 % (4070818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.85/3.20 % (4070818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.85/3.20 % (4070818)CaDiCaL version: 2.1.3 % 15.85/3.20 % (4070818)Termination reason: Instruction limit % 15.85/3.20 % (4070818)Termination phase: Property scanning % 15.85/3.20 % (4070818)Time elapsed: 0.058 s % 15.85/3.20 % (4070818)Peak memory usage: 86 MB % 15.85/3.20 % (4070818)Instructions burned: 75 (million) % 15.85/3.20 % (4070825)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1412818768:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi) % 15.85/3.20 % (4070822)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=110023143:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2986 on theBenchmark for (2986ds/294Mi) % 15.85/3.20 % (4070827)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2872076851:i=131:rtra=on_2986 on theBenchmark for (2986ds/131Mi) % 15.85/3.20 % (4070825)Instruction limit reached! % 15.85/3.20 % (4070825)------------------------------ % 15.85/3.20 % (4070825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.85/3.20 % (4070825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.85/3.20 % (4070825)CaDiCaL version: 2.1.3 % 15.85/3.20 % (4070825)Termination reason: Instruction limit % 15.85/3.20 % (4070825)Termination phase: Twee Goal Transformation % 15.85/3.20 % (4070825)Time elapsed: 0.053 s % 15.85/3.20 % (4070825)Peak memory usage: 87 MB % 15.85/3.20 % (4070825)Instructions burned: 132 (million) % 15.85/3.20 % (4070827)Instruction limit reached! % 15.85/3.20 % (4070827)------------------------------ % 15.85/3.20 % (4070827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.85/3.20 % (4070827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.22/3.60 % (4070827)CaDiCaL version: 2.1.3 % 17.22/3.60 % (4070827)Termination reason: Instruction limit % 17.22/3.60 % (4070827)Termination phase: Saturation % 17.22/3.60 % (4070827)Time elapsed: 0.151 s % 17.22/3.60 % (4070827)Peak memory usage: 128 MB % 17.22/3.60 % (4070827)Instructions burned: 132 (million) % 17.22/3.60 % (4070822)Instruction limit reached! % 17.22/3.60 % (4070822)------------------------------ % 17.22/3.60 % (4070822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.22/3.60 % (4070822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.22/3.60 % (4070822)CaDiCaL version: 2.1.3 % 17.22/3.60 % (4070822)Termination reason: Instruction limit % 17.22/3.60 % (4070822)Termination phase: Saturation % 17.22/3.60 % (4070822)Time elapsed: 0.173 s % 17.22/3.60 % (4070822)Peak memory usage: 90 MB % 17.22/3.60 % (4070822)Instructions burned: 298 (million) % 17.22/3.60 % (4070831)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3504832194:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi) % 17.22/3.60 % (4070838)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3355077596:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2983 on theBenchmark for (2983ds/598Mi) % 17.22/3.60 % (4070809)------------------------------ % 17.22/3.60 % (4070809)------------------------------ % 17.22/3.60 % (4070835)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1963801261:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi) % 17.22/3.60 % (4070831)Instruction limit reached! % 17.22/3.60 % (4070831)------------------------------ % 17.22/3.60 % (4070831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.22/3.60 % (4070831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.22/3.60 % (4070831)CaDiCaL version: 2.1.3 % 17.22/3.60 % (4070831)Termination reason: Instruction limit % 17.22/3.60 % (4070831)Termination phase: Property scanning % 17.22/3.60 % (4070831)Time elapsed: 0.031 s % 17.22/3.60 % (4070831)Peak memory usage: 85 MB % 17.22/3.60 % (4070831)Instructions burned: 41 (million) % 17.22/3.60 % (4070813)------------------------------ % 17.22/3.60 % (4070813)------------------------------ % 17.22/3.60 % (4070838)Instruction limit reached! % 17.22/3.60 % (4070838)------------------------------ % 17.22/3.60 % (4070838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.22/3.60 % (4070838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.22/3.60 % (4070838)CaDiCaL version: 2.1.3 % 17.22/3.60 % (4070838)Termination reason: Instruction limit % 17.22/3.60 % (4070838)Termination phase: Saturation % 17.22/3.60 % (4070838)Time elapsed: 0.162 s % 17.22/3.60 % (4070838)Peak memory usage: 136 MB % 17.22/3.60 % (4070838)Instructions burned: 601 (million) % 17.22/3.60 % (4070835)Refutation not found, incomplete strategy % 17.22/3.60 % (4070835)------------------------------ % 17.22/3.60 % (4070835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.22/3.60 % (4070835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.22/3.60 % (4070835)CaDiCaL version: 2.1.3 % 17.22/3.60 % (4070835)Termination reason: Refutation not found, incomplete strategy % 17.22/3.60 % (4070835)Time elapsed: 0.172 s % 17.22/3.60 % (4070835)Peak memory usage: 89 MB % 17.22/3.60 % (4070835)Instructions burned: 226 (million) % 17.22/3.60 % (4070841)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1226439999:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi) % 17.22/3.60 % (4070840)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1910906203:i=131:canc=cautious:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/131Mi) % 17.22/3.60 % (4070847)dis+10_1_si=on:random_seed=645110947:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi) % 17.22/3.60 % (4070849)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1686568291:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi) % 17.22/3.60 % (4070841)Refutation not found, incomplete strategy % 17.22/3.60 % (4070841)------------------------------ % 17.22/3.60 % (4070841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.22/3.60 % (4070841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.22/3.60 % (4070841)CaDiCaL version: 2.1.3 % 17.22/3.60 % (4070841)Termination reason: Refutation not found, incomplete strategy % 20.11/3.89 % (4070841)Time elapsed: 0.091 s % 20.11/3.89 % (4070841)Peak memory usage: 111 MB % 20.11/3.89 % (4070841)Instructions burned: 76 (million) % 20.11/3.89 % (4070851)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=445341543:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi) % 20.11/3.89 % (4070851)Instruction limit reached! % 20.11/3.89 % (4070851)------------------------------ % 20.11/3.89 % (4070851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.11/3.89 % (4070851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.11/3.89 % (4070851)CaDiCaL version: 2.1.3 % 20.11/3.89 % (4070851)Termination reason: Instruction limit % 20.11/3.89 % (4070851)Termination phase: Saturation % 20.11/3.89 % (4070851)Time elapsed: 0.014 s % 20.11/3.89 % (4070851)Peak memory usage: 88 MB % 20.11/3.89 % (4070851)Instructions burned: 66 (million) % 20.11/3.89 % (4070840)Instruction limit reached! % 20.11/3.89 % (4070840)------------------------------ % 20.11/3.89 % (4070840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.11/3.89 % (4070840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.11/3.89 % (4070840)CaDiCaL version: 2.1.3 % 20.11/3.89 % (4070840)Termination reason: Instruction limit % 20.11/3.89 % (4070840)Termination phase: Saturation % 20.11/3.89 % (4070840)Time elapsed: 0.128 s % 20.11/3.89 % (4070840)Peak memory usage: 111 MB % 20.11/3.89 % (4070840)Instructions burned: 131 (million) % 20.11/3.89 % (4070850)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2128087977:i=141:doe=on:rtra=on_2981 on theBenchmark for (2981ds/141Mi) % 20.11/3.89 % (4070850)Instruction limit reached! % 20.11/3.89 % (4070850)------------------------------ % 20.11/3.89 % (4070850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.11/3.89 % (4070850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.11/3.89 % (4070850)CaDiCaL version: 2.1.3 % 20.11/3.89 % (4070850)Termination reason: Instruction limit % 20.11/3.89 % (4070850)Termination phase: Saturation % 20.11/3.89 % (4070850)Time elapsed: 0.107 s % 20.11/3.89 % (4070850)Peak memory usage: 88 MB % 20.11/3.89 % (4070850)Instructions burned: 142 (million) % 20.11/3.89 % (4070857)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=2858325462:i=121:nm=16:rtra=on_2978 on theBenchmark for (2978ds/121Mi) % 20.11/3.89 % (4070849)Instruction limit reached! % 20.11/3.89 % (4070849)------------------------------ % 20.11/3.89 % (4070849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.11/3.89 % (4070849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.11/3.89 % (4070849)CaDiCaL version: 2.1.3 % 20.11/3.89 % (4070849)Termination reason: Instruction limit % 20.11/3.89 % (4070849)Termination phase: Saturation % 20.11/3.89 % (4070849)Time elapsed: 0.241 s % 20.11/3.89 % (4070849)Peak memory usage: 90 MB % 20.11/3.89 % (4070849)Instructions burned: 383 (million) % 20.11/3.89 % (4070857)Instruction limit reached! % 20.11/3.89 % (4070857)------------------------------ % 20.11/3.89 % (4070857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.11/3.89 % (4070857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.11/3.89 % (4070857)CaDiCaL version: 2.1.3 % 20.11/3.89 % (4070857)Termination reason: Instruction limit % 20.11/3.89 % (4070857)Termination phase: Saturation % 20.11/3.89 % (4070857)Time elapsed: 0.047 s % 20.11/3.89 % (4070857)Peak memory usage: 88 MB % 20.11/3.89 % (4070857)Instructions burned: 123 (million) % 20.11/3.89 % (4070835)------------------------------ % 20.11/3.89 % (4070835)------------------------------ % 20.11/3.89 % (4070859)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=3181581648:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi) % 20.11/3.89 % (4070841)------------------------------ % 20.11/3.89 % (4070841)------------------------------ % 20.11/3.89 % (4070860)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=3558765296:i=39:ins=3:rtra=on_2977 on theBenchmark for (2977ds/39Mi) % 20.11/3.89 % (4070859)Instruction limit reached! % 20.11/3.89 % (4070859)------------------------------ % 20.11/3.89 % (4070859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.11/3.89 % (4070859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.11/3.89 % (4070859)CaDiCaL version: 2.1.3 % 24.84/4.41 % (4070859)Termination reason: Instruction limit % 24.84/4.41 % (4070859)Termination phase: Saturation % 24.84/4.41 % (4070859)Time elapsed: 0.100 s % 24.84/4.41 % (4070859)Peak memory usage: 88 MB % 24.84/4.41 % (4070859)Instructions burned: 130 (million) % 24.84/4.41 % (4070860)Instruction limit reached! % 24.84/4.41 % (4070860)------------------------------ % 24.84/4.41 % (4070860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.84/4.41 % (4070860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.84/4.41 % (4070860)CaDiCaL version: 2.1.3 % 24.84/4.41 % (4070860)Termination reason: Instruction limit % 24.84/4.41 % (4070860)Termination phase: Property scanning % 24.84/4.41 % (4070860)Time elapsed: 0.031 s % 24.84/4.41 % (4070860)Peak memory usage: 85 MB % 24.84/4.41 % (4070860)Instructions burned: 40 (million) % 24.84/4.41 % (4070862)dis+1010_1_to=kbo:si=on:random_seed=3595031454:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2976 on theBenchmark for (2976ds/175Mi) % 24.84/4.41 % (4070862)Instruction limit reached! % 24.84/4.41 % (4070862)------------------------------ % 24.84/4.41 % (4070862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.84/4.41 % (4070862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.84/4.41 % (4070862)CaDiCaL version: 2.1.3 % 24.84/4.41 % (4070862)Termination reason: Instruction limit % 24.84/4.41 % (4070862)Termination phase: Saturation % 24.84/4.41 % (4070862)Time elapsed: 0.067 s % 24.84/4.41 % (4070862)Peak memory usage: 86 MB % 24.84/4.41 % (4070862)Instructions burned: 177 (million) % 24.84/4.41 % (4070863)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1504266730:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi) % 24.84/4.41 % (4070864)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1882026812:s2a=on:i=483:doe=on:nm=32:rtra=on_2976 on theBenchmark for (2976ds/483Mi) % 24.84/4.41 % (4070868)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3607479030:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi) % 24.84/4.41 % (4070870)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3786066640:st=2:i=295:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/295Mi) % 24.84/4.41 % (4070867)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3537883061:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi) % 24.84/4.41 % (4070847)Instruction limit reached! % 24.84/4.41 % (4070847)------------------------------ % 24.84/4.41 % (4070847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.84/4.41 % (4070847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.84/4.41 % (4070847)CaDiCaL version: 2.1.3 % 24.84/4.41 % (4070847)Termination reason: Instruction limit % 24.84/4.41 % (4070847)Termination phase: Saturation % 24.84/4.41 % (4070847)Time elapsed: 0.690 s % 24.84/4.41 % (4070847)Peak memory usage: 90 MB % 24.84/4.41 % (4070847)Instructions burned: 1000 (million) % 24.84/4.41 % (4070870)Refutation not found, incomplete strategy % 24.84/4.41 % (4070870)------------------------------ % 24.84/4.41 % (4070870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.84/4.41 % (4070870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.84/4.41 % (4070870)CaDiCaL version: 2.1.3 % 24.84/4.41 % (4070870)Termination reason: Refutation not found, incomplete strategy % 24.84/4.41 % (4070870)Time elapsed: 0.053 s % 24.84/4.41 % (4070870)Peak memory usage: 87 MB % 24.84/4.41 % (4070870)Instructions burned: 70 (million) % 24.84/4.41 % (4070871)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=575437089:i=328:kws=inv_frequency:nm=20:rtra=on_2974 on theBenchmark for (2974ds/328Mi) % 24.84/4.41 % (4070863)Instruction limit reached! % 24.84/4.41 % (4070863)------------------------------ % 24.84/4.41 % (4070863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.84/4.41 % (4070863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.84/4.41 % (4070863)CaDiCaL version: 2.1.3 % 24.84/4.41 % (4070863)Termination reason: Instruction limit % 24.84/4.41 % (4070863)Termination phase: Saturation % 24.84/4.41 % (4070863)Time elapsed: 0.285 s % 24.84/4.41 % (4070863)Peak memory usage: 117 MB % 24.84/4.41 % (4070863)Instructions burned: 330 (million) % 26.04/4.84 % (4070867)Instruction limit reached! % 26.04/4.84 % (4070867)------------------------------ % 26.04/4.84 % (4070867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070867)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070867)Termination reason: Instruction limit % 26.04/4.84 % (4070867)Termination phase: Saturation % 26.04/4.84 % (4070867)Time elapsed: 0.219 s % 26.04/4.84 % (4070867)Peak memory usage: 129 MB % 26.04/4.84 % (4070867)Instructions burned: 215 (million) % 26.04/4.84 % (4070871)Instruction limit reached! % 26.04/4.84 % (4070871)------------------------------ % 26.04/4.84 % (4070871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070871)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070871)Termination reason: Instruction limit % 26.04/4.84 % (4070871)Termination phase: Saturation % 26.04/4.84 % (4070871)Time elapsed: 0.142 s % 26.04/4.84 % (4070871)Peak memory usage: 112 MB % 26.04/4.84 % (4070871)Instructions burned: 330 (million) % 26.04/4.84 % (4070877)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3851243819:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi) % 26.04/4.84 % (4070868)Instruction limit reached! % 26.04/4.84 % (4070868)------------------------------ % 26.04/4.84 % (4070868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070868)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070868)Termination reason: Instruction limit % 26.04/4.84 % (4070868)Termination phase: Saturation % 26.04/4.84 % (4070868)Time elapsed: 0.284 s % 26.04/4.84 % (4070868)Peak memory usage: 112 MB % 26.04/4.84 % (4070868)Instructions burned: 349 (million) % 26.04/4.84 % (4070864)Instruction limit reached! % 26.04/4.84 % (4070864)------------------------------ % 26.04/4.84 % (4070864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070864)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070864)Termination reason: Instruction limit % 26.04/4.84 % (4070864)Termination phase: Saturation % 26.04/4.84 % (4070864)Time elapsed: 0.424 s % 26.04/4.84 % (4070864)Peak memory usage: 133 MB % 26.04/4.84 % (4070864)Instructions burned: 483 (million) % 26.04/4.84 % (4070877)Instruction limit reached! % 26.04/4.84 % (4070877)------------------------------ % 26.04/4.84 % (4070877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070877)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070877)Termination reason: Instruction limit % 26.04/4.84 % (4070877)Termination phase: Saturation % 26.04/4.84 % (4070877)Time elapsed: 0.125 s % 26.04/4.84 % (4070877)Peak memory usage: 112 MB % 26.04/4.84 % (4070877)Instructions burned: 282 (million) % 26.04/4.84 % (4070884)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1739321006:i=416:rtra=on:gtg=position:ss=axioms_2970 on theBenchmark for (2970ds/416Mi) % 26.04/4.84 % (4070870)------------------------------ % 26.04/4.84 % (4070870)------------------------------ % 26.04/4.84 % (4070879)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1278472630:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/484Mi) % 26.04/4.84 % (4070884)Refutation not found, incomplete strategy % 26.04/4.84 % (4070884)------------------------------ % 26.04/4.84 % (4070884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070884)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070884)Termination reason: Refutation not found, incomplete strategy % 26.04/4.84 % (4070884)Time elapsed: 0.049 s % 26.04/4.84 % (4070884)Peak memory usage: 111 MB % 26.04/4.84 % (4070884)Instructions burned: 72 (million) % 26.04/4.84 % (4070879)Refutation not found, incomplete strategy % 26.04/4.84 % (4070879)------------------------------ % 26.04/4.84 % (4070879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.04/4.84 % (4070879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.04/4.84 % (4070879)CaDiCaL version: 2.1.3 % 26.04/4.84 % (4070879)Termination reason: Refutation not found, incomplete strategy % 30.97/5.35 % (4070879)Time elapsed: 0.052 s % 30.97/5.35 % (4070879)Peak memory usage: 88 MB % 30.97/5.35 % (4070879)Instructions burned: 68 (million) % 30.97/5.35 % (4070883)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3864785241:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2970 on theBenchmark for (2970ds/321Mi) % 30.97/5.35 % (4070885)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=1902059185:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi) % 30.97/5.35 % (4070883)Refutation not found, incomplete strategy % 30.97/5.35 % (4070883)------------------------------ % 30.97/5.35 % (4070883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.97/5.35 % (4070883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.97/5.35 % (4070883)CaDiCaL version: 2.1.3 % 30.97/5.35 % (4070883)Termination reason: Refutation not found, incomplete strategy % 30.97/5.35 % (4070883)Time elapsed: 0.088 s % 30.97/5.35 % (4070883)Peak memory usage: 112 MB % 30.97/5.35 % (4070883)Instructions burned: 73 (million) % 30.97/5.35 % (4070886)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1915660057:avsq=on:i=276:avsqr=1,2:rtra=on_2969 on theBenchmark for (2969ds/276Mi) % 30.97/5.35 % (4070888)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3411753669:i=375:kws=inv_arity_squared:rtra=on_2969 on theBenchmark for (2969ds/375Mi) % 30.97/5.35 % (4070892)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1455892378:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/387Mi) % 30.97/5.35 % (4070884)------------------------------ % 30.97/5.35 % (4070884)------------------------------ % 30.97/5.35 % (4070892)Refutation not found, incomplete strategy % 30.97/5.35 % (4070892)------------------------------ % 30.97/5.35 % (4070892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.97/5.35 % (4070892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.97/5.35 % (4070892)CaDiCaL version: 2.1.3 % 30.97/5.35 % (4070892)Termination reason: Refutation not found, incomplete strategy % 30.97/5.35 % (4070892)Time elapsed: 0.095 s % 30.97/5.35 % (4070892)Peak memory usage: 111 MB % 30.97/5.35 % (4070892)Instructions burned: 77 (million) % 30.97/5.35 % (4070888)Instruction limit reached! % 30.97/5.35 % (4070888)------------------------------ % 30.97/5.35 % (4070888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.97/5.35 % (4070888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.97/5.35 % (4070888)CaDiCaL version: 2.1.3 % 30.97/5.35 % (4070888)Termination reason: Instruction limit % 30.97/5.35 % (4070888)Termination phase: Saturation % 30.97/5.35 % (4070888)Time elapsed: 0.201 s % 30.97/5.35 % (4070888)Peak memory usage: 113 MB % 30.97/5.35 % (4070888)Instructions burned: 375 (million) % 30.97/5.35 % (4070879)------------------------------ % 30.97/5.35 % (4070879)------------------------------ % 30.97/5.35 % (4070886)Instruction limit reached! % 30.97/5.35 % (4070886)------------------------------ % 30.97/5.35 % (4070886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.97/5.35 % (4070886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.97/5.35 % (4070886)CaDiCaL version: 2.1.3 % 30.97/5.35 % (4070886)Termination reason: Instruction limit % 30.97/5.35 % (4070886)Termination phase: Saturation % 30.97/5.35 % (4070886)Time elapsed: 0.265 s % 30.97/5.35 % (4070886)Peak memory usage: 130 MB % 30.97/5.35 % (4070886)Instructions burned: 277 (million) % 30.97/5.35 % (4070885)Instruction limit reached! % 30.97/5.35 % (4070885)------------------------------ % 30.97/5.35 % (4070885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.97/5.35 % (4070885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.97/5.35 % (4070885)CaDiCaL version: 2.1.3 % 30.97/5.35 % (4070885)Termination reason: Instruction limit % 30.97/5.35 % (4070885)Termination phase: Saturation % 30.97/5.35 % (4070885)Time elapsed: 0.380 s % 30.97/5.35 % (4070885)Peak memory usage: 113 MB % 30.97/5.35 % (4070885)Instructions burned: 471 (million) % 30.97/5.35 % (4070883)------------------------------ % 30.97/5.35 % (4070883)------------------------------ % 30.97/5.35 % (4070898)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=712679529:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2965 on theBenchmark for (2965ds/513Mi) % 35.49/5.99 % (4070899)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=927675353:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi) % 35.49/5.99 % (4070900)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3178336021:i=359:rtra=on:gtg=exists_top:ss=axioms_2964 on theBenchmark for (2964ds/359Mi) % 35.49/5.99 % (4070900)Refutation not found, incomplete strategy % 35.49/5.99 % (4070900)------------------------------ % 35.49/5.99 % (4070900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.49/5.99 % (4070900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.49/5.99 % (4070900)CaDiCaL version: 2.1.3 % 35.49/5.99 % (4070900)Termination reason: Refutation not found, incomplete strategy % 35.49/5.99 % (4070900)Time elapsed: 0.041 s % 35.49/5.99 % (4070900)Peak memory usage: 88 MB % 35.49/5.99 % (4070900)Instructions burned: 97 (million) % 35.49/5.99 % (4070892)------------------------------ % 35.49/5.99 % (4070892)------------------------------ % 35.49/5.99 % (4070901)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2807750645:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2963 on theBenchmark for (2963ds/341Mi) % 35.49/5.99 % (4070899)Instruction limit reached! % 35.49/5.99 % (4070899)------------------------------ % 35.49/5.99 % (4070899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.49/5.99 % (4070899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.49/5.99 % (4070899)CaDiCaL version: 2.1.3 % 35.49/5.99 % (4070899)Termination reason: Instruction limit % 35.49/5.99 % (4070899)Termination phase: Saturation % 35.49/5.99 % (4070899)Time elapsed: 0.166 s % 35.49/5.99 % (4070899)Peak memory usage: 130 MB % 35.49/5.99 % (4070899)Instructions burned: 335 (million) % 35.49/5.99 % (4070902)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=2806100898:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/261Mi) % 35.49/5.99 % (4070904)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=300495253:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/235Mi) % 35.49/5.99 % (4070902)Refutation not found, incomplete strategy % 35.49/5.99 % (4070902)------------------------------ % 35.49/5.99 % (4070902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.49/5.99 % (4070902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.49/5.99 % (4070902)CaDiCaL version: 2.1.3 % 35.49/5.99 % (4070902)Termination reason: Refutation not found, incomplete strategy % 35.49/5.99 % (4070902)Time elapsed: 0.048 s % 35.49/5.99 % (4070902)Peak memory usage: 111 MB % 35.49/5.99 % (4070902)Instructions burned: 48 (million) % 35.49/5.99 % (4070904)Refutation not found, incomplete strategy % 35.49/5.99 % (4070904)------------------------------ % 35.49/5.99 % (4070904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.49/5.99 % (4070904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.49/5.99 % (4070904)CaDiCaL version: 2.1.3 % 35.49/5.99 % (4070904)Termination reason: Refutation not found, incomplete strategy % 35.49/5.99 % (4070904)Time elapsed: 0.090 s % 35.49/5.99 % (4070904)Peak memory usage: 111 MB % 35.49/5.99 % (4070904)Instructions burned: 76 (million) % 35.49/5.99 % (4070898)Instruction limit reached! % 35.49/5.99 % (4070898)------------------------------ % 35.49/5.99 % (4070898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.49/5.99 % (4070898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.49/5.99 % (4070898)CaDiCaL version: 2.1.3 % 35.49/5.99 % (4070898)Termination reason: Instruction limit % 35.49/5.99 % (4070898)Termination phase: Saturation % 35.49/5.99 % (4070898)Time elapsed: 0.375 s % 35.49/5.99 % (4070898)Peak memory usage: 90 MB % 35.49/5.99 % (4070898)Instructions burned: 514 (million) % 35.49/5.99 % (4070914)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=1025752385:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2961 on theBenchmark for (2961ds/273Mi) % 35.49/5.99 % (4070919)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1797728847:i=146:doe=on:rtra=on_2960 on theBenchmark for (2960ds/146Mi) % 39.86/6.72 % (4070901)Instruction limit reached! % 39.86/6.72 % (4070901)------------------------------ % 39.86/6.72 % (4070901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.86/6.72 % (4070901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.86/6.72 % (4070901)CaDiCaL version: 2.1.3 % 39.86/6.72 % (4070901)Termination reason: Instruction limit % 39.86/6.72 % (4070901)Termination phase: Saturation % 39.86/6.72 % (4070901)Time elapsed: 0.285 s % 39.86/6.72 % (4070901)Peak memory usage: 118 MB % 39.86/6.72 % (4070901)Instructions burned: 341 (million) % 39.86/6.72 % (4070900)------------------------------ % 39.86/6.72 % (4070900)------------------------------ % 39.86/6.72 % (4070919)Instruction limit reached! % 39.86/6.72 % (4070919)------------------------------ % 39.86/6.72 % (4070919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.86/6.72 % (4070919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.86/6.72 % (4070919)CaDiCaL version: 2.1.3 % 39.86/6.72 % (4070919)Termination reason: Instruction limit % 39.86/6.72 % (4070919)Termination phase: Saturation % 39.86/6.72 % (4070919)Time elapsed: 0.059 s % 39.86/6.72 % (4070919)Peak memory usage: 88 MB % 39.86/6.72 % (4070919)Instructions burned: 148 (million) % 39.86/6.72 % (4070902)------------------------------ % 39.86/6.72 % (4070902)------------------------------ % 39.86/6.72 % (4070914)Instruction limit reached! % 39.86/6.72 % (4070914)------------------------------ % 39.86/6.72 % (4070914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.86/6.72 % (4070914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.86/6.72 % (4070914)CaDiCaL version: 2.1.3 % 39.86/6.72 % (4070914)Termination reason: Instruction limit % 39.86/6.72 % (4070914)Termination phase: Saturation % 39.86/6.72 % (4070914)Time elapsed: 0.205 s % 39.86/6.72 % (4070914)Peak memory usage: 91 MB % 39.86/6.72 % (4070914)Instructions burned: 273 (million) % 39.86/6.72 % (4070923)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=51613443:i=4428:doe=on:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/4428Mi) % 39.86/6.72 % (4070926)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=509855331:avsq=on:i=276:avsqr=1,2:rtra=on_2958 on theBenchmark for (2958ds/276Mi) % 39.86/6.72 % (4070928)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1031725597:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2958 on theBenchmark for (2958ds/655Mi) % 39.86/6.72 % (4070904)------------------------------ % 39.86/6.72 % (4070904)------------------------------ % 39.86/6.72 % (4070927)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=32783496:i=1052:rtra=on_2958 on theBenchmark for (2958ds/1052Mi) % 39.86/6.72 % (4070926)Instruction limit reached! % 39.86/6.72 % (4070926)------------------------------ % 39.86/6.72 % (4070926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.86/6.72 % (4070926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.86/6.72 % (4070926)CaDiCaL version: 2.1.3 % 39.86/6.72 % (4070926)Termination reason: Instruction limit % 39.86/6.72 % (4070926)Termination phase: Saturation % 39.86/6.72 % (4070926)Time elapsed: 0.141 s % 39.86/6.72 % (4070926)Peak memory usage: 129 MB % 39.86/6.72 % (4070926)Instructions burned: 277 (million) % 39.86/6.72 % (4070929)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=989994625:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2957 on theBenchmark for (2957ds/1054Mi) % 39.86/6.72 % (4070930)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1902041978:i=107:rtra=on_2956 on theBenchmark for (2956ds/107Mi) % 39.86/6.72 % (4070929)Refutation not found, incomplete strategy % 39.86/6.72 % (4070929)------------------------------ % 39.86/6.72 % (4070929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.86/6.72 % (4070929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.86/6.72 % (4070929)CaDiCaL version: 2.1.3 % 39.86/6.72 % (4070929)Termination reason: Refutation not found, incomplete strategy % 39.86/6.72 % (4070929)Time elapsed: 0.032 s % 39.86/6.72 % (4070929)Peak memory usage: 87 MB % 39.86/6.72 % (4070929)Instructions burned: 42 (million) % 39.86/6.72 % (4070930)Instruction limit reached! % 39.86/6.72 % (4070930)------------------------------ % 39.86/6.72 % (4070930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.54/7.18 % (4070930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.54/7.18 % (4070930)CaDiCaL version: 2.1.3 % 44.54/7.18 % (4070930)Termination reason: Instruction limit % 44.54/7.18 % (4070930)Termination phase: Saturation % 44.54/7.18 % (4070930)Time elapsed: 0.082 s % 44.54/7.18 % (4070930)Peak memory usage: 88 MB % 44.54/7.18 % (4070930)Instructions burned: 108 (million) % 44.54/7.18 % (4070936)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 44.54/7.18 % (4070936)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1721425083:i=1090:aac=none:nm=0:rtra=on:rawr=on_2955 on theBenchmark for (2955ds/1090Mi) % 44.54/7.18 % (4070935)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4021921849:s2a=on:i=450:doe=on:nm=32:rtra=on_2955 on theBenchmark for (2955ds/450Mi) % 44.54/7.18 % (4070939)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2548253598:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2953 on theBenchmark for (2953ds/130Mi) % 44.54/7.18 % (4070928)Refutation not found, incomplete strategy % 44.54/7.18 % (4070928)------------------------------ % 44.54/7.18 % (4070928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.54/7.18 % (4070928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.54/7.18 % (4070928)CaDiCaL version: 2.1.3 % 44.54/7.18 % (4070928)Termination reason: Refutation not found, incomplete strategy % 44.54/7.18 % (4070928)Time elapsed: 0.527 s % 44.54/7.18 % (4070928)Peak memory usage: 95 MB % 44.54/7.18 % (4070928)Instructions burned: 555 (million) % 44.54/7.18 % (4070929)------------------------------ % 44.54/7.18 % (4070929)------------------------------ % 44.54/7.18 % (4070939)Instruction limit reached! % 44.54/7.18 % (4070939)------------------------------ % 44.54/7.18 % (4070939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.54/7.18 % (4070939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.54/7.18 % (4070939)CaDiCaL version: 2.1.3 % 44.54/7.18 % (4070939)Termination reason: Instruction limit % 44.54/7.18 % (4070939)Termination phase: Twee Goal Transformation % 44.54/7.18 % (4070939)Time elapsed: 0.101 s % 44.54/7.18 % (4070939)Peak memory usage: 87 MB % 44.54/7.18 % (4070939)Instructions burned: 131 (million) % 44.54/7.18 % (4070935)Instruction limit reached! % 44.54/7.18 % (4070935)------------------------------ % 44.54/7.18 % (4070935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.54/7.18 % (4070935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.54/7.18 % (4070935)CaDiCaL version: 2.1.3 % 44.54/7.18 % (4070935)Termination reason: Instruction limit % 44.54/7.18 % (4070935)Termination phase: Saturation % 44.54/7.18 % (4070935)Time elapsed: 0.391 s % 44.54/7.18 % (4070935)Peak memory usage: 130 MB % 44.54/7.18 % (4070935)Instructions burned: 450 (million) % 44.54/7.18 % (4070936)Instruction limit reached! % 44.54/7.18 % (4070936)------------------------------ % 44.54/7.18 % (4070936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.54/7.18 % (4070936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.54/7.18 % (4070936)CaDiCaL version: 2.1.3 % 44.54/7.18 % (4070936)Termination reason: Instruction limit % 44.54/7.18 % (4070936)Termination phase: Saturation % 44.54/7.18 % (4070936)Time elapsed: 0.435 s % 44.54/7.18 % (4070936)Peak memory usage: 118 MB % 44.54/7.18 % (4070936)Instructions burned: 1091 (million) % 44.54/7.18 % (4070927)Instruction limit reached! % 44.54/7.18 % (4070927)------------------------------ % 44.54/7.18 % (4070927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.54/7.18 % (4070927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.54/7.18 % (4070927)CaDiCaL version: 2.1.3 % 44.54/7.18 % (4070927)Termination reason: Instruction limit % 44.54/7.18 % (4070927)Termination phase: Saturation % 44.54/7.18 % (4070927)Time elapsed: 0.731 s % 44.54/7.18 % (4070927)Peak memory usage: 91 MB % 44.54/7.18 % (4070927)Instructions burned: 1052 (million) % 44.54/7.18 % (4070945)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3602809915:i=312:kws=inv_frequency:nm=20:rtra=on_2950 on theBenchmark for (2950ds/312Mi) % 44.54/7.18 % (4070928)------------------------------ % 51.73/8.15 % (4070928)------------------------------ % 51.73/8.15 % (4070946)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=3446123952:i=491:doe=on:rtra=on:gtg=position_2949 on theBenchmark for (2949ds/491Mi) % 51.73/8.15 % (4070947)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=1615409357:s2a=on:i=835:s2at=2:rtra=on_2948 on theBenchmark for (2948ds/835Mi) % 51.73/8.15 % (4070948)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=4061018547:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2948 on theBenchmark for (2948ds/307Mi) % 51.73/8.15 % (4070948)Refutation not found, incomplete strategy % 51.73/8.15 % (4070948)------------------------------ % 51.73/8.15 % (4070948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.73/8.15 % (4070948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.73/8.15 % (4070948)CaDiCaL version: 2.1.3 % 51.73/8.15 % (4070948)Termination reason: Refutation not found, incomplete strategy % 51.73/8.15 % (4070948)Time elapsed: 0.082 s % 51.73/8.15 % (4070948)Peak memory usage: 90 MB % 51.73/8.15 % (4070948)Instructions burned: 206 (million) % 51.73/8.15 % (4070949)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=228628057:i=776:doe=on:rtra=on_2948 on theBenchmark for (2948ds/776Mi) % 51.73/8.15 % (4070945)Instruction limit reached! % 51.73/8.15 % (4070945)------------------------------ % 51.73/8.15 % (4070945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.73/8.15 % (4070945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.73/8.15 % (4070945)CaDiCaL version: 2.1.3 % 51.73/8.15 % (4070945)Termination reason: Instruction limit % 51.73/8.15 % (4070945)Termination phase: Saturation % 51.73/8.15 % (4070945)Time elapsed: 0.262 s % 51.73/8.15 % (4070945)Peak memory usage: 112 MB % 51.73/8.15 % (4070945)Instructions burned: 313 (million) % 51.73/8.15 % (4070946)Refutation not found, incomplete strategy % 51.73/8.15 % (4070946)------------------------------ % 51.73/8.15 % (4070946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.73/8.15 % (4070946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.73/8.15 % (4070946)CaDiCaL version: 2.1.3 % 51.73/8.15 % (4070946)Termination reason: Refutation not found, incomplete strategy % 51.73/8.15 % (4070946)Time elapsed: 0.192 s % 51.73/8.15 % (4070946)Peak memory usage: 90 MB % 51.73/8.15 % (4070946)Instructions burned: 251 (million) % 51.73/8.15 % (4070955)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=748244601:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2947 on theBenchmark for (2947ds/646Mi) % 51.73/8.15 % (4070948)------------------------------ % 51.73/8.15 % (4070948)------------------------------ % 51.73/8.15 % (4070958)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=546067566:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2945 on theBenchmark for (2945ds/784Mi) % 51.73/8.15 % (4070947)Instruction limit reached! % 51.73/8.15 % (4070947)------------------------------ % 51.73/8.15 % (4070947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.73/8.15 % (4070947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.73/8.15 % (4070947)CaDiCaL version: 2.1.3 % 51.73/8.15 % (4070947)Termination reason: Instruction limit % 51.73/8.15 % (4070947)Termination phase: Saturation % 51.73/8.15 % (4070947)Time elapsed: 0.572 s % 51.73/8.15 % (4070947)Peak memory usage: 89 MB % 51.73/8.15 % (4070947)Instructions burned: 836 (million) % 51.73/8.15 % (4070946)------------------------------ % 51.73/8.15 % (4070946)------------------------------ % 51.73/8.15 % (4070960)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=3135271848:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2943 on theBenchmark for (2943ds/1131Mi) % 51.73/8.15 % (4070949)Instruction limit reached! % 51.73/8.15 % (4070949)------------------------------ % 51.73/8.15 % (4070949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.73/8.15 % (4070949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.73/8.15 % (4070949)CaDiCaL version: 2.1.3 % 51.73/8.15 % (4070949)Termination reason: Instruction limit % 51.73/8.15 % (4070949)Termination phase: Saturation % 51.73/8.15 % (4070949)Time elapsed: 0.569 s % 51.73/8.15 % (4070949)Peak memory usage: 113 MB % 51.73/8.15 % (4070949)Instructions burned: 776 (million) % 60.63/9.48 % (4070962)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3470526908:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2941 on theBenchmark for (2941ds/246Mi) % 60.63/9.48 % (4070955)Instruction limit reached! % 60.63/9.48 % (4070955)------------------------------ % 60.63/9.48 % (4070955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.63/9.48 % (4070955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.63/9.48 % (4070955)CaDiCaL version: 2.1.3 % 60.63/9.48 % (4070955)Termination reason: Instruction limit % 60.63/9.48 % (4070955)Termination phase: Saturation % 60.63/9.48 % (4070955)Time elapsed: 0.540 s % 60.63/9.48 % (4070955)Peak memory usage: 137 MB % 60.63/9.48 % (4070955)Instructions burned: 646 (million) % 60.63/9.48 % (4070962)Refutation not found, incomplete strategy % 60.63/9.48 % (4070962)------------------------------ % 60.63/9.48 % (4070962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.63/9.48 % (4070962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.63/9.48 % (4070962)CaDiCaL version: 2.1.3 % 60.63/9.48 % (4070962)Termination reason: Refutation not found, incomplete strategy % 60.63/9.48 % (4070962)Time elapsed: 0.065 s % 60.63/9.48 % (4070962)Peak memory usage: 111 MB % 60.63/9.48 % (4070962)Instructions burned: 76 (million) % 60.63/9.48 % (4070964)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=2038964929:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2941 on theBenchmark for (2941ds/775Mi) % 60.63/9.48 % (4070964)Refutation not found, incomplete strategy % 60.63/9.48 % (4070964)------------------------------ % 60.63/9.48 % (4070964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.63/9.48 % (4070964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.63/9.48 % (4070964)CaDiCaL version: 2.1.3 % 60.63/9.48 % (4070964)Termination reason: Refutation not found, incomplete strategy % 60.63/9.48 % (4070964)Time elapsed: 0.031 s % 60.63/9.48 % (4070964)Peak memory usage: 88 MB % 60.63/9.48 % (4070964)Instructions burned: 74 (million) % 60.63/9.48 % (4070958)Instruction limit reached! % 60.63/9.48 % (4070958)------------------------------ % 60.63/9.48 % (4070958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.63/9.48 % (4070958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.63/9.48 % (4070958)CaDiCaL version: 2.1.3 % 60.63/9.48 % (4070958)Termination reason: Instruction limit % 60.63/9.48 % (4070958)Termination phase: Saturation % 60.63/9.48 % (4070958)Time elapsed: 0.486 s % 60.63/9.48 % (4070958)Peak memory usage: 113 MB % 60.63/9.48 % (4070958)Instructions burned: 784 (million) % 60.63/9.48 % (4070965)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3295356578:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2939 on theBenchmark for (2939ds/273Mi) % 60.63/9.48 % (4070960)Instruction limit reached! % 60.63/9.48 % (4070960)------------------------------ % 60.63/9.48 % (4070960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.63/9.48 % (4070960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.63/9.48 % (4070960)CaDiCaL version: 2.1.3 % 60.63/9.48 % (4070960)Termination reason: Instruction limit % 60.63/9.48 % (4070960)Termination phase: Saturation % 60.63/9.48 % (4070960)Time elapsed: 0.464 s % 60.63/9.48 % (4070960)Peak memory usage: 113 MB % 60.63/9.48 % (4070960)Instructions burned: 1133 (million) % 60.63/9.48 % (4070968)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3617918672:i=102:nm=16:rtra=on_2938 on theBenchmark for (2938ds/102Mi) % 60.63/9.48 % (4070968)Instruction limit reached! % 60.63/9.48 % (4070968)------------------------------ % 60.63/9.48 % (4070968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.63/9.48 % (4070968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.63/9.48 % (4070968)CaDiCaL version: 2.1.3 % 60.63/9.48 % (4070968)Termination reason: Instruction limit % 60.63/9.48 % (4070968)Termination phase: Saturation % 60.63/9.48 % (4070968)Time elapsed: 0.078 s % 60.63/9.48 % (4070968)Peak memory usage: 88 MB % 60.63/9.48 % (4070968)Instructions burned: 103 (million) % 60.63/9.48 % (4070969)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=292147573:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2938 on theBenchmark for (2938ds/1094Mi) % 72.25/11.08 % (4070962)------------------------------ % 72.25/11.08 % (4070962)------------------------------ % 72.25/11.08 % (4070964)------------------------------ % 72.25/11.08 % (4070964)------------------------------ % 72.25/11.08 % (4070965)Instruction limit reached! % 72.25/11.08 % (4070965)------------------------------ % 72.25/11.08 % (4070965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.25/11.08 % (4070965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.25/11.08 % (4070965)CaDiCaL version: 2.1.3 % 72.25/11.08 % (4070965)Termination reason: Instruction limit % 72.25/11.08 % (4070965)Termination phase: Saturation % 72.25/11.08 % (4070965)Time elapsed: 0.208 s % 72.25/11.08 % (4070965)Peak memory usage: 91 MB % 72.25/11.08 % (4070965)Instructions burned: 274 (million) % 72.25/11.08 % (4070971)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=575250824:i=6400:doe=on:fsr=off:rtra=on_2936 on theBenchmark for (2936ds/6400Mi) % 72.25/11.08 % (4070974)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=175188187:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2935 on theBenchmark for (2935ds/868Mi) % 72.25/11.08 % (4070975)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3630734055:i=1846:canc=cautious:fsr=off:rtra=on_2934 on theBenchmark for (2934ds/1846Mi) % 72.25/11.08 % (4070977)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2048169068:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2934 on theBenchmark for (2934ds/273Mi) % 72.25/11.08 % (4070976)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3176809103:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2934 on theBenchmark for (2934ds/36816Mi) % 72.25/11.08 % (4070975)Refutation not found, incomplete strategy % 72.25/11.08 % (4070975)------------------------------ % 72.25/11.08 % (4070975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.25/11.08 % (4070975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.25/11.08 % (4070975)CaDiCaL version: 2.1.3 % 72.25/11.08 % (4070975)Termination reason: Refutation not found, incomplete strategy % 72.25/11.08 % (4070975)Time elapsed: 0.128 s % 72.25/11.08 % (4070975)Peak memory usage: 89 MB % 72.25/11.08 % (4070975)Instructions burned: 170 (million) % 72.25/11.08 % (4070977)Instruction limit reached! % 72.25/11.08 % (4070977)------------------------------ % 72.25/11.08 % (4070977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.25/11.08 % (4070977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.25/11.08 % (4070977)CaDiCaL version: 2.1.3 % 72.25/11.08 % (4070977)Termination reason: Instruction limit % 72.25/11.08 % (4070977)Termination phase: Saturation % 72.25/11.08 % (4070977)Time elapsed: 0.206 s % 72.25/11.08 % (4070977)Peak memory usage: 90 MB % 72.25/11.08 % (4070977)Instructions burned: 273 (million) % 72.25/11.08 % (4070983)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=85951798:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2930 on theBenchmark for (2930ds/863Mi) % 72.25/11.08 % (4070969)Instruction limit reached! % 72.25/11.08 % (4070969)------------------------------ % 72.25/11.08 % (4070969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.25/11.08 % (4070969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.25/11.08 % (4070969)CaDiCaL version: 2.1.3 % 72.25/11.08 % (4070969)Termination reason: Instruction limit % 72.25/11.08 % (4070969)Termination phase: Saturation % 72.25/11.08 % (4070969)Time elapsed: 0.751 s % 72.25/11.08 % (4070969)Peak memory usage: 91 MB % 72.25/11.08 % (4070969)Instructions burned: 1094 (million) % 72.25/11.08 % (4070975)------------------------------ % 72.25/11.08 % (4070975)------------------------------ % 72.25/11.08 % (4070974)Instruction limit reached! % 72.25/11.08 % (4070974)------------------------------ % 72.25/11.08 % (4070974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.25/11.08 % (4070974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.25/11.08 % (4070974)CaDiCaL version: 2.1.3 % 72.25/11.08 % (4070974)Termination reason: Instruction limit % 72.25/11.08 % (4070974)Termination phase: Saturation % 72.25/11.08 % (4070974)Time elapsed: 0.737 s % 72.25/11.08 % (4070974)Peak memory usage: 128 MB % 72.25/11.08 % (4070974)Instructions burned: 868 (million) % 82.01/12.58 % (4070923)Instruction limit reached! % 82.01/12.58 % (4070923)------------------------------ % 82.01/12.58 % (4070923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.01/12.58 % (4070923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.01/12.58 % (4070923)CaDiCaL version: 2.1.3 % 82.01/12.58 % (4070923)Termination reason: Instruction limit % 82.01/12.58 % (4070923)Termination phase: Saturation % 82.01/12.58 % (4070923)Time elapsed: 3.114 s % 82.01/12.58 % (4070923)Peak memory usage: 90 MB % 82.01/12.58 % (4070923)Instructions burned: 4428 (million) % 82.01/12.58 % (4070985)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2707687883:i=5811:kws=precedence:nm=0:rtra=on_2927 on theBenchmark for (2927ds/5811Mi) % 82.01/12.58 % (4070986)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=2873382362:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2927 on theBenchmark for (2927ds/2216Mi) % 82.01/12.58 % (4070987)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2632383708:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2925 on theBenchmark for (2925ds/801Mi) % 82.01/12.58 % (4070988)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=472286476:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2925 on theBenchmark for (2925ds/1026Mi) % 82.01/12.58 % (4070988)Refutation not found, incomplete strategy % 82.01/12.58 % (4070988)------------------------------ % 82.01/12.58 % (4070988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.01/12.58 % (4070988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.01/12.58 % (4070988)CaDiCaL version: 2.1.3 % 82.01/12.58 % (4070988)Termination reason: Refutation not found, incomplete strategy % 82.01/12.58 % (4070988)Time elapsed: 0.031 s % 82.01/12.58 % (4070988)Peak memory usage: 87 MB % 82.01/12.58 % (4070988)Instructions burned: 42 (million) % 82.01/12.58 % (4070983)Instruction limit reached! % 82.01/12.58 % (4070983)------------------------------ % 82.01/12.58 % (4070983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.01/12.58 % (4070983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.01/12.58 % (4070983)CaDiCaL version: 2.1.3 % 82.01/12.58 % (4070983)Termination reason: Instruction limit % 82.01/12.58 % (4070983)Termination phase: Saturation % 82.01/12.58 % (4070983)Time elapsed: 0.754 s % 82.01/12.58 % (4070983)Peak memory usage: 128 MB % 82.01/12.58 % (4070983)Instructions burned: 864 (million) % 82.01/12.58 % (4070988)------------------------------ % 82.01/12.58 % (4070988)------------------------------ % 82.01/12.58 % (4070993)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=34401758:i=3509:rtra=on_2920 on theBenchmark for (2920ds/3509Mi) % 82.01/12.58 % (4070987)Refutation not found, incomplete strategy % 82.01/12.58 % (4070987)------------------------------ % 82.01/12.58 % (4070987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.01/12.58 % (4070987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.01/12.58 % (4070987)CaDiCaL version: 2.1.3 % 82.01/12.58 % (4070987)Termination reason: Refutation not found, incomplete strategy % 82.01/12.58 % (4070987)Time elapsed: 0.549 s % 82.01/12.58 % (4070987)Peak memory usage: 96 MB % 82.01/12.58 % (4070987)Instructions burned: 591 (million) % 82.01/12.58 % (4070998)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=192096227:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2918 on theBenchmark for (2918ds/2127Mi) % 82.01/12.58 % (4070998)Refutation not found, incomplete strategy % 82.01/12.58 % (4070998)------------------------------ % 82.01/12.58 % (4070998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.01/12.58 % (4070998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.01/12.58 % (4070998)CaDiCaL version: 2.1.3 % 82.01/12.58 % (4070998)Termination reason: Refutation not found, incomplete strategy % 82.01/12.58 % (4070998)Time elapsed: 0.052 s % 82.01/12.58 % (4070998)Peak memory usage: 88 MB % 82.01/12.58 % (4070998)Instructions burned: 70 (million) % 82.01/12.58 % (4070987)------------------------------ % 82.01/12.58 % (4070987)------------------------------ % 82.01/12.58 % (4070971)Instruction limit reached! % 82.01/12.58 % (4070971)------------------------------ % 82.01/12.58 % (4070971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.01/12.58 % (4070971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.80/17.52 % (4070971)CaDiCaL version: 2.1.3 % 117.80/17.52 % (4070971)Termination reason: Instruction limit % 117.80/17.52 % (4070971)Termination phase: Saturation % 117.80/17.52 % (4070971)Time elapsed: 2.211 s % 117.80/17.52 % (4070971)Peak memory usage: 90 MB % 117.80/17.52 % (4070971)Instructions burned: 6401 (million) % 117.80/17.52 % (4070998)------------------------------ % 117.80/17.52 % (4070998)------------------------------ % 117.80/17.52 % (4071002)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3950369568:s2a=on:i=3553:nm=0:rtra=on_2912 on theBenchmark for (2912ds/3553Mi) % 117.80/17.52 % (4071001)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2215218283:i=1959:rtra=on:fsd=on:proc=on_2913 on theBenchmark for (2913ds/1959Mi) % 117.80/17.52 % (4071003)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2343797367:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2911 on theBenchmark for (2911ds/3201Mi) % 117.80/17.52 % (4070986)Instruction limit reached! % 117.80/17.52 % (4070986)------------------------------ % 117.80/17.52 % (4070986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.80/17.52 % (4070986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.80/17.52 % (4070986)CaDiCaL version: 2.1.3 % 117.80/17.52 % (4070986)Termination reason: Instruction limit % 117.80/17.52 % (4070986)Termination phase: Saturation % 117.80/17.52 % (4070986)Time elapsed: 1.623 s % 117.80/17.52 % (4070986)Peak memory usage: 119 MB % 117.80/17.52 % (4070986)Instructions burned: 2216 (million) % 117.80/17.52 % (4071007)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=4213842874:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2908 on theBenchmark for (2908ds/4093Mi) % 117.80/17.52 % (4071003)Refutation not found, incomplete strategy % 117.80/17.52 % (4071003)------------------------------ % 117.80/17.52 % (4071003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.80/17.52 % (4071003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.80/17.52 % (4071003)CaDiCaL version: 2.1.3 % 117.80/17.52 % (4071003)Termination reason: Refutation not found, incomplete strategy % 117.80/17.52 % (4071003)Time elapsed: 0.450 s % 117.80/17.52 % (4071003)Peak memory usage: 93 MB % 117.80/17.52 % (4071003)Instructions burned: 606 (million) % 117.80/17.52 % (4071003)------------------------------ % 117.80/17.52 % (4071003)------------------------------ % 117.80/17.52 % (4071002)Instruction limit reached! % 117.80/17.52 % (4071002)------------------------------ % 117.80/17.52 % (4071002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.80/17.52 % (4071002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.80/17.52 % (4071002)CaDiCaL version: 2.1.3 % 117.80/17.52 % (4071002)Termination reason: Instruction limit % 117.80/17.52 % (4071002)Termination phase: Saturation % 117.80/17.52 % (4071002)Time elapsed: 1.209 s % 117.80/17.52 % (4071002)Peak memory usage: 91 MB % 117.80/17.52 % (4071002)Instructions burned: 3553 (million) % 117.80/17.52 % (4071011)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=3436218842:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2900 on theBenchmark for (2900ds/21173Mi) % 117.80/17.52 % (4071011)Refutation not found, incomplete strategy % 117.80/17.52 % (4071011)------------------------------ % 117.80/17.52 % (4071011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.80/17.52 % (4071011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.80/17.52 % (4071011)CaDiCaL version: 2.1.3 % 117.80/17.52 % (4071011)Termination reason: Refutation not found, incomplete strategy % 117.80/17.52 % (4071011)Time elapsed: 0.066 s % 117.80/17.52 % (4071011)Peak memory usage: 112 MB % 117.80/17.52 % (4071011)Instructions burned: 41 (million) % 117.80/17.52 % (4071012)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3341798541:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2898 on theBenchmark for (2898ds/10544Mi) % 117.80/17.52 % (4071001)Instruction limit reached! % 117.80/17.52 % (4071001)------------------------------ % 117.80/17.52 % (4071001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.80/17.52 % (4071001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.41/19.90 % (4071001)CaDiCaL version: 2.1.3 % 134.41/19.90 % (4071001)Termination reason: Instruction limit % 134.41/19.90 % (4071001)Termination phase: Saturation % 134.41/19.90 % (4071001)Time elapsed: 1.436 s % 134.41/19.90 % (4071001)Peak memory usage: 119 MB % 134.41/19.90 % (4071001)Instructions burned: 1959 (million) % 134.41/19.90 % (4071015)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1096037322:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2896 on theBenchmark for (2896ds/1262Mi) % 134.41/19.90 % (4071011)------------------------------ % 134.41/19.90 % (4071011)------------------------------ % 134.41/19.90 % (4070993)Instruction limit reached! % 134.41/19.90 % (4070993)------------------------------ % 134.41/19.90 % (4070993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.41/19.90 % (4070993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.41/19.90 % (4070993)CaDiCaL version: 2.1.3 % 134.41/19.90 % (4070993)Termination reason: Instruction limit % 134.41/19.90 % (4070993)Termination phase: Saturation % 134.41/19.90 % (4070993)Time elapsed: 2.434 s % 134.41/19.90 % (4070993)Peak memory usage: 89 MB % 134.41/19.90 % (4070993)Instructions burned: 3510 (million) % 134.41/19.90 % (4071017)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=1852474504:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2893 on theBenchmark for (2893ds/775Mi) % 134.41/19.90 % (4071018)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3565524819:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2892 on theBenchmark for (2892ds/270Mi) % 134.41/19.90 % (4071017)Refutation not found, incomplete strategy % 134.41/19.90 % (4071017)------------------------------ % 134.41/19.90 % (4071017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.41/19.90 % (4071017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.41/19.90 % (4071017)CaDiCaL version: 2.1.3 % 134.41/19.90 % (4071017)Termination reason: Refutation not found, incomplete strategy % 134.41/19.90 % (4071017)Time elapsed: 0.056 s % 134.41/19.90 % (4071017)Peak memory usage: 88 MB % 134.41/19.90 % (4071017)Instructions burned: 74 (million) % 134.41/19.90 % (4071018)Instruction limit reached! % 134.41/19.90 % (4071018)------------------------------ % 134.41/19.90 % (4071018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.41/19.90 % (4071018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.41/19.90 % (4071018)CaDiCaL version: 2.1.3 % 134.41/19.90 % (4071018)Termination reason: Instruction limit % 134.41/19.90 % (4071018)Termination phase: Saturation % 134.41/19.90 % (4071018)Time elapsed: 0.203 s % 134.41/19.90 % (4071018)Peak memory usage: 90 MB % 134.41/19.90 % (4071018)Instructions burned: 270 (million) % 134.41/19.90 % (4071017)------------------------------ % 134.41/19.90 % (4071017)------------------------------ % 134.41/19.90 % (4071021)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3608974759:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2888 on theBenchmark for (2888ds/17165Mi) % 134.41/19.90 % (4071015)Instruction limit reached! % 134.41/19.90 % (4071015)------------------------------ % 134.41/19.90 % (4071015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.41/19.90 % (4071015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.41/19.90 % (4071015)CaDiCaL version: 2.1.3 % 134.41/19.90 % (4071015)Termination reason: Instruction limit % 134.41/19.90 % (4071015)Termination phase: Saturation % 134.41/19.90 % (4071015)Time elapsed: 0.934 s % 134.41/19.90 % (4071015)Peak memory usage: 119 MB % 134.41/19.90 % (4071015)Instructions burned: 1262 (million) % 134.41/19.90 % (4070985)Instruction limit reached! % 134.41/19.90 % (4070985)------------------------------ % 134.41/19.90 % (4070985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.41/19.90 % (4070985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.41/19.90 % (4070985)CaDiCaL version: 2.1.3 % 134.41/19.90 % (4070985)Termination reason: Instruction limit % 134.41/19.90 % (4070985)Termination phase: Saturation % 134.41/19.90 % (4070985)Time elapsed: 4.207 s % 134.41/19.90 % (4070985)Peak memory usage: 119 MB % 134.41/19.90 % (4070985)Instructions burned: 5812 (million) % 134.41/19.90 % (4071022)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=393185311:s2a=on:i=13094:s2at=-1:rtra=on_2885 on theBenchmark for (2885ds/13094Mi) % 134.41/19.90 % (4071024)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2511987730:st=2:i=12633:rtra=on:ss=axioms_2883 on theBenchmark for (2883ds/12633Mi) % 153.90/22.62 % (4071024)Refutation not found, incomplete strategy % 153.90/22.62 % (4071024)------------------------------ % 153.90/22.62 % (4071024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.90/22.62 % (4071024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.90/22.62 % (4071024)CaDiCaL version: 2.1.3 % 153.90/22.62 % (4071024)Termination reason: Refutation not found, incomplete strategy % 153.90/22.62 % (4071024)Time elapsed: 0.050 s % 153.90/22.62 % (4071024)Peak memory usage: 87 MB % 153.90/22.62 % (4071024)Instructions burned: 65 (million) % 153.90/22.62 % (4071025)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3384918657:i=1783:rtra=on:gtg=position_2882 on theBenchmark for (2882ds/1783Mi) % 153.90/22.62 % (4071024)------------------------------ % 153.90/22.62 % (4071024)------------------------------ % 153.90/22.62 % (4071007)Instruction limit reached! % 153.90/22.62 % (4071007)------------------------------ % 153.90/22.62 % (4071007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.90/22.62 % (4071007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.90/22.62 % (4071007)CaDiCaL version: 2.1.3 % 153.90/22.62 % (4071007)Termination reason: Instruction limit % 153.90/22.62 % (4071007)Termination phase: Saturation % 153.90/22.62 % (4071007)Time elapsed: 2.957 s % 153.90/22.62 % (4071007)Peak memory usage: 136 MB % 153.90/22.62 % (4071007)Instructions burned: 4094 (million) % 153.90/22.62 % (4071029)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=139251289:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2876 on theBenchmark for (2876ds/5451Mi) % 153.90/22.62 % (4071030)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1519092932:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2875 on theBenchmark for (2875ds/4975Mi) % 153.90/22.62 % (4071025)Instruction limit reached! % 153.90/22.62 % (4071025)------------------------------ % 153.90/22.62 % (4071025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.90/22.62 % (4071025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.90/22.62 % (4071025)CaDiCaL version: 2.1.3 % 153.90/22.62 % (4071025)Termination reason: Instruction limit % 153.90/22.62 % (4071025)Termination phase: Saturation % 153.90/22.62 % (4071025)Time elapsed: 1.319 s % 153.90/22.62 % (4071025)Peak memory usage: 119 MB % 153.90/22.62 % (4071025)Instructions burned: 1784 (million) % 153.90/22.62 % (4071035)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=3350644484:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2866 on theBenchmark for (2866ds/2076Mi) % 153.90/22.62 % (4071035)Instruction limit reached! % 153.90/22.62 % (4071035)------------------------------ % 153.90/22.62 % (4071035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.90/22.62 % (4071035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.90/22.62 % (4071035)CaDiCaL version: 2.1.3 % 153.90/22.62 % (4071035)Termination reason: Instruction limit % 153.90/22.62 % (4071035)Termination phase: Saturation % 153.90/22.62 % (4071035)Time elapsed: 1.478 s % 153.90/22.62 % (4071035)Peak memory usage: 119 MB % 153.90/22.62 % (4071035)Instructions burned: 2076 (million) % 153.90/22.62 % (4071037)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=4073498773:i=5145:rtra=on_2849 on theBenchmark for (2849ds/5145Mi) % 153.90/22.62 % (4071029)Instruction limit reached! % 153.90/22.62 % (4071029)------------------------------ % 153.90/22.62 % (4071029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.90/22.62 % (4071029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.90/22.62 % (4071029)CaDiCaL version: 2.1.3 % 153.90/22.62 % (4071029)Termination reason: Instruction limit % 153.90/22.62 % (4071029)Termination phase: Saturation % 153.90/22.62 % (4071029)Time elapsed: 3.865 s % 153.90/22.62 % (4071029)Peak memory usage: 120 MB % 153.90/22.62 % (4071029)Instructions burned: 5451 (million) % 153.90/22.62 % (4071039)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=858143758:i=3509:rtra=on_2835 on theBenchmark for (2835ds/3509Mi) % 153.90/22.62 % (4071030)Instruction limit reached! % 153.90/22.62 % (4071030)------------------------------ % 153.90/22.62 % (4071030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.36 % (4071030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.36 % (4071030)CaDiCaL version: 2.1.3 % 244.80/35.36 % (4071030)Termination reason: Instruction limit % 244.80/35.36 % (4071030)Termination phase: Saturation % 244.80/35.36 % (4071030)Time elapsed: 4.116 s % 244.80/35.36 % (4071030)Peak memory usage: 131 MB % 244.80/35.36 % (4071030)Instructions burned: 4975 (million) % 244.80/35.36 % (4071041)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=3001213432:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2831 on theBenchmark for (2831ds/13800Mi) % 244.80/35.36 % (4071041)Refutation not found, incomplete strategy % 244.80/35.36 % (4071041)------------------------------ % 244.80/35.36 % (4071041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.36 % (4071041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.36 % (4071041)CaDiCaL version: 2.1.3 % 244.80/35.36 % (4071041)Termination reason: Refutation not found, incomplete strategy % 244.80/35.36 % (4071041)Time elapsed: 0.053 s % 244.80/35.36 % (4071041)Peak memory usage: 88 MB % 244.80/35.36 % (4071041)Instructions burned: 70 (million) % 244.80/35.36 % (4071041)------------------------------ % 244.80/35.36 % (4071041)------------------------------ % 244.80/35.36 % (4071043)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3796571290:i=1412:rtra=on:fsd=on:proc=on_2824 on theBenchmark for (2824ds/1412Mi) % 244.80/35.36 % (4071043)Instruction limit reached! % 244.80/35.36 % (4071043)------------------------------ % 244.80/35.36 % (4071043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.36 % (4071043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.36 % (4071043)CaDiCaL version: 2.1.3 % 244.80/35.36 % (4071043)Termination reason: Instruction limit % 244.80/35.36 % (4071043)Termination phase: Saturation % 244.80/35.36 % (4071043)Time elapsed: 1.059 s % 244.80/35.36 % (4071043)Peak memory usage: 119 MB % 244.80/35.36 % (4071043)Instructions burned: 1413 (million) % 244.80/35.36 % (4071012)Instruction limit reached! % 244.80/35.36 % (4071012)------------------------------ % 244.80/35.36 % (4071012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.36 % (4071012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.36 % (4071012)CaDiCaL version: 2.1.3 % 244.80/35.36 % (4071012)Termination reason: Instruction limit % 244.80/35.36 % (4071012)Termination phase: Saturation % 244.80/35.36 % (4071012)Time elapsed: 8.582 s % 244.80/35.36 % (4071012)Peak memory usage: 166 MB % 244.80/35.36 % (4071012)Instructions burned: 10545 (million) % 244.80/35.36 % (4071037)Instruction limit reached! % 244.80/35.36 % (4071037)------------------------------ % 244.80/35.36 % (4071037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.36 % (4071037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.36 % (4071037)CaDiCaL version: 2.1.3 % 244.80/35.36 % (4071037)Termination reason: Instruction limit % 244.80/35.36 % (4071037)Termination phase: Saturation % 244.80/35.36 % (4071037)Time elapsed: 3.626 s % 244.80/35.36 % (4071037)Peak memory usage: 95 MB % 244.80/35.36 % (4071037)Instructions burned: 5145 (million) % 244.80/35.36 % (4071049)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 244.80/35.36 % (4071039)Instruction limit reached! % 244.80/35.36 % (4071039)------------------------------ % 244.80/35.36 % (4071039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.80/35.36 % (4071039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.80/35.36 % (4071039)CaDiCaL version: 2.1.3 % 244.80/35.36 % (4071039)Termination reason: Instruction limit % 244.80/35.36 % (4071039)Termination phase: Saturation % 244.80/35.36 % (4071039)Time elapsed: 2.404 s % 244.80/35.36 % (4071039)Peak memory usage: 89 MB % 244.80/35.36 % (4071039)Instructions burned: 3509 (million) % 244.80/35.36 % (4071049)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3753652210:i=11747:aac=none:nm=0:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/11747Mi) % 244.80/35.36 % (4071051)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=780857364:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2810 on theBenchmark for (2810ds/3201Mi) % 244.80/35.36 % (4071050)lrs+1010_1_to=kbo:sil=128000:sTerminated %------------------------------------------------------------------------------