%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV318^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 : n016.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:38:15 AM UTC 2026
% Result : Theorem 7.32s 1.46s
% Output : Refutation 7.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV318^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n016.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 15:41:28 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.07/0.24 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.75/0.37 % (493269)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.75/0.37 % (493279)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2327037113:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.75/0.37 % (493280)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.75/0.37 % (493280)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.75/0.37 % (493274)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2317850508:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.75/0.37 % (493275)lrs+10_16_si=on:nwc=1.5:random_seed=3421710133:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.75/0.37 % (493276)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=494057138:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.75/0.37 % (493280)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=1969208444:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.75/0.37 % (493278)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4110662728:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.75/0.37 % (493277)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=4123227665: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.75/0.37 % (493276)Instruction limit reached!
% 0.75/0.37 % (493276)------------------------------
% 0.75/0.37 % (493276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (493276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (493276)CaDiCaL version: 2.1.3
% 0.75/0.37 % (493276)Termination reason: Instruction limit
% 0.75/0.37 % (493276)Termination phase: Saturation
% 0.75/0.37 % (493276)Time elapsed: 0.003 s
% 0.75/0.37 % (493276)Peak memory usage: 12 MB
% 0.75/0.37 % (493276)Instructions burned: 4 (million)
% 0.75/0.37 % (493275)Instruction limit reached!
% 0.75/0.37 % (493275)------------------------------
% 0.75/0.37 % (493275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (493275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (493275)CaDiCaL version: 2.1.3
% 0.75/0.37 % (493275)Termination reason: Instruction limit
% 0.75/0.37 % (493275)Termination phase: Saturation
% 0.75/0.37 % (493275)Time elapsed: 0.012 s
% 0.75/0.37 % (493275)Peak memory usage: 12 MB
% 0.75/0.37 % (493275)Instructions burned: 19 (million)
% 0.75/0.37 % (493278)Instruction limit reached!
% 0.75/0.37 % (493278)------------------------------
% 0.75/0.37 % (493278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (493278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (493278)CaDiCaL version: 2.1.3
% 0.75/0.37 % (493278)Termination reason: Instruction limit
% 0.75/0.37 % (493278)Termination phase: Saturation
% 0.75/0.37 % (493278)Time elapsed: 0.014 s
% 0.75/0.37 % (493278)Peak memory usage: 12 MB
% 0.75/0.37 % (493278)Instructions burned: 24 (million)
% 0.75/0.37 % (493279)Instruction limit reached!
% 0.75/0.37 % (493279)------------------------------
% 0.75/0.37 % (493279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (493279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (493279)CaDiCaL version: 2.1.3
% 0.75/0.37 % (493279)Termination reason: Instruction limit
% 0.75/0.37 % (493279)Termination phase: Saturation
% 0.75/0.37 % (493279)Time elapsed: 0.022 s
% 0.75/0.37 % (493279)Peak memory usage: 12 MB
% 0.75/0.37 % (493279)Instructions burned: 76 (million)
% 0.75/0.37 % (493288)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=779674157:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.37 % (493290)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.75/0.37 % (493288)Instruction limit reached!
% 0.75/0.40 % (493288)------------------------------
% 0.75/0.40 % (493288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (493288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (493288)CaDiCaL version: 2.1.3
% 0.75/0.40 % (493288)Termination reason: Instruction limit
% 0.75/0.40 % (493288)Termination phase: Saturation
% 0.75/0.40 % (493288)Time elapsed: 0.002 s
% 0.75/0.40 % (493288)Peak memory usage: 12 MB
% 0.75/0.40 % (493288)Instructions burned: 2 (million)
% 0.75/0.40 % (493290)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2049945759:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.75/0.40 % (493290)Instruction limit reached!
% 0.75/0.40 % (493290)------------------------------
% 0.75/0.40 % (493290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (493290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (493290)CaDiCaL version: 2.1.3
% 0.75/0.40 % (493290)Termination reason: Instruction limit
% 0.75/0.41 % (493290)Termination phase: Saturation
% 0.75/0.41 % (493290)Time elapsed: 0.002 s
% 0.75/0.41 % (493290)Peak memory usage: 12 MB
% 0.75/0.41 % (493290)Instructions burned: 7 (million)
% 0.75/0.41 % (493289)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1543804160:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.75/0.41 % (493291)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2628413499:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.75/0.41 % (493289)Instruction limit reached!
% 0.75/0.41 % (493289)------------------------------
% 0.75/0.41 % (493289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.41 % (493289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.41 % (493289)CaDiCaL version: 2.1.3
% 0.75/0.41 % (493289)Termination reason: Instruction limit
% 0.75/0.41 % (493289)Termination phase: Saturation
% 0.75/0.41 % (493289)Time elapsed: 0.004 s
% 0.75/0.41 % (493289)Peak memory usage: 12 MB
% 0.75/0.41 % (493289)Instructions burned: 6 (million)
% 0.75/0.41 % (493295)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=2675714786:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.75/0.41 % (493294)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.75/0.41 % (493294)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.75/0.41 % (493291)Instruction limit reached!
% 0.75/0.41 % (493291)------------------------------
% 0.75/0.41 % (493291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.41 % (493291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.41 % (493291)CaDiCaL version: 2.1.3
% 0.75/0.41 % (493291)Termination reason: Instruction limit
% 0.75/0.41 % (493291)Termination phase: Saturation
% 0.75/0.41 % (493291)Time elapsed: 0.009 s
% 0.75/0.41 % (493291)Peak memory usage: 12 MB
% 0.75/0.41 % (493291)Instructions burned: 15 (million)
% 0.75/0.41 % (493294)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2827312210: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.75/0.41 % (493274)Instruction limit reached!
% 0.75/0.41 % (493274)------------------------------
% 0.75/0.41 % (493274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.41 % (493274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.41 % (493274)CaDiCaL version: 2.1.3
% 0.75/0.41 % (493274)Termination reason: Instruction limit
% 0.75/0.41 % (493274)Termination phase: Saturation
% 0.75/0.41 % (493274)Time elapsed: 0.047 s
% 0.75/0.41 % (493274)Peak memory usage: 12 MB
% 0.75/0.41 % (493274)Instructions burned: 88 (million)
% 0.75/0.41 % (493298)lrs+10_1_si=on:cs=on:random_seed=942920344:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.75/0.41 % (493294)Instruction limit reached!
% 0.75/0.41 % (493294)------------------------------
% 0.75/0.41 % (493294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (493294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (493294)CaDiCaL version: 2.1.3
% 0.75/0.44 % (493294)Termination reason: Instruction limit
% 0.75/0.44 % (493294)Termination phase: Saturation
% 0.75/0.44 % (493294)Time elapsed: 0.014 s
% 0.75/0.44 % (493294)Peak memory usage: 12 MB
% 0.75/0.44 % (493294)Instructions burned: 28 (million)
% 0.75/0.44 % (493301)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.75/0.44 % (493298)Instruction limit reached!
% 0.75/0.44 % (493298)------------------------------
% 0.75/0.44 % (493298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (493298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (493298)CaDiCaL version: 2.1.3
% 0.75/0.44 % (493298)Termination reason: Instruction limit
% 0.75/0.44 % (493298)Termination phase: Saturation
% 0.75/0.44 % (493298)Time elapsed: 0.005 s
% 0.75/0.44 % (493298)Peak memory usage: 12 MB
% 0.75/0.44 % (493298)Instructions burned: 8 (million)
% 0.75/0.44 % (493295)Instruction limit reached!
% 0.75/0.44 % (493295)------------------------------
% 0.75/0.44 % (493295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (493295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (493295)CaDiCaL version: 2.1.3
% 0.75/0.44 % (493295)Termination reason: Instruction limit
% 0.75/0.44 % (493295)Termination phase: Saturation
% 0.75/0.44 % (493295)Time elapsed: 0.023 s
% 0.75/0.44 % (493295)Peak memory usage: 12 MB
% 0.75/0.44 % (493295)Instructions burned: 86 (million)
% 0.75/0.44 % (493301)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=3537428438:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.44 % (493301)Instruction limit reached!
% 0.75/0.44 % (493301)------------------------------
% 0.75/0.44 % (493301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (493301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (493301)CaDiCaL version: 2.1.3
% 0.75/0.44 % (493301)Termination reason: Instruction limit
% 0.75/0.44 % (493301)Termination phase: Saturation
% 0.75/0.44 % (493301)Time elapsed: 0.001 s
% 0.75/0.44 % (493301)Peak memory usage: 11 MB
% 0.75/0.44 % (493301)Instructions burned: 2 (million)
% 0.75/0.44 % (493302)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1401540294:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.75/0.44 % (493306)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3266822498:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.75/0.44 % (493304)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2121875929:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.75/0.44 % (493306)Instruction limit reached!
% 0.75/0.44 % (493306)------------------------------
% 0.75/0.44 % (493306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (493306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (493306)CaDiCaL version: 2.1.3
% 0.75/0.44 % (493306)Termination reason: Instruction limit
% 0.75/0.44 % (493306)Termination phase: Saturation
% 0.75/0.44 % (493306)Time elapsed: 0.005 s
% 0.75/0.44 % (493306)Peak memory usage: 12 MB
% 0.75/0.44 % (493306)Instructions burned: 16 (million)
% 0.75/0.44 % (493305)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2382859840:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.75/0.44 % (493280)Instruction limit reached!
% 0.75/0.44 % (493280)------------------------------
% 0.75/0.44 % (493280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (493280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (493280)CaDiCaL version: 2.1.3
% 0.75/0.44 % (493280)Termination reason: Instruction limit
% 0.75/0.44 % (493280)Termination phase: Saturation
% 0.75/0.44 % (493280)Time elapsed: 0.080 s
% 0.75/0.44 % (493280)Peak memory usage: 12 MB
% 0.75/0.44 % (493280)Instructions burned: 158 (million)
% 0.75/0.44 % (493308)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1037892662:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 1.49/0.49 % (493302)Instruction limit reached!
% 1.49/0.49 % (493302)------------------------------
% 1.49/0.49 % (493302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.49 % (493302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.49 % (493302)CaDiCaL version: 2.1.3
% 1.49/0.49 % (493302)Termination reason: Instruction limit
% 1.49/0.49 % (493302)Termination phase: Saturation
% 1.49/0.49 % (493302)Time elapsed: 0.021 s
% 1.49/0.49 % (493302)Peak memory usage: 12 MB
% 1.49/0.49 % (493302)Instructions burned: 38 (million)
% 1.49/0.49 % (493312)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1525079217:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.49/0.49 % (493312)Instruction limit reached!
% 1.49/0.49 % (493312)------------------------------
% 1.49/0.49 % (493312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.49 % (493312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.49 % (493312)CaDiCaL version: 2.1.3
% 1.49/0.49 % (493312)Termination reason: Instruction limit
% 1.49/0.49 % (493312)Termination phase: Saturation
% 1.49/0.49 % (493312)Time elapsed: 0.005 s
% 1.49/0.49 % (493312)Peak memory usage: 12 MB
% 1.49/0.49 % (493312)Instructions burned: 16 (million)
% 1.49/0.49 % (493305)Instruction limit reached!
% 1.49/0.49 % (493305)------------------------------
% 1.49/0.49 % (493305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.49 % (493305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.49 % (493305)CaDiCaL version: 2.1.3
% 1.49/0.49 % (493305)Termination reason: Instruction limit
% 1.49/0.49 % (493305)Termination phase: Saturation
% 1.49/0.49 % (493305)Time elapsed: 0.015 s
% 1.49/0.49 % (493305)Peak memory usage: 12 MB
% 1.49/0.49 % (493305)Instructions burned: 26 (million)
% 1.49/0.49 % (493314)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1700561851: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)
% 1.49/0.49 % (493314)Instruction limit reached!
% 1.49/0.49 % (493314)------------------------------
% 1.49/0.49 % (493314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.49 % (493314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.49 % (493314)CaDiCaL version: 2.1.3
% 1.49/0.49 % (493314)Termination reason: Instruction limit
% 1.49/0.49 % (493314)Termination phase: Saturation
% 1.49/0.49 % (493314)Time elapsed: 0.002 s
% 1.49/0.49 % (493314)Peak memory usage: 12 MB
% 1.49/0.49 % (493314)Instructions burned: 3 (million)
% 1.49/0.49 % (493318)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3742904990:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.49/0.49 % (493316)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2914233750:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.49/0.49 % (493318)Instruction limit reached!
% 1.49/0.49 % (493318)------------------------------
% 1.49/0.49 % (493318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.49 % (493318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.49 % (493318)CaDiCaL version: 2.1.3
% 1.49/0.49 % (493318)Termination reason: Instruction limit
% 1.49/0.49 % (493318)Termination phase: Saturation
% 1.49/0.49 % (493318)Time elapsed: 0.007 s
% 1.49/0.49 % (493318)Peak memory usage: 11 MB
% 1.49/0.49 % (493318)Instructions burned: 25 (million)
% 1.49/0.49 % (493319)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1115609541:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.49/0.49 % (493321)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.49/0.49 % (493321)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.49/0.49 % (493321)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=2886822233:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.49/0.56 % (493324)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.49/0.56 % (493316)Instruction limit reached!
% 1.49/0.56 % (493316)------------------------------
% 1.49/0.56 % (493316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.56 % (493316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.56 % (493316)CaDiCaL version: 2.1.3
% 1.49/0.56 % (493316)Termination reason: Instruction limit
% 1.49/0.56 % (493316)Termination phase: Saturation
% 1.49/0.56 % (493316)Time elapsed: 0.015 s
% 1.49/0.56 % (493316)Peak memory usage: 12 MB
% 1.49/0.56 % (493316)Instructions burned: 27 (million)
% 1.49/0.56 % (493324)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=2677178584:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.49/0.56 % (493324)Instruction limit reached!
% 1.49/0.56 % (493324)------------------------------
% 1.49/0.56 % (493324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.56 % (493324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.56 % (493324)CaDiCaL version: 2.1.3
% 1.49/0.56 % (493324)Termination reason: Instruction limit
% 1.49/0.56 % (493324)Termination phase: Saturation
% 1.49/0.56 % (493324)Time elapsed: 0.003 s
% 1.49/0.56 % (493324)Peak memory usage: 12 MB
% 1.49/0.56 % (493324)Instructions burned: 9 (million)
% 1.49/0.56 % (493321)Instruction limit reached!
% 1.49/0.56 % (493321)------------------------------
% 1.49/0.56 % (493321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.56 % (493321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.56 % (493321)CaDiCaL version: 2.1.3
% 1.49/0.56 % (493321)Termination reason: Instruction limit
% 1.49/0.56 % (493321)Termination phase: Saturation
% 1.49/0.56 % (493321)Time elapsed: 0.009 s
% 1.49/0.56 % (493321)Peak memory usage: 12 MB
% 1.49/0.56 % (493321)Instructions burned: 15 (million)
% 1.49/0.56 % (493329)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3364538388:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.49/0.56 % (493329)Instruction limit reached!
% 1.49/0.56 % (493329)------------------------------
% 1.49/0.56 % (493329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.56 % (493329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.56 % (493329)CaDiCaL version: 2.1.3
% 1.49/0.56 % (493329)Termination reason: Instruction limit
% 1.49/0.56 % (493329)Termination phase: Saturation
% 1.49/0.56 % (493329)Time elapsed: 0.003 s
% 1.49/0.56 % (493329)Peak memory usage: 12 MB
% 1.49/0.56 % (493329)Instructions burned: 9 (million)
% 1.49/0.56 % (493327)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=1137258744:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.49/0.56 % (493319)Instruction limit reached!
% 1.49/0.56 % (493319)------------------------------
% 1.49/0.56 % (493319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.56 % (493319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.56 % (493319)CaDiCaL version: 2.1.3
% 1.49/0.56 % (493319)Termination reason: Instruction limit
% 1.49/0.56 % (493319)Termination phase: Saturation
% 1.49/0.56 % (493319)Time elapsed: 0.032 s
% 1.49/0.56 % (493319)Peak memory usage: 12 MB
% 1.49/0.56 % (493319)Instructions burned: 60 (million)
% 1.49/0.56 % (493330)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4023300350:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.49/0.56 % (493333)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3594165940:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.49/0.56 % (493327)Instruction limit reached!
% 1.49/0.56 % (493327)------------------------------
% 1.49/0.56 % (493327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.49/0.56 % (493327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.49/0.56 % (493327)CaDiCaL version: 2.1.3
% 1.49/0.56 % (493327)Termination reason: Instruction limit
% 1.49/0.56 % (493327)Termination phase: Saturation
% 1.49/0.56 % (493327)Time elapsed: 0.016 s
% 1.49/0.56 % (493327)Peak memory usage: 12 MB
% 2.15/0.61 % (493327)Instructions burned: 32 (million)
% 2.15/0.61 % (493330)Instruction limit reached!
% 2.15/0.61 % (493330)------------------------------
% 2.15/0.61 % (493330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.61 % (493330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.61 % (493330)CaDiCaL version: 2.1.3
% 2.15/0.61 % (493330)Termination reason: Instruction limit
% 2.15/0.61 % (493330)Termination phase: Saturation
% 2.15/0.61 % (493330)Time elapsed: 0.010 s
% 2.15/0.61 % (493330)Peak memory usage: 11 MB
% 2.15/0.61 % (493330)Instructions burned: 25 (million)
% 2.15/0.61 % (493333)Instruction limit reached!
% 2.15/0.61 % (493333)------------------------------
% 2.15/0.61 % (493333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.61 % (493333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.61 % (493333)CaDiCaL version: 2.1.3
% 2.15/0.61 % (493333)Termination reason: Instruction limit
% 2.15/0.61 % (493333)Termination phase: Saturation
% 2.15/0.61 % (493333)Time elapsed: 0.007 s
% 2.15/0.61 % (493333)Peak memory usage: 12 MB
% 2.15/0.62 % (493333)Instructions burned: 22 (million)
% 2.15/0.62 % (493334)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=110396085:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.15/0.62 % (493339)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4002980110:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.15/0.62 % (493337)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=258947805:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.15/0.62 % (493338)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3970463303:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.15/0.62 % (493339)Instruction limit reached!
% 2.15/0.62 % (493339)------------------------------
% 2.15/0.62 % (493339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (493339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (493339)CaDiCaL version: 2.1.3
% 2.15/0.62 % (493339)Termination reason: Instruction limit
% 2.15/0.62 % (493339)Termination phase: Saturation
% 2.15/0.62 % (493339)Time elapsed: 0.012 s
% 2.15/0.62 % (493339)Peak memory usage: 12 MB
% 2.15/0.62 % (493339)Instructions burned: 42 (million)
% 2.15/0.62 % (493344)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.15/0.62 % (493344)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=185911419:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.15/0.62 % (493344)Instruction limit reached!
% 2.15/0.62 % (493344)------------------------------
% 2.15/0.62 % (493344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (493344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (493344)CaDiCaL version: 2.1.3
% 2.15/0.62 % (493344)Termination reason: Instruction limit
% 2.15/0.62 % (493344)Termination phase: Saturation
% 2.15/0.62 % (493344)Time elapsed: 0.002 s
% 2.15/0.62 % (493344)Peak memory usage: 12 MB
% 2.15/0.62 % (493344)Instructions burned: 7 (million)
% 2.15/0.62 % (493304)Instruction limit reached!
% 2.15/0.62 % (493304)------------------------------
% 2.15/0.62 % (493304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (493277)Instruction limit reached!
% 2.15/0.62 % (493277)------------------------------
% 2.15/0.62 % (493277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.15/0.62 % (493277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (493277)CaDiCaL version: 2.1.3
% 2.15/0.62 % (493277)Termination reason: Instruction limit
% 2.15/0.62 % (493277)Termination phase: Saturation
% 2.15/0.62 % (493277)Time elapsed: 0.204 s
% 2.15/0.62 % (493277)Peak memory usage: 12 MB
% 2.15/0.62 % (493277)Instructions burned: 634 (million)
% 2.15/0.62 % (493304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.15/0.62 % (493304)CaDiCaL version: 2.1.3
% 2.15/0.62 % (493304)Termination reason: Instruction limit
% 2.15/0.62 % (493304)Termination phase: Saturation
% 2.15/0.62 % (493304)Time elapsed: 0.127 s
% 2.15/0.62 % (493304)Peak memory usage: 13 MB
% 2.40/0.68 % (493304)Instructions burned: 250 (million)
% 2.40/0.68 % (493346)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2503542335:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.40/0.68 % (493348)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.40/0.68 % (493348)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1480860570: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.40/0.68 % (493347)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=3767874305: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.40/0.68 % (493348)Instruction limit reached!
% 2.40/0.68 % (493348)------------------------------
% 2.40/0.68 % (493348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.68 % (493348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.68 % (493348)CaDiCaL version: 2.1.3
% 2.40/0.68 % (493348)Termination reason: Instruction limit
% 2.40/0.68 % (493348)Termination phase: Saturation
% 2.40/0.68 % (493348)Time elapsed: 0.004 s
% 2.40/0.68 % (493348)Peak memory usage: 12 MB
% 2.40/0.68 % (493348)Instructions burned: 8 (million)
% 2.40/0.68 % (493308)Instruction limit reached!
% 2.40/0.68 % (493308)------------------------------
% 2.40/0.68 % (493308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.68 % (493308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.68 % (493308)CaDiCaL version: 2.1.3
% 2.40/0.68 % (493308)Termination reason: Instruction limit
% 2.40/0.68 % (493308)Termination phase: Saturation
% 2.40/0.68 % (493308)Time elapsed: 0.158 s
% 2.40/0.68 % (493308)Peak memory usage: 13 MB
% 2.40/0.68 % (493308)Instructions burned: 327 (million)
% 2.40/0.68 % (493352)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1249064261:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.40/0.68 % (493337)Instruction limit reached!
% 2.40/0.68 % (493337)------------------------------
% 2.40/0.68 % (493337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.68 % (493337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.68 % (493337)CaDiCaL version: 2.1.3
% 2.40/0.68 % (493337)Termination reason: Instruction limit
% 2.40/0.68 % (493337)Termination phase: Saturation
% 2.40/0.68 % (493337)Time elapsed: 0.075 s
% 2.40/0.68 % (493337)Peak memory usage: 13 MB
% 2.40/0.68 % (493337)Instructions burned: 145 (million)
% 2.40/0.68 % (493352)Instruction limit reached!
% 2.40/0.68 % (493352)------------------------------
% 2.40/0.68 % (493352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.68 % (493352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.68 % (493352)CaDiCaL version: 2.1.3
% 2.40/0.68 % (493352)Termination reason: Instruction limit
% 2.40/0.68 % (493352)Termination phase: Saturation
% 2.40/0.68 % (493352)Time elapsed: 0.012 s
% 2.40/0.68 % (493352)Peak memory usage: 12 MB
% 2.40/0.68 % (493352)Instructions burned: 23 (million)
% 2.40/0.68 % (493346)Instruction limit reached!
% 2.40/0.68 % (493346)------------------------------
% 2.40/0.68 % (493346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.68 % (493353)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=800292031:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.40/0.68 % (493346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.68 % (493346)CaDiCaL version: 2.1.3
% 2.40/0.68 % (493346)Termination reason: Instruction limit
% 2.40/0.68 % (493346)Termination phase: Saturation
% 2.40/0.68 % (493346)Time elapsed: 0.050 s
% 2.40/0.68 % (493346)Peak memory usage: 13 MB
% 2.40/0.68 % (493346)Instructions burned: 185 (million)
% 2.40/0.68 % (493355)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=3754826337:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.40/0.68 % (493358)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=2583003581: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.22/0.83 % (493353)Instruction limit reached!
% 3.22/0.83 % (493353)------------------------------
% 3.22/0.83 % (493353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.22/0.83 % (493353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/0.83 % (493353)CaDiCaL version: 2.1.3
% 3.22/0.83 % (493353)Termination reason: Instruction limit
% 3.22/0.83 % (493353)Termination phase: Saturation
% 3.22/0.83 % (493353)Time elapsed: 0.011 s
% 3.22/0.83 % (493353)Peak memory usage: 12 MB
% 3.22/0.83 % (493353)Instructions burned: 19 (million)
% 3.22/0.83 % (493356)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=2684968271: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.22/0.83 % (493338)Instruction limit reached!
% 3.22/0.83 % (493338)------------------------------
% 3.22/0.83 % (493338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.22/0.83 % (493338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/0.83 % (493338)CaDiCaL version: 2.1.3
% 3.22/0.83 % (493338)Termination reason: Instruction limit
% 3.22/0.83 % (493338)Termination phase: Saturation
% 3.22/0.83 % (493338)Time elapsed: 0.102 s
% 3.22/0.83 % (493338)Peak memory usage: 13 MB
% 3.22/0.83 % (493338)Instructions burned: 195 (million)
% 3.22/0.83 % (493358)Instruction limit reached!
% 3.22/0.83 % (493358)------------------------------
% 3.22/0.83 % (493358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.22/0.83 % (493358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/0.83 % (493358)CaDiCaL version: 2.1.3
% 3.22/0.83 % (493358)Termination reason: Instruction limit
% 3.22/0.83 % (493358)Termination phase: Saturation
% 3.22/0.83 % (493358)Time elapsed: 0.014 s
% 3.22/0.83 % (493358)Peak memory usage: 12 MB
% 3.22/0.83 % (493358)Instructions burned: 45 (million)
% 3.22/0.83 % (493361)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2449522461:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.22/0.83 % (493364)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.22/0.83 % (493364)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2677486749:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.22/0.83 % (493363)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3216648284:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.22/0.83 % (493347)Instruction limit reached!
% 3.22/0.83 % (493347)------------------------------
% 3.22/0.83 % (493347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.22/0.83 % (493347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/0.83 % (493347)CaDiCaL version: 2.1.3
% 3.22/0.83 % (493347)Termination reason: Instruction limit
% 3.22/0.83 % (493347)Termination phase: Saturation
% 3.22/0.83 % (493347)Time elapsed: 0.079 s
% 3.22/0.83 % (493347)Peak memory usage: 13 MB
% 3.22/0.83 % (493347)Instructions burned: 169 (million)
% 3.22/0.83 % (493363)Instruction limit reached!
% 3.22/0.83 % (493363)------------------------------
% 3.22/0.83 % (493363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.22/0.83 % (493363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/0.83 % (493363)CaDiCaL version: 2.1.3
% 3.22/0.83 % (493363)Termination reason: Instruction limit
% 3.22/0.83 % (493363)Termination phase: Saturation
% 3.22/0.83 % (493363)Time elapsed: 0.013 s
% 3.22/0.83 % (493363)Peak memory usage: 12 MB
% 3.22/0.83 % (493363)Instructions burned: 22 (million)
% 3.22/0.83 % (493368)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=608717741:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.22/0.83 % (493369)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=2683939941:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.73/1.00 % (493368)Instruction limit reached!
% 3.73/1.00 % (493368)------------------------------
% 3.73/1.00 % (493368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/1.00 % (493368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.00 % (493368)CaDiCaL version: 2.1.3
% 3.73/1.00 % (493368)Termination reason: Instruction limit
% 3.73/1.00 % (493368)Termination phase: Saturation
% 3.73/1.00 % (493368)Time elapsed: 0.009 s
% 3.73/1.00 % (493368)Peak memory usage: 12 MB
% 3.73/1.00 % (493368)Instructions burned: 14 (million)
% 3.73/1.00 % (493364)Instruction limit reached!
% 3.73/1.00 % (493364)------------------------------
% 3.73/1.00 % (493364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/1.00 % (493364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.00 % (493364)CaDiCaL version: 2.1.3
% 3.73/1.00 % (493364)Termination reason: Instruction limit
% 3.73/1.00 % (493364)Termination phase: Saturation
% 3.73/1.00 % (493364)Time elapsed: 0.052 s
% 3.73/1.00 % (493364)Peak memory usage: 12 MB
% 3.73/1.00 % (493364)Instructions burned: 202 (million)
% 3.73/1.00 % (493372)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=4145617321:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.73/1.00 % (493373)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=4040708789:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.73/1.00 % (493369)Instruction limit reached!
% 3.73/1.00 % (493369)------------------------------
% 3.73/1.00 % (493369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/1.00 % (493369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.00 % (493369)CaDiCaL version: 2.1.3
% 3.73/1.00 % (493369)Termination reason: Instruction limit
% 3.73/1.00 % (493369)Termination phase: Saturation
% 3.73/1.00 % (493369)Time elapsed: 0.037 s
% 3.73/1.00 % (493369)Peak memory usage: 13 MB
% 3.73/1.00 % (493369)Instructions burned: 66 (million)
% 3.73/1.00 % (493373)Instruction limit reached!
% 3.73/1.00 % (493373)------------------------------
% 3.73/1.00 % (493373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/1.00 % (493373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.00 % (493373)CaDiCaL version: 2.1.3
% 3.73/1.00 % (493373)Termination reason: Instruction limit
% 3.73/1.00 % (493373)Termination phase: Saturation
% 3.73/1.00 % (493373)Time elapsed: 0.008 s
% 3.73/1.00 % (493373)Peak memory usage: 12 MB
% 3.73/1.00 % (493373)Instructions burned: 31 (million)
% 3.73/1.00 % (493372)Instruction limit reached!
% 3.73/1.00 % (493372)------------------------------
% 3.73/1.00 % (493372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/1.00 % (493372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.00 % (493372)CaDiCaL version: 2.1.3
% 3.73/1.00 % (493372)Termination reason: Instruction limit
% 3.73/1.00 % (493372)Termination phase: Saturation
% 3.73/1.00 % (493372)Time elapsed: 0.028 s
% 3.73/1.00 % (493372)Peak memory usage: 12 MB
% 3.73/1.00 % (493372)Instructions burned: 52 (million)
% 3.73/1.00 % (493377)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=3209236617:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.73/1.00 % (493376)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=156012511:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.73/1.00 % (493377)Instruction limit reached!
% 3.73/1.00 % (493377)------------------------------
% 3.73/1.00 % (493377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.73/1.00 % (493377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.00 % (493377)CaDiCaL version: 2.1.3
% 3.73/1.00 % (493377)Termination reason: Instruction limit
% 3.73/1.00 % (493377)Termination phase: Saturation
% 3.73/1.00 % (493377)Time elapsed: 0.009 s
% 3.73/1.00 % (493377)Peak memory usage: 12 MB
% 3.73/1.00 % (493377)Instructions burned: 34 (million)
% 3.73/1.00 % (493379)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2291301577:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.73/1.00 % (493381)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.48/1.09 % (493381)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=2743669467:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.48/1.09 % (493379)Instruction limit reached!
% 5.48/1.09 % (493379)------------------------------
% 5.48/1.09 % (493379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.48/1.09 % (493379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.09 % (493379)CaDiCaL version: 2.1.3
% 5.48/1.09 % (493379)Termination reason: Instruction limit
% 5.48/1.09 % (493379)Termination phase: Saturation
% 5.48/1.09 % (493379)Time elapsed: 0.036 s
% 5.48/1.09 % (493379)Peak memory usage: 12 MB
% 5.48/1.09 % (493379)Instructions burned: 68 (million)
% 5.48/1.09 % (493355)Instruction limit reached!
% 5.48/1.09 % (493355)------------------------------
% 5.48/1.09 % (493355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.48/1.09 % (493355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.09 % (493355)CaDiCaL version: 2.1.3
% 5.48/1.09 % (493355)Termination reason: Instruction limit
% 5.48/1.09 % (493355)Termination phase: Saturation
% 5.48/1.09 % (493355)Time elapsed: 0.166 s
% 5.48/1.09 % (493355)Peak memory usage: 14 MB
% 5.48/1.09 % (493355)Instructions burned: 316 (million)
% 5.48/1.09 % (493376)Instruction limit reached!
% 5.48/1.09 % (493376)------------------------------
% 5.48/1.09 % (493376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.48/1.09 % (493376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.09 % (493376)CaDiCaL version: 2.1.3
% 5.48/1.09 % (493376)Termination reason: Instruction limit
% 5.48/1.09 % (493376)Termination phase: Saturation
% 5.48/1.09 % (493376)Time elapsed: 0.057 s
% 5.48/1.09 % (493376)Peak memory usage: 12 MB
% 5.48/1.09 % (493376)Instructions burned: 139 (million)
% 5.48/1.09 % (493381)Instruction limit reached!
% 5.48/1.09 % (493381)------------------------------
% 5.48/1.09 % (493381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.48/1.09 % (493381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.09 % (493381)CaDiCaL version: 2.1.3
% 5.48/1.09 % (493381)Termination reason: Instruction limit
% 5.48/1.09 % (493381)Termination phase: Saturation
% 5.48/1.09 % (493381)Time elapsed: 0.045 s
% 5.48/1.09 % (493381)Peak memory usage: 14 MB
% 5.48/1.09 % (493381)Instructions burned: 184 (million)
% 5.48/1.09 % (493384)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1847095758:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.48/1.09 % (493387)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1477956467:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.48/1.09 % (493385)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3514993238:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.48/1.09 % (493386)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1508707837:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 5.48/1.09 % (493385)Instruction limit reached!
% 5.48/1.09 % (493385)------------------------------
% 5.48/1.09 % (493385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.48/1.09 % (493385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.09 % (493385)CaDiCaL version: 2.1.3
% 5.48/1.09 % (493385)Termination reason: Instruction limit
% 5.48/1.09 % (493385)Termination phase: Saturation
% 5.48/1.09 % (493385)Time elapsed: 0.051 s
% 5.48/1.09 % (493385)Peak memory usage: 12 MB
% 5.48/1.09 % (493385)Instructions burned: 97 (million)
% 5.48/1.09 % (493392)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=4027644062:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.48/1.09 % (493361)Instruction limit reached!
% 5.48/1.09 % (493361)------------------------------
% 5.48/1.09 % (493361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.48/1.09 % (493361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.48/1.09 % (493361)CaDiCaL version: 2.1.3
% 5.48/1.09 % (493361)Termination reason: Instruction limit
% 5.48/1.09 % (493361)Termination phase: Saturation
% 5.48/1.09 % (493361)Time elapsed: 0.238 s
% 5.48/1.09 % (493361)Peak memory usage: 13 MB
% 5.48/1.09 % (493361)Instructions burned: 482 (million)
% 5.48/1.09 % (493394)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1268033023:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.85/1.19 % (493384)Instruction limit reached!
% 5.85/1.19 % (493384)------------------------------
% 5.85/1.19 % (493384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.19 % (493384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.19 % (493384)CaDiCaL version: 2.1.3
% 5.85/1.19 % (493384)Termination reason: Instruction limit
% 5.85/1.19 % (493384)Termination phase: Saturation
% 5.85/1.19 % (493384)Time elapsed: 0.125 s
% 5.85/1.19 % (493384)Peak memory usage: 12 MB
% 5.85/1.19 % (493384)Instructions burned: 248 (million)
% 5.85/1.19 % (493396)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=557013977:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 5.85/1.19 % (493394)Instruction limit reached!
% 5.85/1.19 % (493394)------------------------------
% 5.85/1.19 % (493394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.19 % (493394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.19 % (493394)CaDiCaL version: 2.1.3
% 5.85/1.19 % (493394)Termination reason: Instruction limit
% 5.85/1.19 % (493394)Termination phase: Saturation
% 5.85/1.19 % (493394)Time elapsed: 0.067 s
% 5.85/1.19 % (493394)Peak memory usage: 12 MB
% 5.85/1.19 % (493394)Instructions burned: 130 (million)
% 5.85/1.19 % (493396)Instruction limit reached!
% 5.85/1.19 % (493396)------------------------------
% 5.85/1.19 % (493396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.19 % (493396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.19 % (493396)CaDiCaL version: 2.1.3
% 5.85/1.19 % (493396)Termination reason: Instruction limit
% 5.85/1.19 % (493396)Termination phase: Saturation
% 5.85/1.19 % (493396)Time elapsed: 0.024 s
% 5.85/1.19 % (493396)Peak memory usage: 12 MB
% 5.85/1.19 % (493396)Instructions burned: 44 (million)
% 5.85/1.19 % (493398)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=91495945:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 5.85/1.19 % (493399)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=508479909:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 5.85/1.19 % (493387)Instruction limit reached!
% 5.85/1.19 % (493387)------------------------------
% 5.85/1.19 % (493387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.19 % (493387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.19 % (493387)CaDiCaL version: 2.1.3
% 5.85/1.19 % (493387)Termination reason: Instruction limit
% 5.85/1.19 % (493387)Termination phase: Saturation
% 5.85/1.19 % (493387)Time elapsed: 0.223 s
% 5.85/1.19 % (493387)Peak memory usage: 14 MB
% 5.85/1.19 % (493387)Instructions burned: 875 (million)
% 5.85/1.19 % (493386)Instruction limit reached!
% 5.85/1.19 % (493386)------------------------------
% 5.85/1.19 % (493386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.19 % (493386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.19 % (493386)CaDiCaL version: 2.1.3
% 5.85/1.19 % (493386)Termination reason: Instruction limit
% 5.85/1.19 % (493386)Termination phase: Saturation
% 5.85/1.19 % (493386)Time elapsed: 0.217 s
% 5.85/1.19 % (493386)Peak memory usage: 14 MB
% 5.85/1.19 % (493386)Instructions burned: 429 (million)
% 5.85/1.19 % (493402)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=137466807:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 5.85/1.19 % (493356)Instruction limit reached!
% 5.85/1.19 % (493356)------------------------------
% 5.85/1.19 % (493356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.85/1.19 % (493356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.19 % (493356)CaDiCaL version: 2.1.3
% 5.85/1.19 % (493356)Termination reason: Instruction limit
% 5.85/1.19 % (493356)Termination phase: Saturation
% 5.85/1.19 % (493356)Time elapsed: 0.420 s
% 5.85/1.19 % (493356)Peak memory usage: 15 MB
% 5.85/1.19 % (493356)Instructions burned: 855 (million)
% 5.85/1.19 % (493403)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=1756934363:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 5.85/1.19 % (493406)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=3321257159: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_2992 on theBenchmark for (2992ds/105Mi)
% 6.46/1.34 % (493402)Instruction limit reached!
% 6.46/1.34 % (493402)------------------------------
% 6.46/1.34 % (493402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.34 % (493402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.34 % (493402)CaDiCaL version: 2.1.3
% 6.46/1.34 % (493402)Termination reason: Instruction limit
% 6.46/1.34 % (493402)Termination phase: Saturation
% 6.46/1.34 % (493402)Time elapsed: 0.029 s
% 6.46/1.34 % (493402)Peak memory usage: 12 MB
% 6.46/1.34 % (493402)Instructions burned: 96 (million)
% 6.46/1.34 % (493408)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=3021465669:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.46/1.34 % (493403)Instruction limit reached!
% 6.46/1.34 % (493403)------------------------------
% 6.46/1.34 % (493403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.34 % (493403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.34 % (493403)CaDiCaL version: 2.1.3
% 6.46/1.34 % (493403)Termination reason: Instruction limit
% 6.46/1.34 % (493403)Termination phase: Saturation
% 6.46/1.34 % (493403)Time elapsed: 0.035 s
% 6.46/1.34 % (493403)Peak memory usage: 12 MB
% 6.46/1.34 % (493403)Instructions burned: 65 (million)
% 6.46/1.34 % (493334)Instruction limit reached!
% 6.46/1.34 % (493334)------------------------------
% 6.46/1.34 % (493334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.34 % (493334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.34 % (493334)CaDiCaL version: 2.1.3
% 6.46/1.34 % (493334)Termination reason: Instruction limit
% 6.46/1.34 % (493334)Termination phase: Saturation
% 6.46/1.34 % (493334)Time elapsed: 0.584 s
% 6.46/1.34 % (493334)Peak memory usage: 14 MB
% 6.46/1.34 % (493334)Instructions burned: 1240 (million)
% 6.46/1.34 % (493410)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=2433747976:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.46/1.34 % (493411)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3934929115:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.46/1.34 % (493406)Instruction limit reached!
% 6.46/1.34 % (493406)------------------------------
% 6.46/1.34 % (493406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.34 % (493406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.34 % (493406)CaDiCaL version: 2.1.3
% 6.46/1.34 % (493406)Termination reason: Instruction limit
% 6.46/1.34 % (493406)Termination phase: Saturation
% 6.46/1.34 % (493406)Time elapsed: 0.053 s
% 6.46/1.34 % (493406)Peak memory usage: 13 MB
% 6.46/1.34 % (493406)Instructions burned: 106 (million)
% 6.46/1.34 % (493392)Instruction limit reached!
% 6.46/1.34 % (493392)------------------------------
% 6.46/1.34 % (493392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.34 % (493392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.46/1.34 % (493392)CaDiCaL version: 2.1.3
% 6.46/1.34 % (493392)Termination reason: Instruction limit
% 6.46/1.34 % (493392)Termination phase: Saturation
% 6.46/1.34 % (493392)Time elapsed: 0.249 s
% 6.46/1.34 % (493392)Peak memory usage: 14 MB
% 6.46/1.34 % (493392)Instructions burned: 515 (million)
% 6.46/1.34 % (493414)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=3374729887:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 6.46/1.34 % (493415)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1646082470:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 6.46/1.34 % (493414)Instruction limit reached!
% 6.46/1.34 % (493414)------------------------------
% 6.46/1.34 % (493414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.46/1.34 % (493414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493414)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493414)Termination reason: Instruction limit
% 7.32/1.46 % (493414)Termination phase: Saturation
% 7.32/1.46 % (493414)Time elapsed: 0.018 s
% 7.32/1.46 % (493414)Peak memory usage: 12 MB
% 7.32/1.46 % (493414)Instructions burned: 34 (million)
% 7.32/1.46 % (493418)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=2923206148:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 7.32/1.46 % (493415)Instruction limit reached!
% 7.32/1.46 % (493415)------------------------------
% 7.32/1.46 % (493415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493415)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493415)Termination reason: Instruction limit
% 7.32/1.46 % (493415)Termination phase: Saturation
% 7.32/1.46 % (493415)Time elapsed: 0.047 s
% 7.32/1.46 % (493415)Peak memory usage: 12 MB
% 7.32/1.46 % (493415)Instructions burned: 91 (million)
% 7.32/1.46 % (493420)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1878642997:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 7.32/1.46 % (493399)Instruction limit reached!
% 7.32/1.46 % (493399)------------------------------
% 7.32/1.46 % (493399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493399)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493399)Termination reason: Instruction limit
% 7.32/1.46 % (493399)Termination phase: Saturation
% 7.32/1.46 % (493399)Time elapsed: 0.219 s
% 7.32/1.46 % (493399)Peak memory usage: 13 MB
% 7.32/1.46 % (493399)Instructions burned: 451 (million)
% 7.32/1.46 % (493418)Instruction limit reached!
% 7.32/1.46 % (493418)------------------------------
% 7.32/1.46 % (493418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493418)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493418)Termination reason: Instruction limit
% 7.32/1.46 % (493418)Termination phase: Saturation
% 7.32/1.46 % (493418)Time elapsed: 0.035 s
% 7.32/1.46 % (493418)Peak memory usage: 12 MB
% 7.32/1.46 % (493418)Instructions burned: 66 (million)
% 7.32/1.46 % (493420)Instruction limit reached!
% 7.32/1.46 % (493420)------------------------------
% 7.32/1.46 % (493420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493420)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493420)Termination reason: Instruction limit
% 7.32/1.46 % (493420)Termination phase: Saturation
% 7.32/1.46 % (493420)Time elapsed: 0.012 s
% 7.32/1.46 % (493420)Peak memory usage: 12 MB
% 7.32/1.46 % (493420)Instructions burned: 24 (million)
% 7.32/1.46 % (493422)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=1783350396:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 7.32/1.46 % (493423)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1295896293:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 7.32/1.46 % (493424)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.32/1.46 % (493424)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3527701490:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2990 on theBenchmark for (2990ds/137Mi)
% 7.32/1.46 % (493423)Instruction limit reached!
% 7.32/1.46 % (493423)------------------------------
% 7.32/1.46 % (493423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493423)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493423)Termination reason: Instruction limit
% 7.32/1.46 % (493423)Termination phase: Saturation
% 7.32/1.46 % (493423)Time elapsed: 0.017 s
% 7.32/1.46 % (493423)Peak memory usage: 12 MB
% 7.32/1.46 % (493423)Instructions burned: 28 (million)
% 7.32/1.46 % (493398)Instruction limit reached!
% 7.32/1.46 % (493398)------------------------------
% 7.32/1.46 % (493398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493398)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493398)Termination reason: Instruction limit
% 7.32/1.46 % (493398)Termination phase: Saturation
% 7.32/1.46 % (493398)Time elapsed: 0.273 s
% 7.32/1.46 % (493398)Peak memory usage: 14 MB
% 7.32/1.46 % (493398)Instructions burned: 572 (million)
% 7.32/1.46 % (493428)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=91022069:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 7.32/1.46 % (493429)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2600647873:i=227:sd=1:bd=all:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/227Mi)
% 7.32/1.46 % (493410)Instruction limit reached!
% 7.32/1.46 % (493410)------------------------------
% 7.32/1.46 % (493410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493410)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493410)Termination reason: Instruction limit
% 7.32/1.46 % (493410)Termination phase: Saturation
% 7.32/1.46 % (493410)Time elapsed: 0.192 s
% 7.32/1.46 % (493410)Peak memory usage: 14 MB
% 7.32/1.46 % (493410)Instructions burned: 376 (million)
% 7.32/1.46 % (493432)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.32/1.46 % (493424)Instruction limit reached!
% 7.32/1.46 % (493424)------------------------------
% 7.32/1.46 % (493424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493424)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493424)Termination reason: Instruction limit
% 7.32/1.46 % (493424)Termination phase: Saturation
% 7.32/1.46 % (493424)Time elapsed: 0.072 s
% 7.32/1.46 % (493424)Peak memory usage: 13 MB
% 7.32/1.46 % (493424)Instructions burned: 137 (million)
% 7.32/1.46 % (493432)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1559433120:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.32/1.46 % (493433)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=337360662:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.32/1.46 % (493411)Instruction limit reached!
% 7.32/1.46 % (493411)------------------------------
% 7.32/1.46 % (493411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493411)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493411)Termination reason: Instruction limit
% 7.32/1.46 % (493411)Termination phase: Saturation
% 7.32/1.46 % (493411)Time elapsed: 0.243 s
% 7.32/1.46 % (493411)Peak memory usage: 14 MB
% 7.32/1.46 % (493411)Instructions burned: 496 (million)
% 7.32/1.46 % (493436)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=155331969:i=575:rtra=on_2989 on theBenchmark for (2989ds/575Mi)
% 7.32/1.46 % (493429)Instruction limit reached!
% 7.32/1.46 % (493429)------------------------------
% 7.32/1.46 % (493429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493429)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493429)Termination reason: Instruction limit
% 7.32/1.46 % (493429)Termination phase: Saturation
% 7.32/1.46 % (493429)Time elapsed: 0.114 s
% 7.32/1.46 % (493429)Peak memory usage: 13 MB
% 7.32/1.46 % (493429)Instructions burned: 229 (million)
% 7.32/1.46 % (493433)Instruction limit reached!
% 7.32/1.46 % (493433)------------------------------
% 7.32/1.46 % (493433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493433)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493433)Termination reason: Instruction limit
% 7.32/1.46 % (493433)Termination phase: Saturation
% 7.32/1.46 % (493433)Time elapsed: 0.061 s
% 7.32/1.46 % (493433)Peak memory usage: 12 MB
% 7.32/1.46 % (493433)Instructions burned: 117 (million)
% 7.32/1.46 % (493422)Instruction limit reached!
% 7.32/1.46 % (493422)------------------------------
% 7.32/1.46 % (493422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493422)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493422)Termination reason: Instruction limit
% 7.32/1.46 % (493422)Termination phase: Saturation
% 7.32/1.46 % (493422)Time elapsed: 0.177 s
% 7.32/1.46 % (493422)Peak memory usage: 15 MB
% 7.32/1.46 % (493422)Instructions burned: 339 (million)
% 7.32/1.46 % (493438)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4179696651:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 7.32/1.46 % (493439)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=1593453628: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_2989 on theBenchmark for (2989ds/9840Mi)
% 7.32/1.46 % (493428)Instruction limit reached!
% 7.32/1.46 % (493428)------------------------------
% 7.32/1.46 % (493428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493428)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493428)Termination reason: Instruction limit
% 7.32/1.46 % (493428)Termination phase: Saturation
% 7.32/1.46 % (493428)Time elapsed: 0.151 s
% 7.32/1.46 % (493428)Peak memory usage: 12 MB
% 7.32/1.46 % (493428)Instructions burned: 340 (million)
% 7.32/1.46 % (493440)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2829899175:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 7.32/1.46 % (493443)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.32/1.46 % (493443)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=1376073500:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/270Mi)
% 7.32/1.46 % (493432)Instruction limit reached!
% 7.32/1.46 % (493432)------------------------------
% 7.32/1.46 % (493432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493432)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493432)Termination reason: Instruction limit
% 7.32/1.46 % (493432)Termination phase: Saturation
% 7.32/1.46 % (493432)Time elapsed: 0.178 s
% 7.32/1.46 % (493432)Peak memory usage: 14 MB
% 7.32/1.46 % (493432)Instructions burned: 374 (million)
% 7.32/1.46 % (493446)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2575392866:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/31Mi)
% 7.32/1.46 % (493443) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-493269-493443"...
% 7.32/1.46 % (493443)...printing done.
% 7.32/1.46 % (493443)Refutation found. Thanks to Tanya!
% 7.32/1.46 % SZS status Theorem for theBenchmark
% 7.32/1.46 % SZS output start Proof for theBenchmark
% 7.32/1.46 thf(type_def_5, type, a: $tType).
% 7.32/1.46 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 7.32/1.46 thf(func_def_3, type, sK0: (a > a > $o)).
% 7.32/1.46 thf(func_def_4, type, sK1: ((a > $o) > a)).
% 7.32/1.46 thf(func_def_5, type, sK2: (a > (a > $o) > a)).
% 7.32/1.46 thf(func_def_6, type, sK3: (a > a)).
% 7.32/1.46 thf(func_def_7, type, sF4: (a > (a > $o) > $o)).
% 7.32/1.46 thf(func_def_8, type, sF5: ((a > $o) > a)).
% 7.32/1.46 thf(func_def_9, type, sF6: ((a > $o) > a > $o)).
% 7.32/1.46 thf(func_def_10, type, sF7: ((a > $o) > a > a)).
% 7.32/1.46 thf(func_def_11, type, sF8: (a > (a > $o) > $o)).
% 7.32/1.46 thf(func_def_12, type, sF9: (a > (a > $o) > $o)).
% 7.32/1.46 thf(func_def_13, type, sF10: (a > (a > $o) > $o)).
% 7.32/1.46 thf(func_def_14, type, sF11: (a > a > $o)).
% 7.32/1.46 thf(func_def_15, type, sF12: (a > a)).
% 7.32/1.46 thf(func_def_16, type, sF13: (a > a > $o)).
% 7.32/1.46 thf(func_def_17, type, sF14: (a > $o)).
% 7.32/1.46 thf(func_def_18, type, sF15: (a > $o)).
% 7.32/1.46 thf(func_def_19, type, vNOT: ($o > $o)).
% 7.32/1.46 thf(func_def_20, type, db0: !>[X0: $tType]:(X0)).
% 7.32/1.46 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.32/1.46 thf(f1,conjecture,(
% 7.32/1.46 ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X5 : (a > $o)] : (! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X6 : a] : (! [X7 : a] : ((X5 @ X7) => (X0 @ X7 @ X6)) => (X0 @ (X1 @ X5) @ X6))) & ! [X4 : a,X2 : a,X3 : a] : (((X0 @ X3 @ X4) & (X0 @ X2 @ X3)) => (X0 @ X2 @ X4))) => ! [X8 : (a > a)] : ((! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3))) & ! [X2 : a,X3 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3)))) => ? [X9 : a] : ((X0 @ X9 @ (X8 @ X9)) & (X0 @ (X8 @ X9) @ X9))))),
% 7.32/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM145_B_pme)).
% 7.32/1.46 thf(f2,negated_conjecture,(
% 7.32/1.46 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X5 : (a > $o)] : (! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X4 : a] : ((X5 @ X4) => (X0 @ X4 @ (X1 @ X5))) & ! [X6 : a] : (! [X7 : a] : ((X5 @ X7) => (X0 @ X7 @ X6)) => (X0 @ (X1 @ X5) @ X6))) & ! [X4 : a,X2 : a,X3 : a] : (((X0 @ X3 @ X4) & (X0 @ X2 @ X3)) => (X0 @ X2 @ X4))) => ! [X8 : (a > a)] : ((! [X3 : a,X2 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3))) & ! [X2 : a,X3 : a] : ((X0 @ X2 @ X3) => (X0 @ (X8 @ X2) @ (X8 @ X3)))) => ? [X9 : a] : ((X0 @ X9 @ (X8 @ X9)) & (X0 @ (X8 @ X9) @ X9))))),
% 7.32/1.46 inference(negated_conjecture,[status(cth)],[f1])).
% 7.32/1.46 thf(f3,plain,(
% 7.32/1.46 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X2 : (a > $o)] : (! [X3 : a] : ((X2 @ X3) => (X0 @ X3 @ (X1 @ X2))) & ! [X4 : a] : ((X2 @ X4) => (X0 @ X4 @ (X1 @ X2))) & ! [X5 : a] : (! [X6 : a] : ((X2 @ X6) => (X0 @ X6 @ X5)) => (X0 @ (X1 @ X2) @ X5))) & ! [X7 : a,X8 : a,X9 : a] : (((X0 @ X9 @ X7) & (X0 @ X8 @ X9)) => (X0 @ X8 @ X7))) => ! [X10 : (a > a)] : ((! [X11 : a,X12 : a] : ((X0 @ X12 @ X11) => (X0 @ (X10 @ X12) @ (X10 @ X11))) & ! [X13 : a,X14 : a] : ((X0 @ X13 @ X14) => (X0 @ (X10 @ X13) @ (X10 @ X14)))) => ? [X15 : a] : ((X0 @ X15 @ (X10 @ X15)) & (X0 @ (X10 @ X15) @ X15))))),
% 7.32/1.46 inference(rectify,[],[f2])).
% 7.32/1.46 thf(f4,plain,(
% 7.32/1.46 ~ ! [X0 : (a > a > $o),X1 : ((a > $o) > a)] : ((! [X8 : a,X9 : a,X7 : a] : ((($true = ((X0 @ X9 @ X7))) & (((X0 @ X8 @ X9)) = $true)) => ($true = ((X0 @ X8 @ X7)))) & ! [X2 : (a > $o)] : (! [X5 : a] : (! [X6 : a] : ((((X2 @ X6)) = $true) => ($true = ((X0 @ X6 @ X5)))) => (((X0 @ (X1 @ X2) @ X5)) = $true)) & ! [X4 : a] : ((((X2 @ X4)) = $true) => ($true = ((X0 @ X4 @ (X1 @ X2))))) & ! [X3 : a] : ((((X2 @ X3)) = $true) => ($true = ((X0 @ X3 @ (X1 @ X2))))))) => ! [X10 : (a > a)] : ((! [X11 : a,X12 : a] : ((((X0 @ X12 @ X11)) = $true) => ($true = ((X0 @ (X10 @ X12) @ (X10 @ X11))))) & ! [X14 : a,X13 : a] : ((((X0 @ X13 @ X14)) = $true) => ($true = ((X0 @ (X10 @ X13) @ (X10 @ X14)))))) => ? [X15 : a] : ((((X0 @ X15 @ (X10 @ X15))) = $true) & (((X0 @ (X10 @ X15) @ X15)) = $true))))),
% 7.32/1.46 inference(fool_elimination,[],[f3])).
% 7.32/1.46 thf(f5,plain,(
% 7.32/1.46 ? [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (? [X10 : (a > a)] : (! [X15 : a] : ((((X0 @ X15 @ (X10 @ X15))) != $true) | (((X0 @ (X10 @ X15) @ X15)) != $true)) & (! [X11 : a,X12 : a] : ((((X0 @ X12 @ X11)) != $true) | ($true = ((X0 @ (X10 @ X12) @ (X10 @ X11))))) & ! [X14 : a,X13 : a] : (($true = ((X0 @ (X10 @ X13) @ (X10 @ X14)))) | (((X0 @ X13 @ X14)) != $true)))) & (! [X8 : a,X9 : a,X7 : a] : (($true = ((X0 @ X8 @ X7))) | (($true != ((X0 @ X9 @ X7))) | (((X0 @ X8 @ X9)) != $true))) & ! [X2 : (a > $o)] : (! [X4 : a] : ((((X2 @ X4)) != $true) | ($true = ((X0 @ X4 @ (X1 @ X2))))) & ! [X3 : a] : (($true = ((X0 @ X3 @ (X1 @ X2)))) | (((X2 @ X3)) != $true)) & ! [X5 : a] : (? [X6 : a] : (($true != ((X0 @ X6 @ X5))) & (((X2 @ X6)) = $true)) | (((X0 @ (X1 @ X2) @ X5)) = $true)))))),
% 7.32/1.46 inference(ennf_transformation,[],[f4])).
% 7.32/1.46 thf(f6,plain,(
% 7.32/1.46 ? [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X2 : (a > $o)] : (! [X4 : a] : ((((X2 @ X4)) != $true) | ($true = ((X0 @ X4 @ (X1 @ X2))))) & ! [X3 : a] : (($true = ((X0 @ X3 @ (X1 @ X2)))) | (((X2 @ X3)) != $true)) & ! [X5 : a] : (? [X6 : a] : (($true != ((X0 @ X6 @ X5))) & (((X2 @ X6)) = $true)) | (((X0 @ (X1 @ X2) @ X5)) = $true))) & ? [X10 : (a > a)] : (! [X11 : a,X12 : a] : ((((X0 @ X12 @ X11)) != $true) | ($true = ((X0 @ (X10 @ X12) @ (X10 @ X11))))) & ! [X14 : a,X13 : a] : (($true = ((X0 @ (X10 @ X13) @ (X10 @ X14)))) | (((X0 @ X13 @ X14)) != $true)) & ! [X15 : a] : ((((X0 @ X15 @ (X10 @ X15))) != $true) | (((X0 @ (X10 @ X15) @ X15)) != $true))) & ! [X7 : a,X9 : a,X8 : a] : ((((X0 @ X8 @ X9)) != $true) | ($true = ((X0 @ X8 @ X7))) | ($true != ((X0 @ X9 @ X7)))))),
% 7.32/1.46 inference(flattening,[],[f5])).
% 7.32/1.46 thf(f7,plain,(
% 7.32/1.46 ? [X0 : (a > a > $o),X1 : ((a > $o) > a)] : (! [X2 : (a > $o)] : (! [X3 : a] : ((((X2 @ X3)) != $true) | ($true = ((X0 @ X3 @ (X1 @ X2))))) & ! [X4 : a] : (($true = ((X0 @ X4 @ (X1 @ X2)))) | (((X2 @ X4)) != $true)) & ! [X5 : a] : (? [X6 : a] : (($true != ((X0 @ X6 @ X5))) & (((X2 @ X6)) = $true)) | (((X0 @ (X1 @ X2) @ X5)) = $true))) & ? [X7 : (a > a)] : (! [X8 : a,X9 : a] : ((((X0 @ X9 @ X8)) != $true) | ($true = ((X0 @ (X7 @ X9) @ (X7 @ X8))))) & ! [X10 : a,X11 : a] : (($true = ((X0 @ (X7 @ X11) @ (X7 @ X10)))) | ($true != ((X0 @ X11 @ X10)))) & ! [X12 : a] : (($true != ((X0 @ X12 @ (X7 @ X12)))) | ($true != ((X0 @ (X7 @ X12) @ X12))))) & ! [X13 : a,X14 : a,X15 : a] : ((((X0 @ X15 @ X14)) != $true) | (((X0 @ X15 @ X13)) = $true) | ($true != ((X0 @ X14 @ X13)))))),
% 7.32/1.46 inference(rectify,[],[f6])).
% 7.32/1.46 thf(f8,plain,(
% 7.32/1.46 ! [X2 : (a > $o)] : (! [X3 : a] : ((((X2 @ X3)) != $true) | ($true = ((sK0 @ X3 @ (sK1 @ X2))))) & ! [X4 : a] : ((((sK0 @ X4 @ (sK1 @ X2))) = $true) | (((X2 @ X4)) != $true)) & ! [X5 : a] : (((((sK0 @ (sK2 @ X5 @ X2) @ X5)) != $true) & ($true = ((X2 @ (sK2 @ X5 @ X2))))) | (((sK0 @ (sK1 @ X2) @ X5)) = $true))) & (! [X8 : a,X9 : a] : ((((sK0 @ X9 @ X8)) != $true) | (((sK0 @ (sK3 @ X9) @ (sK3 @ X8))) = $true)) & ! [X10 : a,X11 : a] : (($true = ((sK0 @ (sK3 @ X11) @ (sK3 @ X10)))) | ($true != ((sK0 @ X11 @ X10)))) & ! [X12 : a] : (($true != ((sK0 @ X12 @ (sK3 @ X12)))) | ($true != ((sK0 @ (sK3 @ X12) @ X12))))) & ! [X13 : a,X14 : a,X15 : a] : (($true != ((sK0 @ X15 @ X14))) | ($true = ((sK0 @ X15 @ X13))) | ($true != ((sK0 @ X14 @ X13))))),
% 7.32/1.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,vAPP,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X6,sK2 @ X5 @ X2),skolemize(X7,sK3)],[f7])).
% 7.32/1.46 thf(f9,plain,(
% 7.32/1.46 ( ! [X14 : a,X15 : a,X13 : a] : (($true != ((sK0 @ X15 @ X14))) | ($true = ((sK0 @ X15 @ X13))) | ($true != ((sK0 @ X14 @ X13)))) )),
% 7.32/1.46 inference(cnf_transformation,[],[f8])).
% 7.32/1.46 thf(f10,plain,(
% 7.32/1.46 ( ! [X12 : a] : (($true != ((sK0 @ X12 @ (sK3 @ X12)))) | ($true != ((sK0 @ (sK3 @ X12) @ X12)))) )),
% 7.32/1.46 inference(cnf_transformation,[],[f8])).
% 7.32/1.46 thf(f11,plain,(
% 7.32/1.46 ( ! [X10 : a,X11 : a] : (($true = ((sK0 @ (sK3 @ X11) @ (sK3 @ X10)))) | ($true != ((sK0 @ X11 @ X10)))) )),
% 7.32/1.46 inference(cnf_transformation,[],[f8])).
% 7.32/1.46 thf(f13,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : (($true = ((X2 @ (sK2 @ X5 @ X2)))) | (((sK0 @ (sK1 @ X2) @ X5)) = $true)) )),
% 7.32/1.46 inference(cnf_transformation,[],[f8])).
% 7.32/1.46 thf(f14,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sK0 @ (sK2 @ X5 @ X2) @ X5)) != $true) | (((sK0 @ (sK1 @ X2) @ X5)) = $true)) )),
% 7.32/1.46 inference(cnf_transformation,[],[f8])).
% 7.32/1.46 thf(f15,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X4 : a] : ((((sK0 @ X4 @ (sK1 @ X2))) = $true) | (((X2 @ X4)) != $true)) )),
% 7.32/1.46 inference(cnf_transformation,[],[f8])).
% 7.32/1.46 thf(f19,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o),X3 : a] : ((((sF4 @ X3 @ X2)) = ((X2 @ X3)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 7.32/1.46 thf(f20,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X3 : a] : ((((X2 @ X3)) = ((sF4 @ X3 @ X2)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f19])).
% 7.32/1.46 thf(f21,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o)] : ((((sF5 @ X2)) = ((sK1 @ X2)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 7.32/1.46 thf(f22,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o),X3 : a] : ((((sF6 @ X2 @ X3)) = ((sK0 @ X3 @ (sF5 @ X2))))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 7.32/1.46 thf(f23,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X3 : a] : ((((sK0 @ X3 @ (sF5 @ X2))) = ((sF6 @ X2 @ X3)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f22])).
% 7.32/1.46 thf(f25,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X4 : a] : ((((sF4 @ X4 @ X2)) != $true) | (((sF6 @ X2 @ X4)) = $true)) )),
% 7.32/1.46 inference(definition_folding,[],[f15,f20,f23,f21])).
% 7.32/1.46 thf(f26,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sF7 @ X2 @ X5)) = ((sK2 @ X5 @ X2)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 7.32/1.46 thf(f27,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sF8 @ X5 @ X2)) = ((sK0 @ (sF7 @ X2 @ X5) @ X5)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 7.32/1.46 thf(f28,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sF9 @ X5 @ X2)) = ((sK0 @ (sF5 @ X2) @ X5)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 7.32/1.46 thf(f29,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sK0 @ (sF5 @ X2) @ X5)) = ((sF9 @ X5 @ X2)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f28])).
% 7.32/1.46 thf(f30,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sF8 @ X5 @ X2)) != $true) | ($true = ((sF9 @ X5 @ X2)))) )),
% 7.32/1.46 inference(definition_folding,[],[f14,f29,f21,f27,f26])).
% 7.32/1.46 thf(f31,definition,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((sF10 @ X5 @ X2)) = ((X2 @ (sF7 @ X2 @ X5))))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 7.32/1.46 thf(f32,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : ((((X2 @ (sF7 @ X2 @ X5))) = ((sF10 @ X5 @ X2)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f31])).
% 7.32/1.46 thf(f33,plain,(
% 7.32/1.46 ( ! [X2 : (a > $o),X5 : a] : (($true = ((sF9 @ X5 @ X2))) | ($true = ((sF10 @ X5 @ X2)))) )),
% 7.32/1.46 inference(definition_folding,[],[f13,f29,f21,f32,f26])).
% 7.32/1.46 thf(f34,definition,(
% 7.32/1.46 ( ! [X8 : a,X9 : a] : ((((sF11 @ X8 @ X9)) = ((sK0 @ X9 @ X8)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 7.32/1.46 thf(f35,plain,(
% 7.32/1.46 ( ! [X8 : a,X9 : a] : ((((sK0 @ X9 @ X8)) = ((sF11 @ X8 @ X9)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f34])).
% 7.32/1.46 thf(f36,definition,(
% 7.32/1.46 ( ! [X9 : a] : ((((sF12 @ X9)) = ((sK3 @ X9)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 7.32/1.46 thf(f37,plain,(
% 7.32/1.46 ( ! [X9 : a] : ((((sK3 @ X9)) = ((sF12 @ X9)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f36])).
% 7.32/1.46 thf(f38,definition,(
% 7.32/1.46 ( ! [X8 : a,X9 : a] : ((((sF13 @ X8 @ X9)) = ((sK0 @ (sF12 @ X9) @ (sF12 @ X8))))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 7.32/1.46 thf(f40,plain,(
% 7.32/1.46 ( ! [X10 : a,X11 : a] : (($true != ((sF11 @ X10 @ X11))) | (((sF13 @ X10 @ X11)) = $true)) )),
% 7.32/1.46 inference(definition_folding,[],[f11,f35,f38,f37,f37])).
% 7.32/1.46 thf(f41,definition,(
% 7.32/1.46 ( ! [X12 : a] : ((((sF14 @ X12)) = ((sK0 @ X12 @ (sF12 @ X12))))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 7.32/1.46 thf(f42,plain,(
% 7.32/1.46 ( ! [X12 : a] : ((((sK0 @ X12 @ (sF12 @ X12))) = ((sF14 @ X12)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f41])).
% 7.32/1.46 thf(f43,definition,(
% 7.32/1.46 ( ! [X12 : a] : ((((sF15 @ X12)) = ((sK0 @ (sF12 @ X12) @ X12)))) )),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 7.32/1.46 thf(f44,plain,(
% 7.32/1.46 ( ! [X12 : a] : ((((sK0 @ (sF12 @ X12) @ X12)) = ((sF15 @ X12)))) )),
% 7.32/1.46 inference(reorient_equations,[],[f43])).
% 7.32/1.46 thf(f45,plain,(
% 7.32/1.46 ( ! [X12 : a] : (($true != ((sF15 @ X12))) | ($true != ((sF14 @ X12)))) )),
% 7.32/1.46 inference(definition_folding,[],[f10,f44,f37,f42,f37])).
% 7.32/1.46 thf(f46,plain,(
% 7.32/1.46 ( ! [X14 : a,X15 : a,X13 : a] : ((((sF11 @ X14 @ X15)) != $true) | (((sF11 @ X13 @ X15)) = $true) | (((sF11 @ X13 @ X14)) != $true)) )),
% 7.32/1.46 inference(definition_folding,[],[f9,f35,f35,f35])).
% 7.32/1.46 thf(f61,plain,(
% 7.32/1.46 ( ! [X0 : a,X1 : a] : (($true != ((sK0 @ X0 @ X1))) | ($true = ((sF13 @ X1 @ X0)))) )),
% 7.32/1.46 inference(superposition,[],[f40,f35])).
% 7.32/1.46 thf(f63,plain,(
% 7.32/1.46 ( ! [X0 : a] : (($true != ((sF14 @ X0))) | (((sF13 @ (sF12 @ X0) @ X0)) = $true)) )),
% 7.32/1.46 inference(superposition,[],[f61,f42])).
% 7.32/1.46 thf(f68,plain,(
% 7.32/1.46 ( ! [X0 : (a > $o)] : ((((sF6 @ X0 @ (sF12 @ (sF5 @ X0)))) = ((sF15 @ (sF5 @ X0))))) )),
% 7.32/1.46 inference(superposition,[],[f44,f23])).
% 7.32/1.46 thf(f69,plain,(
% 7.32/1.46 ( ! [X0 : (a > $o),X1 : a] : ((((sF6 @ X0 @ X1)) != $true) | (((sF13 @ (sF5 @ X0) @ X1)) = $true)) )),
% 7.32/1.46 inference(superposition,[],[f61,f23])).
% 7.32/1.46 thf(f72,plain,(
% 7.32/1.46 ( ! [X0 : a] : ((((sF13 @ (sF12 @ X0) @ X0)) = ((sF14 @ (sF12 @ X0))))) )),
% 7.32/1.46 inference(superposition,[],[f38,f42])).
% 7.32/1.46 thf(f77,plain,(
% 7.32/1.46 ( ! [X0 : a,X1 : a] : ((((sF13 @ X0 @ X1)) = ((sF11 @ (sF12 @ X0) @ (sF12 @ X1))))) )),
% 7.32/1.46 inference(superposition,[],[f35,f38])).
% 7.32/1.46 thf(f88,plain,(
% 7.32/1.46 ( ! [X0 : (a > $o),X1 : a] : (($true != ((X0 @ X1))) | (((sF6 @ X0 @ X1)) = $true)) )),
% 7.32/1.46 inference(superposition,[],[f25,f20])).
% 7.32/1.46 thf(f114,plain,(
% 7.32/1.46 ( ! [X0 : (a > $o)] : ((((sF14 @ (sF5 @ X0))) = ((sF9 @ (sF12 @ (sF5 @ X0)) @ X0)))) )),
% 7.32/1.46 inference(superposition,[],[f29,f42])).
% 7.32/1.46 thf(f136,plain,(
% 7.32/1.46 ( ! [X0 : a] : (($true = ((sF13 @ (sF12 @ (sF7 @ sF14 @ X0)) @ (sF7 @ sF14 @ X0)))) | (((sF10 @ X0 @ sF14)) != $true)) )),
% 7.32/1.46 inference(superposition,[],[f63,f32])).
% 7.32/1.46 thf(f146,plain,(
% 7.32/1.46 ( ! [X0 : a] : ((((sF10 @ X0 @ sF14)) != $true) | ($true = ((sF14 @ (sF12 @ (sF7 @ sF14 @ X0)))))) )),
% 7.32/1.46 inference(forward_demodulation,[],[f136,f72])).
% 7.32/1.46 thf(f201,plain,(
% 7.32/1.46 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sF11 @ X2 @ X1))) | (((sF11 @ X2 @ X0)) = $true) | ($true != ((sK0 @ X0 @ X1)))) )),
% 7.32/1.46 inference(superposition,[],[f46,f35])).
% 7.32/1.46 thf(f405,plain,(
% 7.32/1.46 ( ! [X0 : a,X1 : (a > $o)] : ((((sF8 @ X0 @ X1)) = ((sF11 @ X0 @ (sF7 @ X1 @ X0))))) )),
% 7.32/1.46 inference(superposition,[],[f35,f27])).
% 7.32/1.46 thf(f472,plain,(
% 7.32/1.46 ( ! [X0 : (a > $o)] : (($true = ((sF10 @ (sF12 @ (sF5 @ X0)) @ X0))) | (((sF14 @ (sF5 @ X0))) = $true)) )),
% 7.32/1.46 inference(superposition,[],[f33,f114])).
% 7.32/1.46 thf(f687,plain,(
% 7.32/1.46 ( ! [X2 : a,X0 : a,X1 : a] : (($true != ((sK0 @ X2 @ X0))) | ($true = ((sF11 @ X1 @ X2))) | ($true != ((sK0 @ X0 @ X1)))) )),
% 7.32/1.46 inference(superposition,[],[f201,f35])).
% 7.32/1.46 thf(f771,plain,(
% 7.32/1.46 ( ! [X0 : a,X1 : a] : (($true != ((sK0 @ (sF12 @ X0) @ X1))) | ($true != ((sF14 @ X0))) | (((sF11 @ X1 @ X0)) = $true)) )),
% 7.32/1.46 inference(superposition,[],[f687,f42])).
% 7.32/1.46 thf(f782,plain,(
% 7.32/1.46 ( ! [X0 : a,X1 : a] : ((((sF13 @ X0 @ X1)) != $true) | (((sF11 @ (sF12 @ X0) @ X1)) = $true) | ($true != ((sF14 @ X1)))) )),
% 7.32/1.46 inference(superposition,[],[f771,f38])).
% 7.32/1.46 thf(f1280,plain,(
% 7.32/1.46 ($true != $true) | ($true = ((sF14 @ (sF5 @ sF14)))) | ($true = ((sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))))),
% 7.32/1.46 inference(superposition,[],[f146,f472])).
% 7.32/1.46 thf(f1281,plain,(
% 7.32/1.46 ($true = ((sF14 @ (sF5 @ sF14)))) | ($true = ((sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))))),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1280])).
% 7.32/1.46 thf(f1283,definition,(
% 7.32/1.46 spl16_5 <=> ($true = ((sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))))),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition])).
% 7.32/1.46 thf(f1285,plain,(
% 7.32/1.46 ($true = ((sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | ~spl16_5),
% 7.32/1.46 inference(avatar_component_clause,[],[f1283])).
% 7.32/1.46 thf(f1287,definition,(
% 7.32/1.46 spl16_6 <=> ($true = ((sF14 @ (sF5 @ sF14))))),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition])).
% 7.32/1.46 thf(f1288,plain,(
% 7.32/1.46 ($true != ((sF14 @ (sF5 @ sF14)))) | spl16_6),
% 7.32/1.46 inference(avatar_component_clause,[],[f1287])).
% 7.32/1.46 thf(f1289,plain,(
% 7.32/1.46 ($true = ((sF14 @ (sF5 @ sF14)))) | ~spl16_6),
% 7.32/1.46 inference(avatar_component_clause,[],[f1287])).
% 7.32/1.46 thf(f1290,plain,(
% 7.32/1.46 spl16_5 | spl16_6),
% 7.32/1.46 inference(avatar_split_clause,[],[f1281,f1287,f1283])).
% 7.32/1.46 thf(f1299,plain,(
% 7.32/1.46 ($true = ((sF6 @ sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | ($true != $true) | ~spl16_5),
% 7.32/1.46 inference(superposition,[],[f88,f1285])).
% 7.32/1.46 thf(f1304,plain,(
% 7.32/1.46 ($true = ((sF6 @ sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | ~spl16_5),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1299])).
% 7.32/1.46 thf(f1317,definition,(
% 7.32/1.46 spl16_8 <=> ($true = ((sF10 @ (sF12 @ (sF5 @ sF14)) @ sF14)))),
% 7.32/1.46 introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition])).
% 7.32/1.46 thf(f1318,plain,(
% 7.32/1.46 ($true = ((sF10 @ (sF12 @ (sF5 @ sF14)) @ sF14))) | ~spl16_8),
% 7.32/1.46 inference(avatar_component_clause,[],[f1317])).
% 7.32/1.46 thf(f1319,plain,(
% 7.32/1.46 ($true != ((sF10 @ (sF12 @ (sF5 @ sF14)) @ sF14))) | spl16_8),
% 7.32/1.46 inference(avatar_component_clause,[],[f1317])).
% 7.32/1.46 thf(f1321,plain,(
% 7.32/1.46 ($true != $true) | ($true = ((sF14 @ (sF5 @ sF14)))) | spl16_8),
% 7.32/1.46 inference(superposition,[],[f1319,f472])).
% 7.32/1.46 thf(f1322,plain,(
% 7.32/1.46 ($true = ((sF14 @ (sF5 @ sF14)))) | spl16_8),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1321])).
% 7.32/1.46 thf(f1323,plain,(
% 7.32/1.46 spl16_6 | spl16_8),
% 7.32/1.46 inference(avatar_split_clause,[],[f1322,f1317,f1287])).
% 7.32/1.46 thf(f1327,plain,(
% 7.32/1.46 ($true != $true) | (((sF13 @ (sF12 @ (sF5 @ sF14)) @ (sF5 @ sF14))) = $true) | ~spl16_6),
% 7.32/1.46 inference(superposition,[],[f63,f1289])).
% 7.32/1.46 thf(f1331,plain,(
% 7.32/1.46 (((sF13 @ (sF12 @ (sF5 @ sF14)) @ (sF5 @ sF14))) = $true) | ~spl16_6),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1327])).
% 7.32/1.46 thf(f1336,plain,(
% 7.32/1.46 (((sF14 @ (sF12 @ (sF5 @ sF14)))) = $true) | ~spl16_6),
% 7.32/1.46 inference(forward_demodulation,[],[f1331,f72])).
% 7.32/1.46 thf(f1346,plain,(
% 7.32/1.46 (((sF6 @ sF14 @ (sF12 @ (sF5 @ sF14)))) = $true) | ($true != $true) | ~spl16_6),
% 7.32/1.46 inference(superposition,[],[f88,f1336])).
% 7.32/1.46 thf(f1355,plain,(
% 7.32/1.46 (((sF6 @ sF14 @ (sF12 @ (sF5 @ sF14)))) = $true) | ~spl16_6),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1346])).
% 7.32/1.46 thf(f1359,plain,(
% 7.32/1.46 (((sF15 @ (sF5 @ sF14))) = $true) | ~spl16_6),
% 7.32/1.46 inference(forward_demodulation,[],[f1355,f68])).
% 7.32/1.46 thf(f1364,plain,(
% 7.32/1.46 ($true != $true) | ($true != ((sF14 @ (sF5 @ sF14)))) | ~spl16_6),
% 7.32/1.46 inference(superposition,[],[f45,f1359])).
% 7.32/1.46 thf(f1371,plain,(
% 7.32/1.46 ($true != ((sF14 @ (sF5 @ sF14)))) | ~spl16_6),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1364])).
% 7.32/1.46 thf(f1374,plain,(
% 7.32/1.46 $false | ~spl16_6),
% 7.32/1.46 inference(forward_subsumption_resolution,[],[f1371,f1289])).
% 7.32/1.46 thf(f1375,plain,(
% 7.32/1.46 ~spl16_6),
% 7.32/1.46 inference(avatar_contradiction_clause,[],[f1374])).
% 7.32/1.46 thf(f1406,plain,(
% 7.32/1.46 ($true = ((sF13 @ (sF5 @ sF14) @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | ($true != $true) | ~spl16_5),
% 7.32/1.46 inference(superposition,[],[f69,f1304])).
% 7.32/1.46 thf(f1410,plain,(
% 7.32/1.46 ($true = ((sF13 @ (sF5 @ sF14) @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | ~spl16_5),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1406])).
% 7.32/1.46 thf(f1493,plain,(
% 7.32/1.46 ($true != ((sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | ($true != $true) | (((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) = $true) | ~spl16_5),
% 7.32/1.46 inference(superposition,[],[f782,f1410])).
% 7.32/1.46 thf(f1500,plain,(
% 7.32/1.46 ($true != ((sF14 @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))))) | (((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) = $true) | ~spl16_5),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1493])).
% 7.32/1.46 thf(f1504,plain,(
% 7.32/1.46 (((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF12 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) = $true) | ~spl16_5),
% 7.32/1.46 inference(forward_subsumption_resolution,[],[f1500,f1285])).
% 7.32/1.46 thf(f1505,plain,(
% 7.32/1.46 (((sF13 @ (sF5 @ sF14) @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))) = $true) | ~spl16_5),
% 7.32/1.46 inference(forward_demodulation,[],[f1504,f77])).
% 7.32/1.46 thf(f1506,plain,(
% 7.32/1.46 (((sF14 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))) != $true) | ($true = ((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) | ($true != $true) | ~spl16_5),
% 7.32/1.46 inference(superposition,[],[f782,f1505])).
% 7.32/1.46 thf(f1514,plain,(
% 7.32/1.46 (((sF14 @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14))))) != $true) | ($true = ((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) | ~spl16_5),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1506])).
% 7.32/1.46 thf(f1517,plain,(
% 7.32/1.46 ($true != ((sF10 @ (sF12 @ (sF5 @ sF14)) @ sF14))) | ($true = ((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) | ~spl16_5),
% 7.32/1.46 inference(forward_demodulation,[],[f1514,f32])).
% 7.32/1.46 thf(f1518,plain,(
% 7.32/1.46 ($true = ((sF11 @ (sF12 @ (sF5 @ sF14)) @ (sF7 @ sF14 @ (sF12 @ (sF5 @ sF14)))))) | (~spl16_5 | ~spl16_8)),
% 7.32/1.46 inference(forward_subsumption_resolution,[],[f1517,f1318])).
% 7.32/1.46 thf(f1519,plain,(
% 7.32/1.46 ($true = ((sF8 @ (sF12 @ (sF5 @ sF14)) @ sF14))) | (~spl16_5 | ~spl16_8)),
% 7.32/1.46 inference(forward_demodulation,[],[f1518,f405])).
% 7.32/1.46 thf(f1520,plain,(
% 7.32/1.46 ($true != $true) | (((sF9 @ (sF12 @ (sF5 @ sF14)) @ sF14)) = $true) | (~spl16_5 | ~spl16_8)),
% 7.32/1.46 inference(superposition,[],[f30,f1519])).
% 7.32/1.46 thf(f1521,plain,(
% 7.32/1.46 (((sF9 @ (sF12 @ (sF5 @ sF14)) @ sF14)) = $true) | (~spl16_5 | ~spl16_8)),
% 7.32/1.46 inference(trivial_inequality_removal,[],[f1520])).
% 7.32/1.46 thf(f1522,plain,(
% 7.32/1.46 ($true = ((sF14 @ (sF5 @ sF14)))) | (~spl16_5 | ~spl16_8)),
% 7.32/1.46 inference(forward_demodulation,[],[f1521,f114])).
% 7.32/1.46 thf(f1523,plain,(
% 7.32/1.46 $false | (~spl16_5 | spl16_6 | ~spl16_8)),
% 7.32/1.46 inference(forward_subsumption_resolution,[],[f1522,f1288])).
% 7.32/1.46 thf(f1524,plain,(
% 7.32/1.46 ~spl16_5 | spl16_6 | ~spl16_8),
% 7.32/1.46 inference(avatar_contradiction_clause,[],[f1523])).
% 7.32/1.46 cnf(s4, plain, spl16_5 | spl16_6, inference(sat_conversion,[],[f1290])).
% 7.32/1.46 cnf(s6, plain, spl16_6 | spl16_8, inference(sat_conversion,[],[f1323])).
% 7.32/1.46 cnf(s7, plain, ~spl16_6, inference(sat_conversion,[],[f1375])).
% 7.32/1.46 cnf(s8, plain, ~spl16_5 | spl16_6 | ~spl16_8, inference(sat_conversion,[],[f1524])).
% 7.32/1.46 cnf(s9, plain, spl16_8, inference(rat,[],[s6,s7])).
% 7.32/1.46 cnf(s10, plain, ~spl16_5, inference(rat,[],[s8,s7,s9])).
% 7.32/1.46 cnf(s11, plain, $false, inference(rat,[],[s4,s7,s10])).
% 7.32/1.46 thf(f1525,plain,(
% 7.32/1.46 $false),
% 7.32/1.46 inference(avatar_sat_refutation,[],[s11])).
% 7.32/1.46 % SZS output end Proof for theBenchmark
% 7.32/1.46 % (493443)------------------------------
% 7.32/1.46 % (493443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.32/1.46 % (493443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.32/1.46 % (493443)CaDiCaL version: 2.1.3
% 7.32/1.46 % (493443)Termination reason: Refutation
% 7.32/1.46 % (493443)Time elapsed: 0.081 s
% 7.32/1.46 % (493443)Peak memory usage: 14 MB
% 7.32/1.46 % (493443)Instructions burned: 148 (million)
% 7.32/1.46 % (493269)Success in time 1.208 s
% 7.32/1.46 % Vampire exiting
%------------------------------------------------------------------------------