%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX141_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n010.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:58 PM UTC 2026 % Result : Timeout 286.85s 41.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX141_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n010.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 15:05:02 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.52/1.52 % (1990949)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.52/1.52 % (1991001)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=386005509:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2996 on theBenchmark for (2996ds/12Mi) % 3.52/1.52 % (1991001)Instruction limit reached! % 3.52/1.52 % (1991001)------------------------------ % 3.52/1.52 % (1991001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.52 % (1991001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.52 % (1991001)CaDiCaL version: 2.1.3 % 3.52/1.52 % (1991001)Termination reason: Instruction limit % 3.52/1.52 % (1991001)Termination phase: Property scanning % 3.52/1.52 % (1991001)Time elapsed: 0.003 s % 3.52/1.52 % (1991001)Peak memory usage: 85 MB % 3.52/1.52 % (1991001)Instructions burned: 15 (million) % 3.52/1.52 % (1991004)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=83510668:s2a=on:i=7:rtra=on:inst=on_2996 on theBenchmark for (2996ds/7Mi) % 3.52/1.52 % (1991005)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3175801863:i=4:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 3.52/1.52 % (1991002)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=322398364:i=307:kws=precedence:nm=0:rtra=on_2996 on theBenchmark for (2996ds/307Mi) % 3.52/1.52 % (1991006)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3766473143:i=46:rtra=on_2996 on theBenchmark for (2996ds/46Mi) % 3.52/1.52 % (1991007)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3371410621:i=33:rtra=on_2996 on theBenchmark for (2996ds/33Mi) % 3.52/1.52 % (1991003)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1066670786:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/201Mi) % 3.52/1.52 % (1991005)Instruction limit reached! % 3.52/1.52 % (1991005)------------------------------ % 3.52/1.52 % (1991005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.52 % (1991005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.52 % (1991005)CaDiCaL version: 2.1.3 % 3.52/1.52 % (1991005)Termination reason: Instruction limit % 3.52/1.52 % (1991005)Termination phase: shuffling % 3.52/1.52 % (1991005)Time elapsed: 0.002 s % 3.52/1.52 % (1991005)Peak memory usage: 85 MB % 3.52/1.52 % (1991005)Instructions burned: 4 (million) % 3.52/1.52 % (1991004)Instruction limit reached! % 3.52/1.52 % (1991004)------------------------------ % 3.52/1.52 % (1991004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.52 % (1991004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.52 % (1991004)CaDiCaL version: 2.1.3 % 3.52/1.52 % (1991004)Termination reason: Instruction limit % 3.52/1.52 % (1991004)Termination phase: shuffling % 3.52/1.52 % (1991004)Time elapsed: 0.003 s % 3.52/1.52 % (1991004)Peak memory usage: 85 MB % 3.52/1.52 % (1991004)Instructions burned: 7 (million) % 3.52/1.52 % (1991007)Instruction limit reached! % 3.52/1.52 % (1991007)------------------------------ % 3.52/1.52 % (1991007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.52 % (1991007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.52 % (1991007)CaDiCaL version: 2.1.3 % 3.52/1.52 % (1991007)Termination reason: Instruction limit % 3.52/1.52 % (1991007)Termination phase: Property scanning % 3.52/1.52 % (1991007)Time elapsed: 0.014 s % 3.52/1.52 % (1991007)Peak memory usage: 85 MB % 3.52/1.52 % (1991007)Instructions burned: 33 (million) % 3.52/1.52 % (1991006)Instruction limit reached! % 3.52/1.52 % (1991006)------------------------------ % 3.52/1.52 % (1991006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.52 % (1991006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.52 % (1991006)CaDiCaL version: 2.1.3 % 3.52/1.52 % (1991006)Termination reason: Instruction limit % 3.52/1.52 % (1991006)Termination phase: Property scanning % 3.52/1.52 % (1991006)Time elapsed: 0.019 s % 3.52/1.52 % (1991006)Peak memory usage: 85 MB % 3.52/1.52 % (1991006)Instructions burned: 49 (million) % 3.52/1.52 % (1991003)Instruction limit reached! % 3.52/1.52 % (1991003)------------------------------ % 3.52/1.52 % (1991003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.52 % (1991003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.13/1.67 % (1991003)CaDiCaL version: 2.1.3 % 4.13/1.67 % (1991003)Termination reason: Instruction limit % 4.13/1.67 % (1991003)Termination phase: Property scanning % 4.13/1.67 % (1991003)Time elapsed: 0.074 s % 4.13/1.67 % (1991003)Peak memory usage: 85 MB % 4.13/1.67 % (1991003)Instructions burned: 201 (million) % 4.13/1.67 % (1991009)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=813044:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2994 on theBenchmark for (2994ds/14Mi) % 4.13/1.67 % (1991009)Instruction limit reached! % 4.13/1.67 % (1991009)------------------------------ % 4.13/1.67 % (1991009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.13/1.67 % (1991009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.13/1.67 % (1991009)CaDiCaL version: 2.1.3 % 4.13/1.67 % (1991009)Termination reason: Instruction limit % 4.13/1.67 % (1991009)Termination phase: shuffling % 4.13/1.67 % (1991009)Time elapsed: 0.004 s % 4.13/1.67 % (1991009)Peak memory usage: 85 MB % 4.13/1.67 % (1991009)Instructions burned: 18 (million) % 4.13/1.67 % (1991002)Instruction limit reached! % 4.13/1.67 % (1991002)------------------------------ % 4.13/1.67 % (1991002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.13/1.67 % (1991002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.13/1.67 % (1991002)CaDiCaL version: 2.1.3 % 4.13/1.67 % (1991002)Termination reason: Instruction limit % 4.13/1.67 % (1991002)Termination phase: Saturation % 4.13/1.67 % (1991002)Time elapsed: 0.136 s % 4.13/1.67 % (1991002)Peak memory usage: 112 MB % 4.13/1.67 % (1991002)Instructions burned: 309 (million) % 4.13/1.67 % (1991018)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4192716746:i=24:canc=force:rtra=on_2994 on theBenchmark for (2994ds/24Mi) % 4.13/1.67 % (1991019)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=2028767747:i=27:canc=cautious:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/27Mi) % 4.13/1.67 % (1991017)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1994108767:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/16Mi) % 4.13/1.67 % (1991016)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=3791425629:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2994 on theBenchmark for (2994ds/29Mi) % 4.13/1.67 % (1991017)Instruction limit reached! % 4.13/1.67 % (1991017)------------------------------ % 4.13/1.67 % (1991017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.13/1.67 % (1991017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.13/1.67 % (1991017)CaDiCaL version: 2.1.3 % 4.13/1.67 % (1991017)Termination reason: Instruction limit % 4.13/1.67 % (1991017)Termination phase: shuffling % 4.13/1.67 % (1991017)Time elapsed: 0.008 s % 4.13/1.67 % (1991017)Peak memory usage: 85 MB % 4.13/1.67 % (1991017)Instructions burned: 18 (million) % 4.13/1.67 % (1991018)Instruction limit reached! % 4.13/1.67 % (1991018)------------------------------ % 4.13/1.67 % (1991018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.13/1.67 % (1991018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.13/1.67 % (1991018)CaDiCaL version: 2.1.3 % 4.13/1.67 % (1991018)Termination reason: Instruction limit % 4.13/1.67 % (1991018)Termination phase: Property scanning % 4.13/1.67 % (1991018)Time elapsed: 0.011 s % 4.13/1.67 % (1991018)Peak memory usage: 85 MB % 4.13/1.67 % (1991018)Instructions burned: 26 (million) % 4.13/1.67 % (1991019)Instruction limit reached! % 4.13/1.67 % (1991019)------------------------------ % 4.13/1.67 % (1991019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.13/1.67 % (1991019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.13/1.67 % (1991019)CaDiCaL version: 2.1.3 % 4.13/1.67 % (1991019)Termination reason: Instruction limit % 4.13/1.67 % (1991019)Termination phase: Property scanning % 4.13/1.67 % (1991019)Time elapsed: 0.012 s % 4.13/1.67 % (1991019)Peak memory usage: 85 MB % 4.13/1.67 % (1991019)Instructions burned: 28 (million) % 4.13/1.67 % (1991016)Instruction limit reached! % 4.13/1.67 % (1991016)------------------------------ % 4.13/1.67 % (1991016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.13/1.67 % (1991016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.23/1.83 % (1991016)CaDiCaL version: 2.1.3 % 5.23/1.83 % (1991016)Termination reason: Instruction limit % 5.23/1.83 % (1991016)Termination phase: Property scanning % 5.23/1.83 % (1991016)Time elapsed: 0.013 s % 5.23/1.83 % (1991016)Peak memory usage: 85 MB % 5.23/1.83 % (1991016)Instructions burned: 31 (million) % 5.23/1.83 % (1991022)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=4135039182:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2993 on theBenchmark for (2993ds/2Mi) % 5.23/1.83 % (1991022)Instruction limit reached! % 5.23/1.83 % (1991022)------------------------------ % 5.23/1.83 % (1991022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.23/1.83 % (1991022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.23/1.83 % (1991022)CaDiCaL version: 2.1.3 % 5.23/1.83 % (1991022)Termination reason: Instruction limit % 5.23/1.83 % (1991022)Termination phase: shuffling % 5.23/1.83 % (1991022)Time elapsed: 0.001 s % 5.23/1.83 % (1991022)Peak memory usage: 85 MB % 5.23/1.83 % (1991022)Instructions burned: 4 (million) % 5.23/1.83 % (1991020)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4188987438:i=85:gtgl=4:rtra=on:gtg=exists_sym_2993 on theBenchmark for (2993ds/85Mi) % 5.23/1.83 % (1991020)Instruction limit reached! % 5.23/1.83 % (1991020)------------------------------ % 5.23/1.83 % (1991020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.23/1.83 % (1991020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.23/1.83 % (1991020)CaDiCaL version: 2.1.3 % 5.23/1.83 % (1991020)Termination reason: Instruction limit % 5.23/1.83 % (1991020)Termination phase: Property scanning % 5.23/1.83 % (1991020)Time elapsed: 0.032 s % 5.23/1.83 % (1991020)Peak memory usage: 85 MB % 5.23/1.83 % (1991020)Instructions burned: 88 (million) % 5.23/1.83 % (1991023)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=400924584:i=181:rtra=on:ss=axioms:ev=cautious_2993 on theBenchmark for (2993ds/181Mi) % 5.23/1.83 % (1991028)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4203517154:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi) % 5.23/1.83 % (1991029)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=253799984:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2992 on theBenchmark for (2992ds/66Mi) % 5.23/1.83 % (1991028)Instruction limit reached! % 5.23/1.83 % (1991028)------------------------------ % 5.23/1.83 % (1991028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.23/1.83 % (1991028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.23/1.83 % (1991028)CaDiCaL version: 2.1.3 % 5.23/1.83 % (1991028)Termination reason: Instruction limit % 5.23/1.83 % (1991028)Termination phase: shuffling % 5.23/1.83 % (1991028)Time elapsed: 0.002 s % 5.23/1.83 % (1991028)Peak memory usage: 85 MB % 5.23/1.83 % (1991028)Instructions burned: 4 (million) % 5.23/1.83 % (1991034)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=3637522388:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi) % 5.23/1.83 % (1991034)Instruction limit reached! % 5.23/1.83 % (1991034)------------------------------ % 5.23/1.83 % (1991034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.23/1.83 % (1991034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.23/1.83 % (1991034)CaDiCaL version: 2.1.3 % 5.23/1.83 % (1991034)Termination reason: Instruction limit % 5.23/1.83 % (1991034)Termination phase: shuffling % 5.23/1.83 % (1991034)Time elapsed: 0.001 s % 5.23/1.83 % (1991034)Peak memory usage: 85 MB % 5.23/1.83 % (1991034)Instructions burned: 4 (million) % 5.23/1.83 % (1991030)lrs+10_1_thi=all:si=on:fd=off:random_seed=1059292106:i=53:rtra=on:gtg=all_2992 on theBenchmark for (2992ds/53Mi) % 5.23/1.83 % (1991031)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=3848867304:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/8Mi) % 5.23/1.83 % (1991029)Instruction limit reached! % 5.23/1.83 % (1991029)------------------------------ % 5.23/1.83 % (1991029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.23/1.83 % (1991029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.23/1.83 % (1991029)CaDiCaL version: 2.1.3 % 5.23/1.83 % (1991029)Termination reason: Instruction limit % 6.40/2.00 % (1991029)Termination phase: Property scanning % 6.40/2.00 % (1991029)Time elapsed: 0.026 s % 6.40/2.00 % (1991029)Peak memory usage: 85 MB % 6.40/2.00 % (1991029)Instructions burned: 67 (million) % 6.40/2.00 % (1991031)Instruction limit reached! % 6.40/2.00 % (1991031)------------------------------ % 6.40/2.00 % (1991031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.40/2.00 % (1991031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.40/2.00 % (1991031)CaDiCaL version: 2.1.3 % 6.40/2.00 % (1991031)Termination reason: Instruction limit % 6.40/2.00 % (1991031)Termination phase: Property scanning % 6.40/2.00 % (1991031)Time elapsed: 0.004 s % 6.40/2.00 % (1991031)Peak memory usage: 85 MB % 6.40/2.00 % (1991031)Instructions burned: 11 (million) % 6.40/2.00 % (1991030)Instruction limit reached! % 6.40/2.00 % (1991030)------------------------------ % 6.40/2.00 % (1991030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.40/2.00 % (1991030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.40/2.00 % (1991030)CaDiCaL version: 2.1.3 % 6.40/2.00 % (1991030)Termination reason: Instruction limit % 6.40/2.00 % (1991030)Termination phase: Property scanning % 6.40/2.00 % (1991030)Time elapsed: 0.020 s % 6.40/2.00 % (1991030)Peak memory usage: 85 MB % 6.40/2.00 % (1991030)Instructions burned: 54 (million) % 6.40/2.00 % (1991023)Refutation not found, incomplete strategy % 6.40/2.00 % (1991023)------------------------------ % 6.40/2.00 % (1991023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.40/2.00 % (1991023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.40/2.00 % (1991023)CaDiCaL version: 2.1.3 % 6.40/2.00 % (1991023)Termination reason: Refutation not found, incomplete strategy % 6.40/2.00 % (1991023)Time elapsed: 0.063 s % 6.40/2.00 % (1991023)Peak memory usage: 88 MB % 6.40/2.00 % (1991023)Instructions burned: 173 (million) % 6.40/2.00 % (1991035)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=971249399:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi) % 6.40/2.00 % (1991035)Instruction limit reached! % 6.40/2.00 % (1991035)------------------------------ % 6.40/2.00 % (1991035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.40/2.00 % (1991035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.40/2.00 % (1991035)CaDiCaL version: 2.1.3 % 6.40/2.00 % (1991035)Termination reason: Instruction limit % 6.40/2.00 % (1991035)Termination phase: shuffling % 6.40/2.00 % (1991035)Time elapsed: 0.002 s % 6.40/2.00 % (1991035)Peak memory usage: 85 MB % 6.40/2.00 % (1991035)Instructions burned: 4 (million) % 6.40/2.00 % (1991043)dis+10_1_si=on:random_seed=3995201365:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi) % 6.40/2.00 % (1991039)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3041719976:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi) % 6.40/2.00 % (1991043)Instruction limit reached! % 6.40/2.00 % (1991043)------------------------------ % 6.40/2.00 % (1991043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.40/2.00 % (1991043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.40/2.00 % (1991043)CaDiCaL version: 2.1.3 % 6.40/2.00 % (1991043)Termination reason: Instruction limit % 6.40/2.00 % (1991043)Termination phase: shuffling % 6.40/2.00 % (1991043)Time elapsed: 0.003 s % 6.40/2.00 % (1991043)Peak memory usage: 85 MB % 6.40/2.00 % (1991043)Instructions burned: 13 (million) % 6.40/2.00 % (1991045)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3515602871: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_2991 on theBenchmark for (2991ds/35Mi) % 6.40/2.00 % (1991044)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2103604151:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi) % 6.40/2.00 % (1991039)Instruction limit reached! % 6.40/2.00 % (1991039)------------------------------ % 6.40/2.00 % (1991039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.40/2.00 % (1991039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.40/2.00 % (1991039)CaDiCaL version: 2.1.3 % 6.40/2.00 % (1991039)Termination reason: Instruction limit % 6.40/2.00 % (1991039)Termination phase: Property scanning % 6.40/2.00 % (1991039)Time elapsed: 0.048 s % 6.40/2.00 % (1991039)Peak memory usage: 86 MB % 8.17/2.17 % (1991039)Instructions burned: 128 (million) % 8.17/2.17 % (1991044)Instruction limit reached! % 8.17/2.17 % (1991044)------------------------------ % 8.17/2.17 % (1991044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.17/2.17 % (1991044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/2.17 % (1991044)CaDiCaL version: 2.1.3 % 8.17/2.17 % (1991044)Termination reason: Instruction limit % 8.17/2.17 % (1991044)Termination phase: Property scanning % 8.17/2.17 % (1991044)Time elapsed: 0.012 s % 8.17/2.17 % (1991044)Peak memory usage: 85 MB % 8.17/2.17 % (1991044)Instructions burned: 28 (million) % 8.17/2.17 % (1991045)Instruction limit reached! % 8.17/2.17 % (1991045)------------------------------ % 8.17/2.17 % (1991045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.17/2.17 % (1991045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/2.17 % (1991045)CaDiCaL version: 2.1.3 % 8.17/2.17 % (1991045)Termination reason: Instruction limit % 8.17/2.17 % (1991045)Termination phase: Property scanning % 8.17/2.17 % (1991045)Time elapsed: 0.015 s % 8.17/2.17 % (1991045)Peak memory usage: 85 MB % 8.17/2.17 % (1991045)Instructions burned: 36 (million) % 8.17/2.17 % (1991046)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2340076007:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi) % 8.17/2.17 % (1991046)Instruction limit reached! % 8.17/2.17 % (1991046)------------------------------ % 8.17/2.17 % (1991046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.17/2.17 % (1991046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/2.17 % (1991046)CaDiCaL version: 2.1.3 % 8.17/2.17 % (1991046)Termination reason: Instruction limit % 8.17/2.17 % (1991046)Termination phase: shuffling % 8.17/2.17 % (1991046)Time elapsed: 0.002 s % 8.17/2.17 % (1991046)Peak memory usage: 85 MB % 8.17/2.17 % (1991046)Instructions burned: 4 (million) % 8.17/2.17 % (1991051)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1275865463:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi) % 8.17/2.17 % (1991048)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3345136712:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi) % 8.17/2.17 % (1991048)Instruction limit reached! % 8.17/2.17 % (1991048)------------------------------ % 8.17/2.17 % (1991048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.17/2.17 % (1991048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/2.17 % (1991048)CaDiCaL version: 2.1.3 % 8.17/2.17 % (1991048)Termination reason: Instruction limit % 8.17/2.17 % (1991048)Termination phase: shuffling % 8.17/2.17 % (1991048)Time elapsed: 0.004 s % 8.17/2.17 % (1991048)Peak memory usage: 85 MB % 8.17/2.17 % (1991048)Instructions burned: 10 (million) % 8.17/2.17 % (1991023)------------------------------ % 8.17/2.17 % (1991023)------------------------------ % 8.17/2.17 % (1991051)Instruction limit reached! % 8.17/2.17 % (1991051)------------------------------ % 8.17/2.17 % (1991051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.17/2.17 % (1991051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/2.17 % (1991051)CaDiCaL version: 2.1.3 % 8.17/2.17 % (1991051)Termination reason: Instruction limit % 8.17/2.17 % (1991051)Termination phase: Saturation % 8.17/2.17 % (1991051)Time elapsed: 0.071 s % 8.17/2.17 % (1991051)Peak memory usage: 88 MB % 8.17/2.17 % (1991051)Instructions burned: 372 (million) % 8.17/2.17 % (1991054)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1022807129:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi) % 8.17/2.17 % (1991055)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4157052124:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi) % 8.17/2.17 % (1991054)Instruction limit reached! % 8.17/2.17 % (1991054)------------------------------ % 8.17/2.17 % (1991054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.17/2.17 % (1991054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.17/2.17 % (1991054)CaDiCaL version: 2.1.3 % 8.17/2.17 % (1991054)Termination reason: Instruction limit % 8.17/2.17 % (1991054)Termination phase: Property scanning % 8.17/2.17 % (1991054)Time elapsed: 0.006 s % 8.17/2.17 % (1991054)Peak memory usage: 85 MB % 8.88/2.35 % (1991054)Instructions burned: 16 (million) % 8.88/2.35 % (1991056)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3966361791:i=10:rtra=on_2989 on theBenchmark for (2989ds/10Mi) % 8.88/2.35 % (1991056)Instruction limit reached! % 8.88/2.35 % (1991056)------------------------------ % 8.88/2.35 % (1991056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.88/2.35 % (1991056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.88/2.35 % (1991056)CaDiCaL version: 2.1.3 % 8.88/2.35 % (1991056)Termination reason: Instruction limit % 8.88/2.35 % (1991056)Termination phase: shuffling % 8.88/2.35 % (1991056)Time elapsed: 0.005 s % 8.88/2.35 % (1991056)Peak memory usage: 85 MB % 8.88/2.35 % (1991056)Instructions burned: 12 (million) % 8.88/2.35 % (1991058)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1659424287:i=71:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/71Mi) % 8.88/2.35 % (1991058)Instruction limit reached! % 8.88/2.35 % (1991058)------------------------------ % 8.88/2.35 % (1991058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.88/2.35 % (1991058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.88/2.35 % (1991058)CaDiCaL version: 2.1.3 % 8.88/2.35 % (1991058)Termination reason: Instruction limit % 8.88/2.35 % (1991058)Termination phase: Property scanning % 8.88/2.35 % (1991058)Time elapsed: 0.027 s % 8.88/2.35 % (1991058)Peak memory usage: 85 MB % 8.88/2.35 % (1991058)Instructions burned: 73 (million) % 8.88/2.35 % (1991061)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=1559528963:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi) % 8.88/2.35 % (1991055)Instruction limit reached! % 8.88/2.35 % (1991055)------------------------------ % 8.88/2.35 % (1991055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.88/2.35 % (1991055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.88/2.35 % (1991055)CaDiCaL version: 2.1.3 % 8.88/2.35 % (1991055)Termination reason: Instruction limit % 8.88/2.35 % (1991055)Termination phase: Property scanning % 8.88/2.35 % (1991055)Time elapsed: 0.085 s % 8.88/2.35 % (1991055)Peak memory usage: 85 MB % 8.88/2.35 % (1991055)Instructions burned: 228 (million) % 8.88/2.35 % (1991063)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=346416750:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi) % 8.88/2.35 % (1991062)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=3003772205:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2988 on theBenchmark for (2988ds/294Mi) % 8.88/2.35 % (1991061)Instruction limit reached! % 8.88/2.35 % (1991061)------------------------------ % 8.88/2.35 % (1991061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.88/2.35 % (1991061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.88/2.35 % (1991061)CaDiCaL version: 2.1.3 % 8.88/2.35 % (1991061)Termination reason: Instruction limit % 8.88/2.35 % (1991061)Termination phase: Property scanning % 8.88/2.35 % (1991061)Time elapsed: 0.030 s % 8.88/2.35 % (1991061)Peak memory usage: 86 MB % 8.88/2.35 % (1991061)Instructions burned: 77 (million) % 8.88/2.35 % (1991063)Instruction limit reached! % 8.88/2.35 % (1991063)------------------------------ % 8.88/2.35 % (1991063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.88/2.35 % (1991063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.88/2.35 % (1991063)CaDiCaL version: 2.1.3 % 8.88/2.35 % (1991063)Termination reason: Instruction limit % 8.88/2.35 % (1991063)Termination phase: Property scanning % 8.88/2.35 % (1991063)Time elapsed: 0.026 s % 8.88/2.35 % (1991063)Peak memory usage: 85 MB % 8.88/2.35 % (1991063)Instructions burned: 134 (million) % 8.88/2.35 % (1991066)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3055287330:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi) % 8.88/2.35 % (1991069)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2172530302:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/40Mi) % 8.88/2.35 % (1991069)Instruction limit reached! % 8.88/2.35 % (1991069)------------------------------ % 8.88/2.35 % (1991069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.96/2.57 % (1991069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.96/2.57 % (1991069)CaDiCaL version: 2.1.3 % 9.96/2.57 % (1991069)Termination reason: Instruction limit % 9.96/2.57 % (1991069)Termination phase: Property scanning % 9.96/2.57 % (1991069)Time elapsed: 0.015 s % 9.96/2.57 % (1991069)Peak memory usage: 85 MB % 9.96/2.57 % (1991069)Instructions burned: 41 (million) % 9.96/2.57 % (1991070)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=462019512:i=307:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/307Mi) % 9.96/2.57 % (1991066)Instruction limit reached! % 9.96/2.57 % (1991066)------------------------------ % 9.96/2.57 % (1991066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.96/2.57 % (1991066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.96/2.57 % (1991066)CaDiCaL version: 2.1.3 % 9.96/2.57 % (1991066)Termination reason: Instruction limit % 9.96/2.57 % (1991066)Termination phase: Property scanning % 9.96/2.57 % (1991066)Time elapsed: 0.049 s % 9.96/2.57 % (1991066)Peak memory usage: 86 MB % 9.96/2.57 % (1991066)Instructions burned: 131 (million) % 9.96/2.57 % (1991062)Instruction limit reached! % 9.96/2.57 % (1991062)------------------------------ % 9.96/2.57 % (1991062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.96/2.57 % (1991062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.96/2.57 % (1991062)CaDiCaL version: 2.1.3 % 9.96/2.57 % (1991062)Termination reason: Instruction limit % 9.96/2.57 % (1991062)Termination phase: Property scanning % 9.96/2.57 % (1991062)Time elapsed: 0.108 s % 9.96/2.57 % (1991062)Peak memory usage: 86 MB % 9.96/2.57 % (1991062)Instructions burned: 296 (million) % 9.96/2.57 % (1991076)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=3908827170:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi) % 9.96/2.57 % (1991072)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1674281620:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/598Mi) % 9.96/2.57 % (1991075)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4240310062:i=131:canc=cautious:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/131Mi) % 9.96/2.57 % (1991076)Instruction limit reached! % 9.96/2.57 % (1991076)------------------------------ % 9.96/2.57 % (1991076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.96/2.57 % (1991076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.96/2.57 % (1991076)CaDiCaL version: 2.1.3 % 9.96/2.57 % (1991076)Termination reason: Instruction limit % 9.96/2.57 % (1991076)Termination phase: Unused predicate definition removal % 9.96/2.57 % (1991076)Time elapsed: 0.052 s % 9.96/2.57 % (1991076)Peak memory usage: 86 MB % 9.96/2.57 % (1991076)Instructions burned: 264 (million) % 9.96/2.57 % (1991070)Instruction limit reached! % 9.96/2.57 % (1991070)------------------------------ % 9.96/2.57 % (1991070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.96/2.57 % (1991070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.96/2.57 % (1991070)CaDiCaL version: 2.1.3 % 9.96/2.57 % (1991070)Termination reason: Instruction limit % 9.96/2.57 % (1991070)Termination phase: Property scanning % 9.96/2.57 % (1991070)Time elapsed: 0.113 s % 9.96/2.57 % (1991070)Peak memory usage: 86 MB % 9.96/2.57 % (1991070)Instructions burned: 307 (million) % 9.96/2.57 % (1991075)Instruction limit reached! % 9.96/2.57 % (1991075)------------------------------ % 9.96/2.57 % (1991075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.96/2.57 % (1991075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.96/2.57 % (1991075)CaDiCaL version: 2.1.3 % 9.96/2.57 % (1991075)Termination reason: Instruction limit % 9.96/2.57 % (1991075)Termination phase: Property scanning % 9.96/2.57 % (1991075)Time elapsed: 0.049 s % 9.96/2.57 % (1991075)Peak memory usage: 86 MB % 9.96/2.57 % (1991075)Instructions burned: 132 (million) % 9.96/2.57 % (1991079)dis+10_1_si=on:random_seed=2798705401:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi) % 9.96/2.57 % (1991081)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3588240847:i=383:fsr=off:rtra=on:ev=force_2986 on theBenchmark for (2986ds/383Mi) % 12.49/2.88 % (1991082)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3087677005:i=141:doe=on:rtra=on_2986 on theBenchmark for (2986ds/141Mi) % 12.49/2.88 % (1991086)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=859302457:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi) % 12.49/2.88 % (1991086)Instruction limit reached! % 12.49/2.88 % (1991086)------------------------------ % 12.49/2.88 % (1991086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.49/2.88 % (1991086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.49/2.88 % (1991086)CaDiCaL version: 2.1.3 % 12.49/2.88 % (1991086)Termination reason: Instruction limit % 12.49/2.88 % (1991086)Termination phase: Property scanning % 12.49/2.88 % (1991086)Time elapsed: 0.014 s % 12.49/2.88 % (1991086)Peak memory usage: 86 MB % 12.49/2.88 % (1991086)Instructions burned: 70 (million) % 12.49/2.88 % (1991082)Instruction limit reached! % 12.49/2.88 % (1991082)------------------------------ % 12.49/2.88 % (1991082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.49/2.88 % (1991082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.49/2.88 % (1991082)CaDiCaL version: 2.1.3 % 12.49/2.88 % (1991082)Termination reason: Instruction limit % 12.49/2.88 % (1991082)Termination phase: Property scanning % 12.49/2.88 % (1991082)Time elapsed: 0.053 s % 12.49/2.88 % (1991082)Peak memory usage: 86 MB % 12.49/2.88 % (1991082)Instructions burned: 141 (million) % 12.49/2.88 % (1991088)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=84895949:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi) % 12.49/2.88 % (1991087)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=139796109:i=121:nm=16:rtra=on_2985 on theBenchmark for (2985ds/121Mi) % 12.49/2.88 % (1991081)Instruction limit reached! % 12.49/2.88 % (1991081)------------------------------ % 12.49/2.88 % (1991081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.49/2.88 % (1991081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.49/2.88 % (1991081)CaDiCaL version: 2.1.3 % 12.49/2.88 % (1991081)Termination reason: Instruction limit % 12.49/2.88 % (1991081)Termination phase: Saturation % 12.49/2.88 % (1991081)Time elapsed: 0.142 s % 12.49/2.88 % (1991081)Peak memory usage: 89 MB % 12.49/2.88 % (1991081)Instructions burned: 385 (million) % 12.49/2.88 % (1991072)Instruction limit reached! % 12.49/2.88 % (1991072)------------------------------ % 12.49/2.88 % (1991072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.49/2.88 % (1991072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.49/2.88 % (1991072)CaDiCaL version: 2.1.3 % 12.49/2.88 % (1991072)Termination reason: Instruction limit % 12.49/2.88 % (1991072)Termination phase: Saturation % 12.49/2.88 % (1991072)Time elapsed: 0.271 s % 12.49/2.88 % (1991072)Peak memory usage: 130 MB % 12.49/2.88 % (1991072)Instructions burned: 599 (million) % 12.49/2.88 % (1991087)Instruction limit reached! % 12.49/2.88 % (1991087)------------------------------ % 12.49/2.88 % (1991087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.49/2.88 % (1991087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.49/2.88 % (1991087)CaDiCaL version: 2.1.3 % 12.49/2.88 % (1991087)Termination reason: Instruction limit % 12.49/2.88 % (1991087)Termination phase: Property scanning % 12.49/2.88 % (1991087)Time elapsed: 0.047 s % 12.49/2.88 % (1991087)Peak memory usage: 85 MB % 12.49/2.88 % (1991087)Instructions burned: 125 (million) % 12.49/2.88 % (1991088)Instruction limit reached! % 12.49/2.88 % (1991088)------------------------------ % 12.49/2.88 % (1991088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.49/2.88 % (1991088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.49/2.88 % (1991088)CaDiCaL version: 2.1.3 % 12.49/2.88 % (1991088)Termination reason: Instruction limit % 12.49/2.88 % (1991088)Termination phase: Property scanning % 12.49/2.88 % (1991088)Time elapsed: 0.049 s % 12.49/2.88 % (1991088)Peak memory usage: 86 MB % 12.49/2.88 % (1991088)Instructions burned: 131 (million) % 12.49/2.88 % (1991093)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=896163639:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi) % 12.49/2.88 % (1991093)Instruction limit reached! % 12.49/2.88 % (1991093)------------------------------ % 15.53/3.16 % (1991093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.53/3.16 % (1991093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.53/3.16 % (1991093)CaDiCaL version: 2.1.3 % 15.53/3.16 % (1991093)Termination reason: Instruction limit % 15.53/3.16 % (1991093)Termination phase: Property scanning % 15.53/3.16 % (1991093)Time elapsed: 0.009 s % 15.53/3.16 % (1991093)Peak memory usage: 86 MB % 15.53/3.16 % (1991093)Instructions burned: 41 (million) % 15.53/3.16 % (1991094)dis+1010_1_to=kbo:si=on:random_seed=2246139808:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi) % 15.53/3.16 % (1991097)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2994578203:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi) % 15.53/3.16 % (1991094)Instruction limit reached! % 15.53/3.16 % (1991094)------------------------------ % 15.53/3.16 % (1991094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.53/3.16 % (1991094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.53/3.16 % (1991094)CaDiCaL version: 2.1.3 % 15.53/3.16 % (1991094)Termination reason: Instruction limit % 15.53/3.16 % (1991094)Termination phase: Property scanning % 15.53/3.16 % (1991094)Time elapsed: 0.064 s % 15.53/3.16 % (1991094)Peak memory usage: 85 MB % 15.53/3.16 % (1991094)Instructions burned: 176 (million) % 15.53/3.16 % (1991102)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=2833119102:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi) % 15.53/3.16 % (1991101)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=92952388:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi) % 15.53/3.16 % (1991099)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4155471906:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi) % 15.53/3.16 % (1991098)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2993263471:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi) % 15.53/3.16 % (1991079)Instruction limit reached! % 15.53/3.16 % (1991079)------------------------------ % 15.53/3.16 % (1991079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.53/3.16 % (1991079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.53/3.16 % (1991079)CaDiCaL version: 2.1.3 % 15.53/3.16 % (1991079)Termination reason: Instruction limit % 15.53/3.16 % (1991079)Termination phase: Saturation % 15.53/3.16 % (1991079)Time elapsed: 0.369 s % 15.53/3.16 % (1991079)Peak memory usage: 89 MB % 15.53/3.16 % (1991079)Instructions burned: 1002 (million) % 15.53/3.16 % (1991102)Refutation not found, incomplete strategy % 15.53/3.16 % (1991102)------------------------------ % 15.53/3.16 % (1991102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.53/3.16 % (1991102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.53/3.16 % (1991102)CaDiCaL version: 2.1.3 % 15.53/3.16 % (1991102)Termination reason: Refutation not found, incomplete strategy % 15.53/3.16 % (1991102)Time elapsed: 0.055 s % 15.53/3.16 % (1991102)Peak memory usage: 88 MB % 15.53/3.16 % (1991102)Instructions burned: 289 (million) % 15.53/3.16 % (1991099)Instruction limit reached! % 15.53/3.16 % (1991099)------------------------------ % 15.53/3.16 % (1991099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.53/3.16 % (1991099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.53/3.16 % (1991099)CaDiCaL version: 2.1.3 % 15.53/3.16 % (1991099)Termination reason: Instruction limit % 15.53/3.16 % (1991099)Termination phase: Property scanning % 15.53/3.16 % (1991099)Time elapsed: 0.079 s % 15.53/3.16 % (1991099)Peak memory usage: 86 MB % 15.53/3.16 % (1991099)Instructions burned: 217 (million) % 15.53/3.16 % (1991097)Instruction limit reached! % 15.53/3.16 % (1991097)------------------------------ % 15.53/3.16 % (1991097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.53/3.16 % (1991097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.53/3.16 % (1991097)CaDiCaL version: 2.1.3 % 15.53/3.16 % (1991097)Termination reason: Instruction limit % 15.53/3.16 % (1991097)Termination phase: Property scanning % 15.53/3.16 % (1991097)Time elapsed: 0.120 s % 15.53/3.16 % (1991097)Peak memory usage: 86 MB % 15.43/3.37 % (1991097)Instructions burned: 330 (million) % 15.43/3.37 % (1991101)Instruction limit reached! % 15.43/3.37 % (1991101)------------------------------ % 15.43/3.37 % (1991101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.43/3.37 % (1991101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.43/3.37 % (1991101)CaDiCaL version: 2.1.3 % 15.43/3.37 % (1991101)Termination reason: Instruction limit % 15.43/3.37 % (1991101)Termination phase: Saturation % 15.43/3.37 % (1991101)Time elapsed: 0.151 s % 15.43/3.37 % (1991101)Peak memory usage: 112 MB % 15.43/3.37 % (1991101)Instructions burned: 350 (million) % 15.43/3.37 % (1991105)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=551183370:i=328:kws=inv_frequency:nm=20:rtra=on_2981 on theBenchmark for (2981ds/328Mi) % 15.43/3.37 % (1991110)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2669435716:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi) % 15.43/3.37 % (1991102)------------------------------ % 15.43/3.37 % (1991102)------------------------------ % 15.43/3.37 % (1991098)Instruction limit reached! % 15.43/3.37 % (1991098)------------------------------ % 15.43/3.37 % (1991098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.43/3.37 % (1991098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.43/3.37 % (1991098)CaDiCaL version: 2.1.3 % 15.43/3.37 % (1991098)Termination reason: Instruction limit % 15.43/3.37 % (1991098)Termination phase: Saturation % 15.43/3.37 % (1991098)Time elapsed: 0.224 s % 15.43/3.37 % (1991098)Peak memory usage: 129 MB % 15.43/3.37 % (1991098)Instructions burned: 483 (million) % 15.43/3.37 % (1991111)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2454727008:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 15.43/3.37 % (1991112)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=3708367970:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi) % 15.43/3.37 % (1991105)Instruction limit reached! % 15.43/3.37 % (1991105)------------------------------ % 15.43/3.37 % (1991105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.43/3.37 % (1991105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.43/3.37 % (1991105)CaDiCaL version: 2.1.3 % 15.43/3.37 % (1991105)Termination reason: Instruction limit % 15.43/3.37 % (1991105)Termination phase: Property scanning % 15.43/3.37 % (1991105)Time elapsed: 0.121 s % 15.43/3.37 % (1991105)Peak memory usage: 86 MB % 15.43/3.37 % (1991105)Instructions burned: 330 (million) % 15.43/3.37 % (1991110)Instruction limit reached! % 15.43/3.37 % (1991110)------------------------------ % 15.43/3.37 % (1991110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.43/3.37 % (1991110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.43/3.37 % (1991110)CaDiCaL version: 2.1.3 % 15.43/3.37 % (1991110)Termination reason: Instruction limit % 15.43/3.37 % (1991110)Termination phase: Property scanning % 15.43/3.37 % (1991110)Time elapsed: 0.105 s % 15.43/3.37 % (1991110)Peak memory usage: 86 MB % 15.43/3.37 % (1991110)Instructions burned: 282 (million) % 15.43/3.37 % (1991114)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3460343415:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi) % 15.43/3.37 % (1991116)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=436602654:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi) % 15.43/3.37 % (1991111)Refutation not found, incomplete strategy % 15.43/3.37 % (1991111)------------------------------ % 15.43/3.37 % (1991111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.43/3.37 % (1991111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.43/3.37 % (1991111)CaDiCaL version: 2.1.3 % 15.43/3.37 % (1991111)Termination reason: Refutation not found, incomplete strategy % 15.43/3.37 % (1991111)Time elapsed: 0.122 s % 15.43/3.37 % (1991111)Peak memory usage: 88 MB % 15.43/3.37 % (1991111)Instructions burned: 282 (million) % 15.43/3.37 % (1991118)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=1629798423:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 15.43/3.37 % (1991112)Refutation not found, incomplete strategy % 17.32/3.62 % (1991112)------------------------------ % 17.32/3.62 % (1991112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.32/3.62 % (1991112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.32/3.62 % (1991112)CaDiCaL version: 2.1.3 % 17.32/3.62 % (1991112)Termination reason: Refutation not found, incomplete strategy % 17.32/3.62 % (1991112)Time elapsed: 0.148 s % 17.32/3.62 % (1991112)Peak memory usage: 112 MB % 17.32/3.62 % (1991112)Instructions burned: 286 (million) % 17.32/3.62 % (1991120)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2583110939:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 17.32/3.62 % (1991114)Refutation not found, incomplete strategy % 17.32/3.62 % (1991114)------------------------------ % 17.32/3.62 % (1991114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.32/3.62 % (1991114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.32/3.62 % (1991114)CaDiCaL version: 2.1.3 % 17.32/3.62 % (1991114)Termination reason: Refutation not found, incomplete strategy % 17.32/3.62 % (1991114)Time elapsed: 0.130 s % 17.32/3.62 % (1991114)Peak memory usage: 112 MB % 17.32/3.62 % (1991114)Instructions burned: 286 (million) % 17.32/3.62 % (1991122)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=3389759851:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi) % 17.32/3.62 % (1991116)Instruction limit reached! % 17.32/3.62 % (1991116)------------------------------ % 17.32/3.62 % (1991116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.32/3.62 % (1991116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.32/3.62 % (1991116)CaDiCaL version: 2.1.3 % 17.32/3.62 % (1991116)Termination reason: Instruction limit % 17.32/3.62 % (1991116)Termination phase: Saturation % 17.32/3.62 % (1991116)Time elapsed: 0.139 s % 17.32/3.62 % (1991116)Peak memory usage: 114 MB % 17.32/3.62 % (1991116)Instructions burned: 472 (million) % 17.32/3.62 % (1991118)Instruction limit reached! % 17.32/3.62 % (1991118)------------------------------ % 17.32/3.62 % (1991118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.32/3.62 % (1991118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.32/3.62 % (1991118)CaDiCaL version: 2.1.3 % 17.32/3.62 % (1991118)Termination reason: Instruction limit % 17.32/3.62 % (1991118)Termination phase: Property scanning % 17.32/3.62 % (1991118)Time elapsed: 0.101 s % 17.32/3.62 % (1991118)Peak memory usage: 86 MB % 17.32/3.62 % (1991118)Instructions burned: 277 (million) % 17.32/3.62 % (1991122)Refutation not found, incomplete strategy % 17.32/3.62 % (1991122)------------------------------ % 17.32/3.62 % (1991122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.32/3.62 % (1991122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.32/3.62 % (1991122)CaDiCaL version: 2.1.3 % 17.32/3.62 % (1991122)Termination reason: Refutation not found, incomplete strategy % 17.32/3.62 % (1991122)Time elapsed: 0.133 s % 17.32/3.62 % (1991122)Peak memory usage: 112 MB % 17.32/3.62 % (1991122)Instructions burned: 302 (million) % 17.32/3.62 % (1991120)Instruction limit reached! % 17.32/3.62 % (1991120)------------------------------ % 17.32/3.62 % (1991120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.32/3.62 % (1991120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.32/3.62 % (1991120)CaDiCaL version: 2.1.3 % 17.32/3.62 % (1991120)Termination reason: Instruction limit % 17.32/3.62 % (1991120)Termination phase: Saturation % 17.32/3.62 % (1991120)Time elapsed: 0.160 s % 17.32/3.62 % (1991120)Peak memory usage: 112 MB % 17.32/3.62 % (1991120)Instructions burned: 375 (million) % 17.32/3.62 % (1991127)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1573444982:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 17.32/3.62 % (1991111)------------------------------ % 17.32/3.62 % (1991111)------------------------------ % 17.32/3.62 % (1991128)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1400951299:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi) % 17.32/3.62 % (1991112)------------------------------ % 17.32/3.62 % (1991112)------------------------------ % 17.32/3.62 % (1991114)------------------------------ % 17.32/3.62 % (1991114)------------------------------ % 17.32/3.62 % (1991127)Instruction limit reached! % 21.93/4.03 % (1991127)------------------------------ % 21.93/4.03 % (1991127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.93/4.03 % (1991127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/4.03 % (1991127)CaDiCaL version: 2.1.3 % 21.93/4.03 % (1991127)Termination reason: Instruction limit % 21.93/4.03 % (1991127)Termination phase: Property scanning % 21.93/4.03 % (1991127)Time elapsed: 0.099 s % 21.93/4.03 % (1991127)Peak memory usage: 86 MB % 21.93/4.03 % (1991127)Instructions burned: 515 (million) % 21.93/4.03 % (1991130)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=4041832278:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi) % 21.93/4.03 % (1991131)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=2272292424:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi) % 21.93/4.03 % (1991133)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1130755136:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi) % 21.93/4.03 % (1991135)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3685280920:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi) % 21.93/4.03 % (1991128)Instruction limit reached! % 21.93/4.03 % (1991128)------------------------------ % 21.93/4.03 % (1991128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.93/4.03 % (1991128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/4.03 % (1991128)CaDiCaL version: 2.1.3 % 21.93/4.03 % (1991128)Termination reason: Instruction limit % 21.93/4.03 % (1991128)Termination phase: Saturation % 21.93/4.03 % (1991128)Time elapsed: 0.166 s % 21.93/4.03 % (1991128)Peak memory usage: 129 MB % 21.93/4.03 % (1991128)Instructions burned: 335 (million) % 21.93/4.03 % (1991122)------------------------------ % 21.93/4.03 % (1991122)------------------------------ % 21.93/4.03 % (1991134)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=1920230567:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2975 on theBenchmark for (2975ds/235Mi) % 21.93/4.03 % (1991135)Instruction limit reached! % 21.93/4.03 % (1991135)------------------------------ % 21.93/4.03 % (1991135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.93/4.03 % (1991135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/4.03 % (1991135)CaDiCaL version: 2.1.3 % 21.93/4.03 % (1991135)Termination reason: Instruction limit % 21.93/4.03 % (1991135)Termination phase: Property scanning % 21.93/4.03 % (1991135)Time elapsed: 0.052 s % 21.93/4.03 % (1991135)Peak memory usage: 86 MB % 21.93/4.03 % (1991135)Instructions burned: 274 (million) % 21.93/4.03 % (1991130)Instruction limit reached! % 21.93/4.03 % (1991130)------------------------------ % 21.93/4.03 % (1991130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.93/4.03 % (1991130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/4.03 % (1991130)CaDiCaL version: 2.1.3 % 21.93/4.03 % (1991130)Termination reason: Instruction limit % 21.93/4.03 % (1991130)Termination phase: SInE selection % 21.93/4.03 % (1991130)Time elapsed: 0.132 s % 21.93/4.03 % (1991130)Peak memory usage: 86 MB % 21.93/4.03 % (1991130)Instructions burned: 359 (million) % 21.93/4.03 % (1991133)Refutation not found, incomplete strategy % 21.93/4.03 % (1991133)------------------------------ % 21.93/4.03 % (1991133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.93/4.03 % (1991133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/4.03 % (1991133)CaDiCaL version: 2.1.3 % 21.93/4.03 % (1991133)Termination reason: Refutation not found, incomplete strategy % 21.93/4.03 % (1991133)Time elapsed: 0.095 s % 21.93/4.03 % (1991133)Peak memory usage: 112 MB % 21.93/4.03 % (1991133)Instructions burned: 193 (million) % 21.93/4.03 % (1991131)Instruction limit reached! % 21.93/4.03 % (1991131)------------------------------ % 21.93/4.03 % (1991131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.93/4.03 % (1991131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.93/4.03 % (1991131)CaDiCaL version: 2.1.3 % 21.93/4.03 % (1991131)Termination reason: Instruction limit % 21.93/4.03 % (1991131)Termination phase: Property scanning % 23.35/4.38 % (1991131)Time elapsed: 0.125 s % 23.35/4.38 % (1991131)Peak memory usage: 86 MB % 23.35/4.38 % (1991131)Instructions burned: 342 (million) % 23.35/4.38 % (1991134)Instruction limit reached! % 23.35/4.38 % (1991134)------------------------------ % 23.35/4.38 % (1991134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.35/4.38 % (1991134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.35/4.38 % (1991134)CaDiCaL version: 2.1.3 % 23.35/4.38 % (1991134)Termination reason: Instruction limit % 23.35/4.38 % (1991134)Termination phase: SInE selection % 23.35/4.38 % (1991134)Time elapsed: 0.087 s % 23.35/4.38 % (1991134)Peak memory usage: 86 MB % 23.35/4.38 % (1991134)Instructions burned: 238 (million) % 23.35/4.38 % (1991143)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=4231319016:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi) % 23.35/4.38 % (1991140)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4121512653:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi) % 23.35/4.38 % (1991142)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=1448529232:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 23.35/4.38 % (1991143)Instruction limit reached! % 23.35/4.38 % (1991143)------------------------------ % 23.35/4.38 % (1991143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.35/4.38 % (1991143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.35/4.38 % (1991143)CaDiCaL version: 2.1.3 % 23.35/4.38 % (1991143)Termination reason: Instruction limit % 23.35/4.38 % (1991143)Termination phase: Property scanning % 23.35/4.38 % (1991143)Time elapsed: 0.054 s % 23.35/4.38 % (1991143)Peak memory usage: 86 MB % 23.35/4.38 % (1991143)Instructions burned: 278 (million) % 23.35/4.38 % (1991140)Instruction limit reached! % 23.35/4.38 % (1991140)------------------------------ % 23.35/4.38 % (1991140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.35/4.38 % (1991140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.35/4.38 % (1991140)CaDiCaL version: 2.1.3 % 23.35/4.38 % (1991140)Termination reason: Instruction limit % 23.35/4.38 % (1991140)Termination phase: Property scanning % 23.35/4.38 % (1991140)Time elapsed: 0.056 s % 23.35/4.38 % (1991140)Peak memory usage: 86 MB % 23.35/4.38 % (1991140)Instructions burned: 148 (million) % 23.35/4.38 % (1991144)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3724810447:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi) % 23.35/4.38 % (1991145)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=140515147:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi) % 23.35/4.38 % (1991146)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=64351846:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi) % 23.35/4.38 % (1991146)Refutation not found, incomplete strategy % 23.35/4.38 % (1991146)------------------------------ % 23.35/4.38 % (1991146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.35/4.38 % (1991146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.35/4.38 % (1991146)CaDiCaL version: 2.1.3 % 23.35/4.38 % (1991146)Termination reason: Refutation not found, incomplete strategy % 23.35/4.38 % (1991146)Time elapsed: 0.065 s % 23.35/4.38 % (1991146)Peak memory usage: 88 MB % 23.35/4.38 % (1991146)Instructions burned: 181 (million) % 23.35/4.38 % (1991133)------------------------------ % 23.35/4.38 % (1991133)------------------------------ % 23.35/4.38 % (1991150)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=2540135981:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi) % 23.35/4.38 % (1991150)Instruction limit reached! % 23.35/4.38 % (1991150)------------------------------ % 23.35/4.38 % (1991150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.35/4.38 % (1991150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.35/4.38 % (1991150)CaDiCaL version: 2.1.3 % 23.35/4.38 % (1991150)Termination reason: Instruction limit % 23.35/4.38 % (1991150)Termination phase: Property scanning % 23.35/4.38 % (1991150)Time elapsed: 0.021 s % 23.35/4.38 % (1991150)Peak memory usage: 86 MB % 23.35/4.38 % (1991150)Instructions burned: 109 (million) % 25.29/4.70 % (1991151)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4000018807:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi) % 25.29/4.70 % (1991156)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 % 25.29/4.70 % (1991157)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3087834404:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2970 on theBenchmark for (2970ds/130Mi) % 25.29/4.70 % (1991156)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3735963357:i=1090:aac=none:nm=0:rtra=on:rawr=on_2970 on theBenchmark for (2970ds/1090Mi) % 25.29/4.70 % (1991145)Instruction limit reached! % 25.29/4.70 % (1991145)------------------------------ % 25.29/4.70 % (1991145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.29/4.70 % (1991145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.29/4.70 % (1991145)CaDiCaL version: 2.1.3 % 25.29/4.70 % (1991145)Termination reason: Instruction limit % 25.29/4.70 % (1991145)Termination phase: Saturation % 25.29/4.70 % (1991145)Time elapsed: 0.240 s % 25.29/4.70 % (1991145)Peak memory usage: 89 MB % 25.29/4.70 % (1991145)Instructions burned: 658 (million) % 25.29/4.70 % (1991157)Instruction limit reached! % 25.29/4.70 % (1991157)------------------------------ % 25.29/4.70 % (1991157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.29/4.70 % (1991157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.29/4.70 % (1991157)CaDiCaL version: 2.1.3 % 25.29/4.70 % (1991157)Termination reason: Instruction limit % 25.29/4.70 % (1991157)Termination phase: Property scanning % 25.29/4.70 % (1991157)Time elapsed: 0.026 s % 25.29/4.70 % (1991157)Peak memory usage: 85 MB % 25.29/4.70 % (1991157)Instructions burned: 136 (million) % 25.29/4.70 % (1991146)------------------------------ % 25.29/4.70 % (1991146)------------------------------ % 25.29/4.70 % (1991151)Instruction limit reached! % 25.29/4.70 % (1991151)------------------------------ % 25.29/4.70 % (1991151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.29/4.70 % (1991151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.29/4.70 % (1991151)CaDiCaL version: 2.1.3 % 25.29/4.70 % (1991151)Termination reason: Instruction limit % 25.29/4.70 % (1991151)Termination phase: Saturation % 25.29/4.70 % (1991151)Time elapsed: 0.212 s % 25.29/4.70 % (1991151)Peak memory usage: 129 MB % 25.29/4.70 % (1991151)Instructions burned: 452 (million) % 25.29/4.70 % (1991162)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=588244282:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi) % 25.29/4.70 % (1991144)Instruction limit reached! % 25.29/4.70 % (1991144)------------------------------ % 25.29/4.70 % (1991144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.29/4.70 % (1991144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.29/4.70 % (1991144)CaDiCaL version: 2.1.3 % 25.29/4.70 % (1991144)Termination reason: Instruction limit % 25.29/4.70 % (1991144)Termination phase: Saturation % 25.29/4.70 % (1991144)Time elapsed: 0.398 s % 25.29/4.70 % (1991144)Peak memory usage: 95 MB % 25.29/4.70 % (1991144)Instructions burned: 1055 (million) % 25.29/4.70 % (1991161)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3532072653:i=312:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/312Mi) % 25.29/4.70 % (1991162)Instruction limit reached! % 25.29/4.70 % (1991162)------------------------------ % 25.29/4.70 % (1991162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.29/4.70 % (1991162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.29/4.70 % (1991162)CaDiCaL version: 2.1.3 % 25.29/4.70 % (1991162)Termination reason: Instruction limit % 25.29/4.70 % (1991162)Termination phase: Property scanning % 25.29/4.70 % (1991162)Time elapsed: 0.092 s % 25.29/4.70 % (1991162)Peak memory usage: 87 MB % 25.29/4.70 % (1991162)Instructions burned: 492 (million) % 25.29/4.70 % (1991163)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=162733181:s2a=on:i=835:s2at=2:rtra=on_2968 on theBenchmark for (2968ds/835Mi) % 25.29/4.70 % (1991164)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3080657397:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 29.44/5.14 % (1991161)Instruction limit reached! % 29.44/5.14 % (1991161)------------------------------ % 29.44/5.14 % (1991161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.44/5.14 % (1991161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.44/5.14 % (1991161)CaDiCaL version: 2.1.3 % 29.44/5.14 % (1991161)Termination reason: Instruction limit % 29.44/5.14 % (1991161)Termination phase: Property scanning % 29.44/5.14 % (1991161)Time elapsed: 0.113 s % 29.44/5.14 % (1991161)Peak memory usage: 86 MB % 29.44/5.14 % (1991161)Instructions burned: 312 (million) % 29.44/5.14 % (1991166)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1950966085:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 29.44/5.14 % (1991169)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1782018184:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2966 on theBenchmark for (2966ds/646Mi) % 29.44/5.14 % (1991164)Instruction limit reached! % 29.44/5.14 % (1991164)------------------------------ % 29.44/5.14 % (1991164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.44/5.14 % (1991164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.44/5.14 % (1991164)CaDiCaL version: 2.1.3 % 29.44/5.14 % (1991164)Termination reason: Instruction limit % 29.44/5.14 % (1991164)Termination phase: Property scanning % 29.44/5.14 % (1991164)Time elapsed: 0.112 s % 29.44/5.14 % (1991164)Peak memory usage: 86 MB % 29.44/5.14 % (1991164)Instructions burned: 307 (million) % 29.44/5.14 % (1991156)Instruction limit reached! % 29.44/5.14 % (1991156)------------------------------ % 29.44/5.14 % (1991156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.44/5.14 % (1991156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.44/5.14 % (1991156)CaDiCaL version: 2.1.3 % 29.44/5.14 % (1991156)Termination reason: Instruction limit % 29.44/5.14 % (1991156)Termination phase: Saturation % 29.44/5.14 % (1991156)Time elapsed: 0.439 s % 29.44/5.14 % (1991156)Peak memory usage: 113 MB % 29.44/5.14 % (1991156)Instructions burned: 1093 (million) % 29.44/5.14 % (1991171)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=3186501567:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2966 on theBenchmark for (2966ds/784Mi) % 29.44/5.14 % (1991169)Instruction limit reached! % 29.44/5.14 % (1991169)------------------------------ % 29.44/5.14 % (1991169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.44/5.14 % (1991169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.44/5.14 % (1991169)CaDiCaL version: 2.1.3 % 29.44/5.14 % (1991169)Termination reason: Instruction limit % 29.44/5.14 % (1991169)Termination phase: Saturation % 29.44/5.14 % (1991169)Time elapsed: 0.156 s % 29.44/5.14 % (1991169)Peak memory usage: 131 MB % 29.44/5.14 % (1991169)Instructions burned: 651 (million) % 29.44/5.14 % (1991174)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=1894934946:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2965 on theBenchmark for (2965ds/1131Mi) % 29.44/5.14 % (1991163)Instruction limit reached! % 29.44/5.14 % (1991163)------------------------------ % 29.44/5.14 % (1991163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.44/5.14 % (1991163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.44/5.14 % (1991163)CaDiCaL version: 2.1.3 % 29.44/5.14 % (1991163)Termination reason: Instruction limit % 29.44/5.14 % (1991163)Termination phase: Saturation % 29.44/5.14 % (1991163)Time elapsed: 0.314 s % 29.44/5.14 % (1991163)Peak memory usage: 92 MB % 29.44/5.14 % (1991163)Instructions burned: 835 (million) % 29.44/5.14 % (1991175)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=444516282:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2964 on theBenchmark for (2964ds/246Mi) % 29.44/5.14 % (1991177)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=168626734:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2964 on theBenchmark for (2964ds/775Mi) % 29.44/5.14 % (1991166)Instruction limit reached! % 29.44/5.14 % (1991166)------------------------------ % 29.44/5.14 % (1991166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (1991166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (1991166)CaDiCaL version: 2.1.3 % 36.14/6.09 % (1991166)Termination reason: Instruction limit % 36.14/6.09 % (1991166)Termination phase: Saturation % 36.14/6.09 % (1991166)Time elapsed: 0.321 s % 36.14/6.09 % (1991166)Peak memory usage: 117 MB % 36.14/6.09 % (1991166)Instructions burned: 778 (million) % 36.14/6.09 % (1991177)Refutation not found, incomplete strategy % 36.14/6.09 % (1991177)------------------------------ % 36.14/6.09 % (1991177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (1991177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (1991177)CaDiCaL version: 2.1.3 % 36.14/6.09 % (1991177)Termination reason: Refutation not found, incomplete strategy % 36.14/6.09 % (1991177)Time elapsed: 0.058 s % 36.14/6.09 % (1991177)Peak memory usage: 88 MB % 36.14/6.09 % (1991177)Instructions burned: 304 (million) % 36.14/6.09 % (1991175)Instruction limit reached! % 36.14/6.09 % (1991175)------------------------------ % 36.14/6.09 % (1991175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (1991175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (1991175)CaDiCaL version: 2.1.3 % 36.14/6.09 % (1991175)Termination reason: Instruction limit % 36.14/6.09 % (1991175)Termination phase: SInE selection % 36.14/6.09 % (1991175)Time elapsed: 0.091 s % 36.14/6.09 % (1991175)Peak memory usage: 86 MB % 36.14/6.09 % (1991175)Instructions burned: 247 (million) % 36.14/6.09 % (1991179)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3194885686:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2963 on theBenchmark for (2963ds/273Mi) % 36.14/6.09 % (1991171)Instruction limit reached! % 36.14/6.09 % (1991171)------------------------------ % 36.14/6.09 % (1991171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (1991171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (1991171)CaDiCaL version: 2.1.3 % 36.14/6.09 % (1991171)Termination reason: Instruction limit % 36.14/6.09 % (1991171)Termination phase: Saturation % 36.14/6.09 % (1991171)Time elapsed: 0.307 s % 36.14/6.09 % (1991171)Peak memory usage: 112 MB % 36.14/6.09 % (1991171)Instructions burned: 784 (million) % 36.14/6.09 % (1991182)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=74883932:i=102:nm=16:rtra=on_2962 on theBenchmark for (2962ds/102Mi) % 36.14/6.09 % (1991179)Instruction limit reached! % 36.14/6.09 % (1991179)------------------------------ % 36.14/6.09 % (1991179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (1991179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (1991179)CaDiCaL version: 2.1.3 % 36.14/6.09 % (1991179)Termination reason: Instruction limit % 36.14/6.09 % (1991179)Termination phase: Property scanning % 36.14/6.09 % (1991179)Time elapsed: 0.101 s % 36.14/6.09 % (1991179)Peak memory usage: 86 MB % 36.14/6.09 % (1991179)Instructions burned: 276 (million) % 36.14/6.09 % (1991177)------------------------------ % 36.14/6.09 % (1991177)------------------------------ % 36.14/6.09 % (1991182)Instruction limit reached! % 36.14/6.09 % (1991182)------------------------------ % 36.14/6.09 % (1991182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.14/6.09 % (1991182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.14/6.09 % (1991182)CaDiCaL version: 2.1.3 % 36.14/6.09 % (1991182)Termination reason: Instruction limit % 36.14/6.09 % (1991182)Termination phase: Property scanning % 36.14/6.09 % (1991182)Time elapsed: 0.039 s % 36.14/6.09 % (1991182)Peak memory usage: 86 MB % 36.14/6.09 % (1991182)Instructions burned: 103 (million) % 36.14/6.09 % (1991183)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=16085343:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2962 on theBenchmark for (2962ds/1094Mi) % 36.14/6.09 % (1991185)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=291432808:i=6400:doe=on:fsr=off:rtra=on_2961 on theBenchmark for (2961ds/6400Mi) % 36.14/6.09 % (1991188)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=2536473290:i=1846:canc=cautious:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/1846Mi) % 36.14/6.09 % (1991187)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=4258500899:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi) % 43.79/7.17 % (1991189)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=3064469103:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2960 on theBenchmark for (2960ds/36816Mi) % 43.79/7.17 % (1991174)Instruction limit reached! % 43.79/7.17 % (1991174)------------------------------ % 43.79/7.17 % (1991174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.79/7.17 % (1991174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.79/7.17 % (1991174)CaDiCaL version: 2.1.3 % 43.79/7.17 % (1991174)Termination reason: Instruction limit % 43.79/7.17 % (1991174)Termination phase: Saturation % 43.79/7.17 % (1991174)Time elapsed: 0.447 s % 43.79/7.17 % (1991174)Peak memory usage: 119 MB % 43.79/7.17 % (1991174)Instructions burned: 1132 (million) % 43.79/7.17 % (1991188)Refutation not found, incomplete strategy % 43.79/7.17 % (1991188)------------------------------ % 43.79/7.17 % (1991188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.79/7.17 % (1991188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.79/7.17 % (1991188)CaDiCaL version: 2.1.3 % 43.79/7.17 % (1991188)Termination reason: Refutation not found, incomplete strategy % 43.79/7.17 % (1991188)Time elapsed: 0.133 s % 43.79/7.17 % (1991188)Peak memory usage: 91 MB % 43.79/7.17 % (1991188)Instructions burned: 676 (million) % 43.79/7.17 % (1991195)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3020474568:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2959 on theBenchmark for (2959ds/273Mi) % 43.79/7.17 % (1991188)------------------------------ % 43.79/7.17 % (1991188)------------------------------ % 43.79/7.17 % (1991195)Instruction limit reached! % 43.79/7.17 % (1991195)------------------------------ % 43.79/7.17 % (1991195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.79/7.17 % (1991195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.79/7.17 % (1991195)CaDiCaL version: 2.1.3 % 43.79/7.17 % (1991195)Termination reason: Instruction limit % 43.79/7.17 % (1991195)Termination phase: Property scanning % 43.79/7.17 % (1991195)Time elapsed: 0.099 s % 43.79/7.17 % (1991195)Peak memory usage: 86 MB % 43.79/7.17 % (1991195)Instructions burned: 274 (million) % 43.79/7.17 % (1991183)Instruction limit reached! % 43.79/7.17 % (1991183)------------------------------ % 43.79/7.17 % (1991183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.79/7.17 % (1991183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.79/7.17 % (1991183)CaDiCaL version: 2.1.3 % 43.79/7.17 % (1991183)Termination reason: Instruction limit % 43.79/7.17 % (1991183)Termination phase: Saturation % 43.79/7.17 % (1991183)Time elapsed: 0.412 s % 43.79/7.17 % (1991183)Peak memory usage: 96 MB % 43.79/7.17 % (1991183)Instructions burned: 1096 (million) % 43.79/7.17 % (1991187)Instruction limit reached! % 43.79/7.17 % (1991187)------------------------------ % 43.79/7.17 % (1991187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.79/7.17 % (1991187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.79/7.17 % (1991187)CaDiCaL version: 2.1.3 % 43.79/7.17 % (1991187)Termination reason: Instruction limit % 43.79/7.17 % (1991187)Termination phase: Saturation % 43.79/7.17 % (1991187)Time elapsed: 0.330 s % 43.79/7.17 % (1991187)Peak memory usage: 116 MB % 43.79/7.17 % (1991187)Instructions burned: 868 (million) % 43.79/7.17 % (1991197)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=4236611950:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/863Mi) % 43.79/7.17 % (1991142)Instruction limit reached! % 43.79/7.17 % (1991142)------------------------------ % 43.79/7.17 % (1991142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.79/7.17 % (1991142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.79/7.17 % (1991142)CaDiCaL version: 2.1.3 % 43.79/7.17 % (1991142)Termination reason: Instruction limit % 43.79/7.17 % (1991142)Termination phase: Saturation % 43.79/7.17 % (1991142)Time elapsed: 1.694 s % 43.79/7.17 % (1991142)Peak memory usage: 92 MB % 43.79/7.17 % (1991142)Instructions burned: 4430 (million) % 43.79/7.17 % (1991198)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1277265514:i=5811:kws=precedence:nm=0:rtra=on_2956 on theBenchmark for (2956ds/5811Mi) % 45.47/7.60 % (1991199)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=3798541863:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2956 on theBenchmark for (2956ds/2216Mi) % 45.47/7.60 % (1991200)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=4038274932:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2956 on theBenchmark for (2956ds/801Mi) % 45.47/7.60 % (1991197)Instruction limit reached! % 45.47/7.60 % (1991197)------------------------------ % 45.47/7.60 % (1991197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.60 % (1991197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.60 % (1991197)CaDiCaL version: 2.1.3 % 45.47/7.60 % (1991197)Termination reason: Instruction limit % 45.47/7.60 % (1991197)Termination phase: Saturation % 45.47/7.60 % (1991197)Time elapsed: 0.177 s % 45.47/7.60 % (1991197)Peak memory usage: 116 MB % 45.47/7.60 % (1991197)Instructions burned: 865 (million) % 45.47/7.60 % (1991202)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1645385633:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2955 on theBenchmark for (2955ds/1026Mi) % 45.47/7.60 % (1991202)Refutation not found, incomplete strategy % 45.47/7.60 % (1991202)------------------------------ % 45.47/7.60 % (1991202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.60 % (1991202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.60 % (1991202)CaDiCaL version: 2.1.3 % 45.47/7.60 % (1991202)Termination reason: Refutation not found, incomplete strategy % 45.47/7.60 % (1991202)Time elapsed: 0.065 s % 45.47/7.60 % (1991202)Peak memory usage: 88 MB % 45.47/7.60 % (1991202)Instructions burned: 181 (million) % 45.47/7.60 % (1991206)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=361784565:i=3509:rtra=on_2953 on theBenchmark for (2953ds/3509Mi) % 45.47/7.60 % (1991200)Instruction limit reached! % 45.47/7.60 % (1991200)------------------------------ % 45.47/7.60 % (1991200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.60 % (1991200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.60 % (1991200)CaDiCaL version: 2.1.3 % 45.47/7.60 % (1991200)Termination reason: Instruction limit % 45.47/7.60 % (1991200)Termination phase: Saturation % 45.47/7.60 % (1991200)Time elapsed: 0.287 s % 45.47/7.60 % (1991200)Peak memory usage: 92 MB % 45.47/7.60 % (1991200)Instructions burned: 802 (million) % 45.47/7.60 % (1991202)------------------------------ % 45.47/7.60 % (1991202)------------------------------ % 45.47/7.60 % (1991209)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2717687316:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2951 on theBenchmark for (2951ds/2127Mi) % 45.47/7.60 % (1991209)Refutation not found, incomplete strategy % 45.47/7.60 % (1991209)------------------------------ % 45.47/7.60 % (1991209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.60 % (1991209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.60 % (1991209)CaDiCaL version: 2.1.3 % 45.47/7.60 % (1991209)Termination reason: Refutation not found, incomplete strategy % 45.47/7.60 % (1991209)Time elapsed: 0.104 s % 45.47/7.60 % (1991209)Peak memory usage: 88 MB % 45.47/7.60 % (1991209)Instructions burned: 289 (million) % 45.47/7.60 % (1991210)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=3013175262:i=1959:rtra=on:fsd=on:proc=on_2950 on theBenchmark for (2950ds/1959Mi) % 45.47/7.60 % (1991209)------------------------------ % 45.47/7.60 % (1991209)------------------------------ % 45.47/7.60 % (1991199)Instruction limit reached! % 45.47/7.60 % (1991199)------------------------------ % 45.47/7.60 % (1991199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.47/7.60 % (1991199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.47/7.60 % (1991199)CaDiCaL version: 2.1.3 % 45.47/7.60 % (1991199)Termination reason: Instruction limit % 45.47/7.60 % (1991199)Termination phase: Saturation % 45.47/7.60 % (1991199)Time elapsed: 0.846 s % 45.47/7.60 % (1991199)Peak memory usage: 120 MB % 45.47/7.60 % (1991199)Instructions burned: 2225 (million) % 45.47/7.60 % (1991206)Instruction limit reached! % 45.47/7.60 % (1991206)------------------------------ % 45.47/7.60 % (1991206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.23/10.16 % (1991206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.23/10.16 % (1991206)CaDiCaL version: 2.1.3 % 65.23/10.16 % (1991206)Termination reason: Instruction limit % 65.23/10.16 % (1991206)Termination phase: Saturation % 65.23/10.16 % (1991206)Time elapsed: 0.690 s % 65.23/10.16 % (1991206)Peak memory usage: 93 MB % 65.23/10.16 % (1991206)Instructions burned: 3518 (million) % 65.23/10.16 % (1991213)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3042107473:s2a=on:i=3553:nm=0:rtra=on_2946 on theBenchmark for (2946ds/3553Mi) % 65.23/10.16 % (1991214)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3863464142:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2946 on theBenchmark for (2946ds/3201Mi) % 65.23/10.16 % (1991215)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=1239379847:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2945 on theBenchmark for (2945ds/4093Mi) % 65.23/10.16 % (1991210)Instruction limit reached! % 65.23/10.16 % (1991210)------------------------------ % 65.23/10.16 % (1991210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.23/10.16 % (1991210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.23/10.16 % (1991210)CaDiCaL version: 2.1.3 % 65.23/10.16 % (1991210)Termination reason: Instruction limit % 65.23/10.16 % (1991210)Termination phase: Saturation % 65.23/10.16 % (1991210)Time elapsed: 0.756 s % 65.23/10.16 % (1991210)Peak memory usage: 122 MB % 65.23/10.16 % (1991210)Instructions burned: 1960 (million) % 65.23/10.16 % (1991219)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=144460079:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2941 on theBenchmark for (2941ds/21173Mi) % 65.23/10.16 % (1991219)Refutation not found, incomplete strategy % 65.23/10.16 % (1991219)------------------------------ % 65.23/10.16 % (1991219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.23/10.16 % (1991219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.23/10.16 % (1991219)CaDiCaL version: 2.1.3 % 65.23/10.16 % (1991219)Termination reason: Refutation not found, incomplete strategy % 65.23/10.16 % (1991219)Time elapsed: 0.079 s % 65.23/10.16 % (1991219)Peak memory usage: 113 MB % 65.23/10.16 % (1991219)Instructions burned: 147 (million) % 65.23/10.16 % (1991214)Refutation not found, incomplete strategy % 65.23/10.16 % (1991214)------------------------------ % 65.23/10.16 % (1991214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.23/10.16 % (1991214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.23/10.16 % (1991214)CaDiCaL version: 2.1.3 % 65.23/10.16 % (1991214)Termination reason: Refutation not found, incomplete strategy % 65.23/10.16 % (1991214)Time elapsed: 0.711 s % 65.23/10.16 % (1991214)Peak memory usage: 99 MB % 65.23/10.16 % (1991214)Instructions burned: 1890 (million) % 65.23/10.16 % (1991219)------------------------------ % 65.23/10.16 % (1991219)------------------------------ % 65.23/10.16 % (1991215)Instruction limit reached! % 65.23/10.16 % (1991215)------------------------------ % 65.23/10.16 % (1991215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.23/10.16 % (1991215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.23/10.16 % (1991215)CaDiCaL version: 2.1.3 % 65.23/10.16 % (1991215)Termination reason: Instruction limit % 65.23/10.16 % (1991215)Termination phase: Saturation % 65.23/10.16 % (1991215)Time elapsed: 0.829 s % 65.23/10.16 % (1991215)Peak memory usage: 135 MB % 65.23/10.16 % (1991215)Instructions burned: 4098 (million) % 65.23/10.16 % (1991185)Instruction limit reached! % 65.23/10.16 % (1991185)------------------------------ % 65.23/10.16 % (1991185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.23/10.16 % (1991185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.23/10.16 % (1991185)CaDiCaL version: 2.1.3 % 65.23/10.16 % (1991185)Termination reason: Instruction limit % 65.23/10.16 % (1991185)Termination phase: Saturation % 65.23/10.16 % (1991185)Time elapsed: 2.429 s % 65.23/10.16 % (1991185)Peak memory usage: 92 MB % 65.23/10.16 % (1991185)Instructions burned: 6402 (million) % 65.23/10.16 % (1991214)------------------------------ % 65.23/10.16 % (1991214)------------------------------ % 65.23/10.16 % (1991222)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=1252464892:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2936 on theBenchmark for (2936ds/1262Mi) % 75.58/11.66 % (1991221)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=3912800460:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2936 on theBenchmark for (2936ds/10544Mi) % 75.58/11.66 % (1991223)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=443081276:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/775Mi) % 75.58/11.66 % (1991224)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2691592684:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/270Mi) % 75.58/11.66 % (1991198)Instruction limit reached! % 75.58/11.66 % (1991198)------------------------------ % 75.58/11.66 % (1991198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.58/11.66 % (1991198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.58/11.66 % (1991198)CaDiCaL version: 2.1.3 % 75.58/11.66 % (1991198)Termination reason: Instruction limit % 75.58/11.66 % (1991198)Termination phase: Saturation % 75.58/11.66 % (1991198)Time elapsed: 2.163 s % 75.58/11.66 % (1991198)Peak memory usage: 125 MB % 75.58/11.66 % (1991198)Instructions burned: 5812 (million) % 75.58/11.66 % (1991223)Refutation not found, incomplete strategy % 75.58/11.66 % (1991223)------------------------------ % 75.58/11.66 % (1991223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.58/11.66 % (1991223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.58/11.66 % (1991223)CaDiCaL version: 2.1.3 % 75.58/11.66 % (1991223)Termination reason: Refutation not found, incomplete strategy % 75.58/11.66 % (1991223)Time elapsed: 0.109 s % 75.58/11.66 % (1991223)Peak memory usage: 88 MB % 75.58/11.66 % (1991223)Instructions burned: 304 (million) % 75.58/11.66 % (1991224)Instruction limit reached! % 75.58/11.66 % (1991224)------------------------------ % 75.58/11.66 % (1991224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.58/11.66 % (1991224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.58/11.66 % (1991224)CaDiCaL version: 2.1.3 % 75.58/11.66 % (1991224)Termination reason: Instruction limit % 75.58/11.66 % (1991224)Termination phase: Property scanning % 75.58/11.66 % (1991224)Time elapsed: 0.099 s % 75.58/11.66 % (1991224)Peak memory usage: 86 MB % 75.58/11.66 % (1991224)Instructions burned: 270 (million) % 75.58/11.66 % (1991222)Instruction limit reached! % 75.58/11.66 % (1991222)------------------------------ % 75.58/11.66 % (1991222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.58/11.66 % (1991222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.58/11.66 % (1991222)CaDiCaL version: 2.1.3 % 75.58/11.66 % (1991222)Termination reason: Instruction limit % 75.58/11.66 % (1991222)Termination phase: Saturation % 75.58/11.66 % (1991222)Time elapsed: 0.264 s % 75.58/11.66 % (1991222)Peak memory usage: 116 MB % 75.58/11.66 % (1991222)Instructions burned: 1265 (million) % 75.58/11.66 % (1991213)Instruction limit reached! % 75.58/11.66 % (1991213)------------------------------ % 75.58/11.66 % (1991213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.58/11.66 % (1991213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.58/11.66 % (1991213)CaDiCaL version: 2.1.3 % 75.58/11.66 % (1991213)Termination reason: Instruction limit % 75.58/11.66 % (1991213)Termination phase: Saturation % 75.58/11.66 % (1991213)Time elapsed: 1.333 s % 75.58/11.66 % (1991213)Peak memory usage: 93 MB % 75.58/11.66 % (1991213)Instructions burned: 3554 (million) % 75.58/11.66 % (1991229)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=2042442301:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2933 on theBenchmark for (2933ds/17165Mi) % 75.58/11.66 % (1991230)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=1597287850:s2a=on:i=13094:s2at=-1:rtra=on_2932 on theBenchmark for (2932ds/13094Mi) % 75.58/11.66 % (1991231)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=3139546231:st=2:i=12633:rtra=on:ss=axioms_2932 on theBenchmark for (2932ds/12633Mi) % 75.58/11.66 % (1991223)------------------------------ % 75.58/11.66 % (1991223)------------------------------ % 75.58/11.66 % (1991231)Refutation not found, incomplete strategy % 75.58/11.66 % (1991231)------------------------------ % 92.87/14.04 % (1991231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.87/14.04 % (1991231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.87/14.04 % (1991231)CaDiCaL version: 2.1.3 % 92.87/14.04 % (1991231)Termination reason: Refutation not found, incomplete strategy % 92.87/14.04 % (1991231)Time elapsed: 0.050 s % 92.87/14.04 % (1991231)Peak memory usage: 88 MB % 92.87/14.04 % (1991231)Instructions burned: 257 (million) % 92.87/14.04 % (1991232)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=968530112:i=1783:rtra=on:gtg=position_2931 on theBenchmark for (2931ds/1783Mi) % 92.87/14.04 % (1991231)------------------------------ % 92.87/14.04 % (1991231)------------------------------ % 92.87/14.04 % (1991236)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=3558310222:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2930 on theBenchmark for (2930ds/5451Mi) % 92.87/14.04 % (1991238)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=2248331522:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2929 on theBenchmark for (2929ds/4975Mi) % 92.87/14.04 % (1991232)Instruction limit reached! % 92.87/14.04 % (1991232)------------------------------ % 92.87/14.04 % (1991232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.87/14.04 % (1991232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.87/14.04 % (1991232)CaDiCaL version: 2.1.3 % 92.87/14.04 % (1991232)Termination reason: Instruction limit % 92.87/14.04 % (1991232)Termination phase: Saturation % 92.87/14.04 % (1991232)Time elapsed: 0.672 s % 92.87/14.04 % (1991232)Peak memory usage: 114 MB % 92.87/14.04 % (1991232)Instructions burned: 1784 (million) % 92.87/14.04 % (1991241)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=2683168765:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2923 on theBenchmark for (2923ds/2076Mi) % 92.87/14.04 % (1991238)Instruction limit reached! % 92.87/14.04 % (1991238)------------------------------ % 92.87/14.04 % (1991238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.87/14.04 % (1991238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.87/14.04 % (1991238)CaDiCaL version: 2.1.3 % 92.87/14.04 % (1991238)Termination reason: Instruction limit % 92.87/14.04 % (1991238)Termination phase: Saturation % 92.87/14.04 % (1991238)Time elapsed: 1.270 s % 92.87/14.04 % (1991238)Peak memory usage: 164 MB % 92.87/14.04 % (1991238)Instructions burned: 4979 (million) % 92.87/14.04 % (1991241)Instruction limit reached! % 92.87/14.04 % (1991241)------------------------------ % 92.87/14.04 % (1991241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.87/14.04 % (1991241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.87/14.04 % (1991241)CaDiCaL version: 2.1.3 % 92.87/14.04 % (1991241)Termination reason: Instruction limit % 92.87/14.04 % (1991241)Termination phase: Saturation % 92.87/14.04 % (1991241)Time elapsed: 0.785 s % 92.87/14.04 % (1991241)Peak memory usage: 116 MB % 92.87/14.04 % (1991241)Instructions burned: 2078 (million) % 92.87/14.04 % (1991243)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=691422990:i=5145:rtra=on_2914 on theBenchmark for (2914ds/5145Mi) % 92.87/14.04 % (1991244)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3703260568:i=3509:rtra=on_2913 on theBenchmark for (2913ds/3509Mi) % 92.87/14.04 % (1991236)Instruction limit reached! % 92.87/14.04 % (1991236)------------------------------ % 92.87/14.04 % (1991236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.87/14.04 % (1991236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.87/14.04 % (1991236)CaDiCaL version: 2.1.3 % 92.87/14.04 % (1991236)Termination reason: Instruction limit % 92.87/14.04 % (1991236)Termination phase: Saturation % 92.87/14.04 % (1991236)Time elapsed: 2.107 s % 92.87/14.04 % (1991236)Peak memory usage: 125 MB % 92.87/14.04 % (1991236)Instructions burned: 5451 (million) % 92.87/14.04 % (1991247)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2651444725:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2907 on theBenchmark for (2907ds/13800Mi) % 92.87/14.04 % (1991247)Refutation not found, incomplete strategy % 92.87/14.04 % (1991247)------------------------------ % 92.87/14.04 % (1991247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.98/23.20 % (1991247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.98/23.20 % (1991247)CaDiCaL version: 2.1.3 % 157.98/23.20 % (1991247)Termination reason: Refutation not found, incomplete strategy % 157.98/23.20 % (1991247)Time elapsed: 0.103 s % 157.98/23.20 % (1991247)Peak memory usage: 88 MB % 157.98/23.20 % (1991247)Instructions burned: 289 (million) % 157.98/23.20 % (1991243)Instruction limit reached! % 157.98/23.20 % (1991243)------------------------------ % 157.98/23.20 % (1991243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.98/23.20 % (1991243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.98/23.20 % (1991243)CaDiCaL version: 2.1.3 % 157.98/23.20 % (1991243)Termination reason: Instruction limit % 157.98/23.20 % (1991243)Termination phase: Saturation % 157.98/23.20 % (1991243)Time elapsed: 0.995 s % 157.98/23.20 % (1991243)Peak memory usage: 95 MB % 157.98/23.20 % (1991243)Instructions burned: 5150 (million) % 157.98/23.20 % (1991247)------------------------------ % 157.98/23.20 % (1991247)------------------------------ % 157.98/23.20 % (1991249)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=2552218988:i=1412:rtra=on:fsd=on:proc=on_2903 on theBenchmark for (2903ds/1412Mi) % 157.98/23.20 % (1991250)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 % 157.98/23.20 % (1991250)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=858700371:i=11747:aac=none:nm=0:rtra=on:rawr=on_2902 on theBenchmark for (2902ds/11747Mi) % 157.98/23.20 % (1991249)Instruction limit reached! % 157.98/23.20 % (1991249)------------------------------ % 157.98/23.20 % (1991249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.98/23.20 % (1991249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.98/23.20 % (1991249)CaDiCaL version: 2.1.3 % 157.98/23.20 % (1991249)Termination reason: Instruction limit % 157.98/23.20 % (1991249)Termination phase: Saturation % 157.98/23.20 % (1991249)Time elapsed: 0.293 s % 157.98/23.20 % (1991249)Peak memory usage: 117 MB % 157.98/23.20 % (1991249)Instructions burned: 1415 (million) % 157.98/23.20 % (1991244)Instruction limit reached! % 157.98/23.20 % (1991244)------------------------------ % 157.98/23.20 % (1991244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.98/23.20 % (1991244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.98/23.20 % (1991244)CaDiCaL version: 2.1.3 % 157.98/23.20 % (1991244)Termination reason: Instruction limit % 157.98/23.20 % (1991244)Termination phase: Saturation % 157.98/23.20 % (1991244)Time elapsed: 1.317 s % 157.98/23.20 % (1991244)Peak memory usage: 92 MB % 157.98/23.20 % (1991244)Instructions burned: 3511 (million) % 157.98/23.20 % (1991253)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=3777185600:s2a=on:i=3553:nm=0:rtra=on_2899 on theBenchmark for (2899ds/3553Mi) % 157.98/23.20 % (1991254)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=450438966:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2899 on theBenchmark for (2899ds/3201Mi) % 157.98/23.20 % (1991253)Instruction limit reached! % 157.98/23.20 % (1991253)------------------------------ % 157.98/23.20 % (1991253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.98/23.20 % (1991253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.98/23.20 % (1991253)CaDiCaL version: 2.1.3 % 157.98/23.20 % (1991253)Termination reason: Instruction limit % 157.98/23.20 % (1991253)Termination phase: Saturation % 157.98/23.20 % (1991253)Time elapsed: 0.693 s % 157.98/23.20 % (1991253)Peak memory usage: 94 MB % 157.98/23.20 % (1991253)Instructions burned: 3554 (million) % 157.98/23.20 % (1991254)Refutation not found, incomplete strategy % 157.98/23.20 % (1991254)------------------------------ % 157.98/23.20 % (1991254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.98/23.20 % (1991254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.98/23.20 % (1991254)CaDiCaL version: 2.1.3 % 157.98/23.20 % (1991254)Termination reason: Refutation not found, incomplete strategy % 157.98/23.20 % (1991254)Time elapsed: 0.685 s % 157.98/23.20 % (1991254)Peak memory usage: 99 MB % 157.98/23.20 % (1991254)Instructions burned: 1829 (million) % 157.98/23.20 % (1991257)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=1559178204:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2891 on theBenchmark for (2891ds/4081Mi) % 175.52/25.78 % (1991254)------------------------------ % 175.52/25.78 % (1991254)------------------------------ % 175.52/25.78 % (1991221)Instruction limit reached! % 175.52/25.78 % (1991221)------------------------------ % 175.52/25.78 % (1991221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.52/25.78 % (1991221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.52/25.78 % (1991221)CaDiCaL version: 2.1.3 % 175.52/25.78 % (1991221)Termination reason: Instruction limit % 175.52/25.78 % (1991221)Termination phase: Saturation % 175.52/25.78 % (1991221)Time elapsed: 4.704 s % 175.52/25.78 % (1991221)Peak memory usage: 167 MB % 175.52/25.78 % (1991221)Instructions burned: 10544 (million) % 175.52/25.78 % (1991259)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=3908785971:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2888 on theBenchmark for (2888ds/20260Mi) % 175.52/25.78 % (1991260)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=1366134565:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2887 on theBenchmark for (2887ds/58627Mi) % 175.52/25.78 % (1991259)Refutation not found, incomplete strategy % 175.52/25.78 % (1991259)------------------------------ % 175.52/25.78 % (1991259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.52/25.78 % (1991259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.52/25.78 % (1991259)CaDiCaL version: 2.1.3 % 175.52/25.78 % (1991259)Termination reason: Refutation not found, incomplete strategy % 175.52/25.78 % (1991259)Time elapsed: 0.080 s % 175.52/25.78 % (1991259)Peak memory usage: 113 MB % 175.52/25.78 % (1991259)Instructions burned: 147 (million) % 175.52/25.78 % (1991230)Instruction limit reached! % 175.52/25.78 % (1991230)------------------------------ % 175.52/25.78 % (1991230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.52/25.78 % (1991230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.52/25.78 % (1991230)CaDiCaL version: 2.1.3 % 175.52/25.79 % (1991230)Termination reason: Instruction limit % 175.52/25.79 % (1991230)Termination phase: Saturation % 175.52/25.79 % (1991230)Time elapsed: 4.695 s % 175.52/25.79 % (1991230)Peak memory usage: 97 MB % 175.52/25.79 % (1991230)Instructions burned: 13094 (million) % 175.52/25.79 % (1991259)------------------------------ % 175.52/25.79 % (1991259)------------------------------ % 175.52/25.79 % (1991263)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=794666968:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2884 on theBenchmark for (2884ds/6258Mi) % 175.52/25.79 % (1991257)Instruction limit reached! % 175.52/25.79 % (1991257)------------------------------ % 175.52/25.79 % (1991257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.52/25.79 % (1991257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.52/25.79 % (1991257)CaDiCaL version: 2.1.3 % 175.52/25.79 % (1991257)Termination reason: Instruction limit % 175.52/25.79 % (1991257)Termination phase: Saturation % 175.52/25.79 % (1991257)Time elapsed: 0.832 s % 175.52/25.79 % (1991257)Peak memory usage: 134 MB % 175.52/25.79 % (1991257)Instructions burned: 4083 (million) % 175.52/25.79 % (1991264)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3554413737:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2883 on theBenchmark for (2883ds/34001Mi) % 175.52/25.79 % (1991266)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=390290572:s2a=on:i=71622:s2at=-1:rtra=on_2881 on theBenchmark for (2881ds/71622Mi) % 175.52/25.79 % (1991229)Instruction limit reached! % 175.52/25.79 % (1991229)------------------------------ % 175.52/25.79 % (1991229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 175.52/25.79 % (1991229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 175.52/25.79 % (1991229)CaDiCaL version: 2.1.3 % 175.52/25.79 % (1991229)Termination reason: Instruction limit % 175.52/25.79 % (1991229)Termination phase: Saturation % 175.52/25.79 % (1991229)Time elapsed: 6.406 s % 175.52/25.79 % (1991229)Peak memory usage: 93 MB % 175.52/25.79 % (1991229)Instructions burned: 17168 (million) % 175.52/25.79 % (1991271)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4225272343:i=24001:kws=precedence:nm=0:rtra=on_2867 on theBenchmark for (2867ds/24001Mi) % 195.46/28.52 % (1991263)Instruction limit reached! % 195.46/28.52 % (1991263)------------------------------ % 195.46/28.52 % (1991263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.46/28.52 % (1991263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.46/28.52 % (1991263)CaDiCaL version: 2.1.3 % 195.46/28.52 % (1991263)Termination reason: Instruction limit % 195.46/28.52 % (1991263)Termination phase: Saturation % 195.46/28.52 % (1991263)Time elapsed: 2.276 s % 195.46/28.52 % (1991263)Peak memory usage: 128 MB % 195.46/28.52 % (1991263)Instructions burned: 6259 (million) % 195.46/28.52 % (1991417)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=2824694462:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2859 on theBenchmark for (2859ds/2076Mi) % 195.46/28.52 % (1991250)Instruction limit reached! % 195.46/28.52 % (1991250)------------------------------ % 195.46/28.52 % (1991250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.46/28.52 % (1991250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.46/28.52 % (1991250)CaDiCaL version: 2.1.3 % 195.46/28.52 % (1991250)Termination reason: Instruction limit % 195.46/28.52 % (1991250)Termination phase: Saturation % 195.46/28.52 % (1991250)Time elapsed: 4.326 s % 195.46/28.52 % (1991250)Peak memory usage: 126 MB % 195.46/28.52 % (1991250)Instructions burned: 11749 (million) % 195.46/28.52 % (1991497)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=10464006:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2857 on theBenchmark for (2857ds/83971Mi) % 195.46/28.52 % (1991417)Instruction limit reached! % 195.46/28.52 % (1991417)------------------------------ % 195.46/28.52 % (1991417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.46/28.52 % (1991417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.46/28.52 % (1991417)CaDiCaL version: 2.1.3 % 195.46/28.52 % (1991417)Termination reason: Instruction limit % 195.46/28.52 % (1991417)Termination phase: Saturation % 195.46/28.52 % (1991417)Time elapsed: 1.194 s % 195.46/28.52 % (1991417)Peak memory usage: 116 MB % 195.46/28.52 % (1991417)Instructions burned: 2077 (million) % 195.46/28.52 % (1991661)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=3952096751:i=83944:rtra=on_2846 on theBenchmark for (2846ds/83944Mi) % 195.46/28.52 % (1991189)Instruction limit reached! % 195.46/28.52 % (1991189)------------------------------ % 195.46/28.52 % (1991189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.46/28.52 % (1991189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.46/28.52 % (1991189)CaDiCaL version: 2.1.3 % 195.46/28.52 % (1991189)Termination reason: Instruction limit % 195.46/28.52 % (1991189)Termination phase: Saturation % 195.46/28.52 % (1991189)Time elapsed: 14.174 s % 195.46/28.52 % (1991189)Peak memory usage: 119 MB % 195.46/28.52 % (1991189)Instructions burned: 36819 (million) % 195.46/28.52 % (1991834)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2270264310:i=9201:rtra=on_2817 on theBenchmark for (2817ds/9201Mi) % 195.46/28.52 % (1991834)Instruction limit reached! % 195.46/28.52 % (1991834)------------------------------ % 195.46/28.52 % (1991834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.46/28.52 % (1991834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.46/28.52 % (1991834)CaDiCaL version: 2.1.3 % 195.46/28.52 % (1991834)Termination reason: Instruction limit % 195.46/28.52 % (1991834)Termination phase: Saturation % 195.46/28.52 % (1991834)Time elapsed: 3.376 s % 195.46/28.52 % (1991834)Peak memory usage: 92 MB % 195.46/28.52 % (1991834)Instructions burned: 9203 (million) % 195.46/28.52 % (1991836)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 % 195.46/28.52 % (1991836)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3057478677:i=6806:aac=none:nm=0:rtra=on:rawr=on_2782 on theBenchmark for (2782ds/6806Mi) % 195.46/28.52 % (1991271)Instruction limit reached! % 195.46/28.52 % (1991271)------------------------------ % 195.46/28.52 % (1991271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.46/28.52 % (1991271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.63/29.81 % (1991271)CaDiCaL version: 2.1.3 % 204.63/29.81 % (1991271)Termination reason: Instruction limit % 204.63/29.81 % (1991271)Termination phase: Saturation % 204.63/29.81 % (1991271)Time elapsed: 9.156 s % 204.63/29.81 % (1991271)Peak memory usage: 144 MB % 204.63/29.81 % (1991271)Instructions burned: 24002 (million) % 204.63/29.81 % (1991838)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=4043307966:s2a=on:i=3553:nm=0:rtra=on_2774 on theBenchmark for (2774ds/3553Mi) % 204.63/29.81 % (1991838)Instruction limit reached! % 204.63/29.81 % (1991838)------------------------------ % 204.63/29.81 % (1991838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.63/29.81 % (1991838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.63/29.81 % (1991838)CaDiCaL version: 2.1.3 % 204.63/29.81 % (1991838)Termination reason: Instruction limit % 204.63/29.81 % (1991838)Termination phase: Saturation % 204.63/29.81 % (1991838)Time elapsed: 1.291 s % 204.63/29.81 % (1991838)Peak memory usage: 95 MB % 204.63/29.81 % (1991838)Instructions burned: 3553 (million) % 204.63/29.81 % (1991840)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=2555701374:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2759 on theBenchmark for (2759ds/2064Mi) % 204.63/29.81 % (1991836)Instruction limit reached! % 204.63/29.81 % (1991836)------------------------------ % 204.63/29.81 % (1991836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.63/29.81 % (1991836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.63/29.81 % (1991836)CaDiCaL version: 2.1.3 % 204.63/29.81 % (1991836)Termination reason: Instruction limit % 204.63/29.81 % (1991836)Termination phase: Saturation % 204.63/29.81 % (1991836)Time elapsed: 2.492 s % 204.63/29.81 % (1991836)Peak memory usage: 125 MB % 204.63/29.81 % (1991836)Instructions burned: 6807 (million) % 204.63/29.81 % (1991842)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=1063712118:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2755 on theBenchmark for (2755ds/20260Mi) % 204.63/29.81 % (1991842)Refutation not found, incomplete strategy % 204.63/29.81 % (1991842)------------------------------ % 204.63/29.81 % (1991842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.63/29.81 % (1991842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.63/29.81 % (1991842)CaDiCaL version: 2.1.3 % 204.63/29.81 % (1991842)Termination reason: Refutation not found, incomplete strategy % 204.63/29.81 % (1991842)Time elapsed: 0.079 s % 204.63/29.81 % (1991842)Peak memory usage: 113 MB % 204.63/29.81 % (1991842)Instructions burned: 147 (million) % 204.63/29.81 % (1991842)------------------------------ % 204.63/29.81 % (1991842)------------------------------ % 204.63/29.81 % (1991264)Instruction limit reached! % 204.63/29.81 % (1991264)------------------------------ % 204.63/29.81 % (1991264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.63/29.81 % (1991264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.63/29.81 % (1991264)CaDiCaL version: 2.1.3 % 204.63/29.81 % (1991264)Termination reason: Instruction limit % 204.63/29.81 % (1991264)Termination phase: Saturation % 204.63/29.81 % (1991264)Time elapsed: 13.118 s % 204.63/29.81 % (1991264)Peak memory usage: 93 MB % 204.63/29.81 % (1991264)Instructions burned: 34002 (million) % 204.63/29.81 % (1991840)Instruction limit reached! % 204.63/29.81 % (1991840)------------------------------ % 204.63/29.81 % (1991840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.63/29.81 % (1991840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.63/29.81 % (1991840)CaDiCaL version: 2.1.3 % 204.63/29.81 % (1991840)Termination reason: Instruction limit % 204.63/29.81 % (1991840)Termination phase: Saturation % 204.63/29.81 % (1991840)Time elapsed: 0.801 s % 204.63/29.81 % (1991840)Peak memory usage: 133 MB % 204.63/29.81 % (1991840)Instructions burned: 2065 (million) % 204.63/29.81 % (1991844)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=458253278:avsq=on:i=1244:avsqr=1,16:rtra=on:rawr=on_2750 on theBenchmark for (2750ds/1244Mi) % 204.63/29.81 % (1991845)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=1842770119:i=58261:doe=on:nm=0:rtra=on:gtg=exists_sym_2750 on theBenchmark for (2750ds/58261Mi) % 204.63/29.81 % (1991846)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 % 212.47/30.92 % (1991846)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1956412045:i=6806:aac=none:nm=0:rtra=on:rawr=on_2750 on theBenchmark for (2750ds/6806Mi) % 212.47/30.92 % (1991844)Instruction limit reached! % 212.47/30.92 % (1991844)------------------------------ % 212.47/30.92 % (1991844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.47/30.92 % (1991844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.92 % (1991844)CaDiCaL version: 2.1.3 % 212.47/30.92 % (1991844)Termination reason: Instruction limit % 212.47/30.92 % (1991844)Termination phase: Saturation % 212.47/30.92 % (1991844)Time elapsed: 0.475 s % 212.47/30.92 % (1991844)Peak memory usage: 114 MB % 212.47/30.92 % (1991844)Instructions burned: 1245 (million) % 212.47/30.92 % (1991850)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=3888720799:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2744 on theBenchmark for (2744ds/4081Mi) % 212.47/30.92 % (1991266)Instruction limit reached! % 212.47/30.92 % (1991266)------------------------------ % 212.47/30.92 % (1991266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.47/30.92 % (1991266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.92 % (1991266)CaDiCaL version: 2.1.3 % 212.47/30.92 % (1991266)Termination reason: Instruction limit % 212.47/30.92 % (1991266)Termination phase: Saturation % 212.47/30.92 % (1991266)Time elapsed: 14.014 s % 212.47/30.92 % (1991266)Peak memory usage: 110 MB % 212.47/30.92 % (1991266)Instructions burned: 71625 (million) % 212.47/30.92 % (1991852)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2881220375:avsq=on:i=1701:avsqr=1,16:rtra=on:rawr=on_2740 on theBenchmark for (2740ds/1701Mi) % 212.47/30.92 % (1991852)Instruction limit reached! % 212.47/30.92 % (1991852)------------------------------ % 212.47/30.92 % (1991852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.47/30.92 % (1991852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.92 % (1991852)CaDiCaL version: 2.1.3 % 212.47/30.92 % (1991852)Termination reason: Instruction limit % 212.47/30.92 % (1991852)Termination phase: Saturation % 212.47/30.92 % (1991852)Time elapsed: 0.345 s % 212.47/30.92 % (1991852)Peak memory usage: 117 MB % 212.47/30.92 % (1991852)Instructions burned: 1705 (million) % 212.47/30.92 % (1991854)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=2206095549:i=57001:doe=on:nm=0:rtra=on:gtg=exists_sym_2735 on theBenchmark for (2735ds/57001Mi) % 212.47/30.92 % (1991850)Instruction limit reached! % 212.47/30.92 % (1991850)------------------------------ % 212.47/30.92 % (1991850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.47/30.92 % (1991850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.92 % (1991850)CaDiCaL version: 2.1.3 % 212.47/30.92 % (1991850)Termination reason: Instruction limit % 212.47/30.92 % (1991850)Termination phase: Saturation % 212.47/30.92 % (1991850)Time elapsed: 1.543 s % 212.47/30.92 % (1991850)Peak memory usage: 135 MB % 212.47/30.92 % (1991850)Instructions burned: 4083 (million) % 212.47/30.92 % (1991856)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 % 212.47/30.92 % (1991856)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3926188849:i=8622:aac=none:nm=0:rtra=on:rawr=on_2727 on theBenchmark for (2727ds/8622Mi) % 212.47/30.92 % (1991846)Instruction limit reached! % 212.47/30.92 % (1991846)------------------------------ % 212.47/30.92 % (1991846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.47/30.92 % (1991846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.47/30.92 % (1991846)CaDiCaL version: 2.1.3 % 212.47/30.92 % (1991846)Termination reason: Instruction limit % 212.47/30.92 % (1991846)Termination phase: Saturation % 212.47/30.92 % (1991846)Time elapsed: 2.542 s % 212.47/30.92 % (1991846)Peak memory usage: 125 MB % 212.47/30.92 % (1991846)Instructions burned: 6808 (million) % 212.47/30.92 % (1991858)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=222823289:i=24:doe=on:rtra=on:gtg=exists_top:ss=axioms_2723 on theBenchmark for (2723ds/24Mi) % 217.73/31.73 % (1991858)Instruction limit reached! % 217.73/31.73 % (1991858)------------------------------ % 217.73/31.73 % (1991858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.73/31.73 % (1991858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.73/31.73 % (1991858)CaDiCaL version: 2.1.3 % 217.73/31.73 % (1991858)Termination reason: Instruction limit % 217.73/31.73 % (1991858)Termination phase: Property scanning % 217.73/31.73 % (1991858)Time elapsed: 0.010 s % 217.73/31.73 % (1991858)Peak memory usage: 85 MB % 217.73/31.73 % (1991858)Instructions burned: 26 (million) % 217.73/31.73 % (1991860)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3373722378:i=614:kws=precedence:nm=0:rtra=on_2721 on theBenchmark for (2721ds/614Mi) % 217.73/31.73 % (1991860)Instruction limit reached! % 217.73/31.73 % (1991860)------------------------------ % 217.73/31.73 % (1991860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.73/31.73 % (1991860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.73/31.73 % (1991860)CaDiCaL version: 2.1.3 % 217.73/31.73 % (1991860)Termination reason: Instruction limit % 217.73/31.73 % (1991860)Termination phase: Saturation % 217.73/31.73 % (1991860)Time elapsed: 0.249 s % 217.73/31.73 % (1991860)Peak memory usage: 113 MB % 217.73/31.73 % (1991860)Instructions burned: 615 (million) % 217.73/31.73 % (1991863)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4133103241:i=402:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2717 on theBenchmark for (2717ds/402Mi) % 217.73/31.73 % (1991863)Instruction limit reached! % 217.73/31.73 % (1991863)------------------------------ % 217.73/31.73 % (1991863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.73/31.73 % (1991863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.73/31.73 % (1991863)CaDiCaL version: 2.1.3 % 217.73/31.73 % (1991863)Termination reason: Instruction limit % 217.73/31.73 % (1991863)Termination phase: Property scanning % 217.73/31.73 % (1991863)Time elapsed: 0.148 s % 217.73/31.73 % (1991863)Peak memory usage: 86 MB % 217.73/31.73 % (1991863)Instructions burned: 403 (million) % 217.73/31.73 % (1991866)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=548321002:s2a=on:i=14:rtra=on:inst=on_2714 on theBenchmark for (2714ds/14Mi) % 217.73/31.73 % (1991866)Instruction limit reached! % 217.73/31.73 % (1991866)------------------------------ % 217.73/31.73 % (1991866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.73/31.73 % (1991866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.73/31.73 % (1991866)CaDiCaL version: 2.1.3 % 217.73/31.73 % (1991866)Termination reason: Instruction limit % 217.73/31.73 % (1991866)Termination phase: shuffling % 217.73/31.73 % (1991866)Time elapsed: 0.006 s % 217.73/31.73 % (1991866)Peak memory usage: 85 MB % 217.73/31.73 % (1991866)Instructions burned: 15 (million) % 217.73/31.73 % (1991871)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3980826386:i=8:rtra=on_2712 on theBenchmark for (2712ds/8Mi) % 217.73/31.73 % (1991871)Instruction limit reached! % 217.73/31.73 % (1991871)------------------------------ % 217.73/31.73 % (1991871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.73/31.73 % (1991871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.73/31.73 % (1991871)CaDiCaL version: 2.1.3 % 217.73/31.73 % (1991871)Termination reason: Instruction limit % 217.73/31.73 % (1991871)Termination phase: shuffling % 217.73/31.73 % (1991871)Time elapsed: 0.004 s % 217.73/31.73 % (1991871)Peak memory usage: 85 MB % 217.73/31.73 % (1991871)Instructions burned: 10 (million) % 217.73/31.73 % (1991903)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=586070470:i=92:rtra=on_2710 on theBenchmark for (2710ds/92Mi) % 217.73/31.73 % (1991903)Instruction limit reached! % 217.73/31.73 % (1991903)------------------------------ % 217.73/31.73 % (1991903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.73/31.73 % (1991903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.73/31.73 % (1991903)CaDiCaL version: 2.1.3 % 217.73/31.73 % (1991903)Termination reason: Instruction limit % 217.73/31.73 % (1991903)Termination phase: Property scanning % 217.73/31.73 % (1991903)Time elapsed: 0.035 s % 217.73/31.73 % (1991903)Peak memory usage: 86 MB % 222.38/32.35 % (1991903)Instructions burned: 93 (million) % 222.38/32.35 % (1991932)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1416662487:i=66:rtra=on_2708 on theBenchmark for (2708ds/66Mi) % 222.38/32.35 % (1991932)Instruction limit reached! % 222.38/32.35 % (1991932)------------------------------ % 222.38/32.35 % (1991932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.38/32.35 % (1991932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.38/32.35 % (1991932)CaDiCaL version: 2.1.3 % 222.38/32.35 % (1991932)Termination reason: Instruction limit % 222.38/32.35 % (1991932)Termination phase: Property scanning % 222.38/32.35 % (1991932)Time elapsed: 0.025 s % 222.38/32.35 % (1991932)Peak memory usage: 86 MB % 222.38/32.35 % (1991932)Instructions burned: 67 (million) % 222.38/32.35 % (1991934)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2201177265:st=5:i=28:sd=10:rtra=on:ss=axioms:rawr=on_2706 on theBenchmark for (2706ds/28Mi) % 222.38/32.35 % (1991934)Instruction limit reached! % 222.38/32.35 % (1991934)------------------------------ % 222.38/32.35 % (1991934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.38/32.35 % (1991934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.38/32.35 % (1991934)CaDiCaL version: 2.1.3 % 222.38/32.35 % (1991934)Termination reason: Instruction limit % 222.38/32.35 % (1991934)Termination phase: Property scanning % 222.38/32.35 % (1991934)Time elapsed: 0.013 s % 222.38/32.35 % (1991934)Peak memory usage: 86 MB % 222.38/32.35 % (1991934)Instructions burned: 31 (million) % 222.38/32.35 % (1991936)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=2897071415:i=58:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2704 on theBenchmark for (2704ds/58Mi) % 222.38/32.35 % (1991936)Instruction limit reached! % 222.38/32.35 % (1991936)------------------------------ % 222.38/32.35 % (1991936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.38/32.35 % (1991936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.38/32.35 % (1991936)CaDiCaL version: 2.1.3 % 222.38/32.35 % (1991936)Termination reason: Instruction limit % 222.38/32.35 % (1991936)Termination phase: Property scanning % 222.38/32.35 % (1991936)Time elapsed: 0.023 s % 222.38/32.35 % (1991936)Peak memory usage: 86 MB % 222.38/32.35 % (1991936)Instructions burned: 60 (million) % 222.38/32.35 % (1991938)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1587602545:cond=on:i=32:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2703 on theBenchmark for (2703ds/32Mi) % 222.38/32.35 % (1991938)Instruction limit reached! % 222.38/32.35 % (1991938)------------------------------ % 222.38/32.35 % (1991938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.38/32.35 % (1991938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.38/32.35 % (1991938)CaDiCaL version: 2.1.3 % 222.38/32.35 % (1991938)Termination reason: Instruction limit % 222.38/32.35 % (1991938)Termination phase: Property scanning % 222.38/32.35 % (1991938)Time elapsed: 0.014 s % 222.38/32.35 % (1991938)Peak memory usage: 85 MB % 222.38/32.35 % (1991938)Instructions burned: 34 (million) % 222.38/32.35 % (1991940)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2879845173:i=48:canc=force:rtra=on_2701 on theBenchmark for (2701ds/48Mi) % 222.38/32.35 % (1991940)Instruction limit reached! % 222.38/32.35 % (1991940)------------------------------ % 222.38/32.35 % (1991940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.38/32.35 % (1991940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.38/32.35 % (1991940)CaDiCaL version: 2.1.3 % 222.38/32.35 % (1991940)Termination reason: Instruction limit % 222.38/32.35 % (1991940)Termination phase: Property scanning % 222.38/32.35 % (1991940)Time elapsed: 0.019 s % 222.38/32.35 % (1991940)Peak memory usage: 85 MB % 222.38/32.35 % (1991940)Instructions burned: 48 (million) % 222.38/32.35 % (1991942)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=1223979086:i=54:canc=cautious:fsr=off:rtra=on_2699 on theBenchmark for (2699ds/54Mi) % 222.38/32.35 % (1991942)Instruction limit reached! % 222.38/32.35 % (1991942)------------------------------ % 222.38/32.35 % (1991942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.38/32.35 % (1991942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.38/32.35 % (1991942)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991942)Termination reason: Instruction limit % 227.73/33.05 % (1991942)Termination phase: Property scanning % 227.73/33.05 % (1991942)Time elapsed: 0.022 s % 227.73/33.05 % (1991942)Peak memory usage: 85 MB % 227.73/33.05 % (1991942)Instructions burned: 56 (million) % 227.73/33.05 % (1991944)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3178473874:i=170:gtgl=4:rtra=on:gtg=exists_sym_2697 on theBenchmark for (2697ds/170Mi) % 227.73/33.05 % (1991944)Instruction limit reached! % 227.73/33.05 % (1991944)------------------------------ % 227.73/33.05 % (1991944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.73/33.05 % (1991944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.73/33.05 % (1991944)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991944)Termination reason: Instruction limit % 227.73/33.05 % (1991944)Termination phase: Property scanning % 227.73/33.05 % (1991944)Time elapsed: 0.063 s % 227.73/33.05 % (1991944)Peak memory usage: 85 MB % 227.73/33.05 % (1991944)Instructions burned: 173 (million) % 227.73/33.05 % (1991856)Instruction limit reached! % 227.73/33.05 % (1991856)------------------------------ % 227.73/33.05 % (1991856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.73/33.05 % (1991856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.73/33.05 % (1991856)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991856)Termination reason: Instruction limit % 227.73/33.05 % (1991856)Termination phase: Saturation % 227.73/33.05 % (1991856)Time elapsed: 3.231 s % 227.73/33.05 % (1991856)Peak memory usage: 126 MB % 227.73/33.05 % (1991856)Instructions burned: 8625 (million) % 227.73/33.05 % (1991946)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3740543844:i=4:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2694 on theBenchmark for (2694ds/4Mi) % 227.73/33.05 % (1991946)Instruction limit reached! % 227.73/33.05 % (1991946)------------------------------ % 227.73/33.05 % (1991946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.73/33.05 % (1991946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.73/33.05 % (1991946)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991946)Termination reason: Instruction limit % 227.73/33.05 % (1991946)Termination phase: shuffling % 227.73/33.05 % (1991946)Time elapsed: 0.002 s % 227.73/33.05 % (1991946)Peak memory usage: 85 MB % 227.73/33.05 % (1991946)Instructions burned: 4 (million) % 227.73/33.05 % (1991947)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=545744788:i=362:rtra=on:ss=axioms:ev=cautious_2693 on theBenchmark for (2693ds/362Mi) % 227.73/33.05 % (1991949)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=741050928:i=8:ep=RST:ins=2:rtra=on_2693 on theBenchmark for (2693ds/8Mi) % 227.73/33.05 % (1991949)Instruction limit reached! % 227.73/33.05 % (1991949)------------------------------ % 227.73/33.05 % (1991949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.73/33.05 % (1991949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.73/33.05 % (1991949)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991949)Termination reason: Instruction limit % 227.73/33.05 % (1991949)Termination phase: shuffling % 227.73/33.05 % (1991949)Time elapsed: 0.004 s % 227.73/33.05 % (1991949)Peak memory usage: 85 MB % 227.73/33.05 % (1991949)Instructions burned: 9 (million) % 227.73/33.05 % (1991947)Refutation not found, incomplete strategy % 227.73/33.05 % (1991947)------------------------------ % 227.73/33.05 % (1991947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.73/33.05 % (1991947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.73/33.05 % (1991947)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991947)Termination reason: Refutation not found, incomplete strategy % 227.73/33.05 % (1991947)Time elapsed: 0.062 s % 227.73/33.05 % (1991947)Peak memory usage: 88 MB % 227.73/33.05 % (1991947)Instructions burned: 174 (million) % 227.73/33.05 % (1991952)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3530271377:i=132:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2691 on theBenchmark for (2691ds/132Mi) % 227.73/33.05 % (1991952)Instruction limit reached! % 227.73/33.05 % (1991952)------------------------------ % 227.73/33.05 % (1991952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.73/33.05 % (1991952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.73/33.05 % (1991952)CaDiCaL version: 2.1.3 % 227.73/33.05 % (1991952)Termination reason: Instruction limit % 227.73/33.05 % (1991952)Termination phase: Property scanning % 233.43/33.95 % (1991952)Time elapsed: 0.049 s % 233.43/33.95 % (1991952)Peak memory usage: 86 MB % 233.43/33.95 % (1991952)Instructions burned: 132 (million) % 233.43/33.95 % (1991947)------------------------------ % 233.43/33.95 % (1991947)------------------------------ % 233.43/33.95 % (1991954)lrs+10_1_thi=all:si=on:fd=off:random_seed=2747378180:i=106:rtra=on:gtg=all_2689 on theBenchmark for (2689ds/106Mi) % 233.43/33.95 % (1991954)Instruction limit reached! % 233.43/33.95 % (1991954)------------------------------ % 233.43/33.95 % (1991954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.43/33.95 % (1991954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.43/33.95 % (1991954)CaDiCaL version: 2.1.3 % 233.43/33.95 % (1991954)Termination reason: Instruction limit % 233.43/33.95 % (1991954)Termination phase: shuffling % 233.43/33.95 % (1991954)Time elapsed: 0.039 s % 233.43/33.95 % (1991954)Peak memory usage: 85 MB % 233.43/33.95 % (1991954)Instructions burned: 108 (million) % 233.43/33.95 % (1991955)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=321034719:i=16:ep=RST:nm=16:rtra=on:gtg=exists_top_2688 on theBenchmark for (2688ds/16Mi) % 233.43/33.95 % (1991955)Instruction limit reached! % 233.43/33.95 % (1991955)------------------------------ % 233.43/33.95 % (1991955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.43/33.95 % (1991955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.43/33.95 % (1991955)CaDiCaL version: 2.1.3 % 233.43/33.95 % (1991955)Termination reason: Instruction limit % 233.43/33.95 % (1991955)Termination phase: Property scanning % 233.43/33.95 % (1991955)Time elapsed: 0.007 s % 233.43/33.95 % (1991955)Peak memory usage: 85 MB % 233.43/33.95 % (1991955)Instructions burned: 19 (million) % 233.43/33.95 % (1991957)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4190604574:st=3:i=4:rtra=on:ss=axioms_2687 on theBenchmark for (2687ds/4Mi) % 233.43/33.95 % (1991957)Instruction limit reached! % 233.43/33.95 % (1991957)------------------------------ % 233.43/33.95 % (1991957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.43/33.95 % (1991957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.43/33.95 % (1991957)CaDiCaL version: 2.1.3 % 233.43/33.95 % (1991957)Termination reason: Instruction limit % 233.43/33.95 % (1991957)Termination phase: shuffling % 233.43/33.95 % (1991957)Time elapsed: 0.002 s % 233.43/33.95 % (1991957)Peak memory usage: 85 MB % 233.43/33.95 % (1991957)Instructions burned: 4 (million) % 233.43/33.95 % (1991959)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1194987772:i=4:doe=on:canc=force:asg=cautious:rtra=on_2686 on theBenchmark for (2686ds/4Mi) % 233.43/33.95 % (1991959)Instruction limit reached! % 233.43/33.95 % (1991959)------------------------------ % 233.43/33.95 % (1991959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.43/33.95 % (1991959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.43/33.95 % (1991959)CaDiCaL version: 2.1.3 % 233.43/33.95 % (1991959)Termination reason: Instruction limit % 233.43/33.95 % (1991959)Termination phase: shuffling % 233.43/33.95 % (1991959)Time elapsed: 0.002 s % 233.43/33.95 % (1991959)Peak memory usage: 85 MB % 233.43/33.95 % (1991959)Instructions burned: 4 (million) % 233.43/33.95 % (1991961)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=208122905:i=254:doe=on:rtra=on_2685 on theBenchmark for (2685ds/254Mi) % 233.43/33.95 % (1991963)dis+10_1_si=on:random_seed=1758889917:i=20:ep=R:rtra=on_2685 on theBenchmark for (2685ds/20Mi) % 233.43/33.95 % (1991963)Instruction limit reached! % 233.43/33.95 % (1991963)------------------------------ % 233.43/33.95 % (1991963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.43/33.95 % (1991963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.43/33.95 % (1991963)CaDiCaL version: 2.1.3 % 233.43/33.95 % (1991963)Termination reason: Instruction limit % 233.43/33.95 % (1991963)Termination phase: Property scanning % 233.43/33.95 % (1991963)Time elapsed: 0.009 s % 233.43/33.95 % (1991963)Peak memory usage: 86 MB % 233.43/33.95 % (1991963)Instructions burned: 22 (million) % 233.43/33.95 % (1991961)Instruction limit reached! % 233.43/33.95 % (1991961)------------------------------ % 233.43/33.95 % (1991961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.43/33.95 % (1991961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.43/33.95 % (1991961)CaDiCaL version: 2.1.3 % 233.43/33.95 % (1991961)Termination reason: Instruction limit % 233.43/33.95 % (1991961)Termination phase: Property scanning % 237.90/34.61 % (1991961)Time elapsed: 0.094 s % 237.90/34.61 % (1991961)Peak memory usage: 86 MB % 237.90/34.61 % (1991961)Instructions burned: 256 (million) % 237.90/34.61 % (1991966)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3706219632:i=52:canc=cautious:av=off:rtra=on_2683 on theBenchmark for (2683ds/52Mi) % 237.90/34.61 % (1991966)Instruction limit reached! % 237.90/34.61 % (1991966)------------------------------ % 237.90/34.61 % (1991966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.90/34.61 % (1991966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.90/34.61 % (1991966)CaDiCaL version: 2.1.3 % 237.90/34.61 % (1991966)Termination reason: Instruction limit % 237.90/34.61 % (1991966)Termination phase: Property scanning % 237.90/34.61 % (1991966)Time elapsed: 0.021 s % 237.90/34.61 % (1991966)Peak memory usage: 86 MB % 237.90/34.61 % (1991966)Instructions burned: 54 (million) % 237.90/34.61 % (1991967)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3051103970:avsq=on:i=70:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2683 on theBenchmark for (2683ds/70Mi) % 237.90/34.61 % (1991967)Instruction limit reached! % 237.90/34.61 % (1991967)------------------------------ % 237.90/34.61 % (1991967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.90/34.61 % (1991967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.90/34.61 % (1991967)CaDiCaL version: 2.1.3 % 237.90/34.61 % (1991967)Termination reason: Instruction limit % 237.90/34.61 % (1991967)Termination phase: Property scanning % 237.90/34.61 % (1991967)Time elapsed: 0.027 s % 237.90/34.61 % (1991967)Peak memory usage: 86 MB % 237.90/34.61 % (1991967)Instructions burned: 71 (million) % 237.90/34.61 % (1991969)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2169891785:i=4:fsr=off:rtra=on:inst=on_2681 on theBenchmark for (2681ds/4Mi) % 237.90/34.61 % (1991969)Instruction limit reached! % 237.90/34.61 % (1991969)------------------------------ % 237.90/34.61 % (1991969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.90/34.61 % (1991969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.90/34.61 % (1991969)CaDiCaL version: 2.1.3 % 237.90/34.61 % (1991969)Termination reason: Instruction limit % 237.90/34.61 % (1991969)Termination phase: shuffling % 237.90/34.61 % (1991969)Time elapsed: 0.002 s % 237.90/34.61 % (1991969)Peak memory usage: 85 MB % 237.90/34.61 % (1991969)Instructions burned: 4 (million) % 237.90/34.61 % (1991971)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2097408154:s2a=on:i=16:kws=inv_precedence:doe=on:rtra=on_2681 on theBenchmark for (2681ds/16Mi) % 237.90/34.61 % (1991971)Instruction limit reached! % 237.90/34.61 % (1991971)------------------------------ % 237.90/34.61 % (1991971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.90/34.61 % (1991971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.90/34.61 % (1991971)CaDiCaL version: 2.1.3 % 237.90/34.61 % (1991971)Termination reason: Instruction limit % 237.90/34.61 % (1991971)Termination phase: shuffling % 237.90/34.61 % (1991971)Time elapsed: 0.007 s % 237.90/34.61 % (1991971)Peak memory usage: 85 MB % 237.90/34.61 % (1991971)Instructions burned: 17 (million) % 237.90/34.61 % (1991973)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1620561986:i=740:ep=RS:fsr=off:rtra=on_2680 on theBenchmark for (2680ds/740Mi) % 237.90/34.61 % (1991975)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2614178282:i=26:av=off:rtra=on:gtg=exists_sym:ev=force_2679 on theBenchmark for (2679ds/26Mi) % 237.90/34.61 % (1991975)Instruction limit reached! % 237.90/34.61 % (1991975)------------------------------ % 237.90/34.61 % (1991975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.90/34.61 % (1991975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.90/34.61 % (1991975)CaDiCaL version: 2.1.3 % 237.90/34.61 % (1991975)Termination reason: Instruction limit % 237.90/34.61 % (1991975)Termination phase: Property scanning % 237.90/34.61 % (1991975)Time elapsed: 0.010 s % 237.90/34.61 % (1991975)Peak memory usage: 85 MB % 237.90/34.61 % (1991975)Instructions burned: 28 (million) % 237.90/34.61 % (1991978)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3840451247:i=452:rtra=on:gtg=position:ss=axioms_2677 on theBenchmark for (2677ds/452Mi) % 237.90/34.61 % (1991973)Refutation not found, incomplete strategy % 245.04/35.59 % (1991973)------------------------------ % 245.04/35.59 % (1991973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.04/35.59 % (1991973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.04/35.59 % (1991973)CaDiCaL version: 2.1.3 % 245.04/35.59 % (1991973)Termination reason: Refutation not found, incomplete strategy % 245.04/35.59 % (1991973)Time elapsed: 0.237 s % 245.04/35.59 % (1991973)Peak memory usage: 89 MB % 245.04/35.59 % (1991973)Instructions burned: 640 (million) % 245.04/35.59 % (1991978)Refutation not found, incomplete strategy % 245.04/35.59 % (1991978)------------------------------ % 245.04/35.59 % (1991978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.04/35.59 % (1991978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.04/35.59 % (1991978)CaDiCaL version: 2.1.3 % 245.04/35.59 % (1991978)Termination reason: Refutation not found, incomplete strategy % 245.04/35.59 % (1991978)Time elapsed: 0.126 s % 245.04/35.59 % (1991978)Peak memory usage: 112 MB % 245.04/35.59 % (1991978)Instructions burned: 286 (million) % 245.04/35.59 % (1991973)------------------------------ % 245.04/35.59 % (1991973)------------------------------ % 245.04/35.59 % (1991978)------------------------------ % 245.04/35.59 % (1991978)------------------------------ % 245.04/35.59 % (1991980)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1180134339:i=20:rtra=on_2673 on theBenchmark for (2673ds/20Mi) % 245.04/35.59 % (1991980)Instruction limit reached! % 245.04/35.59 % (1991980)------------------------------ % 245.04/35.59 % (1991980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.04/35.59 % (1991980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.04/35.59 % (1991980)CaDiCaL version: 2.1.3 % 245.04/35.59 % (1991980)Termination reason: Instruction limit % 245.04/35.59 % (1991980)Termination phase: Property scanning % 245.04/35.59 % (1991980)Time elapsed: 0.009 s % 245.04/35.59 % (1991980)Peak memory usage: 86 MB % 245.04/35.59 % (1991980)Instructions burned: 22 (million) % 245.04/35.59 % (1991981)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=310181172:i=142:rtra=on:gtg=exists_top_2672 on theBenchmark for (2672ds/142Mi) % 245.04/35.59 % (1991981)Instruction limit reached! % 245.04/35.59 % (1991981)------------------------------ % 245.04/35.59 % (1991981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.04/35.59 % (1991981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.04/35.59 % (1991981)CaDiCaL version: 2.1.3 % 245.04/35.59 % (1991981)Termination reason: Instruction limit % 245.04/35.59 % (1991981)Termination phase: Property scanning % 245.04/35.59 % (1991981)Time elapsed: 0.052 s % 245.04/35.59 % (1991981)Peak memory usage: 86 MB % 245.04/35.59 % (1991981)Instructions burned: 142 (million) % 245.04/35.59 % (1991983)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=92831832:i=150:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2671 on theBenchmark for (2671ds/150Mi) % 245.04/35.59 % (1991983)Instruction limit reached! % 245.04/35.59 % (1991983)------------------------------ % 245.04/35.59 % (1991983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.04/35.59 % (1991983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.04/35.59 % (1991983)CaDiCaL version: 2.1.3 % 245.04/35.59 % (1991983)Termination reason: Instruction limit % 245.04/35.59 % (1991983)Termination phase: Property scanning % 245.04/35.59 % (1991983)Time elapsed: 0.055 s % 245.04/35.59 % (1991983)Peak memory usage: 86 MB % 245.04/35.59 % (1991983)Instructions burned: 151 (million) % 245.04/35.59 % (1991985)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=572405612:i=588:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2670 on theBenchmark for (2670ds/588Mi) % 245.04/35.59 % (1991987)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1931633080:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2669 on theBenchmark for (2669ds/260Mi) % 245.04/35.59 % (1991987)Instruction limit reached! % 245.04/35.59 % (1991987)------------------------------ % 245.04/35.59 % (1991987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.04/35.59 % (1991987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.04/35.59 % (1991987)CaDiCaL version: 2.1.3 % 245.04/35.59 % (1991987)Termination reason: Instruction limit % 245.04/35.59 % (1991987)Termination phase: Property scanning % 250.15/36.27 % (1991987)Time elapsed: 0.094 s % 250.15/36.27 % (1991987)Peak memory usage: 86 MB % 250.15/36.27 % (1991987)Instructions burned: 260 (million) % 250.15/36.27 % (1991985)Instruction limit reached! % 250.15/36.27 % (1991985)------------------------------ % 250.15/36.27 % (1991985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.15/36.27 % (1991985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.15/36.27 % (1991985)CaDiCaL version: 2.1.3 % 250.15/36.27 % (1991985)Termination reason: Instruction limit % 250.15/36.27 % (1991985)Termination phase: Saturation % 250.15/36.27 % (1991985)Time elapsed: 0.225 s % 250.15/36.27 % (1991985)Peak memory usage: 96 MB % 250.15/36.27 % (1991985)Instructions burned: 589 (million) % 250.15/36.27 % (1991990)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1288914627:i=262:rtra=on_2667 on theBenchmark for (2667ds/262Mi) % 250.15/36.27 % (1991991)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2657401498:i=80:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2666 on theBenchmark for (2666ds/80Mi) % 250.15/36.27 % (1991991)Instruction limit reached! % 250.15/36.27 % (1991991)------------------------------ % 250.15/36.27 % (1991991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.15/36.27 % (1991991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.15/36.27 % (1991991)CaDiCaL version: 2.1.3 % 250.15/36.27 % (1991991)Termination reason: Instruction limit % 250.15/36.27 % (1991991)Termination phase: Property scanning % 250.15/36.27 % (1991991)Time elapsed: 0.029 s % 250.15/36.27 % (1991991)Peak memory usage: 85 MB % 250.15/36.27 % (1991991)Instructions burned: 81 (million) % 250.15/36.27 % (1991990)Instruction limit reached! % 250.15/36.27 % (1991990)------------------------------ % 250.15/36.27 % (1991990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.15/36.27 % (1991990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.15/36.27 % (1991990)CaDiCaL version: 2.1.3 % 250.15/36.27 % (1991990)Termination reason: Instruction limit % 250.15/36.27 % (1991990)Termination phase: Saturation % 250.15/36.27 % (1991990)Time elapsed: 0.134 s % 250.15/36.27 % (1991990)Peak memory usage: 128 MB % 250.15/36.27 % (1991990)Instructions burned: 262 (million) % 250.15/36.27 % (1991260)Instruction limit reached! % 250.15/36.27 % (1991260)------------------------------ % 250.15/36.27 % (1991260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.15/36.27 % (1991260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.15/36.27 % (1991260)CaDiCaL version: 2.1.3 % 250.15/36.27 % (1991260)Termination reason: Instruction limit % 250.15/36.27 % (1991260)Termination phase: Saturation % 250.15/36.27 % (1991260)Time elapsed: 22.258 s % 250.15/36.27 % (1991260)Peak memory usage: 125 MB % 250.15/36.27 % (1991260)Instructions burned: 58628 (million) % 250.15/36.27 % (1991994)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3872232481:i=614:rtra=on:gtg=exists_top_2664 on theBenchmark for (2664ds/614Mi) % 250.15/36.27 % (1991995)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1082542401:s2a=on:i=1196:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2663 on theBenchmark for (2663ds/1196Mi) % 250.15/36.27 % (1991996)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3179011385:i=262:canc=cautious:fsr=off:rtra=on_2663 on theBenchmark for (2663ds/262Mi) % 250.15/36.27 % (1991996)Instruction limit reached! % 250.15/36.27 % (1991996)------------------------------ % 250.15/36.27 % (1991996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.15/36.27 % (1991996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.15/36.27 % (1991996)CaDiCaL version: 2.1.3 % 250.15/36.27 % (1991996)Termination reason: Instruction limit % 250.15/36.27 % (1991996)Termination phase: Property scanning % 250.15/36.27 % (1991996)Time elapsed: 0.095 s % 250.15/36.27 % (1991996)Peak memory usage: 86 MB % 250.15/36.27 % (1991996)Instructions burned: 262 (million) % 250.15/36.27 % (1991994)Instruction limit reached! % 250.15/36.27 % (1991994)------------------------------ % 250.15/36.27 % (1991994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.15/36.27 % (1991994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.15/36.27 % (1991994)CaDiCaL version: 2.1.3 % 250.15/36.27 % (1991994)Termination reason: Instruction limit % 250.15/36.27 % (1991994)Termination phase: Saturation % 250.15/36.27 % (1991994)Time elapsed: 0.220 s % 250.15/36.27 % (1991994)Peak memory usage: 89 MB % 254.63/36.94 % (1991994)Instructions burned: 615 (million) % 254.63/36.94 % (1992001)dis+10_1_si=on:random_seed=1349194897:s2a=on:i=2000:rtra=on:gtg=exists_all_2660 on theBenchmark for (2660ds/2000Mi) % 254.63/36.94 % (1992000)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=2829538006:s2pl=no:i=518:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2660 on theBenchmark for (2660ds/518Mi) % 254.63/36.94 % (1992000)Refutation not found, incomplete strategy % 254.63/36.94 % (1992000)------------------------------ % 254.63/36.94 % (1992000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.63/36.94 % (1992000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.63/36.94 % (1992000)CaDiCaL version: 2.1.3 % 254.63/36.94 % (1992000)Termination reason: Refutation not found, incomplete strategy % 254.63/36.94 % (1992000)Time elapsed: 0.132 s % 254.63/36.94 % (1992000)Peak memory usage: 112 MB % 254.63/36.94 % (1992000)Instructions burned: 300 (million) % 254.63/36.94 % (1991995)Instruction limit reached! % 254.63/36.94 % (1991995)------------------------------ % 254.63/36.94 % (1991995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.63/36.94 % (1991995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.63/36.94 % (1991995)CaDiCaL version: 2.1.3 % 254.63/36.94 % (1991995)Termination reason: Instruction limit % 254.63/36.94 % (1991995)Termination phase: Saturation % 254.63/36.94 % (1991995)Time elapsed: 0.489 s % 254.63/36.94 % (1991995)Peak memory usage: 132 MB % 254.63/36.94 % (1991995)Instructions burned: 1199 (million) % 254.63/36.94 % (1992004)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=34211898:i=766:fsr=off:rtra=on:ev=force_2657 on theBenchmark for (2657ds/766Mi) % 254.63/36.94 % (1992000)------------------------------ % 254.63/36.94 % (1992000)------------------------------ % 254.63/36.94 % (1992006)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1866131785:i=282:doe=on:rtra=on_2655 on theBenchmark for (2655ds/282Mi) % 254.63/36.94 % (1992004)Instruction limit reached! % 254.63/36.94 % (1992004)------------------------------ % 254.63/36.94 % (1992004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.63/36.94 % (1992004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.63/36.94 % (1992004)CaDiCaL version: 2.1.3 % 254.63/36.94 % (1992004)Termination reason: Instruction limit % 254.63/36.94 % (1992004)Termination phase: Saturation % 254.63/36.94 % (1992004)Time elapsed: 0.290 s % 254.63/36.94 % (1992004)Peak memory usage: 89 MB % 254.63/36.94 % (1992004)Instructions burned: 766 (million) % 254.63/36.94 % (1992006)Instruction limit reached! % 254.63/36.94 % (1992006)------------------------------ % 254.63/36.94 % (1992006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.63/36.94 % (1992006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.63/36.94 % (1992006)CaDiCaL version: 2.1.3 % 254.63/36.94 % (1992006)Termination reason: Instruction limit % 254.63/36.94 % (1992006)Termination phase: Property scanning % 254.63/36.94 % (1992006)Time elapsed: 0.102 s % 254.63/36.94 % (1992006)Peak memory usage: 86 MB % 254.63/36.94 % (1992006)Instructions burned: 285 (million) % 254.63/36.94 % (1992001)Instruction limit reached! % 254.63/36.94 % (1992001)------------------------------ % 254.63/36.94 % (1992001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.63/36.95 % (1992001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.63/36.95 % (1992001)CaDiCaL version: 2.1.3 % 254.63/36.95 % (1992001)Termination reason: Instruction limit % 254.63/36.95 % (1992001)Termination phase: Saturation % 254.63/36.95 % (1992001)Time elapsed: 0.754 s % 254.63/36.95 % (1992001)Peak memory usage: 95 MB % 254.63/36.95 % (1992001)Instructions burned: 2001 (million) % 254.63/36.95 % (1992008)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4246045402:i=130:nm=16:rtra=on_2652 on theBenchmark for (2652ds/130Mi) % 254.63/36.95 % (1992009)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=799495760:i=242:nm=16:rtra=on_2652 on theBenchmark for (2652ds/242Mi) % 254.63/36.95 % (1992008)Instruction limit reached! % 254.63/36.95 % (1992008)------------------------------ % 254.63/36.95 % (1992008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 254.63/36.95 % (1992008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 254.63/36.95 % (1992008)CaDiCaL version: 2.1.3 % 261.60/37.94 % (1992008)Termination reason: Instruction limit % 261.60/37.94 % (1992008)Termination phase: Property scanning % 261.60/37.94 % (1992008)Time elapsed: 0.049 s % 261.60/37.94 % (1992008)Peak memory usage: 86 MB % 261.60/37.94 % (1992008)Instructions burned: 133 (million) % 261.60/37.94 % (1992009)Instruction limit reached! % 261.60/37.94 % (1992009)------------------------------ % 261.60/37.94 % (1992009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.60/37.94 % (1992009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.60/37.94 % (1992009)CaDiCaL version: 2.1.3 % 261.60/37.94 % (1992009)Termination reason: Instruction limit % 261.60/37.94 % (1992009)Termination phase: Property scanning % 261.60/37.94 % (1992009)Time elapsed: 0.090 s % 261.60/37.94 % (1992009)Peak memory usage: 86 MB % 261.60/37.94 % (1992009)Instructions burned: 244 (million) % 261.60/37.94 % (1992010)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=2047318717:s2a=on:i=256:s2at=5:ins=3:rtra=on_2651 on theBenchmark for (2651ds/256Mi) % 261.60/37.94 % (1992013)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=3194994065:i=78:ins=3:rtra=on_2650 on theBenchmark for (2650ds/78Mi) % 261.60/37.94 % (1992013)Instruction limit reached! % 261.60/37.94 % (1992013)------------------------------ % 261.60/37.94 % (1992013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.60/37.94 % (1992013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.60/37.94 % (1992013)CaDiCaL version: 2.1.3 % 261.60/37.94 % (1992013)Termination reason: Instruction limit % 261.60/37.94 % (1992013)Termination phase: Property scanning % 261.60/37.94 % (1992013)Time elapsed: 0.029 s % 261.60/37.94 % (1992013)Peak memory usage: 86 MB % 261.60/37.94 % (1992013)Instructions burned: 78 (million) % 261.60/37.94 % (1992010)Instruction limit reached! % 261.60/37.94 % (1992010)------------------------------ % 261.60/37.94 % (1992010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.60/37.94 % (1992010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.60/37.94 % (1992010)CaDiCaL version: 2.1.3 % 261.60/37.94 % (1992010)Termination reason: Instruction limit % 261.60/37.94 % (1992010)Termination phase: Unused predicate definition removal % 261.60/37.94 % (1992010)Time elapsed: 0.096 s % 261.60/37.94 % (1992010)Peak memory usage: 86 MB % 261.60/37.94 % (1992010)Instructions burned: 258 (million) % 261.60/37.94 % (1992014)dis+1010_1_to=kbo:si=on:random_seed=2654631023:i=350:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2649 on theBenchmark for (2649ds/350Mi) % 261.60/37.94 % (1992017)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3936852645:i=658:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2648 on theBenchmark for (2648ds/658Mi) % 261.60/37.94 % (1992018)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1592130056:s2a=on:i=966:doe=on:nm=32:rtra=on_2648 on theBenchmark for (2648ds/966Mi) % 261.60/37.94 % (1992014)Instruction limit reached! % 261.60/37.94 % (1992014)------------------------------ % 261.60/37.94 % (1992014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.60/37.94 % (1992014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.60/37.94 % (1992014)CaDiCaL version: 2.1.3 % 261.60/37.94 % (1992014)Termination reason: Instruction limit % 261.60/37.94 % (1992014)Termination phase: Property scanning % 261.60/37.94 % (1992014)Time elapsed: 0.128 s % 261.60/37.94 % (1992014)Peak memory usage: 86 MB % 261.60/37.94 % (1992014)Instructions burned: 351 (million) % 261.60/37.94 % (1992022)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2936164810:thitd=on:i=430:nm=0:rtra=on:ev=force_2646 on theBenchmark for (2646ds/430Mi) % 261.60/37.94 % (1992017)Instruction limit reached! % 261.60/37.94 % (1992017)------------------------------ % 261.60/37.94 % (1992017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.60/37.94 % (1992017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.60/37.94 % (1992017)CaDiCaL version: 2.1.3 % 261.60/37.94 % (1992017)Termination reason: Instruction limit % 261.60/37.94 % (1992017)Termination phase: Property scanning % 261.60/37.94 % (1992017)Time elapsed: 0.237 s % 261.60/37.94 % (1992017)Peak memory usage: 87 MB % 261.60/37.94 % (1992017)Instructions burned: 660 (million) % 261.60/37.94 % (1992022)Instruction limit reached! % 261.60/37.94 % (1992022)------------------------------ % 261.60/37.94 % (1992022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.86/38.78 % (1992022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.86/38.78 % (1992022)CaDiCaL version: 2.1.3 % 266.86/38.78 % (1992022)Termination reason: Instruction limit % 266.86/38.78 % (1992022)Termination phase: Property scanning % 266.86/38.78 % (1992022)Time elapsed: 0.153 s % 266.86/38.78 % (1992022)Peak memory usage: 87 MB % 266.86/38.78 % (1992022)Instructions burned: 432 (million) % 266.86/38.78 % (1992024)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1996277886:i=698:rtra=on_2645 on theBenchmark for (2645ds/698Mi) % 266.86/38.78 % (1992018)Instruction limit reached! % 266.86/38.78 % (1992018)------------------------------ % 266.86/38.78 % (1992018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.86/38.78 % (1992018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.86/38.78 % (1992018)CaDiCaL version: 2.1.3 % 266.86/38.78 % (1992018)Termination reason: Instruction limit % 266.86/38.78 % (1992018)Termination phase: Saturation % 266.86/38.78 % (1992018)Time elapsed: 0.405 s % 266.86/38.78 % (1992018)Peak memory usage: 130 MB % 266.86/38.78 % (1992018)Instructions burned: 966 (million) % 266.86/38.78 % (1992025)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1659916935:st=2:i=590:rtra=on:ss=axioms_2643 on theBenchmark for (2643ds/590Mi) % 266.86/38.78 % (1992027)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1081611489:i=656:kws=inv_frequency:nm=20:rtra=on_2643 on theBenchmark for (2643ds/656Mi) % 266.86/38.78 % (1992025)Refutation not found, incomplete strategy % 266.86/38.78 % (1992025)------------------------------ % 266.86/38.78 % (1992025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.86/38.78 % (1992025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.86/38.78 % (1992025)CaDiCaL version: 2.1.3 % 266.86/38.78 % (1992025)Termination reason: Refutation not found, incomplete strategy % 266.86/38.78 % (1992025)Time elapsed: 0.104 s % 266.86/38.78 % (1992025)Peak memory usage: 88 MB % 266.86/38.78 % (1992025)Instructions burned: 289 (million) % 266.86/38.78 % (1992024)Instruction limit reached! % 266.86/38.78 % (1992024)------------------------------ % 266.86/38.78 % (1992024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.86/38.78 % (1992024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.86/38.78 % (1992024)CaDiCaL version: 2.1.3 % 266.86/38.78 % (1992024)Termination reason: Instruction limit % 266.86/38.78 % (1992024)Termination phase: Saturation % 266.86/38.78 % (1992024)Time elapsed: 0.281 s % 266.86/38.78 % (1992024)Peak memory usage: 113 MB % 266.86/38.78 % (1992024)Instructions burned: 700 (million) % 266.86/38.78 % (1992030)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1847845060:i=562:gtgl=2:rtra=on:gtg=all_2640 on theBenchmark for (2640ds/562Mi) % 266.86/38.78 % (1992027)Instruction limit reached! % 266.86/38.78 % (1992027)------------------------------ % 266.86/38.78 % (1992027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.86/38.78 % (1992027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.86/38.78 % (1992027)CaDiCaL version: 2.1.3 % 266.86/38.78 % (1992027)Termination reason: Instruction limit % 266.86/38.78 % (1992027)Termination phase: Saturation % 266.86/38.78 % (1992027)Time elapsed: 0.260 s % 266.86/38.78 % (1992027)Peak memory usage: 112 MB % 266.86/38.78 % (1992027)Instructions burned: 658 (million) % 266.86/38.78 % (1992025)------------------------------ % 266.86/38.78 % (1992025)------------------------------ % 266.86/38.78 % (1992033)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1418477194:i=642:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2638 on theBenchmark for (2638ds/642Mi) % 266.86/38.78 % (1992032)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=3152839773:i=968:doe=on:nm=0:av=off:rtra=on:ss=axioms_2638 on theBenchmark for (2638ds/968Mi) % 266.86/38.78 % (1992030)Instruction limit reached! % 266.86/38.78 % (1992030)------------------------------ % 266.86/38.78 % (1992030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.86/38.78 % (1992030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.86/38.78 % (1992030)CaDiCaL version: 2.1.3 % 266.86/38.78 % (1992030)Termination reason: Instruction limit % 266.86/38.78 % (1992030)Termination phase: Property scanning % 266.86/38.78 % (1992030)Time elapsed: 0.200 s % 266.86/38.78 % (1992030)Peak memory usage: 86 MB % 266.86/38.78 % (1992030)Instructions burned: 562 (million) % 278.54/40.25 % (1992032)Refutation not found, incomplete strategy % 278.54/40.25 % (1992032)------------------------------ % 278.54/40.25 % (1992032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.54/40.25 % (1992032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.54/40.25 % (1992032)CaDiCaL version: 2.1.3 % 278.54/40.25 % (1992032)Termination reason: Refutation not found, incomplete strategy % 278.54/40.25 % (1992032)Time elapsed: 0.100 s % 278.54/40.25 % (1992032)Peak memory usage: 88 MB % 278.54/40.25 % (1992032)Instructions burned: 282 (million) % 278.54/40.25 % (1992033)Refutation not found, incomplete strategy % 278.54/40.25 % (1992033)------------------------------ % 278.54/40.25 % (1992033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.54/40.25 % (1992033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.54/40.25 % (1992033)CaDiCaL version: 2.1.3 % 278.54/40.25 % (1992033)Termination reason: Refutation not found, incomplete strategy % 278.54/40.25 % (1992033)Time elapsed: 0.125 s % 278.54/40.25 % (1992033)Peak memory usage: 112 MB % 278.54/40.25 % (1992033)Instructions burned: 286 (million) % 278.54/40.25 % (1992036)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3103314426:i=832:rtra=on:gtg=position:ss=axioms_2637 on theBenchmark for (2637ds/832Mi) % 278.54/40.25 % (1992036)Refutation not found, incomplete strategy % 278.54/40.25 % (1992036)------------------------------ % 278.54/40.25 % (1992036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.54/40.25 % (1992036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.54/40.25 % (1992036)CaDiCaL version: 2.1.3 % 278.54/40.25 % (1992036)Termination reason: Refutation not found, incomplete strategy % 278.54/40.25 % (1992036)Time elapsed: 0.125 s % 278.54/40.25 % (1992036)Peak memory usage: 112 MB % 278.54/40.25 % (1992036)Instructions burned: 286 (million) % 278.54/40.25 % (1992032)------------------------------ % 278.54/40.25 % (1992032)------------------------------ % 278.54/40.25 % (1992033)------------------------------ % 278.54/40.25 % (1992033)------------------------------ % 278.54/40.25 % (1992038)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2584284615:i=942:thf=on:kws=precedence:rtra=on_2633 on theBenchmark for (2633ds/942Mi) % 278.54/40.25 % (1992036)------------------------------ % 278.54/40.25 % (1992036)------------------------------ % 278.54/40.25 % (1992039)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=2251650433:avsq=on:i=552:avsqr=1,2:rtra=on_2633 on theBenchmark for (2633ds/552Mi) % 278.54/40.25 % (1992042)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=169741417:i=750:kws=inv_arity_squared:rtra=on_2631 on theBenchmark for (2631ds/750Mi) % 278.54/40.25 % (1992039)Instruction limit reached! % 278.54/40.25 % (1992039)------------------------------ % 278.54/40.25 % (1992039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.54/40.25 % (1992039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.54/40.25 % (1992039)CaDiCaL version: 2.1.3 % 278.54/40.25 % (1992039)Termination reason: Instruction limit % 278.54/40.25 % (1992039)Termination phase: Saturation % 278.54/40.25 % (1992039)Time elapsed: 0.240 s % 278.54/40.25 % (1992039)Peak memory usage: 129 MB % 278.54/40.25 % (1992039)Instructions burned: 554 (million) % 278.54/40.25 % (1992038)Instruction limit reached! % 278.54/40.25 % (1992038)------------------------------ % 278.54/40.25 % (1992038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.54/40.25 % (1992038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.54/40.25 % (1992038)CaDiCaL version: 2.1.3 % 278.54/40.25 % (1992038)Termination reason: Instruction limit % 278.54/40.25 % (1992038)Termination phase: Saturation % 278.54/40.25 % (1992038)Time elapsed: 0.394 s % 278.54/40.25 % (1992038)Peak memory usage: 115 MB % 278.54/40.25 % (1992038)Instructions burned: 943 (million) % 278.54/40.25 % (1992044)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1694187477:i=774:bd=preordered:rtra=on:ss=axioms:sgt=8_2629 on theBenchmark for (2629ds/774Mi) % 278.54/40.25 % (1992042)Instruction limit reached! % 278.54/40.25 % (1992042)------------------------------ % 278.54/40.25 % (1992042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.54/40.25 % (1992042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/41.44 % (1992042)CaDiCaL version: 2.1.3 % 286.85/41.44 % (1992042)Termination reason: Instruction limit % 286.85/41.44 % (1992042)Termination phase: Saturation % 286.85/41.44 % (1992042)Time elapsed: 0.299 s % 286.85/41.44 % (1992042)Peak memory usage: 113 MB % 286.85/41.44 % (1992042)Instructions burned: 752 (million) % 286.85/41.44 % (1992045)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3912594009:i=1026:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2628 on theBenchmark for (2628ds/1026Mi) % 286.85/41.44 % (1992044)Refutation not found, incomplete strategy % 286.85/41.44 % (1992044)------------------------------ % 286.85/41.44 % (1992044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.85/41.44 % (1992044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/41.44 % (1992044)CaDiCaL version: 2.1.3 % 286.85/41.44 % (1992044)Termination reason: Refutation not found, incomplete strategy % 286.85/41.44 % (1992044)Time elapsed: 0.132 s % 286.85/41.44 % (1992044)Peak memory usage: 112 MB % 286.85/41.44 % (1992044)Instructions burned: 302 (million) % 286.85/41.44 % (1992047)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3971967042:i=668:rtra=on_2627 on theBenchmark for (2627ds/668Mi) % 286.85/41.44 % (1992044)------------------------------ % 286.85/41.44 % (1992044)------------------------------ % 286.85/41.44 % (1992045)Instruction limit reached! % 286.85/41.44 % (1992045)------------------------------ % 286.85/41.44 % (1992045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.85/41.44 % (1992045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/41.44 % (1992045)CaDiCaL version: 2.1.3 % 286.85/41.44 % (1992045)Termination reason: Instruction limit % 286.85/41.44 % (1992045)Termination phase: Saturation % 286.85/41.44 % (1992045)Time elapsed: 0.375 s % 286.85/41.44 % (1992045)Peak memory usage: 92 MB % 286.85/41.44 % (1992045)Instructions burned: 1028 (million) % 286.85/41.44 % (1992047)Instruction limit reached! % 286.85/41.44 % (1992047)------------------------------ % 286.85/41.44 % (1992047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.85/41.44 % (1992047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/41.44 % (1992047)CaDiCaL version: 2.1.3 % 286.85/41.44 % (1992047)Termination reason: Instruction limit % 286.85/41.44 % (1992047)Termination phase: Saturation % 286.85/41.44 % (1992047)Time elapsed: 0.288 s % 286.85/41.44 % (1992047)Peak memory usage: 130 MB % 286.85/41.44 % (1992047)Instructions burned: 670 (million) % 286.85/41.44 % (1992050)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=3050630968:i=718:rtra=on:gtg=exists_top:ss=axioms_2624 on theBenchmark for (2624ds/718Mi) % 286.85/41.44 % (1992051)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1724781288:i=682:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2622 on theBenchmark for (2622ds/682Mi) % 286.85/41.44 % (1992050)Refutation not found, incomplete strategy % 286.85/41.44 % (1992050)------------------------------ % 286.85/41.44 % (1992050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.85/41.44 % (1992050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/41.44 % (1992050)CaDiCaL version: 2.1.3 % 286.85/41.44 % (1992050)Termination reason: Refutation not found, incomplete strategy % 286.85/41.44 % (1992050)Time elapsed: 0.143 s % 286.85/41.44 % (1992050)Peak memory usage: 89 MB % 286.85/41.44 % (1992050)Instructions burned: 397 (million) % 286.85/41.44 % (1992053)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=650681776:st=1.5:i=522:sd=1:kws=precedence:rtra=on:ss=axioms_2622 on theBenchmark for (2622ds/522Mi) % 286.85/41.44 % (1992053)Refutation not found, incomplete strategy % 286.85/41.44 % (1992053)------------------------------ % 286.85/41.44 % (1992053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.85/41.44 % (1992053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.85/41.44 % (1992053)CaDiCaL version: 2.1.3 % 286.85/41.44 % (1992053)Termination reason: Refutation not found, incomplete strategy % 286.85/41.44 % (1992053)Time elapsed: 0.092 s % 286.85/41.44 % (1992053)Peak memory usage: 112 MB % 286.85/41.44 % (1992053)Instructions burned: 193 (million) % 286.85/41.44 % (1992050)------------------------------ % 286.85/41.44 % (1992050)------------------------------ % 286.85/41.44 % (1992051)Instruction limit reached! % 286.85/41.44 % (1992051)------------------------------ % 295.09/42.63 % (1992051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.09/42.63 % (1992051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.09/42.63 % (1992051)CaDiCaL version: 2.1.3 % 295.09/42.63 % (1992051)Termination reason: Instruction limit % 295.09/42.63 % (1992051)Termination phase: Saturation % 295.09/42.63 % (1992051)Time elapsed: 0.268 s % 295.09/42.63 % (1992051)Peak memory usage: 113 MB % 295.09/42.63 % (1992051)Instructions burned: 683 (million) % 295.09/42.63 % (1992053)------------------------------ % 295.09/42.63 % (1992053)------------------------------ % 295.09/42.63 % (1992056)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=235598715:s2pl=no:i=470:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2618 on theBenchmark for (2618ds/470Mi) % 295.09/42.63 % (1992057)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2043013102:i=546:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2618 on theBenchmark for (2618ds/546Mi) % 295.09/42.63 % (1992058)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3236428317:i=292:doe=on:rtra=on_2617 on theBenchmark for (2617ds/292Mi) % 295.09/42.63 % (1992056)Refutation not found, incomplete strategy % 295.09/42.63 % (1992056)------------------------------ % 295.09/42.63 % (1992056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.09/42.63 % (1992056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.09/42.63 % (1992056)CaDiCaL version: 2.1.3 % 295.09/42.63 % (1992056)Termination reason: Refutation not found, incomplete strategy % 295.09/42.63 % (1992056)Time elapsed: 0.130 s % 295.09/42.63 % (1992056)Peak memory usage: 112 MB % 295.09/42.63 % (1992056)Instructions burned: 301 (million) % 295.09/42.63 % (1992057)Instruction limit reached! % 295.09/42.63 % (1992057)------------------------------ % 295.09/42.63 % (1992057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.09/42.63 % (1992057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.09/42.63 % (1992057)CaDiCaL version: 2.1.3 % 295.09/42.63 % (1992057)Termination reason: Instruction limit % 295.09/42.63 % (1992057)Termination phase: Saturation % 295.09/42.63 % (1992057)Time elapsed: 0.195 s % 295.09/42.63 % (1992057)Peak memory usage: 88 MB % 295.09/42.63 % (1992057)Instructions burned: 549 (million) % 295.09/42.63 % (1992058)Instruction limit reached! % 295.09/42.63 % (1992058)------------------------------ % 295.09/42.63 % (1992058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.09/42.63 % (1992058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.09/42.63 % (1992058)CaDiCaL version: 2.1.3 % 295.09/42.63 % (1992058)Termination reason: Instruction limit % 295.09/42.63 % (1992058)Termination phase: Property scanning % 295.09/42.63 % (1992058)Time elapsed: 0.106 s % 295.09/42.63 % (1992058)Peak memory usage: 86 MB % 295.09/42.63 % (1992058)Instructions burned: 295 (million) % 295.09/42.63 % (1992062)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=2497089636:i=8856:doe=on:fsr=off:rtra=on_2615 on theBenchmark for (2615ds/8856Mi) % 295.09/42.63 % (1992056)------------------------------ % 295.09/42.63 % (1992056)------------------------------ % 295.09/42.63 % (1992063)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=296424929:avsq=on:i=552:avsqr=1,2:rtra=on_2614 on theBenchmark for (2614ds/552Mi) % 295.09/42.63 % (1992066)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=567679433:i=2104:rtra=on_2613 on theBenchmark for (2613ds/2104Mi) % 295.09/42.63 % (1992063)Instruction limit reached! % 295.09/42.63 % (1992063)------------------------------ % 295.09/42.63 % (1992063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.09/42.63 % (1992063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.09/42.63 % (1992063)CaDiCaL version: 2.1.3 % 295.09/42.63 % (1992063)Termination reason: Instruction limit % 295.09/42.63 % (1992063)Termination phase: Saturation % 295.09/42.63 % (1992063)Time elapsed: 0.242 s % 295.09/42.63 % (1992063)Peak memory usage: 129 MB % 295.09/42.63 % (1992063)Instructions burned: 554 (million) % 295.09/42.63 % (1992068)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=2535806893:i=1310:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2610 on theBenchmark for (2610ds/1310Mi) % 295.09/42.63 % (1992066)Instruction limit reached! % 299.71/43.24 % (1992066)------------------------------ % 299.71/43.24 % (1992066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.24 % (1992066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.24 % (1992066)CaDiCaL version: 2.1.3 % 299.71/43.24 % (1992066)Termination reason: Instruction limit % 299.71/43.24 % (1992066)Termination phase: Saturation % 299.71/43.24 % (1992066)Time elapsed: 0.774 s % 299.71/43.24 % (1992066)Peak memory usage: 95 MB % 299.71/43.24 % (1992066)Instructions burned: 2106 (million) % 299.71/43.24 % (1992068)Instruction limit reached! % 299.71/43.24 % (1992068)------------------------------ % 299.71/43.24 % (1992068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.24 % (1992068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.24 % (1992068)CaDiCaL version: 2.1.3 % 299.71/43.24 % (1992068)Termination reason: Instruction limit % 299.71/43.24 % (1992068)Termination phase: Saturation % 299.71/43.24 % (1992068)Time elapsed: 0.650 s % 299.71/43.24 % (1992068)Peak memory usage: 102 MB % 299.71/43.24 % (1992068)Instructions burned: 1310 (million) % 299.71/43.24 % (1992070)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=3017429995:st=5:i=2108:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2604 on theBenchmark for (2604ds/2108Mi) % 299.71/43.24 % (1992070)Refutation not found, incomplete strategy % 299.71/43.24 % (1992070)------------------------------ % 299.71/43.24 % (1992070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.24 % (1992070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.24 % (1992070)CaDiCaL version: 2.1.3 % 299.71/43.24 % (1992070)Termination reason: Refutation not found, incomplete strategy % 299.71/43.24 % (1992070)Time elapsed: 0.066 s % 299.71/43.24 % (1992070)Peak memory usage: 88 MB % 299.71/43.24 % (1992070)Instructions burned: 181 (million) % 299.71/43.24 % (1992071)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=3502903705:i=214:rtra=on_2602 on theBenchmark for (2602ds/214Mi) % 299.71/43.24 % (1992071)Instruction limit reached! % 299.71/43.24 % (1992071)------------------------------ % 299.71/43.24 % (1992071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.24 % (1992071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.24 % (1992071)CaDiCaL version: 2.1.3 % 299.71/43.24 % (1992071)Termination reason: Instruction limit % 299.71/43.24 % (1992071)Termination phase: Property scanning % 299.71/43.24 % (1992071)Time elapsed: 0.079 s % 299.71/43.24 % (1992071)Peak memory usage: 86 MB % 299.71/43.24 % (1992071)Instructions burned: 217 (million) % 299.71/43.24 % (1992070)------------------------------ % 299.71/43.24 % (1992070)------------------------------ % 299.71/43.24 % (1992074)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=2125702210:s2a=on:i=900:doe=on:nm=32:rtra=on_2600 on theBenchmark for (2600ds/900Mi) % 299.71/43.24 % (1992075)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 % 299.71/43.24 % (1992075)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3952677583:i=2180:aac=none:nm=0:rtra=on:rawr=on_2599 on theBenchmark for (2599ds/2180Mi) % 299.71/43.24 % (1992074)Instruction limit reached! % 299.71/43.24 % (1992074)------------------------------ % 299.71/43.24 % (1992074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.24 % (1992074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.24 % (1992074)CaDiCaL version: 2.1.3 % 299.71/43.24 % (1992074)Termination reason: Instruction limit % 299.71/43.24 % (1992074)Termination phase: Saturation % 299.71/43.24 % (1992074)Time elapsed: 0.377 s % 299.71/43.24 % (1992074)Peak memory usage: 130 MB % 299.71/43.24 % (1992074)Instructions burned: 903 (million) % 299.71/43.24 % (1992078)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2003864679:i=260:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2594 on theBenchmark for (2594ds/260Mi) % 299.71/43.24 % (1992078)Instruction limit reached! % 299.71/43.24 % (1992078)------------------------------ % 299.71/43.24 % (1992078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.71/43.24 % (1992078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.71/43.24 % (1992078)CaDiCaL version:Terminated %------------------------------------------------------------------------------