%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO330^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 : Wed Sep 30 08:47:27 AM UTC 2026
% Result : Theorem 13.44s 2.21s
% Output : Refutation 13.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO330^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n003.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 16:47:59 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.35 % (2735702)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.35 % (2735707)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1938251079:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.35 % (2735713)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.35 % (2735713)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.35 % (2735708)lrs+10_16_si=on:nwc=1.5:random_seed=1351791267:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.35 % (2735709)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4090178671:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.35 % (2735712)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3115664398:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.35 % (2735710)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=1868076157:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.35 % (2735711)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1707770518:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.35 % (2735713)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=3236263470:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.35 % (2735709)Instruction limit reached!
% 0.21/0.35 % (2735709)------------------------------
% 0.21/0.35 % (2735709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2735709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2735709)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2735709)Termination reason: Instruction limit
% 0.21/0.35 % (2735709)Termination phase: Saturation
% 0.21/0.35 % (2735709)Time elapsed: 0.003 s
% 0.21/0.35 % (2735709)Peak memory usage: 12 MB
% 0.21/0.35 % (2735709)Instructions burned: 4 (million)
% 0.21/0.35 % (2735708)Instruction limit reached!
% 0.21/0.35 % (2735708)------------------------------
% 0.21/0.35 % (2735708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2735708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2735708)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2735708)Termination reason: Instruction limit
% 0.21/0.35 % (2735708)Termination phase: Saturation
% 0.21/0.35 % (2735708)Time elapsed: 0.010 s
% 0.21/0.35 % (2735708)Peak memory usage: 12 MB
% 0.21/0.35 % (2735708)Instructions burned: 20 (million)
% 0.21/0.35 % (2735711)Instruction limit reached!
% 0.21/0.35 % (2735711)------------------------------
% 0.21/0.35 % (2735711)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2735711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2735711)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2735711)Termination reason: Instruction limit
% 0.21/0.35 % (2735711)Termination phase: Saturation
% 0.21/0.35 % (2735711)Time elapsed: 0.014 s
% 0.21/0.35 % (2735711)Peak memory usage: 12 MB
% 0.21/0.35 % (2735711)Instructions burned: 25 (million)
% 0.21/0.35 % (2735707)Instruction limit reached!
% 0.21/0.35 % (2735707)------------------------------
% 0.21/0.35 % (2735707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2735707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2735707)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2735707)Termination reason: Instruction limit
% 0.21/0.35 % (2735707)Termination phase: Saturation
% 0.21/0.35 % (2735707)Time elapsed: 0.025 s
% 0.21/0.35 % (2735707)Peak memory usage: 12 MB
% 0.21/0.35 % (2735707)Instructions burned: 89 (million)
% 0.21/0.35 % (2735721)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4196666676:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.35 % (2735721)Instruction limit reached!
% 0.21/0.35 % (2735721)------------------------------
% 0.21/0.35 % (2735721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2735721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2735721)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2735721)Termination reason: Instruction limit
% 0.81/0.38 % (2735721)Termination phase: Saturation
% 0.81/0.38 % (2735721)Time elapsed: 0.002 s
% 0.81/0.38 % (2735721)Peak memory usage: 12 MB
% 0.81/0.38 % (2735721)Instructions burned: 2 (million)
% 0.81/0.38 % (2735723)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.81/0.38 % (2735722)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3604989383:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.81/0.38 % (2735723)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1586831276:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.81/0.38 % (2735722)Instruction limit reached!
% 0.81/0.38 % (2735722)------------------------------
% 0.81/0.38 % (2735722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2735722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2735722)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2735722)Termination reason: Instruction limit
% 0.81/0.38 % (2735722)Termination phase: Saturation
% 0.81/0.38 % (2735722)Time elapsed: 0.004 s
% 0.81/0.38 % (2735722)Peak memory usage: 12 MB
% 0.81/0.38 % (2735722)Instructions burned: 6 (million)
% 0.81/0.38 % (2735724)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2359733289:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.81/0.38 % (2735723)Instruction limit reached!
% 0.81/0.38 % (2735723)------------------------------
% 0.81/0.38 % (2735723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2735723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2735723)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2735723)Termination reason: Instruction limit
% 0.81/0.38 % (2735723)Termination phase: Saturation
% 0.81/0.38 % (2735723)Time elapsed: 0.004 s
% 0.81/0.38 % (2735723)Peak memory usage: 12 MB
% 0.81/0.38 % (2735723)Instructions burned: 7 (million)
% 0.81/0.38 % (2735726)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.81/0.38 % (2735726)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.81/0.38 % (2735712)Instruction limit reached!
% 0.81/0.38 % (2735712)------------------------------
% 0.81/0.38 % (2735712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2735712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2735712)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2735712)Termination reason: Instruction limit
% 0.81/0.38 % (2735712)Termination phase: Saturation
% 0.81/0.38 % (2735712)Time elapsed: 0.040 s
% 0.81/0.38 % (2735712)Peak memory usage: 12 MB
% 0.81/0.38 % (2735712)Instructions burned: 75 (million)
% 0.81/0.38 % (2735726)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1763833558:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.81/0.38 % (2735724)Instruction limit reached!
% 0.81/0.38 % (2735724)------------------------------
% 0.81/0.38 % (2735724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.38 % (2735724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.38 % (2735724)CaDiCaL version: 2.1.3
% 0.81/0.38 % (2735724)Termination reason: Instruction limit
% 0.81/0.38 % (2735724)Termination phase: Saturation
% 0.81/0.38 % (2735724)Time elapsed: 0.007 s
% 0.81/0.38 % (2735724)Peak memory usage: 12 MB
% 0.81/0.38 % (2735724)Instructions burned: 12 (million)
% 0.81/0.38 % (2735729)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=39381744:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.81/0.38 % (2735732)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.81/0.41 % (2735731)lrs+10_1_si=on:cs=on:random_seed=3198179832:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.81/0.41 % (2735732)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=4158607671:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.81/0.41 % (2735726)Instruction limit reached!
% 0.81/0.41 % (2735726)------------------------------
% 0.81/0.41 % (2735726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2735726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2735726)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2735726)Termination reason: Instruction limit
% 0.81/0.41 % (2735726)Termination phase: Saturation
% 0.81/0.41 % (2735726)Time elapsed: 0.016 s
% 0.81/0.41 % (2735726)Peak memory usage: 12 MB
% 0.81/0.41 % (2735726)Instructions burned: 33 (million)
% 0.81/0.41 % (2735734)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2835973841:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.81/0.41 % (2735732)Instruction limit reached!
% 0.81/0.41 % (2735732)------------------------------
% 0.81/0.41 % (2735732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2735732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2735732)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2735732)Termination reason: Instruction limit
% 0.81/0.41 % (2735732)Termination phase: Saturation
% 0.81/0.41 % (2735732)Time elapsed: 0.001 s
% 0.81/0.41 % (2735732)Peak memory usage: 11 MB
% 0.81/0.41 % (2735732)Instructions burned: 2 (million)
% 0.81/0.41 % (2735731)Instruction limit reached!
% 0.81/0.41 % (2735731)------------------------------
% 0.81/0.41 % (2735731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2735731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2735731)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2735731)Termination reason: Instruction limit
% 0.81/0.41 % (2735731)Termination phase: Saturation
% 0.81/0.41 % (2735731)Time elapsed: 0.004 s
% 0.81/0.41 % (2735731)Peak memory usage: 12 MB
% 0.81/0.41 % (2735731)Instructions burned: 8 (million)
% 0.81/0.41 % (2735713)Refutation not found, incomplete strategy
% 0.81/0.41 % (2735713)------------------------------
% 0.81/0.41 % (2735713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2735713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2735713)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2735713)Termination reason: Refutation not found, incomplete strategy
% 0.81/0.41 % (2735713)Time elapsed: 0.062 s
% 0.81/0.41 % (2735713)Peak memory usage: 13 MB
% 0.81/0.41 % (2735713)Instructions burned: 117 (million)
% 0.81/0.41 % (2735713)------------------------------
% 0.81/0.41 % (2735713)------------------------------
% 0.81/0.41 % (2735710)Refutation not found, incomplete strategy
% 0.81/0.41 % (2735710)------------------------------
% 0.81/0.41 % (2735710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2735710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2735710)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2735710)Termination reason: Refutation not found, incomplete strategy
% 0.81/0.41 % (2735710)Time elapsed: 0.071 s
% 0.81/0.41 % (2735710)Peak memory usage: 13 MB
% 0.81/0.41 % (2735710)Instructions burned: 119 (million)
% 0.81/0.41 % (2735710)------------------------------
% 0.81/0.41 % (2735710)------------------------------
% 0.81/0.41 % (2735734)Instruction limit reached!
% 0.81/0.41 % (2735734)------------------------------
% 0.81/0.41 % (2735734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.41 % (2735734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.41 % (2735734)CaDiCaL version: 2.1.3
% 0.81/0.41 % (2735734)Termination reason: Instruction limit
% 0.81/0.41 % (2735734)Termination phase: Saturation
% 0.81/0.41 % (2735734)Time elapsed: 0.013 s
% 0.81/0.41 % (2735734)Peak memory usage: 12 MB
% 0.81/0.41 % (2735734)Instructions burned: 39 (million)
% 0.81/0.41 % (2735739)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3783078082:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.81/0.41 % (2735740)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2371370872:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.81/0.45 % (2735741)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3768170758:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.81/0.45 % (2735742)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2495127838:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.81/0.45 % (2735744)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=472109005:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.81/0.45 % (2735744)Instruction limit reached!
% 0.81/0.45 % (2735744)------------------------------
% 0.81/0.45 % (2735744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2735744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2735744)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2735744)Termination reason: Instruction limit
% 0.81/0.45 % (2735744)Termination phase: Saturation
% 0.81/0.45 % (2735744)Time elapsed: 0.001 s
% 0.81/0.45 % (2735744)Peak memory usage: 12 MB
% 0.81/0.45 % (2735744)Instructions burned: 4 (million)
% 0.81/0.45 % (2735741)Instruction limit reached!
% 0.81/0.45 % (2735741)------------------------------
% 0.81/0.45 % (2735741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2735741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2735741)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2735741)Termination reason: Instruction limit
% 0.81/0.45 % (2735741)Termination phase: Saturation
% 0.81/0.45 % (2735741)Time elapsed: 0.009 s
% 0.81/0.45 % (2735741)Peak memory usage: 12 MB
% 0.81/0.45 % (2735741)Instructions burned: 15 (million)
% 0.81/0.45 % (2735740)Refutation not found, incomplete strategy
% 0.81/0.45 % (2735740)------------------------------
% 0.81/0.45 % (2735740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2735740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2735740)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2735740)Termination reason: Refutation not found, incomplete strategy
% 0.81/0.45 % (2735740)Time elapsed: 0.009 s
% 0.81/0.45 % (2735740)Peak memory usage: 12 MB
% 0.81/0.45 % (2735740)Instructions burned: 15 (million)
% 0.81/0.45 % (2735743)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3986281934:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.81/0.45 % (2735740)------------------------------
% 0.81/0.45 % (2735740)------------------------------
% 0.81/0.45 % (2735729)Instruction limit reached!
% 0.81/0.45 % (2735729)------------------------------
% 0.81/0.45 % (2735729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2735729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2735729)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2735729)Termination reason: Instruction limit
% 0.81/0.45 % (2735729)Termination phase: Saturation
% 0.81/0.45 % (2735729)Time elapsed: 0.038 s
% 0.81/0.45 % (2735729)Peak memory usage: 12 MB
% 0.81/0.45 % (2735729)Instructions burned: 87 (million)
% 0.81/0.45 % (2735750)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1585446545:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.81/0.45 % (2735743)Instruction limit reached!
% 0.81/0.45 % (2735743)------------------------------
% 0.81/0.45 % (2735743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2735743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2735743)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2735743)Termination reason: Instruction limit
% 0.81/0.45 % (2735743)Termination phase: Saturation
% 0.81/0.45 % (2735743)Time elapsed: 0.008 s
% 0.81/0.45 % (2735743)Peak memory usage: 12 MB
% 0.81/0.45 % (2735743)Instructions burned: 15 (million)
% 0.81/0.45 % (2735750)Instruction limit reached!
% 0.81/0.45 % (2735750)------------------------------
% 0.81/0.45 % (2735750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.81/0.45 % (2735750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.81/0.45 % (2735750)CaDiCaL version: 2.1.3
% 0.81/0.45 % (2735750)Termination reason: Instruction limit
% 0.81/0.45 % (2735750)Termination phase: Saturation
% 0.81/0.45 % (2735750)Time elapsed: 0.008 s
% 1.58/0.50 % (2735750)Peak memory usage: 12 MB
% 1.58/0.50 % (2735750)Instructions burned: 29 (million)
% 1.58/0.50 % (2735754)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.58/0.50 % (2735754)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.58/0.50 % (2735751)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2947704832:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.58/0.50 % (2735753)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4110265977:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.58/0.50 % (2735754)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=2202389828:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.58/0.50 % (2735757)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=2429121831:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.58/0.50 % (2735756)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.58/0.50 % (2735756)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=89084947:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.58/0.50 % (2735754)Instruction limit reached!
% 1.58/0.50 % (2735754)------------------------------
% 1.58/0.50 % (2735754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (2735754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (2735754)CaDiCaL version: 2.1.3
% 1.58/0.50 % (2735754)Termination reason: Instruction limit
% 1.58/0.50 % (2735754)Termination phase: Saturation
% 1.58/0.50 % (2735754)Time elapsed: 0.008 s
% 1.58/0.50 % (2735754)Peak memory usage: 12 MB
% 1.58/0.50 % (2735754)Instructions burned: 15 (million)
% 1.58/0.50 % (2735751)Instruction limit reached!
% 1.58/0.50 % (2735751)------------------------------
% 1.58/0.50 % (2735751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (2735751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (2735751)CaDiCaL version: 2.1.3
% 1.58/0.50 % (2735751)Termination reason: Instruction limit
% 1.58/0.50 % (2735751)Termination phase: Saturation
% 1.58/0.50 % (2735751)Time elapsed: 0.012 s
% 1.58/0.50 % (2735751)Peak memory usage: 11 MB
% 1.58/0.50 % (2735751)Instructions burned: 23 (million)
% 1.58/0.50 % (2735757)Instruction limit reached!
% 1.58/0.50 % (2735757)------------------------------
% 1.58/0.50 % (2735757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (2735757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (2735757)CaDiCaL version: 2.1.3
% 1.58/0.50 % (2735757)Termination reason: Instruction limit
% 1.58/0.50 % (2735757)Termination phase: Saturation
% 1.58/0.50 % (2735757)Time elapsed: 0.009 s
% 1.58/0.50 % (2735757)Peak memory usage: 12 MB
% 1.58/0.50 % (2735757)Instructions burned: 33 (million)
% 1.58/0.50 % (2735756)Instruction limit reached!
% 1.58/0.50 % (2735756)------------------------------
% 1.58/0.50 % (2735756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.50 % (2735756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.50 % (2735756)CaDiCaL version: 2.1.3
% 1.58/0.50 % (2735756)Termination reason: Instruction limit
% 1.58/0.50 % (2735756)Termination phase: Saturation
% 1.58/0.50 % (2735756)Time elapsed: 0.006 s
% 1.58/0.50 % (2735756)Peak memory usage: 12 MB
% 1.58/0.50 % (2735756)Instructions burned: 9 (million)
% 1.58/0.50 % (2735765)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3915893168:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.58/0.50 % (2735763)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=17163813:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.58/0.50 % (2735764)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3126511235:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.29/0.58 % (2735765)Instruction limit reached!
% 2.29/0.58 % (2735765)------------------------------
% 2.29/0.58 % (2735765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.58 % (2735765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.58 % (2735765)CaDiCaL version: 2.1.3
% 2.29/0.58 % (2735765)Termination reason: Instruction limit
% 2.29/0.58 % (2735765)Termination phase: Saturation
% 2.29/0.58 % (2735765)Time elapsed: 0.006 s
% 2.29/0.58 % (2735765)Peak memory usage: 12 MB
% 2.29/0.58 % (2735765)Instructions burned: 21 (million)
% 2.29/0.58 % (2735763)Instruction limit reached!
% 2.29/0.58 % (2735763)------------------------------
% 2.29/0.58 % (2735763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.58 % (2735763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.58 % (2735763)CaDiCaL version: 2.1.3
% 2.29/0.58 % (2735763)Termination reason: Instruction limit
% 2.29/0.58 % (2735763)Termination phase: Saturation
% 2.29/0.58 % (2735763)Time elapsed: 0.004 s
% 2.29/0.58 % (2735763)Peak memory usage: 12 MB
% 2.29/0.58 % (2735763)Instructions burned: 7 (million)
% 2.29/0.58 % (2735766)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1599139373:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.29/0.58 % (2735753)Instruction limit reached!
% 2.29/0.58 % (2735753)------------------------------
% 2.29/0.58 % (2735753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.58 % (2735753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.58 % (2735753)CaDiCaL version: 2.1.3
% 2.29/0.58 % (2735753)Termination reason: Instruction limit
% 2.29/0.58 % (2735753)Termination phase: Saturation
% 2.29/0.58 % (2735753)Time elapsed: 0.035 s
% 2.29/0.58 % (2735753)Peak memory usage: 12 MB
% 2.29/0.58 % (2735753)Instructions burned: 60 (million)
% 2.29/0.58 % (2735764)Instruction limit reached!
% 2.29/0.58 % (2735764)------------------------------
% 2.29/0.58 % (2735764)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.58 % (2735764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.58 % (2735764)CaDiCaL version: 2.1.3
% 2.29/0.58 % (2735764)Termination reason: Instruction limit
% 2.29/0.58 % (2735764)Termination phase: Saturation
% 2.29/0.58 % (2735764)Time elapsed: 0.010 s
% 2.29/0.58 % (2735764)Peak memory usage: 11 MB
% 2.29/0.58 % (2735764)Instructions burned: 25 (million)
% 2.29/0.58 % (2735770)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=634961699:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.29/0.58 % (2735771)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2074144299:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.29/0.58 % (2735774)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.29/0.58 % (2735773)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1745782957:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.29/0.58 % (2735774)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1265377503:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 2.29/0.58 % (2735774)Instruction limit reached!
% 2.29/0.58 % (2735774)------------------------------
% 2.29/0.58 % (2735774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.58 % (2735774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.58 % (2735774)CaDiCaL version: 2.1.3
% 2.29/0.58 % (2735774)Termination reason: Instruction limit
% 2.29/0.58 % (2735774)Termination phase: Saturation
% 2.29/0.58 % (2735774)Time elapsed: 0.004 s
% 2.29/0.58 % (2735774)Peak memory usage: 12 MB
% 2.29/0.58 % (2735774)Instructions burned: 8 (million)
% 2.29/0.58 % (2735739)Refutation not found, incomplete strategy
% 2.29/0.58 % (2735739)------------------------------
% 2.29/0.58 % (2735739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.58 % (2735739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.58 % (2735739)CaDiCaL version: 2.1.3
% 2.29/0.58 % (2735739)Termination reason: Refutation not found, incomplete strategy
% 2.59/0.67 % (2735739)Time elapsed: 0.094 s
% 2.59/0.67 % (2735739)Peak memory usage: 13 MB
% 2.59/0.67 % (2735739)Instructions burned: 171 (million)
% 2.59/0.67 % (2735739)------------------------------
% 2.59/0.67 % (2735739)------------------------------
% 2.59/0.67 % (2735773)Instruction limit reached!
% 2.59/0.67 % (2735773)------------------------------
% 2.59/0.67 % (2735773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.67 % (2735773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.67 % (2735773)CaDiCaL version: 2.1.3
% 2.59/0.67 % (2735773)Termination reason: Instruction limit
% 2.59/0.67 % (2735773)Termination phase: Saturation
% 2.59/0.67 % (2735773)Time elapsed: 0.022 s
% 2.59/0.67 % (2735773)Peak memory usage: 12 MB
% 2.59/0.67 % (2735773)Instructions burned: 42 (million)
% 2.59/0.67 % (2735770)Instruction limit reached!
% 2.59/0.67 % (2735770)------------------------------
% 2.59/0.67 % (2735770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.67 % (2735770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.67 % (2735770)CaDiCaL version: 2.1.3
% 2.59/0.67 % (2735770)Termination reason: Instruction limit
% 2.59/0.67 % (2735770)Termination phase: Saturation
% 2.59/0.67 % (2735770)Time elapsed: 0.038 s
% 2.59/0.67 % (2735770)Peak memory usage: 13 MB
% 2.59/0.67 % (2735770)Instructions burned: 145 (million)
% 2.59/0.67 % (2735779)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3103682632:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.59/0.67 % (2735780)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=3746790742:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.59/0.67 % (2735782)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2714354521:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.59/0.67 % (2735781)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.59/0.67 % (2735782)Instruction limit reached!
% 2.59/0.67 % (2735782)------------------------------
% 2.59/0.67 % (2735782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.67 % (2735782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.67 % (2735782)CaDiCaL version: 2.1.3
% 2.59/0.67 % (2735782)Termination reason: Instruction limit
% 2.59/0.67 % (2735782)Termination phase: Saturation
% 2.59/0.67 % (2735782)Time elapsed: 0.005 s
% 2.59/0.67 % (2735782)Peak memory usage: 12 MB
% 2.59/0.67 % (2735782)Instructions burned: 23 (million)
% 2.59/0.67 % (2735781)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3765874692:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.59/0.67 % (2735781)Instruction limit reached!
% 2.59/0.67 % (2735781)------------------------------
% 2.59/0.67 % (2735781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.67 % (2735781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.67 % (2735781)CaDiCaL version: 2.1.3
% 2.59/0.67 % (2735781)Termination reason: Instruction limit
% 2.59/0.67 % (2735781)Termination phase: Saturation
% 2.59/0.67 % (2735781)Time elapsed: 0.004 s
% 2.59/0.67 % (2735781)Peak memory usage: 12 MB
% 2.59/0.67 % (2735781)Instructions burned: 7 (million)
% 2.59/0.67 % (2735786)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2040077596:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.59/0.67 % (2735786)Instruction limit reached!
% 2.59/0.67 % (2735786)------------------------------
% 2.59/0.67 % (2735786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.59/0.67 % (2735786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.59/0.67 % (2735786)CaDiCaL version: 2.1.3
% 2.59/0.67 % (2735786)Termination reason: Instruction limit
% 2.59/0.67 % (2735786)Termination phase: Saturation
% 2.59/0.67 % (2735786)Time elapsed: 0.006 s
% 2.59/0.67 % (2735786)Peak memory usage: 12 MB
% 2.59/0.67 % (2735786)Instructions burned: 22 (million)
% 2.59/0.67 % (2735788)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3430322008:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.16/0.72 % (2735790)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=3409139789:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 3.16/0.72 % (2735742)Instruction limit reached!
% 3.16/0.72 % (2735742)------------------------------
% 3.16/0.72 % (2735742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.72 % (2735742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.72 % (2735742)CaDiCaL version: 2.1.3
% 3.16/0.72 % (2735742)Termination reason: Instruction limit
% 3.16/0.72 % (2735742)Termination phase: Saturation
% 3.16/0.72 % (2735742)Time elapsed: 0.181 s
% 3.16/0.72 % (2735742)Peak memory usage: 14 MB
% 3.16/0.72 % (2735742)Instructions burned: 328 (million)
% 3.16/0.72 % (2735780)Instruction limit reached!
% 3.16/0.72 % (2735780)------------------------------
% 3.16/0.72 % (2735780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.72 % (2735780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.72 % (2735780)CaDiCaL version: 2.1.3
% 3.16/0.72 % (2735780)Termination reason: Instruction limit
% 3.16/0.72 % (2735780)Termination phase: Saturation
% 3.16/0.72 % (2735780)Time elapsed: 0.072 s
% 3.16/0.72 % (2735780)Peak memory usage: 13 MB
% 3.16/0.72 % (2735780)Instructions burned: 171 (million)
% 3.16/0.72 % (2735771)Instruction limit reached!
% 3.16/0.72 % (2735771)------------------------------
% 3.16/0.72 % (2735771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.72 % (2735771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.72 % (2735771)CaDiCaL version: 2.1.3
% 3.16/0.72 % (2735771)Termination reason: Instruction limit
% 3.16/0.72 % (2735771)Termination phase: Saturation
% 3.16/0.72 % (2735771)Time elapsed: 0.107 s
% 3.16/0.72 % (2735771)Peak memory usage: 13 MB
% 3.16/0.72 % (2735771)Instructions burned: 194 (million)
% 3.16/0.72 % (2735793)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=1209837636:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 3.16/0.72 % (2735794)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1969998357:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 3.16/0.72 % (2735779)Instruction limit reached!
% 3.16/0.72 % (2735779)------------------------------
% 3.16/0.72 % (2735779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.72 % (2735795)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3893255004:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/21Mi)
% 3.16/0.72 % (2735779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.72 % (2735779)CaDiCaL version: 2.1.3
% 3.16/0.72 % (2735779)Termination reason: Instruction limit
% 3.16/0.72 % (2735779)Termination phase: Saturation
% 3.16/0.72 % (2735779)Time elapsed: 0.095 s
% 3.16/0.72 % (2735779)Peak memory usage: 13 MB
% 3.16/0.72 % (2735779)Instructions burned: 182 (million)
% 3.16/0.72 % (2735795)Instruction limit reached!
% 3.16/0.72 % (2735795)------------------------------
% 3.16/0.72 % (2735795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.16/0.72 % (2735795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.16/0.72 % (2735795)CaDiCaL version: 2.1.3
% 3.16/0.72 % (2735795)Termination reason: Instruction limit
% 3.16/0.72 % (2735795)Termination phase: Saturation
% 3.16/0.72 % (2735795)Time elapsed: 0.012 s
% 3.16/0.72 % (2735795)Peak memory usage: 12 MB
% 3.16/0.72 % (2735795)Instructions burned: 21 (million)
% 3.16/0.72 % (2735799)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.16/0.72 % (2735799)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=373164621:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.16/0.72 % (2735793)Instruction limit reached!
% 3.16/0.72 % (2735793)------------------------------
% 3.16/0.72 % (2735793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.81 % (2735793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.81 % (2735793)CaDiCaL version: 2.1.3
% 3.68/0.81 % (2735793)Termination reason: Instruction limit
% 3.68/0.81 % (2735793)Termination phase: Saturation
% 3.68/0.81 % (2735793)Time elapsed: 0.028 s
% 3.68/0.81 % (2735793)Peak memory usage: 12 MB
% 3.68/0.81 % (2735793)Instructions burned: 46 (million)
% 3.68/0.81 % (2735800)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3610375448:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.68/0.81 % (2735800)Instruction limit reached!
% 3.68/0.81 % (2735800)------------------------------
% 3.68/0.81 % (2735800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.81 % (2735800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.81 % (2735800)CaDiCaL version: 2.1.3
% 3.68/0.81 % (2735800)Termination reason: Instruction limit
% 3.68/0.81 % (2735800)Termination phase: Saturation
% 3.68/0.81 % (2735800)Time elapsed: 0.008 s
% 3.68/0.81 % (2735800)Peak memory usage: 12 MB
% 3.68/0.81 % (2735800)Instructions burned: 13 (million)
% 3.68/0.81 % (2735802)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=351963834:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.68/0.81 % (2735804)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=4147361477:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.68/0.81 % (2735802)Instruction limit reached!
% 3.68/0.81 % (2735802)------------------------------
% 3.68/0.81 % (2735802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.81 % (2735802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.81 % (2735802)CaDiCaL version: 2.1.3
% 3.68/0.81 % (2735802)Termination reason: Instruction limit
% 3.68/0.81 % (2735802)Termination phase: Saturation
% 3.68/0.81 % (2735802)Time elapsed: 0.039 s
% 3.68/0.81 % (2735802)Peak memory usage: 13 MB
% 3.68/0.81 % (2735802)Instructions burned: 66 (million)
% 3.68/0.81 % (2735804)Instruction limit reached!
% 3.68/0.81 % (2735804)------------------------------
% 3.68/0.81 % (2735804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.81 % (2735804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.81 % (2735804)CaDiCaL version: 2.1.3
% 3.68/0.81 % (2735804)Termination reason: Instruction limit
% 3.68/0.81 % (2735804)Termination phase: Saturation
% 3.68/0.81 % (2735804)Time elapsed: 0.026 s
% 3.68/0.81 % (2735804)Peak memory usage: 12 MB
% 3.68/0.81 % (2735804)Instructions burned: 51 (million)
% 3.68/0.81 % (2735794)Refutation not found, incomplete strategy
% 3.68/0.81 % (2735794)------------------------------
% 3.68/0.81 % (2735794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.81 % (2735794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.81 % (2735794)CaDiCaL version: 2.1.3
% 3.68/0.81 % (2735794)Termination reason: Refutation not found, incomplete strategy
% 3.68/0.81 % (2735794)Time elapsed: 0.097 s
% 3.68/0.81 % (2735794)Peak memory usage: 13 MB
% 3.68/0.81 % (2735794)Instructions burned: 180 (million)
% 3.68/0.81 % (2735794)------------------------------
% 3.68/0.81 % (2735794)------------------------------
% 3.68/0.81 % (2735807)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=4203023747:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.68/0.81 % (2735808)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2415436683:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.68/0.81 % (2735766)Refutation not found, incomplete strategy
% 3.68/0.81 % (2735766)------------------------------
% 3.68/0.81 % (2735766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.68/0.81 % (2735766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/0.81 % (2735766)CaDiCaL version: 2.1.3
% 3.68/0.81 % (2735766)Termination reason: Refutation not found, incomplete strategy
% 3.68/0.81 % (2735766)Time elapsed: 0.251 s
% 3.68/0.81 % (2735766)Peak memory usage: 14 MB
% 3.68/0.81 % (2735766)Instructions burned: 493 (million)
% 3.68/0.81 % (2735766)------------------------------
% 3.68/0.81 % (2735766)------------------------------
% 3.91/0.98 % (2735788)Instruction limit reached!
% 3.91/0.98 % (2735788)------------------------------
% 3.91/0.98 % (2735788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.98 % (2735788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.98 % (2735788)CaDiCaL version: 2.1.3
% 3.91/0.98 % (2735788)Termination reason: Instruction limit
% 3.91/0.98 % (2735788)Termination phase: Saturation
% 3.91/0.98 % (2735788)Time elapsed: 0.166 s
% 3.91/0.98 % (2735788)Peak memory usage: 13 MB
% 3.91/0.98 % (2735788)Instructions burned: 317 (million)
% 3.91/0.98 % (2735799)Instruction limit reached!
% 3.91/0.98 % (2735799)------------------------------
% 3.91/0.98 % (2735799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.98 % (2735799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.98 % (2735799)CaDiCaL version: 2.1.3
% 3.91/0.98 % (2735799)Termination reason: Instruction limit
% 3.91/0.98 % (2735799)Termination phase: Saturation
% 3.91/0.98 % (2735799)Time elapsed: 0.093 s
% 3.91/0.98 % (2735799)Peak memory usage: 12 MB
% 3.91/0.98 % (2735799)Instructions burned: 202 (million)
% 3.91/0.98 % (2735809)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=162225128:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.91/0.98 % (2735807)Refutation not found, incomplete strategy
% 3.91/0.98 % (2735807)------------------------------
% 3.91/0.98 % (2735807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.98 % (2735807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.98 % (2735807)CaDiCaL version: 2.1.3
% 3.91/0.98 % (2735807)Termination reason: Refutation not found, incomplete strategy
% 3.91/0.98 % (2735807)Time elapsed: 0.017 s
% 3.91/0.98 % (2735807)Peak memory usage: 12 MB
% 3.91/0.98 % (2735807)Instructions burned: 30 (million)
% 3.91/0.98 % (2735807)------------------------------
% 3.91/0.98 % (2735807)------------------------------
% 3.91/0.98 % (2735813)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.91/0.98 % (2735812)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2350403035:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.91/0.98 % (2735813)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=197567027:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.91/0.98 % (2735814)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1508691451:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.91/0.98 % (2735809)Instruction limit reached!
% 3.91/0.98 % (2735809)------------------------------
% 3.91/0.98 % (2735809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.98 % (2735809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.98 % (2735809)CaDiCaL version: 2.1.3
% 3.91/0.98 % (2735809)Termination reason: Instruction limit
% 3.91/0.98 % (2735809)Termination phase: Saturation
% 3.91/0.98 % (2735809)Time elapsed: 0.017 s
% 3.91/0.98 % (2735809)Peak memory usage: 12 MB
% 3.91/0.98 % (2735809)Instructions burned: 34 (million)
% 3.91/0.98 % (2735816)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3301130152:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.91/0.98 % (2735820)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1446231670:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 3.91/0.98 % (2735790)Instruction limit reached!
% 3.91/0.98 % (2735790)------------------------------
% 3.91/0.98 % (2735790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.98 % (2735790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.91/0.98 % (2735790)CaDiCaL version: 2.1.3
% 3.91/0.98 % (2735790)Termination reason: Instruction limit
% 3.91/0.98 % (2735790)Termination phase: Saturation
% 3.91/0.98 % (2735790)Time elapsed: 0.215 s
% 3.91/0.98 % (2735790)Peak memory usage: 14 MB
% 3.91/0.98 % (2735790)Instructions burned: 854 (million)
% 3.91/0.98 % (2735812)Instruction limit reached!
% 3.91/0.98 % (2735812)------------------------------
% 3.91/0.98 % (2735812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.91/0.98 % (2735812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.05 % (2735812)CaDiCaL version: 2.1.3
% 5.64/1.05 % (2735812)Termination reason: Instruction limit
% 5.64/1.05 % (2735812)Termination phase: Saturation
% 5.64/1.05 % (2735812)Time elapsed: 0.035 s
% 5.64/1.05 % (2735812)Peak memory usage: 12 MB
% 5.64/1.05 % (2735812)Instructions burned: 67 (million)
% 5.64/1.05 % (2735823)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1060107306:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.64/1.05 % (2735808)Instruction limit reached!
% 5.64/1.05 % (2735808)------------------------------
% 5.64/1.05 % (2735808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.05 % (2735808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.05 % (2735808)CaDiCaL version: 2.1.3
% 5.64/1.05 % (2735808)Termination reason: Instruction limit
% 5.64/1.05 % (2735808)Termination phase: Saturation
% 5.64/1.05 % (2735808)Time elapsed: 0.073 s
% 5.64/1.05 % (2735808)Peak memory usage: 13 MB
% 5.64/1.05 % (2735808)Instructions burned: 138 (million)
% 5.64/1.05 % (2735824)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2394316323:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 5.64/1.05 % (2735816)Instruction limit reached!
% 5.64/1.05 % (2735816)------------------------------
% 5.64/1.05 % (2735816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.05 % (2735816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.05 % (2735816)CaDiCaL version: 2.1.3
% 5.64/1.05 % (2735816)Termination reason: Instruction limit
% 5.64/1.05 % (2735816)Termination phase: Saturation
% 5.64/1.05 % (2735816)Time elapsed: 0.052 s
% 5.64/1.05 % (2735816)Peak memory usage: 12 MB
% 5.64/1.05 % (2735816)Instructions burned: 96 (million)
% 5.64/1.05 % (2735826)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3148119943:st=1.5:i=130:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/130Mi)
% 5.64/1.05 % (2735828)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=335366595:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.64/1.05 % (2735813)Instruction limit reached!
% 5.64/1.05 % (2735813)------------------------------
% 5.64/1.05 % (2735813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.05 % (2735813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.05 % (2735813)CaDiCaL version: 2.1.3
% 5.64/1.05 % (2735813)Termination reason: Instruction limit
% 5.64/1.05 % (2735813)Termination phase: Saturation
% 5.64/1.05 % (2735813)Time elapsed: 0.083 s
% 5.64/1.05 % (2735813)Peak memory usage: 14 MB
% 5.64/1.05 % (2735813)Instructions burned: 181 (million)
% 5.64/1.05 % (2735814)Refutation not found, incomplete strategy
% 5.64/1.05 % (2735814)------------------------------
% 5.64/1.05 % (2735814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.05 % (2735814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.05 % (2735814)CaDiCaL version: 2.1.3
% 5.64/1.05 % (2735814)Termination reason: Refutation not found, incomplete strategy
% 5.64/1.05 % (2735814)Time elapsed: 0.092 s
% 5.64/1.05 % (2735814)Peak memory usage: 13 MB
% 5.64/1.05 % (2735814)Instructions burned: 169 (million)
% 5.64/1.05 % (2735814)------------------------------
% 5.64/1.05 % (2735814)------------------------------
% 5.64/1.05 % (2735831)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3412732292:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.64/1.05 % (2735828)Instruction limit reached!
% 5.64/1.05 % (2735828)------------------------------
% 5.64/1.05 % (2735828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.64/1.05 % (2735828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.64/1.05 % (2735828)CaDiCaL version: 2.1.3
% 5.64/1.05 % (2735828)Termination reason: Instruction limit
% 5.64/1.05 % (2735828)Termination phase: Saturation
% 5.64/1.05 % (2735828)Time elapsed: 0.024 s
% 5.64/1.05 % (2735828)Peak memory usage: 12 MB
% 5.64/1.05 % (2735828)Instructions burned: 44 (million)
% 5.64/1.05 % (2735832)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2950907398:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 5.64/1.05 % (2735834)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1102072734:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/95Mi)
% 6.29/1.20 % (2735826)Instruction limit reached!
% 6.29/1.20 % (2735826)------------------------------
% 6.29/1.20 % (2735826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.20 % (2735826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.20 % (2735826)CaDiCaL version: 2.1.3
% 6.29/1.20 % (2735826)Termination reason: Instruction limit
% 6.29/1.20 % (2735826)Termination phase: Saturation
% 6.29/1.20 % (2735826)Time elapsed: 0.070 s
% 6.29/1.20 % (2735826)Peak memory usage: 13 MB
% 6.29/1.20 % (2735826)Instructions burned: 131 (million)
% 6.29/1.20 % (2735837)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=922786626:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2994 on theBenchmark for (2994ds/65Mi)
% 6.29/1.20 % (2735834)Instruction limit reached!
% 6.29/1.20 % (2735834)------------------------------
% 6.29/1.20 % (2735834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.20 % (2735834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.20 % (2735834)CaDiCaL version: 2.1.3
% 6.29/1.20 % (2735834)Termination reason: Instruction limit
% 6.29/1.20 % (2735834)Termination phase: Saturation
% 6.29/1.20 % (2735834)Time elapsed: 0.055 s
% 6.29/1.20 % (2735834)Peak memory usage: 13 MB
% 6.29/1.20 % (2735834)Instructions burned: 95 (million)
% 6.29/1.20 % (2735837)Instruction limit reached!
% 6.29/1.20 % (2735837)------------------------------
% 6.29/1.20 % (2735837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.20 % (2735837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.20 % (2735837)CaDiCaL version: 2.1.3
% 6.29/1.20 % (2735837)Termination reason: Instruction limit
% 6.29/1.20 % (2735837)Termination phase: Saturation
% 6.29/1.20 % (2735837)Time elapsed: 0.035 s
% 6.29/1.20 % (2735837)Peak memory usage: 12 MB
% 6.29/1.20 % (2735837)Instructions burned: 66 (million)
% 6.29/1.20 % (2735839)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=39558952:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2993 on theBenchmark for (2993ds/105Mi)
% 6.29/1.20 % (2735840)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=2875290551:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 6.29/1.20 % (2735820)Instruction limit reached!
% 6.29/1.20 % (2735820)------------------------------
% 6.29/1.20 % (2735820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.20 % (2735820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.20 % (2735820)CaDiCaL version: 2.1.3
% 6.29/1.20 % (2735820)Termination reason: Instruction limit
% 6.29/1.20 % (2735820)Termination phase: Saturation
% 6.29/1.20 % (2735820)Time elapsed: 0.211 s
% 6.29/1.20 % (2735820)Peak memory usage: 14 MB
% 6.29/1.20 % (2735820)Instructions burned: 428 (million)
% 6.29/1.20 % (2735839)Instruction limit reached!
% 6.29/1.20 % (2735839)------------------------------
% 6.29/1.20 % (2735839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.20 % (2735839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.20 % (2735839)CaDiCaL version: 2.1.3
% 6.29/1.20 % (2735839)Termination reason: Instruction limit
% 6.29/1.20 % (2735839)Termination phase: Saturation
% 6.29/1.20 % (2735839)Time elapsed: 0.053 s
% 6.29/1.20 % (2735839)Peak memory usage: 13 MB
% 6.29/1.20 % (2735839)Instructions burned: 105 (million)
% 6.29/1.20 % (2735843)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=4001857255:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/375Mi)
% 6.29/1.20 % (2735844)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1451827349:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/495Mi)
% 6.29/1.20 % (2735824)Instruction limit reached!
% 6.29/1.20 % (2735824)------------------------------
% 6.29/1.20 % (2735824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.20 % (2735824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.24 % (2735824)CaDiCaL version: 2.1.3
% 6.29/1.24 % (2735824)Termination reason: Instruction limit
% 6.29/1.24 % (2735824)Termination phase: Saturation
% 6.29/1.24 % (2735824)Time elapsed: 0.236 s
% 6.29/1.24 % (2735824)Peak memory usage: 14 MB
% 6.29/1.24 % (2735824)Instructions burned: 516 (million)
% 6.29/1.24 % (2735823)Instruction limit reached!
% 6.29/1.24 % (2735823)------------------------------
% 6.29/1.24 % (2735823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.24 % (2735823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.24 % (2735823)CaDiCaL version: 2.1.3
% 6.29/1.24 % (2735823)Termination reason: Instruction limit
% 6.29/1.24 % (2735823)Termination phase: Saturation
% 6.29/1.24 % (2735823)Time elapsed: 0.249 s
% 6.29/1.24 % (2735823)Peak memory usage: 16 MB
% 6.29/1.24 % (2735823)Instructions burned: 877 (million)
% 6.29/1.24 % (2735848)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=4204640633:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.29/1.24 % (2735847)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=1036320699:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.29/1.24 % (2735847)Instruction limit reached!
% 6.29/1.24 % (2735847)------------------------------
% 6.29/1.24 % (2735847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.24 % (2735847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.24 % (2735847)CaDiCaL version: 2.1.3
% 6.29/1.24 % (2735847)Termination reason: Instruction limit
% 6.29/1.24 % (2735847)Termination phase: Saturation
% 6.29/1.24 % (2735847)Time elapsed: 0.017 s
% 6.29/1.24 % (2735847)Peak memory usage: 12 MB
% 6.29/1.24 % (2735847)Instructions burned: 34 (million)
% 6.29/1.24 % (2735848)Instruction limit reached!
% 6.29/1.24 % (2735848)------------------------------
% 6.29/1.24 % (2735848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.24 % (2735848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.24 % (2735848)CaDiCaL version: 2.1.3
% 6.29/1.24 % (2735848)Termination reason: Instruction limit
% 6.29/1.24 % (2735848)Termination phase: Saturation
% 6.29/1.24 % (2735848)Time elapsed: 0.028 s
% 6.29/1.24 % (2735848)Peak memory usage: 12 MB
% 6.29/1.24 % (2735848)Instructions burned: 103 (million)
% 6.29/1.24 % (2735832)Instruction limit reached!
% 6.29/1.24 % (2735832)------------------------------
% 6.29/1.24 % (2735832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.24 % (2735832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.24 % (2735832)CaDiCaL version: 2.1.3
% 6.29/1.24 % (2735832)Termination reason: Instruction limit
% 6.29/1.24 % (2735832)Termination phase: Saturation
% 6.29/1.24 % (2735832)Time elapsed: 0.220 s
% 6.29/1.24 % (2735832)Peak memory usage: 13 MB
% 6.29/1.24 % (2735832)Instructions burned: 451 (million)
% 6.29/1.24 % (2735852)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2658044889:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2992 on theBenchmark for (2992ds/22Mi)
% 6.29/1.24 % (2735851)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3176610835:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 6.29/1.24 % (2735852)Instruction limit reached!
% 6.29/1.24 % (2735852)------------------------------
% 6.29/1.24 % (2735852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.24 % (2735852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.24 % (2735852)CaDiCaL version: 2.1.3
% 6.29/1.24 % (2735852)Termination reason: Instruction limit
% 6.29/1.24 % (2735852)Termination phase: Saturation
% 6.29/1.24 % (2735852)Time elapsed: 0.005 s
% 6.29/1.24 % (2735852)Peak memory usage: 12 MB
% 6.29/1.24 % (2735852)Instructions burned: 22 (million)
% 6.29/1.24 % (2735853)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=4153056122:i=338:bd=all:ins=4:rtra=on_2992 on theBenchmark for (2992ds/338Mi)
% 6.29/1.24 % (2735856)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3531687572:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/28Mi)
% 6.29/1.24 % (2735856)Instruction limit reached!
% 6.29/1.24 % (2735856)------------------------------
% 7.19/1.37 % (2735856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.37 % (2735856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.37 % (2735856)CaDiCaL version: 2.1.3
% 7.19/1.37 % (2735856)Termination reason: Instruction limit
% 7.19/1.37 % (2735856)Termination phase: Saturation
% 7.19/1.37 % (2735856)Time elapsed: 0.008 s
% 7.19/1.37 % (2735856)Peak memory usage: 12 MB
% 7.19/1.37 % (2735856)Instructions burned: 29 (million)
% 7.19/1.37 % (2735859)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.19/1.37 % (2735831)Instruction limit reached!
% 7.19/1.37 % (2735831)------------------------------
% 7.19/1.37 % (2735831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.37 % (2735831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.37 % (2735859)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=403710556:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.19/1.37 % (2735831)CaDiCaL version: 2.1.3
% 7.19/1.37 % (2735831)Termination reason: Instruction limit
% 7.19/1.37 % (2735831)Termination phase: Saturation
% 7.19/1.37 % (2735831)Time elapsed: 0.273 s
% 7.19/1.37 % (2735831)Peak memory usage: 14 MB
% 7.19/1.37 % (2735831)Instructions burned: 572 (million)
% 7.19/1.37 % (2735851)Instruction limit reached!
% 7.19/1.37 % (2735851)------------------------------
% 7.19/1.37 % (2735851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.37 % (2735851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.37 % (2735851)CaDiCaL version: 2.1.3
% 7.19/1.37 % (2735851)Termination reason: Instruction limit
% 7.19/1.37 % (2735851)Termination phase: Saturation
% 7.19/1.37 % (2735851)Time elapsed: 0.039 s
% 7.19/1.37 % (2735851)Peak memory usage: 12 MB
% 7.19/1.37 % (2735851)Instructions burned: 68 (million)
% 7.19/1.37 % (2735861)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=3473847095:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.19/1.37 % (2735862)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=937850756:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 7.19/1.37 % (2735859)Refutation not found, incomplete strategy
% 7.19/1.37 % (2735859)------------------------------
% 7.19/1.37 % (2735859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.37 % (2735859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.37 % (2735859)CaDiCaL version: 2.1.3
% 7.19/1.37 % (2735859)Termination reason: Refutation not found, incomplete strategy
% 7.19/1.37 % (2735859)Time elapsed: 0.038 s
% 7.19/1.37 % (2735859)Peak memory usage: 13 MB
% 7.19/1.37 % (2735859)Instructions burned: 132 (million)
% 7.19/1.37 % (2735859)------------------------------
% 7.19/1.37 % (2735859)------------------------------
% 7.19/1.37 % (2735865)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.19/1.37 % (2735865)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1686935728:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/373Mi)
% 7.19/1.37 % (2735843)Instruction limit reached!
% 7.19/1.37 % (2735843)------------------------------
% 7.19/1.37 % (2735843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.37 % (2735843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/1.37 % (2735843)CaDiCaL version: 2.1.3
% 7.19/1.37 % (2735843)Termination reason: Instruction limit
% 7.19/1.37 % (2735843)Termination phase: Saturation
% 7.19/1.37 % (2735843)Time elapsed: 0.212 s
% 7.19/1.37 % (2735843)Peak memory usage: 14 MB
% 7.19/1.37 % (2735843)Instructions burned: 375 (million)
% 7.19/1.37 % (2735867)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2488929236:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.19/1.37 % (2735853)Instruction limit reached!
% 7.19/1.37 % (2735853)------------------------------
% 7.19/1.37 % (2735853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/1.37 % (2735853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/1.45 % (2735853)CaDiCaL version: 2.1.3
% 7.83/1.45 % (2735853)Termination reason: Instruction limit
% 7.83/1.45 % (2735853)Termination phase: Saturation
% 7.83/1.45 % (2735853)Time elapsed: 0.157 s
% 7.83/1.45 % (2735853)Peak memory usage: 14 MB
% 7.83/1.45 % (2735853)Instructions burned: 340 (million)
% 7.83/1.45 % (2735865)Instruction limit reached!
% 7.83/1.45 % (2735865)------------------------------
% 7.83/1.45 % (2735865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.83/1.45 % (2735865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/1.45 % (2735865)CaDiCaL version: 2.1.3
% 7.83/1.45 % (2735865)Termination reason: Instruction limit
% 7.83/1.45 % (2735865)Termination phase: Saturation
% 7.83/1.45 % (2735865)Time elapsed: 0.087 s
% 7.83/1.45 % (2735865)Peak memory usage: 13 MB
% 7.83/1.45 % (2735865)Instructions burned: 373 (million)
% 7.83/1.45 % (2735844)Instruction limit reached!
% 7.83/1.45 % (2735844)------------------------------
% 7.83/1.45 % (2735844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.83/1.45 % (2735844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/1.45 % (2735844)CaDiCaL version: 2.1.3
% 7.83/1.45 % (2735844)Termination reason: Instruction limit
% 7.83/1.45 % (2735844)Termination phase: Saturation
% 7.83/1.45 % (2735844)Time elapsed: 0.244 s
% 7.83/1.45 % (2735844)Peak memory usage: 15 MB
% 7.83/1.45 % (2735844)Instructions burned: 497 (million)
% 7.83/1.45 % (2735870)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=721373982:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2990 on theBenchmark for (2990ds/270Mi)
% 7.83/1.45 % (2735862)Instruction limit reached!
% 7.83/1.45 % (2735862)------------------------------
% 7.83/1.45 % (2735862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.83/1.45 % (2735862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/1.45 % (2735862)CaDiCaL version: 2.1.3
% 7.83/1.45 % (2735862)Termination reason: Instruction limit
% 7.83/1.45 % (2735862)Termination phase: Saturation
% 7.83/1.45 % (2735862)Time elapsed: 0.121 s
% 7.83/1.45 % (2735862)Peak memory usage: 13 MB
% 7.83/1.45 % (2735862)Instructions burned: 228 (million)
% 7.83/1.45 % (2735869)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=3463685126:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 7.83/1.45 % (2735871)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=3177575001:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2990 on theBenchmark for (2990ds/9840Mi)
% 7.83/1.45 % (2735861)Instruction limit reached!
% 7.83/1.45 % (2735861)------------------------------
% 7.83/1.45 % (2735861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.83/1.45 % (2735861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/1.45 % (2735861)CaDiCaL version: 2.1.3
% 7.83/1.45 % (2735861)Termination reason: Instruction limit
% 7.83/1.45 % (2735861)Termination phase: Saturation
% 7.83/1.45 % (2735861)Time elapsed: 0.141 s
% 7.83/1.45 % (2735861)Peak memory usage: 13 MB
% 7.83/1.45 % (2735861)Instructions burned: 341 (million)
% 7.83/1.45 % (2735873)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2170249996:i=421:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/421Mi)
% 7.83/1.45 % (2735867)Instruction limit reached!
% 7.83/1.45 % (2735867)------------------------------
% 7.83/1.45 % (2735867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.83/1.45 % (2735867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.83/1.45 % (2735867)CaDiCaL version: 2.1.3
% 7.83/1.45 % (2735867)Termination reason: Instruction limit
% 7.83/1.45 % (2735867)Termination phase: Saturation
% 7.83/1.45 % (2735867)Time elapsed: 0.062 s
% 7.83/1.45 % (2735867)Peak memory usage: 12 MB
% 7.83/1.45 % (2735867)Instructions burned: 117 (million)
% 7.83/1.45 % (2735876)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 7.83/1.45 % (2735876)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=3352308443:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/270Mi)
% 8.41/1.58 % (2735878)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3040507441:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/31Mi)
% 8.41/1.58 % (2735878)Refutation not found, incomplete strategy
% 8.41/1.58 % (2735878)------------------------------
% 8.41/1.58 % (2735878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.41/1.58 % (2735878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.41/1.58 % (2735878)CaDiCaL version: 2.1.3
% 8.41/1.58 % (2735878)Termination reason: Refutation not found, incomplete strategy
% 8.41/1.58 % (2735878)Time elapsed: 0.016 s
% 8.41/1.58 % (2735878)Peak memory usage: 12 MB
% 8.41/1.58 % (2735878)Instructions burned: 28 (million)
% 8.41/1.58 % (2735878)------------------------------
% 8.41/1.58 % (2735878)------------------------------
% 8.41/1.58 % (2735870)Instruction limit reached!
% 8.41/1.58 % (2735870)------------------------------
% 8.41/1.58 % (2735870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.41/1.58 % (2735870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.41/1.58 % (2735870)CaDiCaL version: 2.1.3
% 8.41/1.58 % (2735870)Termination reason: Instruction limit
% 8.41/1.58 % (2735870)Termination phase: Saturation
% 8.41/1.58 % (2735870)Time elapsed: 0.067 s
% 8.41/1.58 % (2735870)Peak memory usage: 13 MB
% 8.41/1.58 % (2735870)Instructions burned: 271 (million)
% 8.41/1.58 % (2735881)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 8.41/1.58 % (2735881)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 8.41/1.58 % (2735882)dis+10_2_sil=128000:si=on:random_seed=2978662329:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2989 on theBenchmark for (2989ds/339Mi)
% 8.41/1.58 % (2735881)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=500200048:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2989 on theBenchmark for (2989ds/1440Mi)
% 8.41/1.58 % (2735871)Refutation not found, incomplete strategy
% 8.41/1.58 % (2735871)------------------------------
% 8.41/1.58 % (2735871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.41/1.58 % (2735871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.41/1.58 % (2735871)CaDiCaL version: 2.1.3
% 8.41/1.58 % (2735871)Termination reason: Refutation not found, incomplete strategy
% 8.41/1.58 % (2735871)Time elapsed: 0.074 s
% 8.41/1.58 % (2735871)Peak memory usage: 13 MB
% 8.41/1.58 % (2735871)Instructions burned: 126 (million)
% 8.41/1.58 % (2735871)------------------------------
% 8.41/1.58 % (2735871)------------------------------
% 8.41/1.58 % (2735885)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=677907633:i=111:add=on:fgj=on:rtra=on:fdi=1024_2989 on theBenchmark for (2989ds/111Mi)
% 8.41/1.58 % (2735881)Refutation not found, incomplete strategy
% 8.41/1.58 % (2735881)------------------------------
% 8.41/1.58 % (2735881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.41/1.58 % (2735881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.41/1.58 % (2735881)CaDiCaL version: 2.1.3
% 8.41/1.58 % (2735881)Termination reason: Refutation not found, incomplete strategy
% 8.41/1.58 % (2735881)Time elapsed: 0.055 s
% 8.41/1.58 % (2735881)Peak memory usage: 12 MB
% 8.41/1.58 % (2735881)Instructions burned: 105 (million)
% 8.41/1.58 % (2735881)------------------------------
% 8.41/1.58 % (2735881)------------------------------
% 8.41/1.58 % (2735887)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1098035000:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2988 on theBenchmark for (2988ds/122Mi)
% 8.41/1.58 % (2735885)Instruction limit reached!
% 8.41/1.58 % (2735885)------------------------------
% 8.41/1.58 % (2735885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.41/1.58 % (2735885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.41/1.58 % (2735885)CaDiCaL version: 2.1.3
% 9.67/1.72 % (2735885)Termination reason: Instruction limit
% 9.67/1.72 % (2735885)Termination phase: Saturation
% 9.67/1.72 % (2735885)Time elapsed: 0.056 s
% 9.67/1.72 % (2735885)Peak memory usage: 12 MB
% 9.67/1.72 % (2735885)Instructions burned: 111 (million)
% 9.67/1.72 % (2735882)Instruction limit reached!
% 9.67/1.72 % (2735882)------------------------------
% 9.67/1.72 % (2735882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.67/1.72 % (2735882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/1.72 % (2735882)CaDiCaL version: 2.1.3
% 9.67/1.72 % (2735882)Termination reason: Instruction limit
% 9.67/1.72 % (2735882)Termination phase: Saturation
% 9.67/1.72 % (2735882)Time elapsed: 0.086 s
% 9.67/1.72 % (2735882)Peak memory usage: 13 MB
% 9.67/1.72 % (2735882)Instructions burned: 343 (million)
% 9.67/1.72 % (2735890)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=829815027:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2988 on theBenchmark for (2988ds/232Mi)
% 9.67/1.72 % (2735876)Instruction limit reached!
% 9.67/1.72 % (2735876)------------------------------
% 9.67/1.72 % (2735876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.67/1.72 % (2735876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/1.72 % (2735876)CaDiCaL version: 2.1.3
% 9.67/1.72 % (2735876)Termination reason: Instruction limit
% 9.67/1.72 % (2735876)Termination phase: Saturation
% 9.67/1.72 % (2735876)Time elapsed: 0.144 s
% 9.67/1.72 % (2735876)Peak memory usage: 13 MB
% 9.67/1.72 % (2735876)Instructions burned: 270 (million)
% 9.67/1.72 % (2735890)Refutation not found, incomplete strategy
% 9.67/1.72 % (2735890)------------------------------
% 9.67/1.72 % (2735890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.67/1.72 % (2735890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/1.72 % (2735890)CaDiCaL version: 2.1.3
% 9.67/1.72 % (2735890)Termination reason: Refutation not found, incomplete strategy
% 9.67/1.72 % (2735890)Time elapsed: 0.004 s
% 9.67/1.72 % (2735890)Peak memory usage: 12 MB
% 9.67/1.72 % (2735890)Instructions burned: 13 (million)
% 9.67/1.72 % (2735890)------------------------------
% 9.67/1.72 % (2735890)------------------------------
% 9.67/1.72 % (2735889)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=2654885476:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/136Mi)
% 9.67/1.72 % (2735893)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 9.67/1.72 % (2735893)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=1187630438:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2988 on theBenchmark for (2988ds/281Mi)
% 9.67/1.72 % (2735892)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=2665362027:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/1254Mi)
% 9.67/1.72 % (2735887)Instruction limit reached!
% 9.67/1.72 % (2735887)------------------------------
% 9.67/1.72 % (2735887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.67/1.72 % (2735887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/1.72 % (2735887)CaDiCaL version: 2.1.3
% 9.67/1.72 % (2735887)Termination reason: Instruction limit
% 9.67/1.72 % (2735887)Termination phase: Saturation
% 9.67/1.72 % (2735887)Time elapsed: 0.053 s
% 9.67/1.72 % (2735887)Peak memory usage: 12 MB
% 9.67/1.72 % (2735887)Instructions burned: 124 (million)
% 9.67/1.72 % (2735897)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=732941535:i=619:add=on:rtra=on_2988 on theBenchmark for (2988ds/619Mi)
% 9.67/1.72 % (2735873)Instruction limit reached!
% 9.67/1.72 % (2735873)------------------------------
% 9.67/1.72 % (2735873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.67/1.72 % (2735873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.67/1.72 % (2735873)CaDiCaL version: 2.1.3
% 9.67/1.72 % (2735873)Termination reason: Instruction limit
% 9.67/1.72 % (2735873)Termination phase: Saturation
% 9.67/1.72 % (2735873)Time elapsed: 0.223 s
% 9.67/1.72 % (2735873)Peak memory usage: 14 MB
% 9.67/1.72 % (2735873)Instructions burned: 421 (million)
% 10.31/1.91 % (2735889)Instruction limit reached!
% 10.31/1.91 % (2735889)------------------------------
% 10.31/1.91 % (2735889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.31/1.91 % (2735889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/1.91 % (2735889)CaDiCaL version: 2.1.3
% 10.31/1.91 % (2735889)Termination reason: Instruction limit
% 10.31/1.91 % (2735889)Termination phase: Saturation
% 10.31/1.91 % (2735889)Time elapsed: 0.069 s
% 10.31/1.91 % (2735889)Peak memory usage: 13 MB
% 10.31/1.91 % (2735889)Instructions burned: 136 (million)
% 10.31/1.91 % (2735893)Instruction limit reached!
% 10.31/1.91 % (2735893)------------------------------
% 10.31/1.91 % (2735893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.31/1.91 % (2735893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/1.91 % (2735893)CaDiCaL version: 2.1.3
% 10.31/1.91 % (2735893)Termination reason: Instruction limit
% 10.31/1.91 % (2735893)Termination phase: Saturation
% 10.31/1.91 % (2735893)Time elapsed: 0.073 s
% 10.31/1.91 % (2735893)Peak memory usage: 13 MB
% 10.31/1.91 % (2735893)Instructions burned: 284 (million)
% 10.31/1.91 % (2735899)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3549991037:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/865Mi)
% 10.31/1.91 % (2735900)lrs+10_1_sil=128000:si=on:urr=on:random_seed=4110751132:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/212Mi)
% 10.31/1.91 % (2735902)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3304364195:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/130Mi)
% 10.31/1.91 % (2735869)Instruction limit reached!
% 10.31/1.91 % (2735869)------------------------------
% 10.31/1.91 % (2735869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.31/1.91 % (2735869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/1.91 % (2735869)CaDiCaL version: 2.1.3
% 10.31/1.91 % (2735869)Termination reason: Instruction limit
% 10.31/1.91 % (2735869)Termination phase: Saturation
% 10.31/1.91 % (2735869)Time elapsed: 0.282 s
% 10.31/1.91 % (2735869)Peak memory usage: 14 MB
% 10.31/1.91 % (2735869)Instructions burned: 576 (million)
% 10.31/1.91 % (2735905)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2608220916:st=1.5:i=346:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/346Mi)
% 10.31/1.91 % (2735902)Instruction limit reached!
% 10.31/1.91 % (2735902)------------------------------
% 10.31/1.91 % (2735902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.31/1.91 % (2735902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/1.91 % (2735902)CaDiCaL version: 2.1.3
% 10.31/1.91 % (2735902)Termination reason: Instruction limit
% 10.31/1.91 % (2735902)Termination phase: Saturation
% 10.31/1.91 % (2735902)Time elapsed: 0.038 s
% 10.31/1.91 % (2735902)Peak memory usage: 13 MB
% 10.31/1.91 % (2735902)Instructions burned: 132 (million)
% 10.31/1.91 % (2735907)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3908657846:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2987 on theBenchmark for (2987ds/152Mi)
% 10.31/1.91 % (2735897)Refutation not found, incomplete strategy
% 10.31/1.91 % (2735897)------------------------------
% 10.31/1.91 % (2735897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.31/1.91 % (2735897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/1.91 % (2735897)CaDiCaL version: 2.1.3
% 10.31/1.91 % (2735897)Termination reason: Refutation not found, incomplete strategy
% 10.31/1.91 % (2735897)Time elapsed: 0.117 s
% 10.31/1.91 % (2735897)Peak memory usage: 13 MB
% 10.31/1.91 % (2735897)Instructions burned: 224 (million)
% 10.31/1.91 % (2735897)------------------------------
% 10.31/1.91 % (2735897)------------------------------
% 10.31/1.91 % (2735907)Instruction limit reached!
% 10.31/1.91 % (2735907)------------------------------
% 10.31/1.91 % (2735907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.31/1.91 % (2735907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/1.91 % (2735907)CaDiCaL version: 2.1.3
% 10.31/1.91 % (2735907)Termination reason: Instruction limit
% 10.31/1.91 % (2735907)Termination phase: Saturation
% 10.31/1.91 % (2735907)Time elapsed: 0.038 s
% 10.31/1.91 % (2735907)Peak memory usage: 13 MB
% 10.31/1.91 % (2735907)Instructions burned: 156 (million)
% 10.31/1.91 % (2735909)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3826114582:i=75:ep=R:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/75Mi)
% 12.68/2.09 % (2735910)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=2223205337:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/387Mi)
% 12.68/2.09 % (2735900)Instruction limit reached!
% 12.68/2.09 % (2735900)------------------------------
% 12.68/2.09 % (2735900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.68/2.09 % (2735900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.09 % (2735900)CaDiCaL version: 2.1.3
% 12.68/2.09 % (2735900)Termination reason: Instruction limit
% 12.68/2.09 % (2735900)Termination phase: Saturation
% 12.68/2.09 % (2735900)Time elapsed: 0.108 s
% 12.68/2.09 % (2735900)Peak memory usage: 13 MB
% 12.68/2.09 % (2735900)Instructions burned: 212 (million)
% 12.68/2.09 % (2735913)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=3377921427:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2986 on theBenchmark for (2986ds/148Mi)
% 12.68/2.09 % (2735909)Instruction limit reached!
% 12.68/2.09 % (2735909)------------------------------
% 12.68/2.09 % (2735909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.68/2.09 % (2735909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.09 % (2735909)CaDiCaL version: 2.1.3
% 12.68/2.09 % (2735909)Termination reason: Instruction limit
% 12.68/2.09 % (2735909)Termination phase: Saturation
% 12.68/2.09 % (2735909)Time elapsed: 0.038 s
% 12.68/2.09 % (2735909)Peak memory usage: 12 MB
% 12.68/2.09 % (2735909)Instructions burned: 75 (million)
% 12.68/2.09 % (2735905)Refutation not found, incomplete strategy
% 12.68/2.09 % (2735905)------------------------------
% 12.68/2.09 % (2735905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.68/2.09 % (2735905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.09 % (2735905)CaDiCaL version: 2.1.3
% 12.68/2.09 % (2735905)Termination reason: Refutation not found, incomplete strategy
% 12.68/2.09 % (2735905)Time elapsed: 0.101 s
% 12.68/2.09 % (2735905)Peak memory usage: 13 MB
% 12.68/2.09 % (2735905)Instructions burned: 191 (million)
% 12.68/2.09 % (2735905)------------------------------
% 12.68/2.09 % (2735905)------------------------------
% 12.68/2.09 % (2735915)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1029060834:i=161:piset=and:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/161Mi)
% 12.68/2.09 % (2735916)lrs+10_1_sil=128000:si=on:random_seed=1069805063:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/888Mi)
% 12.68/2.09 % (2735910)Instruction limit reached!
% 12.68/2.09 % (2735910)------------------------------
% 12.68/2.09 % (2735910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.68/2.09 % (2735910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.09 % (2735910)CaDiCaL version: 2.1.3
% 12.68/2.09 % (2735910)Termination reason: Instruction limit
% 12.68/2.09 % (2735910)Termination phase: Saturation
% 12.68/2.09 % (2735910)Time elapsed: 0.096 s
% 12.68/2.09 % (2735910)Peak memory usage: 13 MB
% 12.68/2.09 % (2735910)Instructions burned: 388 (million)
% 12.68/2.09 % (2735913)Instruction limit reached!
% 12.68/2.09 % (2735913)------------------------------
% 12.68/2.09 % (2735913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.68/2.09 % (2735913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.09 % (2735913)CaDiCaL version: 2.1.3
% 12.68/2.09 % (2735913)Termination reason: Instruction limit
% 12.68/2.09 % (2735913)Termination phase: Saturation
% 12.68/2.09 % (2735913)Time elapsed: 0.071 s
% 12.68/2.09 % (2735913)Peak memory usage: 12 MB
% 12.68/2.09 % (2735913)Instructions burned: 148 (million)
% 12.68/2.09 % (2735919)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=2270660310:i=136:add=on:ins=4:rtra=on:sup=off_2985 on theBenchmark for (2985ds/136Mi)
% 12.68/2.09 % (2735920)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=2312814820:i=88:s2at=3:nm=2:rtra=on:rawr=on_2985 on theBenchmark for (2985ds/88Mi)
% 12.68/2.09 % (2735915)Instruction limit reached!
% 12.68/2.09 % (2735915)------------------------------
% 13.24/2.15 % (2735915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.24/2.15 % (2735915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.15 % (2735915)CaDiCaL version: 2.1.3
% 13.24/2.15 % (2735915)Termination reason: Instruction limit
% 13.24/2.15 % (2735915)Termination phase: Saturation
% 13.24/2.15 % (2735915)Time elapsed: 0.086 s
% 13.24/2.15 % (2735915)Peak memory usage: 13 MB
% 13.24/2.15 % (2735915)Instructions burned: 163 (million)
% 13.24/2.15 % (2735919)Instruction limit reached!
% 13.24/2.15 % (2735919)------------------------------
% 13.24/2.15 % (2735919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.24/2.15 % (2735919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.15 % (2735919)CaDiCaL version: 2.1.3
% 13.24/2.15 % (2735919)Termination reason: Instruction limit
% 13.24/2.15 % (2735919)Termination phase: Saturation
% 13.24/2.15 % (2735919)Time elapsed: 0.034 s
% 13.24/2.15 % (2735919)Peak memory usage: 12 MB
% 13.24/2.15 % (2735919)Instructions burned: 140 (million)
% 13.24/2.15 % (2735924)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2803553422:i=2186:rtra=on:ixr=off_2985 on theBenchmark for (2985ds/2186Mi)
% 13.24/2.15 % (2735923)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=2864146595:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2985 on theBenchmark for (2985ds/93Mi)
% 13.24/2.15 % (2735920)Instruction limit reached!
% 13.24/2.15 % (2735920)------------------------------
% 13.24/2.15 % (2735920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.24/2.15 % (2735920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.15 % (2735920)CaDiCaL version: 2.1.3
% 13.24/2.15 % (2735920)Termination reason: Instruction limit
% 13.24/2.15 % (2735920)Termination phase: Saturation
% 13.24/2.15 % (2735920)Time elapsed: 0.052 s
% 13.24/2.15 % (2735920)Peak memory usage: 13 MB
% 13.24/2.15 % (2735920)Instructions burned: 88 (million)
% 13.24/2.15 % (2735927)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3126599163:s2a=on:i=240:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/240Mi)
% 13.24/2.15 % (2735923)Instruction limit reached!
% 13.24/2.15 % (2735923)------------------------------
% 13.24/2.15 % (2735923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.24/2.15 % (2735923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.15 % (2735923)CaDiCaL version: 2.1.3
% 13.24/2.15 % (2735923)Termination reason: Instruction limit
% 13.24/2.15 % (2735923)Termination phase: Saturation
% 13.24/2.15 % (2735923)Time elapsed: 0.048 s
% 13.24/2.15 % (2735923)Peak memory usage: 13 MB
% 13.24/2.15 % (2735923)Instructions burned: 95 (million)
% 13.24/2.15 % (2735929)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=727002079:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2984 on theBenchmark for (2984ds/805Mi)
% 13.24/2.15 % (2735927)Instruction limit reached!
% 13.24/2.15 % (2735927)------------------------------
% 13.24/2.15 % (2735927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.24/2.15 % (2735927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.15 % (2735927)CaDiCaL version: 2.1.3
% 13.24/2.15 % (2735927)Termination reason: Instruction limit
% 13.24/2.15 % (2735927)Termination phase: Saturation
% 13.24/2.15 % (2735927)Time elapsed: 0.118 s
% 13.24/2.15 % (2735927)Peak memory usage: 13 MB
% 13.24/2.15 % (2735927)Instructions burned: 241 (million)
% 13.24/2.15 % (2735924)Refutation not found, incomplete strategy
% 13.24/2.15 % (2735924)------------------------------
% 13.24/2.15 % (2735924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.24/2.15 % (2735924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.24/2.15 % (2735924)CaDiCaL version: 2.1.3
% 13.24/2.15 % (2735924)Termination reason: Refutation not found, incomplete strategy
% 13.24/2.15 % (2735924)Time elapsed: 0.165 s
% 13.24/2.15 % (2735924)Peak memory usage: 14 MB
% 13.24/2.15 % (2735924)Instructions burned: 621 (million)
% 13.24/2.15 % (2735924)------------------------------
% 13.24/2.15 % (2735924)------------------------------
% 13.24/2.15 % (2735931)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 13.24/2.15 % (2735931)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=27721286:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2983 on theBenchmark for (2983ds/391Mi)
% 13.44/2.21 % (2735932)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=3858371495:i=355:av=off:fsr=off:rtra=on:ixr=off_2983 on theBenchmark for (2983ds/355Mi)
% 13.44/2.21 % (2735899)Instruction limit reached!
% 13.44/2.21 % (2735899)------------------------------
% 13.44/2.21 % (2735899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735899)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735899)Termination reason: Instruction limit
% 13.44/2.21 % (2735899)Termination phase: Saturation
% 13.44/2.21 % (2735899)Time elapsed: 0.451 s
% 13.44/2.21 % (2735899)Peak memory usage: 14 MB
% 13.44/2.21 % (2735899)Instructions burned: 867 (million)
% 13.44/2.21 % (2735935)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=1123055971:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/314Mi)
% 13.44/2.21 % (2735892)Instruction limit reached!
% 13.44/2.21 % (2735892)------------------------------
% 13.44/2.21 % (2735892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735892)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735892)Termination reason: Instruction limit
% 13.44/2.21 % (2735892)Termination phase: Saturation
% 13.44/2.21 % (2735892)Time elapsed: 0.597 s
% 13.44/2.21 % (2735892)Peak memory usage: 14 MB
% 13.44/2.21 % (2735892)Instructions burned: 1261 (million)
% 13.44/2.21 % (2735932)Instruction limit reached!
% 13.44/2.21 % (2735932)------------------------------
% 13.44/2.21 % (2735932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735932)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735932)Termination reason: Instruction limit
% 13.44/2.21 % (2735932)Termination phase: Saturation
% 13.44/2.21 % (2735932)Time elapsed: 0.094 s
% 13.44/2.21 % (2735932)Peak memory usage: 12 MB
% 13.44/2.21 % (2735932)Instructions burned: 367 (million)
% 13.44/2.21 % (2735937)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=931313170:s2a=on:i=251:fsr=off:rtra=on_2982 on theBenchmark for (2982ds/251Mi)
% 13.44/2.21 % (2735938)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=1043327216:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2982 on theBenchmark for (2982ds/2470Mi)
% 13.44/2.21 % (2735916)Instruction limit reached!
% 13.44/2.21 % (2735916)------------------------------
% 13.44/2.21 % (2735916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735916)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735916)Termination reason: Instruction limit
% 13.44/2.21 % (2735916)Termination phase: Saturation
% 13.44/2.21 % (2735916)Time elapsed: 0.436 s
% 13.44/2.21 % (2735916)Peak memory usage: 16 MB
% 13.44/2.21 % (2735916)Instructions burned: 888 (million)
% 13.44/2.21 % (2735937)Instruction limit reached!
% 13.44/2.21 % (2735937)------------------------------
% 13.44/2.21 % (2735937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735937)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735937)Termination reason: Instruction limit
% 13.44/2.21 % (2735937)Termination phase: Saturation
% 13.44/2.21 % (2735937)Time elapsed: 0.064 s
% 13.44/2.21 % (2735937)Peak memory usage: 13 MB
% 13.44/2.21 % (2735937)Instructions burned: 253 (million)
% 13.44/2.21 % (2735942)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=152412590:i=116:ep=RSTC:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/116Mi)
% 13.44/2.21 % (2735931)Instruction limit reached!
% 13.44/2.21 % (2735931)------------------------------
% 13.44/2.21 % (2735931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735931)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735931)Termination reason: Instruction limit
% 13.44/2.21 % (2735931)Termination phase: Saturation
% 13.44/2.21 % (2735931)Time elapsed: 0.181 s
% 13.44/2.21 % (2735931)Peak memory usage: 13 MB
% 13.44/2.21 % (2735931)Instructions burned: 392 (million)
% 13.44/2.21 % (2735941)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=547475299:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2981 on theBenchmark for (2981ds/673Mi)
% 13.44/2.21 % (2735944)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=826977370:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2981 on theBenchmark for (2981ds/270Mi)
% 13.44/2.21 % (2735935)Instruction limit reached!
% 13.44/2.21 % (2735935)------------------------------
% 13.44/2.21 % (2735935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735935)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735935)Termination reason: Instruction limit
% 13.44/2.21 % (2735935)Termination phase: Saturation
% 13.44/2.21 % (2735935)Time elapsed: 0.169 s
% 13.44/2.21 % (2735935)Peak memory usage: 14 MB
% 13.44/2.21 % (2735935)Instructions burned: 315 (million)
% 13.44/2.21 % (2735942)Instruction limit reached!
% 13.44/2.21 % (2735942)------------------------------
% 13.44/2.21 % (2735942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735942)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735942)Termination reason: Instruction limit
% 13.44/2.21 % (2735942)Termination phase: Saturation
% 13.44/2.21 % (2735942)Time elapsed: 0.033 s
% 13.44/2.21 % (2735942)Peak memory usage: 12 MB
% 13.44/2.21 % (2735942)Instructions burned: 119 (million)
% 13.44/2.21 % (2735948)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 13.44/2.21 % (2735948)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=2721176392:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2981 on theBenchmark for (2981ds/39Mi)
% 13.44/2.21 % (2735947)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=2937689861:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2981 on theBenchmark for (2981ds/30Mi)
% 13.44/2.21 % (2735929)Instruction limit reached!
% 13.44/2.21 % (2735929)------------------------------
% 13.44/2.21 % (2735929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735929)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735929)Termination reason: Instruction limit
% 13.44/2.21 % (2735929)Termination phase: Saturation
% 13.44/2.21 % (2735929)Time elapsed: 0.327 s
% 13.44/2.21 % (2735929)Peak memory usage: 14 MB
% 13.44/2.21 % (2735929)Instructions burned: 807 (million)
% 13.44/2.21 % (2735948)Instruction limit reached!
% 13.44/2.21 % (2735948)------------------------------
% 13.44/2.21 % (2735948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735948)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735948)Termination reason: Instruction limit
% 13.44/2.21 % (2735948)Termination phase: Saturation
% 13.44/2.21 % (2735948)Time elapsed: 0.011 s
% 13.44/2.21 % (2735948)Peak memory usage: 12 MB
% 13.44/2.21 % (2735948)Instructions burned: 40 (million)
% 13.44/2.21 % (2735947)Instruction limit reached!
% 13.44/2.21 % (2735947)------------------------------
% 13.44/2.21 % (2735947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735947)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735947)Termination reason: Instruction limit
% 13.44/2.21 % (2735947)Termination phase: Saturation
% 13.44/2.21 % (2735947)Time elapsed: 0.018 s
% 13.44/2.21 % (2735947)Peak memory usage: 12 MB
% 13.44/2.21 % (2735947)Instructions burned: 30 (million)
% 13.44/2.21 % (2735951)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3774987071:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2981 on theBenchmark for (2981ds/365Mi)
% 13.44/2.21 % (2735952)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1974164919:i=158:av=off:rtra=on_2980 on theBenchmark for (2980ds/158Mi)
% 13.44/2.21 % (2735954)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 13.44/2.21 % (2735954)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=2887584366:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/252Mi)
% 13.44/2.21 % (2735952)Instruction limit reached!
% 13.44/2.21 % (2735952)------------------------------
% 13.44/2.21 % (2735952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735952)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735952)Termination reason: Instruction limit
% 13.44/2.21 % (2735952)Termination phase: Saturation
% 13.44/2.21 % (2735952)Time elapsed: 0.041 s
% 13.44/2.21 % (2735952)Peak memory usage: 12 MB
% 13.44/2.21 % (2735952)Instructions burned: 160 (million)
% 13.44/2.21 % (2735941) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2735702-2735941"...
% 13.44/2.21 % (2735957)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=3102529311:i=213:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/213Mi)
% 13.44/2.21 % (2735941)...printing done.
% 13.44/2.21 % (2735941)Refutation found. Thanks to Tanya!
% 13.44/2.21 % SZS status Theorem for theBenchmark
% 13.44/2.21 % SZS output start Proof for theBenchmark
% 13.44/2.21 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 13.44/2.21 thf(func_def_0, type, cNUMBER: ($i > $o)).
% 13.44/2.21 thf(func_def_1, type, cODD: ($i > $o)).
% 13.44/2.21 thf(func_def_2, type, cEVEN: ($i > $o)).
% 13.44/2.21 thf(func_def_3, type, cS: ($i > $i)).
% 13.44/2.21 thf(func_def_9, type, sK1: (($i > $o) > ($i > $o) > $i)).
% 13.44/2.21 thf(func_def_10, type, db0: !>[X0: $tType]:(X0)).
% 13.44/2.21 thf(func_def_11, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 13.44/2.21 thf(func_def_13, type, sF3: !>[X0: $tType]:(($i > ($i > X0) > X0))).
% 13.44/2.21 thf(func_def_14, type, sF4: !>[X0: $tType]:((X0 > (X0 > $i) > $i))).
% 13.44/2.21 thf(func_def_15, type, sF5: !>[X0: $tType, X1: $tType]:((X1 > (X1 > $i) > ($i > X0) > X0))).
% 13.44/2.21 thf(func_def_16, type, sF6: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > X0 > X1 > X2))).
% 13.44/2.21 thf(func_def_17, type, db1: !>[X0: $tType]:(X0)).
% 13.44/2.21 thf(func_def_18, type, sF7: !>[X0: $tType]:((X0 > (X0 > X0) > X0))).
% 13.44/2.21 thf(func_def_19, type, sF8: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > (X1 > X0) > X1 > X2))).
% 13.44/2.21 thf(func_def_20, type, sF9: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > ((X0 > X2) > X1) > X1))).
% 13.44/2.21 thf(func_def_21, type, sF10: !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 13.44/2.21 thf(func_def_22, type, sF11: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > (X0 > X2 > X1) > X2 > X1))).
% 13.44/2.21 thf(func_def_23, type, sF12: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X1 > X0) > ((X1 > X0) > X2 > X3) > X2 > X3))).
% 13.44/2.21 thf(f1,conjecture,(
% 13.44/2.21 (! [X2 : ($i > $o),X1 : ($i > $o)] : (((X2 @ c0) & (X1 @ c0) & ! [X3 : $i] : (((X2 @ X3) & (X1 @ X3)) => ((X1 @ (cS @ X3)) & (X2 @ (cS @ X3))))) => ! [X3 : $i] : ((X2 @ X3) & (X1 @ X3))) & ! [X0 : $i] : ((cNUMBER @ X0) <=> ((cODD @ X0) | (cEVEN @ X0))) & (cODD @ (cS @ c0)) & ! [X0 : $i] : ((cODD @ X0) => (cODD @ (cS @ (cS @ X0)))) & ! [X0 : $i] : ((cEVEN @ X0) => (cEVEN @ (cS @ (cS @ X0)))) & (cEVEN @ c0)) => ! [X0 : $i] : (cNUMBER @ X0)),
% 13.44/2.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cEVEN_ODD_4)).
% 13.44/2.21 thf(f2,negated_conjecture,(
% 13.44/2.21 ~((! [X2 : ($i > $o),X1 : ($i > $o)] : (((X2 @ c0) & (X1 @ c0) & ! [X3 : $i] : (((X2 @ X3) & (X1 @ X3)) => ((X1 @ (cS @ X3)) & (X2 @ (cS @ X3))))) => ! [X3 : $i] : ((X2 @ X3) & (X1 @ X3))) & ! [X0 : $i] : ((cNUMBER @ X0) <=> ((cODD @ X0) | (cEVEN @ X0))) & (cODD @ (cS @ c0)) & ! [X0 : $i] : ((cODD @ X0) => (cODD @ (cS @ (cS @ X0)))) & ! [X0 : $i] : ((cEVEN @ X0) => (cEVEN @ (cS @ (cS @ X0)))) & (cEVEN @ c0)) => ! [X0 : $i] : (cNUMBER @ X0))),
% 13.44/2.21 inference(negated_conjecture,[status(cth)],[f1])).
% 13.44/2.21 thf(f3,plain,(
% 13.44/2.21 ~((! [X0 : ($i > $o),X1 : ($i > $o)] : (((X0 @ c0) & (X1 @ c0) & ! [X2 : $i] : (((X0 @ X2) & (X1 @ X2)) => ((X1 @ (cS @ X2)) & (X0 @ (cS @ X2))))) => ! [X3 : $i] : ((X0 @ X3) & (X1 @ X3))) & ! [X4 : $i] : ((cNUMBER @ X4) <=> ((cODD @ X4) | (cEVEN @ X4))) & (cODD @ (cS @ c0)) & ! [X5 : $i] : ((cODD @ X5) => (cODD @ (cS @ (cS @ X5)))) & ! [X6 : $i] : ((cEVEN @ X6) => (cEVEN @ (cS @ (cS @ X6)))) & (cEVEN @ c0)) => ! [X7 : $i] : (cNUMBER @ X7))),
% 13.44/2.21 inference(rectify,[],[f2])).
% 13.44/2.21 thf(f4,plain,(
% 13.44/2.21 ~((! [X1 : ($i > $o),X0 : ($i > $o)] : (((((X1 @ c0)) = $true) & ($true = ((X0 @ c0))) & ! [X2 : $i] : (((((X1 @ X2)) = $true) & (((X0 @ X2)) = $true)) => ((((X1 @ (cS @ X2))) = $true) & (((X0 @ (cS @ X2))) = $true)))) => ! [X3 : $i] : ((((X1 @ X3)) = $true) & (((X0 @ X3)) = $true))) & ! [X4 : $i] : ((((cNUMBER @ X4)) = $true) <=> ((((cODD @ X4)) = $true) | (((cEVEN @ X4)) = $true))) & (((cEVEN @ c0)) = $true) & ! [X5 : $i] : ((((cODD @ X5)) = $true) => (((cODD @ (cS @ (cS @ X5)))) = $true)) & (((cODD @ (cS @ c0))) = $true) & ! [X6 : $i] : ((((cEVEN @ X6)) = $true) => (((cEVEN @ (cS @ (cS @ X6)))) = $true))) => ! [X7 : $i] : (((cNUMBER @ X7)) = $true))),
% 13.44/2.21 inference(fool_elimination,[],[f3])).
% 13.44/2.21 thf(f5,plain,(
% 13.44/2.21 ? [X7 : $i] : (((cNUMBER @ X7)) != $true) & (! [X1 : ($i > $o),X0 : ($i > $o)] : (! [X3 : $i] : ((((X1 @ X3)) = $true) & (((X0 @ X3)) = $true)) | ((((X1 @ c0)) != $true) | ($true != ((X0 @ c0))) | ? [X2 : $i] : (((((X0 @ (cS @ X2))) != $true) | (((X1 @ (cS @ X2))) != $true)) & ((((X1 @ X2)) = $true) & (((X0 @ X2)) = $true))))) & ! [X4 : $i] : ((((cNUMBER @ X4)) = $true) <=> ((((cODD @ X4)) = $true) | (((cEVEN @ X4)) = $true))) & (((cEVEN @ c0)) = $true) & ! [X5 : $i] : ((((cODD @ X5)) != $true) | (((cODD @ (cS @ (cS @ X5)))) = $true)) & (((cODD @ (cS @ c0))) = $true) & ! [X6 : $i] : ((((cEVEN @ X6)) != $true) | (((cEVEN @ (cS @ (cS @ X6)))) = $true)))),
% 13.44/2.21 inference(ennf_transformation,[],[f4])).
% 13.44/2.21 thf(f6,plain,(
% 13.44/2.21 ! [X4 : $i] : ((((cNUMBER @ X4)) = $true) <=> ((((cODD @ X4)) = $true) | (((cEVEN @ X4)) = $true))) & ! [X5 : $i] : ((((cODD @ X5)) != $true) | (((cODD @ (cS @ (cS @ X5)))) = $true)) & ! [X6 : $i] : ((((cEVEN @ X6)) != $true) | (((cEVEN @ (cS @ (cS @ X6)))) = $true)) & (((cEVEN @ c0)) = $true) & (((cODD @ (cS @ c0))) = $true) & ? [X7 : $i] : (((cNUMBER @ X7)) != $true) & ! [X0 : ($i > $o),X1 : ($i > $o)] : (! [X3 : $i] : ((((X1 @ X3)) = $true) & (((X0 @ X3)) = $true)) | ? [X2 : $i] : ((((X1 @ X2)) = $true) & ((((X0 @ (cS @ X2))) != $true) | (((X1 @ (cS @ X2))) != $true)) & (((X0 @ X2)) = $true)) | ($true != ((X0 @ c0))) | (((X1 @ c0)) != $true))),
% 13.44/2.21 inference(flattening,[],[f5])).
% 13.44/2.21 thf(f7,plain,(
% 13.44/2.21 ! [X4 : $i] : (((((cNUMBER @ X4)) = $true) | ((((cODD @ X4)) != $true) & (((cEVEN @ X4)) != $true))) & (((((cODD @ X4)) = $true) | (((cEVEN @ X4)) = $true)) | (((cNUMBER @ X4)) != $true))) & ! [X5 : $i] : ((((cODD @ X5)) != $true) | (((cODD @ (cS @ (cS @ X5)))) = $true)) & ! [X6 : $i] : ((((cEVEN @ X6)) != $true) | (((cEVEN @ (cS @ (cS @ X6)))) = $true)) & (((cEVEN @ c0)) = $true) & (((cODD @ (cS @ c0))) = $true) & ? [X7 : $i] : (((cNUMBER @ X7)) != $true) & ! [X0 : ($i > $o),X1 : ($i > $o)] : (! [X3 : $i] : ((((X1 @ X3)) = $true) & (((X0 @ X3)) = $true)) | ? [X2 : $i] : ((((X1 @ X2)) = $true) & ((((X0 @ (cS @ X2))) != $true) | (((X1 @ (cS @ X2))) != $true)) & (((X0 @ X2)) = $true)) | ($true != ((X0 @ c0))) | (((X1 @ c0)) != $true))),
% 13.44/2.21 inference(nnf_transformation,[],[f6])).
% 13.44/2.21 thf(f8,plain,(
% 13.44/2.21 ! [X4 : $i] : (((((cNUMBER @ X4)) = $true) | ((((cODD @ X4)) != $true) & (((cEVEN @ X4)) != $true))) & ((((cODD @ X4)) = $true) | (((cEVEN @ X4)) = $true) | (((cNUMBER @ X4)) != $true))) & ! [X5 : $i] : ((((cODD @ X5)) != $true) | (((cODD @ (cS @ (cS @ X5)))) = $true)) & ! [X6 : $i] : ((((cEVEN @ X6)) != $true) | (((cEVEN @ (cS @ (cS @ X6)))) = $true)) & (((cEVEN @ c0)) = $true) & (((cODD @ (cS @ c0))) = $true) & ? [X7 : $i] : (((cNUMBER @ X7)) != $true) & ! [X0 : ($i > $o),X1 : ($i > $o)] : (! [X3 : $i] : ((((X1 @ X3)) = $true) & (((X0 @ X3)) = $true)) | ? [X2 : $i] : ((((X1 @ X2)) = $true) & ((((X0 @ (cS @ X2))) != $true) | (((X1 @ (cS @ X2))) != $true)) & (((X0 @ X2)) = $true)) | ($true != ((X0 @ c0))) | (((X1 @ c0)) != $true))),
% 13.44/2.21 inference(flattening,[],[f7])).
% 13.44/2.21 thf(f9,plain,(
% 13.44/2.21 ! [X0 : $i] : (((((cNUMBER @ X0)) = $true) | ((((cODD @ X0)) != $true) & (((cEVEN @ X0)) != $true))) & ((((cODD @ X0)) = $true) | (((cEVEN @ X0)) = $true) | (((cNUMBER @ X0)) != $true))) & ! [X1 : $i] : (($true != ((cODD @ X1))) | (((cODD @ (cS @ (cS @ X1)))) = $true)) & ! [X2 : $i] : ((((cEVEN @ X2)) != $true) | (((cEVEN @ (cS @ (cS @ X2)))) = $true)) & (((cEVEN @ c0)) = $true) & (((cODD @ (cS @ c0))) = $true) & ? [X3 : $i] : (((cNUMBER @ X3)) != $true) & ! [X4 : ($i > $o),X5 : ($i > $o)] : (! [X6 : $i] : ((((X5 @ X6)) = $true) & (((X4 @ X6)) = $true)) | ? [X7 : $i] : ((((X5 @ X7)) = $true) & ((((X4 @ (cS @ X7))) != $true) | (((X5 @ (cS @ X7))) != $true)) & (((X4 @ X7)) = $true)) | ($true != ((X4 @ c0))) | (((X5 @ c0)) != $true))),
% 13.44/2.21 inference(rectify,[],[f8])).
% 13.44/2.21 thf(f10,plain,(
% 13.44/2.21 ! [X0 : $i] : (((((cNUMBER @ X0)) = $true) | ((((cODD @ X0)) != $true) & (((cEVEN @ X0)) != $true))) & ((((cODD @ X0)) = $true) | (((cEVEN @ X0)) = $true) | (((cNUMBER @ X0)) != $true))) & ! [X1 : $i] : (($true != ((cODD @ X1))) | (((cODD @ (cS @ (cS @ X1)))) = $true)) & ! [X2 : $i] : ((((cEVEN @ X2)) != $true) | (((cEVEN @ (cS @ (cS @ X2)))) = $true)) & (((cEVEN @ c0)) = $true) & (((cODD @ (cS @ c0))) = $true) & (((cNUMBER @ sK0)) != $true) & ! [X4 : ($i > $o),X5 : ($i > $o)] : (! [X6 : $i] : ((((X5 @ X6)) = $true) & (((X4 @ X6)) = $true)) | ((((X5 @ (sK1 @ X5 @ X4))) = $true) & ((((X4 @ (cS @ (sK1 @ X5 @ X4)))) != $true) | (((X5 @ (cS @ (sK1 @ X5 @ X4)))) != $true)) & (((X4 @ (sK1 @ X5 @ X4))) = $true)) | ($true != ((X4 @ c0))) | (((X5 @ c0)) != $true))),
% 13.44/2.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,vAPP]),skolemize(X3,sK0),skolemize(X7,sK1 @ X5 @ X4)],[f9])).
% 13.44/2.21 thf(f11,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o),X5 : ($i > $o)] : (($true != ((X4 @ c0))) | (((X4 @ X6)) = $true) | (((X4 @ (sK1 @ X5 @ X4))) = $true) | (((X5 @ c0)) != $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f12,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o),X5 : ($i > $o)] : ((((X5 @ (cS @ (sK1 @ X5 @ X4)))) != $true) | (((X4 @ X6)) = $true) | ($true != ((X4 @ c0))) | (((X4 @ (cS @ (sK1 @ X5 @ X4)))) != $true) | (((X5 @ c0)) != $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f13,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o),X5 : ($i > $o)] : (($true != ((X4 @ c0))) | (((X4 @ X6)) = $true) | (((X5 @ (sK1 @ X5 @ X4))) = $true) | (((X5 @ c0)) != $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f17,plain,(
% 13.44/2.21 (((cNUMBER @ sK0)) != $true)),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f18,plain,(
% 13.44/2.21 (((cODD @ (cS @ c0))) = $true)),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f19,plain,(
% 13.44/2.21 (((cEVEN @ c0)) = $true)),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f20,plain,(
% 13.44/2.21 ( ! [X2 : $i] : ((((cEVEN @ X2)) != $true) | (((cEVEN @ (cS @ (cS @ X2)))) = $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f21,plain,(
% 13.44/2.21 ( ! [X1 : $i] : (($true != ((cODD @ X1))) | (((cODD @ (cS @ (cS @ X1)))) = $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f22,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ X0)) != $true) | (((cODD @ X0)) = $true) | (((cEVEN @ X0)) = $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f23,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cEVEN @ X0)) != $true) | (((cNUMBER @ X0)) = $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f24,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cODD @ X0)) != $true) | (((cNUMBER @ X0)) = $true)) )),
% 13.44/2.21 inference(cnf_transformation,[],[f10])).
% 13.44/2.21 thf(f27,plain,(
% 13.44/2.21 ($true != $true) | (((cNUMBER @ c0)) = $true)),
% 13.44/2.21 inference(constrained_superposition,[],[f23,f19])).
% 13.44/2.21 thf(f28,plain,(
% 13.44/2.21 (((cNUMBER @ c0)) = $true)),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f27])).
% 13.44/2.21 thf(f29,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ c0))) = $true) | ($true != $true)),
% 13.44/2.21 inference(constrained_superposition,[],[f24,f18])).
% 13.44/2.21 thf(f30,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ c0))) = $true)),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f29])).
% 13.44/2.21 thf(f70,definition,(
% 13.44/2.21 spl2_3 <=> ! [X0 : $i] : (((cNUMBER @ X0)) = $true)),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition])).
% 13.44/2.21 thf(f71,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ X0)) = $true)) ) | ~spl2_3),
% 13.44/2.21 inference(avatar_component_clause,[],[f70])).
% 13.44/2.21 thf(f77,plain,(
% 13.44/2.21 ($true != $true) | ~spl2_3),
% 13.44/2.21 inference(constrained_superposition,[],[f17,f71])).
% 13.44/2.21 thf(f80,plain,(
% 13.44/2.21 $false | ~spl2_3),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f77])).
% 13.44/2.21 thf(f81,plain,(
% 13.44/2.21 ~spl2_3),
% 13.44/2.21 inference(avatar_contradiction_clause,[],[f80])).
% 13.44/2.21 thf(f227,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o)] : ((((X4 @ X6)) = $true) | ((((^[Y0 : $i]: ($true)) @ (cS @ (sK1 @ (^[Y0 : $i]: ($true)) @ X4)))) != $true) | ((((^[Y0 : $i]: ($true)) @ c0)) != $true) | (((X4 @ (cS @ (sK1 @ (^[Y0 : $i]: ($true)) @ X4)))) != $true) | ($true != ((X4 @ c0)))) )),
% 13.44/2.21 inference(imitation,[],[f12])).
% 13.44/2.21 thf(f228,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o)] : (($true != $true) | ($true != $true) | ($true != ((X4 @ c0))) | (((X4 @ X6)) = $true) | (((X4 @ (cS @ (sK1 @ (^[Y0 : $i]: ($true)) @ X4)))) != $true)) )),
% 13.44/2.21 inference(beta-eta_normalization,[],[f227])).
% 13.44/2.21 thf(f229,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o)] : ((((X4 @ X6)) = $true) | ($true != ((X4 @ c0))) | ($true != $true) | (((X4 @ (cS @ (sK1 @ (^[Y0 : $i]: ($true)) @ X4)))) != $true)) )),
% 13.44/2.21 inference(duplicate_literal_removal,[],[f228])).
% 13.44/2.21 thf(f230,plain,(
% 13.44/2.21 ( ! [X6 : $i,X4 : ($i > $o)] : ((((X4 @ (cS @ (sK1 @ (^[Y0 : $i]: ($true)) @ X4)))) != $true) | ($true != ((X4 @ c0))) | (((X4 @ X6)) = $true)) )),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f229])).
% 13.44/2.21 thf(f499,definition,(
% 13.44/2.21 ( ! [X1 : $tType,X0 : $tType,X3 : $tType,X2 : (X0 > X1),X4 : (X3 > X0),X5 : X3] : ((((sF8 @ X0 @ X3 @ X1 @ X2 @ X4 @ X5)) = ((X2 @ (X4 @ X5))))) )),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 13.44/2.21 thf(f510,plain,(
% 13.44/2.21 ( ! [X0 : $tType,X2 : ($i > X0),X3 : $i,X1 : (X0 > $o),X4 : ($i > $o)] : (($true != ((X4 @ c0))) | (((X1 @ (X2 @ c0))) != $true) | (((sF8 @ X0 @ $i @ $o @ X1 @ X2 @ X3)) = $true) | (((sF8 @ X0 @ $i @ $o @ X1 @ X2 @ (sK1 @ X4 @ (sF8 @ X0 @ $i @ $o @ X1 @ X2)))) = $true)) )),
% 13.44/2.21 inference(constrained_superposition,[],[f11,f499])).
% 13.44/2.21 thf(f511,plain,(
% 13.44/2.21 ( ! [X0 : $tType,X2 : ($i > X0),X3 : $i,X1 : (X0 > $o),X4 : ($i > $o)] : ((((sF8 @ X0 @ $i @ $o @ X1 @ X2 @ X3)) = $true) | (((X4 @ (sK1 @ X4 @ (sF8 @ X0 @ $i @ $o @ X1 @ X2)))) = $true) | ($true != ((X4 @ c0))) | (((X1 @ (X2 @ c0))) != $true)) )),
% 13.44/2.21 inference(constrained_superposition,[],[f13,f499])).
% 13.44/2.21 thf(f523,plain,(
% 13.44/2.21 ( ! [X0 : $tType,X2 : ($i > X0),X3 : $i,X1 : (X0 > $o),X4 : ($i > $o)] : (($true != ((X4 @ c0))) | (((X1 @ (X2 @ c0))) != $true) | (((X1 @ (X2 @ X3))) = $true) | (((sF8 @ X0 @ $i @ $o @ X1 @ X2 @ (sK1 @ X4 @ (sF8 @ X0 @ $i @ $o @ X1 @ X2)))) = $true)) )),
% 13.44/2.21 inference(forward_demodulation,[],[f510,f499])).
% 13.44/2.21 thf(f526,plain,(
% 13.44/2.21 ( ! [X0 : $tType,X2 : ($i > X0),X3 : $i,X1 : (X0 > $o),X4 : ($i > $o)] : ((((X1 @ (X2 @ c0))) != $true) | ($true != ((X4 @ c0))) | (((X1 @ (X2 @ X3))) = $true) | (((X4 @ (sK1 @ X4 @ (sF8 @ X0 @ $i @ $o @ X1 @ X2)))) = $true)) )),
% 13.44/2.21 inference(forward_demodulation,[],[f511,f499])).
% 13.44/2.21 thf(f533,plain,(
% 13.44/2.21 ( ! [X0 : $tType,X2 : ($i > X0),X3 : $i,X1 : (X0 > $o),X4 : ($i > $o)] : ((((X1 @ (X2 @ c0))) != $true) | (((X1 @ (X2 @ X3))) = $true) | ($true != ((X4 @ c0))) | (((X1 @ (X2 @ (sK1 @ X4 @ (sF8 @ X0 @ $i @ $o @ X1 @ X2))))) = $true)) )),
% 13.44/2.21 inference(forward_demodulation,[],[f523,f499])).
% 13.44/2.21 thf(f632,plain,(
% 13.44/2.21 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (sK1 @ X0 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ($true != ((X0 @ c0))) | (((cNUMBER @ (cS @ X1))) = $true) | ($true != $true)) )),
% 13.44/2.21 inference(constrained_superposition,[],[f526,f30])).
% 13.44/2.21 thf(f643,plain,(
% 13.44/2.21 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (sK1 @ X0 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ($true != ((X0 @ c0))) | (((cNUMBER @ (cS @ X1))) = $true)) )),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f632])).
% 13.44/2.21 thf(f654,definition,(
% 13.44/2.21 spl2_19 <=> ! [X0 : ($i > $o)] : ((((X0 @ (sK1 @ X0 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ($true != ((X0 @ c0))))),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition])).
% 13.44/2.21 thf(f655,plain,(
% 13.44/2.21 ( ! [X0 : ($i > $o)] : (($true != ((X0 @ c0))) | (((X0 @ (sK1 @ X0 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true)) ) | ~spl2_19),
% 13.44/2.21 inference(avatar_component_clause,[],[f654])).
% 13.44/2.21 thf(f657,definition,(
% 13.44/2.21 spl2_20 <=> ! [X1 : $i] : (((cNUMBER @ (cS @ X1))) = $true)),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_20])],[avatar_definition])).
% 13.44/2.21 thf(f658,plain,(
% 13.44/2.21 ( ! [X1 : $i] : ((((cNUMBER @ (cS @ X1))) = $true)) ) | ~spl2_20),
% 13.44/2.21 inference(avatar_component_clause,[],[f657])).
% 13.44/2.21 thf(f659,plain,(
% 13.44/2.21 spl2_19 | spl2_20),
% 13.44/2.21 inference(avatar_split_clause,[],[f643,f657,f654])).
% 13.44/2.21 thf(f737,plain,(
% 13.44/2.21 ( ! [X0 : $i,X1 : ($i > $o)] : ((((X1 @ c0)) != $true) | (((cNUMBER @ (cS @ (sK1 @ X1 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) = $true) | ($true != $true) | (((cNUMBER @ (cS @ X0))) = $true)) )),
% 13.44/2.21 inference(constrained_superposition,[],[f533,f30])).
% 13.44/2.21 thf(f751,plain,(
% 13.44/2.21 ( ! [X0 : $i,X1 : ($i > $o)] : ((((cNUMBER @ (cS @ X0))) = $true) | (((X1 @ c0)) != $true) | (((cNUMBER @ (cS @ (sK1 @ X1 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) = $true)) )),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f737])).
% 13.44/2.21 thf(f761,definition,(
% 13.44/2.21 spl2_27 <=> ! [X1 : ($i > $o)] : ((((X1 @ c0)) != $true) | (((cNUMBER @ (cS @ (sK1 @ X1 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) = $true))),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition])).
% 13.44/2.21 thf(f762,plain,(
% 13.44/2.21 ( ! [X1 : ($i > $o)] : ((((X1 @ c0)) != $true) | (((cNUMBER @ (cS @ (sK1 @ X1 @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) = $true)) ) | ~spl2_27),
% 13.44/2.21 inference(avatar_component_clause,[],[f761])).
% 13.44/2.21 thf(f763,plain,(
% 13.44/2.21 spl2_27 | spl2_20),
% 13.44/2.21 inference(avatar_split_clause,[],[f751,f657,f761])).
% 13.44/2.21 thf(f775,plain,(
% 13.44/2.21 ( ! [X0 : $i] : (($true != $true) | (((cNUMBER @ c0)) != $true) | (((cNUMBER @ X0)) = $true)) ) | ~spl2_20),
% 13.44/2.21 inference(constrained_superposition,[],[f230,f658])).
% 13.44/2.21 thf(f782,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ c0)) != $true) | (((cNUMBER @ X0)) = $true)) ) | ~spl2_20),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f775])).
% 13.44/2.21 thf(f788,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ X0)) = $true)) ) | ~spl2_20),
% 13.44/2.21 inference(forward_subsumption_resolution,[],[f782,f28])).
% 13.44/2.21 thf(f791,plain,(
% 13.44/2.21 spl2_3 | ~spl2_20),
% 13.44/2.21 inference(avatar_split_clause,[],[f788,f657,f70])).
% 13.44/2.21 thf(f836,plain,(
% 13.44/2.21 ($true != $true) | (((cNUMBER @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ~spl2_19),
% 13.44/2.21 inference(constrained_superposition,[],[f655,f28])).
% 13.44/2.21 thf(f839,plain,(
% 13.44/2.21 (((cNUMBER @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ~spl2_19),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f836])).
% 13.44/2.21 thf(f844,plain,(
% 13.44/2.21 (((cODD @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | (((cEVEN @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ($true != $true) | ~spl2_19),
% 13.44/2.21 inference(constrained_superposition,[],[f22,f839])).
% 13.44/2.21 thf(f845,plain,(
% 13.44/2.21 (((cODD @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | (((cEVEN @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ~spl2_19),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f844])).
% 13.44/2.21 thf(f847,definition,(
% 13.44/2.21 spl2_30 <=> (((cODD @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true)),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_30])],[avatar_definition])).
% 13.44/2.21 thf(f849,plain,(
% 13.44/2.21 (((cODD @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ~spl2_30),
% 13.44/2.21 inference(avatar_component_clause,[],[f847])).
% 13.44/2.21 thf(f851,definition,(
% 13.44/2.21 spl2_31 <=> (((cEVEN @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true)),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition])).
% 13.44/2.21 thf(f853,plain,(
% 13.44/2.21 (((cEVEN @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))) = $true) | ~spl2_31),
% 13.44/2.21 inference(avatar_component_clause,[],[f851])).
% 13.44/2.21 thf(f854,plain,(
% 13.44/2.21 spl2_30 | spl2_31 | ~spl2_19),
% 13.44/2.21 inference(avatar_split_clause,[],[f845,f654,f851,f847])).
% 13.44/2.21 thf(f859,plain,(
% 13.44/2.21 (((cODD @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ($true != $true) | ~spl2_30),
% 13.44/2.21 inference(constrained_superposition,[],[f21,f849])).
% 13.44/2.21 thf(f861,plain,(
% 13.44/2.21 (((cODD @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ~spl2_30),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f859])).
% 13.44/2.21 thf(f886,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ($true != $true) | ~spl2_30),
% 13.44/2.21 inference(constrained_superposition,[],[f24,f861])).
% 13.44/2.21 thf(f887,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ~spl2_30),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f886])).
% 13.44/2.21 thf(f1037,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) = $true) | ($true != $true) | ~spl2_27),
% 13.44/2.21 inference(constrained_superposition,[],[f762,f28])).
% 13.44/2.21 thf(f1041,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) = $true) | ~spl2_27),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f1037])).
% 13.44/2.21 thf(f1132,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ c0)) != $true) | (((cNUMBER @ c0)) != $true) | ($true != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true)) ) | ~spl2_27),
% 13.44/2.21 inference(constrained_superposition,[],[f12,f1041])).
% 13.44/2.21 thf(f1133,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ c0)) != $true) | (((cNUMBER @ c0)) != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true)) ) | ~spl2_27),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f1132])).
% 13.44/2.21 thf(f1136,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS))))) != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ c0)) != $true)) ) | ~spl2_27),
% 13.44/2.21 inference(forward_subsumption_resolution,[],[f1133,f28])).
% 13.44/2.21 thf(f1147,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true) | (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ c0)) != $true)) ) | ~spl2_27),
% 13.44/2.21 inference(forward_demodulation,[],[f1136,f499])).
% 13.44/2.21 thf(f1149,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ c0)) != $true) | (((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true)) ) | (~spl2_27 | ~spl2_30)),
% 13.44/2.21 inference(forward_subsumption_resolution,[],[f1147,f887])).
% 13.44/2.21 thf(f1151,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true) | (((cNUMBER @ (cS @ c0))) != $true)) ) | (~spl2_27 | ~spl2_30)),
% 13.44/2.21 inference(forward_demodulation,[],[f1149,f499])).
% 13.44/2.21 thf(f1153,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ X0)) = $true)) ) | (~spl2_27 | ~spl2_30)),
% 13.44/2.21 inference(forward_subsumption_resolution,[],[f1151,f30])).
% 13.44/2.21 thf(f1155,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ (cS @ X0))) = $true)) ) | (~spl2_27 | ~spl2_30)),
% 13.44/2.21 inference(forward_demodulation,[],[f1153,f499])).
% 13.44/2.21 thf(f1157,plain,(
% 13.44/2.21 spl2_20 | ~spl2_27 | ~spl2_30),
% 13.44/2.21 inference(avatar_split_clause,[],[f1155,f847,f761,f657])).
% 13.44/2.21 thf(f1158,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((sF8 @ $i @ $i @ $o @ cNUMBER @ cS @ c0)) != $true) | (((cNUMBER @ (cS @ X0))) = $true) | (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) != $true)) ) | ~spl2_27),
% 13.44/2.21 inference(forward_demodulation,[],[f1147,f499])).
% 13.44/2.21 thf(f1160,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ (cS @ c0))) != $true) | (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) != $true) | (((cNUMBER @ (cS @ X0))) = $true)) ) | ~spl2_27),
% 13.44/2.21 inference(forward_demodulation,[],[f1158,f499])).
% 13.44/2.21 thf(f1162,plain,(
% 13.44/2.21 ( ! [X0 : $i] : ((((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) != $true) | (((cNUMBER @ (cS @ X0))) = $true)) ) | ~spl2_27),
% 13.44/2.21 inference(forward_subsumption_resolution,[],[f1160,f30])).
% 13.44/2.21 thf(f1164,definition,(
% 13.44/2.21 spl2_36 <=> (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true)),
% 13.44/2.21 introduced(definition,[new_symbols(definition,[spl2_36])],[avatar_definition])).
% 13.44/2.21 thf(f1166,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) != $true) | spl2_36),
% 13.44/2.21 inference(avatar_component_clause,[],[f1164])).
% 13.44/2.21 thf(f1168,plain,(
% 13.44/2.21 ~spl2_36 | spl2_20 | ~spl2_27),
% 13.44/2.21 inference(avatar_split_clause,[],[f1162,f761,f657,f1164])).
% 13.44/2.21 thf(f1169,plain,(
% 13.44/2.21 (((cEVEN @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ($true != $true) | ~spl2_31),
% 13.44/2.21 inference(constrained_superposition,[],[f20,f853])).
% 13.44/2.21 thf(f1171,plain,(
% 13.44/2.21 (((cEVEN @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ~spl2_31),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f1169])).
% 13.44/2.21 thf(f1250,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ($true != $true) | ~spl2_31),
% 13.44/2.21 inference(constrained_superposition,[],[f23,f1171])).
% 13.44/2.21 thf(f1252,plain,(
% 13.44/2.21 (((cNUMBER @ (cS @ (cS @ (sK1 @ cNUMBER @ (sF8 @ $i @ $i @ $o @ cNUMBER @ cS)))))) = $true) | ~spl2_31),
% 13.44/2.21 inference(trivial_inequality_removal,[],[f1250])).
% 13.44/2.21 thf(f1253,plain,(
% 13.44/2.21 $false | (~spl2_31 | spl2_36)),
% 13.44/2.21 inference(forward_subsumption_resolution,[],[f1252,f1166])).
% 13.44/2.21 thf(f1254,plain,(
% 13.44/2.21 ~spl2_31 | spl2_36),
% 13.44/2.21 inference(avatar_contradiction_clause,[],[f1253])).
% 13.44/2.21 cnf(s3, plain, ~spl2_3, inference(sat_conversion,[],[f81])).
% 13.44/2.21 cnf(s14, plain, spl2_19 | spl2_20, inference(sat_conversion,[],[f659])).
% 13.44/2.21 cnf(s20, plain, spl2_20 | spl2_27, inference(sat_conversion,[],[f763])).
% 13.44/2.21 cnf(s21, plain, spl2_3 | ~spl2_20, inference(sat_conversion,[],[f791])).
% 13.44/2.21 cnf(s25, plain, ~spl2_19 | spl2_30 | spl2_31, inference(sat_conversion,[],[f854])).
% 13.44/2.21 cnf(s29, plain, spl2_20 | ~spl2_27 | ~spl2_30, inference(sat_conversion,[],[f1157])).
% 13.44/2.21 cnf(s31, plain, spl2_20 | ~spl2_27 | ~spl2_36, inference(sat_conversion,[],[f1168])).
% 13.44/2.21 cnf(s37, plain, ~spl2_31 | spl2_36, inference(sat_conversion,[],[f1254])).
% 13.44/2.21 cnf(s38, plain, ~spl2_20, inference(rat,[],[s21,s3])).
% 13.44/2.21 cnf(s41, plain, spl2_27, inference(rat,[],[s20,s38])).
% 13.44/2.21 cnf(s43, plain, spl2_19, inference(rat,[],[s14,s38])).
% 13.44/2.21 cnf(s45, plain, ~spl2_36, inference(rat,[],[s31,s38,s41])).
% 13.44/2.21 cnf(s46, plain, ~spl2_30, inference(rat,[],[s29,s38,s41])).
% 13.44/2.21 cnf(s50, plain, ~spl2_31, inference(rat,[],[s37,s45])).
% 13.44/2.21 cnf(s51, plain, $false, inference(rat,[],[s25,s43,s50,s46])).
% 13.44/2.21 thf(f1255,plain,(
% 13.44/2.21 $false),
% 13.44/2.21 inference(avatar_sat_refutation,[],[s51])).
% 13.44/2.21 % SZS output end Proof for theBenchmark
% 13.44/2.21 % (2735941)------------------------------
% 13.44/2.21 % (2735941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.44/2.21 % (2735941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.21 % (2735941)CaDiCaL version: 2.1.3
% 13.44/2.21 % (2735941)Termination reason: Refutation
% 13.44/2.21 % (2735941)Time elapsed: 0.112 s
% 13.44/2.21 % (2735941)Peak memory usage: 13 MB
% 13.44/2.21 % (2735941)Instructions burned: 211 (million)
% 13.44/2.21 % (2735702)Success in time 1.969 s
% 13.44/2.21 % Vampire exiting
%------------------------------------------------------------------------------