%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP146^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:08:33 AM UTC 2026
% Result : Theorem 27.89s 4.36s
% Output : Refutation 27.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP146^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.19 % Computer : n015.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Tue Sep 29 20:04:03 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.23 Running higher-order theorem proving
% 0.23/0.28 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.54/0.41 % (4044789)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.54/0.41 % (4044801)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.54/0.41 % (4044801)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.54/0.41 % (4044799)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3505227293:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.54/0.41 % (4044795)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1075772164:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.54/0.41 % (4044797)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3518295530:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.54/0.41 % (4044800)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2595821086:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.54/0.41 % (4044798)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=3941993358: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.54/0.41 % (4044801)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=4136999395:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.54/0.41 % (4044796)lrs+10_16_si=on:nwc=1.5:random_seed=360116289:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.54/0.41 % (4044797)Instruction limit reached!
% 0.54/0.41 % (4044797)------------------------------
% 0.54/0.41 % (4044797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.41 % (4044797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.41 % (4044797)CaDiCaL version: 2.1.3
% 0.54/0.41 % (4044797)Termination reason: Instruction limit
% 0.54/0.41 % (4044797)Termination phase: shuffling
% 0.54/0.41 % (4044797)Time elapsed: 0.002 s
% 0.54/0.41 % (4044797)Peak memory usage: 10 MB
% 0.54/0.41 % (4044797)Instructions burned: 3 (million)
% 0.54/0.41 % (4044796)Instruction limit reached!
% 0.54/0.41 % (4044796)------------------------------
% 0.54/0.41 % (4044796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.41 % (4044796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.41 % (4044796)CaDiCaL version: 2.1.3
% 0.54/0.41 % (4044796)Termination reason: Instruction limit
% 0.54/0.41 % (4044796)Termination phase: shuffling
% 0.54/0.41 % (4044796)Time elapsed: 0.005 s
% 0.54/0.41 % (4044796)Peak memory usage: 10 MB
% 0.54/0.41 % (4044796)Instructions burned: 21 (million)
% 0.54/0.41 % (4044799)Instruction limit reached!
% 0.54/0.41 % (4044799)------------------------------
% 0.54/0.41 % (4044799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.41 % (4044799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.41 % (4044799)CaDiCaL version: 2.1.3
% 0.54/0.41 % (4044799)Termination reason: Instruction limit
% 0.54/0.41 % (4044799)Termination phase: shuffling
% 0.54/0.41 % (4044799)Time elapsed: 0.010 s
% 0.54/0.41 % (4044799)Peak memory usage: 10 MB
% 0.54/0.41 % (4044799)Instructions burned: 24 (million)
% 0.54/0.41 % (4044810)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1298138698:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.54/0.41 % (4044810)Instruction limit reached!
% 0.54/0.41 % (4044810)------------------------------
% 0.54/0.41 % (4044810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.41 % (4044810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.41 % (4044810)CaDiCaL version: 2.1.3
% 0.54/0.41 % (4044810)Termination reason: Instruction limit
% 0.54/0.41 % (4044810)Termination phase: shuffling
% 0.54/0.41 % (4044810)Time elapsed: 0.002 s
% 0.54/0.41 % (4044810)Peak memory usage: 10 MB
% 0.54/0.41 % (4044810)Instructions burned: 9 (million)
% 0.54/0.41 % (4044809)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1059586732:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.54/0.45 % (4044809)Instruction limit reached!
% 0.54/0.45 % (4044809)------------------------------
% 0.54/0.45 % (4044809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.45 % (4044809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.45 % (4044809)CaDiCaL version: 2.1.3
% 0.54/0.45 % (4044809)Termination reason: Instruction limit
% 0.54/0.45 % (4044809)Termination phase: shuffling
% 0.54/0.45 % (4044809)Time elapsed: 0.003 s
% 0.54/0.45 % (4044809)Peak memory usage: 10 MB
% 0.54/0.45 % (4044809)Instructions burned: 7 (million)
% 0.54/0.45 % (4044811)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.54/0.45 % (4044813)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3440412906:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.54/0.45 % (4044813)Instruction limit reached!
% 0.54/0.45 % (4044813)------------------------------
% 0.54/0.45 % (4044813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.45 % (4044813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.45 % (4044813)CaDiCaL version: 2.1.3
% 0.54/0.45 % (4044813)Termination reason: Instruction limit
% 0.54/0.45 % (4044813)Termination phase: shuffling
% 0.54/0.45 % (4044813)Time elapsed: 0.003 s
% 0.54/0.45 % (4044813)Peak memory usage: 10 MB
% 0.54/0.45 % (4044813)Instructions burned: 14 (million)
% 0.54/0.45 % (4044811)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3737673850:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.54/0.45 % (4044800)Instruction limit reached!
% 0.54/0.45 % (4044800)------------------------------
% 0.54/0.45 % (4044800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.45 % (4044800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.45 % (4044800)CaDiCaL version: 2.1.3
% 0.54/0.45 % (4044800)Termination reason: Instruction limit
% 0.54/0.45 % (4044800)Termination phase: Property scanning
% 0.54/0.45 % (4044800)Time elapsed: 0.034 s
% 0.54/0.45 % (4044800)Peak memory usage: 11 MB
% 0.54/0.45 % (4044800)Instructions burned: 75 (million)
% 0.54/0.45 % (4044811)Instruction limit reached!
% 0.54/0.45 % (4044811)------------------------------
% 0.54/0.45 % (4044811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.45 % (4044811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.45 % (4044811)CaDiCaL version: 2.1.3
% 0.54/0.45 % (4044811)Termination reason: Instruction limit
% 0.54/0.45 % (4044811)Termination phase: shuffling
% 0.54/0.45 % (4044811)Time elapsed: 0.004 s
% 0.54/0.45 % (4044811)Peak memory usage: 10 MB
% 0.54/0.45 % (4044811)Instructions burned: 8 (million)
% 0.54/0.45 % (4044795)Instruction limit reached!
% 0.54/0.45 % (4044795)------------------------------
% 0.54/0.45 % (4044795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.54/0.45 % (4044795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.54/0.45 % (4044795)CaDiCaL version: 2.1.3
% 0.54/0.45 % (4044795)Termination reason: Instruction limit
% 0.54/0.45 % (4044795)Termination phase: Property scanning
% 0.54/0.45 % (4044795)Time elapsed: 0.039 s
% 0.54/0.45 % (4044795)Peak memory usage: 11 MB
% 0.54/0.45 % (4044795)Instructions burned: 88 (million)
% 0.54/0.45 % (4044815)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.54/0.45 % (4044815)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.54/0.45 % (4044818)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=1712892741:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.54/0.45 % (4044815)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=559349721: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.54/0.45 % (4044820)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.24/0.48 % (4044819)lrs+10_1_si=on:cs=on:random_seed=2659043396:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.24/0.48 % (4044820)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=4138605388:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.24/0.48 % (4044821)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2882104123:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.24/0.48 % (4044815)Instruction limit reached!
% 1.24/0.48 % (4044815)------------------------------
% 1.24/0.48 % (4044815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.48 % (4044815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.48 % (4044815)CaDiCaL version: 2.1.3
% 1.24/0.48 % (4044815)Termination reason: Instruction limit
% 1.24/0.48 % (4044815)Termination phase: shuffling
% 1.24/0.48 % (4044815)Time elapsed: 0.013 s
% 1.24/0.48 % (4044815)Peak memory usage: 10 MB
% 1.24/0.48 % (4044815)Instructions burned: 29 (million)
% 1.24/0.48 % (4044819)Instruction limit reached!
% 1.24/0.48 % (4044819)------------------------------
% 1.24/0.48 % (4044819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.48 % (4044819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.48 % (4044819)CaDiCaL version: 2.1.3
% 1.24/0.48 % (4044819)Termination reason: Instruction limit
% 1.24/0.48 % (4044819)Termination phase: shuffling
% 1.24/0.48 % (4044819)Time elapsed: 0.004 s
% 1.24/0.48 % (4044819)Peak memory usage: 10 MB
% 1.24/0.48 % (4044819)Instructions burned: 9 (million)
% 1.24/0.48 % (4044820)Instruction limit reached!
% 1.24/0.48 % (4044820)------------------------------
% 1.24/0.48 % (4044820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.48 % (4044820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.48 % (4044820)CaDiCaL version: 2.1.3
% 1.24/0.48 % (4044820)Termination reason: Instruction limit
% 1.24/0.48 % (4044820)Termination phase: shuffling
% 1.24/0.48 % (4044820)Time elapsed: 0.002 s
% 1.24/0.48 % (4044820)Peak memory usage: 10 MB
% 1.24/0.48 % (4044820)Instructions burned: 3 (million)
% 1.24/0.48 % (4044818)Instruction limit reached!
% 1.24/0.48 % (4044818)------------------------------
% 1.24/0.48 % (4044818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.48 % (4044818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.48 % (4044818)CaDiCaL version: 2.1.3
% 1.24/0.48 % (4044818)Termination reason: Instruction limit
% 1.24/0.48 % (4044818)Termination phase: Property scanning
% 1.24/0.48 % (4044818)Time elapsed: 0.019 s
% 1.24/0.48 % (4044818)Peak memory usage: 11 MB
% 1.24/0.48 % (4044818)Instructions burned: 87 (million)
% 1.24/0.48 % (4044830)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3492669108:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.24/0.48 % (4044821)Instruction limit reached!
% 1.24/0.48 % (4044821)------------------------------
% 1.24/0.48 % (4044821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.48 % (4044821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.48 % (4044821)CaDiCaL version: 2.1.3
% 1.24/0.48 % (4044821)Termination reason: Instruction limit
% 1.24/0.48 % (4044821)Termination phase: Property scanning
% 1.24/0.48 % (4044821)Time elapsed: 0.016 s
% 1.24/0.48 % (4044821)Peak memory usage: 10 MB
% 1.24/0.48 % (4044821)Instructions burned: 38 (million)
% 1.24/0.48 % (4044801)Instruction limit reached!
% 1.24/0.48 % (4044801)------------------------------
% 1.24/0.48 % (4044801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.48 % (4044801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.48 % (4044801)CaDiCaL version: 2.1.3
% 1.24/0.48 % (4044801)Termination reason: Instruction limit
% 1.24/0.48 % (4044801)Termination phase: Saturation
% 1.24/0.48 % (4044801)Time elapsed: 0.075 s
% 1.24/0.48 % (4044801)Peak memory usage: 13 MB
% 1.24/0.48 % (4044801)Instructions burned: 159 (million)
% 1.24/0.48 % (4044827)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3214458320:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.24/0.48 % (4044828)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=632834751:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.24/0.54 % (4044829)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=791040876:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.24/0.54 % (4044829)Instruction limit reached!
% 1.24/0.54 % (4044829)------------------------------
% 1.24/0.54 % (4044829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (4044829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (4044829)CaDiCaL version: 2.1.3
% 1.24/0.54 % (4044829)Termination reason: Instruction limit
% 1.24/0.54 % (4044829)Termination phase: shuffling
% 1.24/0.54 % (4044829)Time elapsed: 0.006 s
% 1.24/0.54 % (4044829)Peak memory usage: 10 MB
% 1.24/0.54 % (4044829)Instructions burned: 14 (million)
% 1.24/0.54 % (4044828)Instruction limit reached!
% 1.24/0.54 % (4044828)------------------------------
% 1.24/0.54 % (4044828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (4044828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (4044828)CaDiCaL version: 2.1.3
% 1.24/0.54 % (4044828)Termination reason: Instruction limit
% 1.24/0.54 % (4044828)Termination phase: shuffling
% 1.24/0.54 % (4044828)Time elapsed: 0.011 s
% 1.24/0.54 % (4044828)Peak memory usage: 10 MB
% 1.24/0.54 % (4044828)Instructions burned: 26 (million)
% 1.24/0.54 % (4044832)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3503014545:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.24/0.54 % (4044833)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2035541721: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.24/0.54 % (4044833)Instruction limit reached!
% 1.24/0.54 % (4044833)------------------------------
% 1.24/0.54 % (4044833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (4044833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (4044833)CaDiCaL version: 2.1.3
% 1.24/0.54 % (4044833)Termination reason: Instruction limit
% 1.24/0.54 % (4044833)Termination phase: shuffling
% 1.24/0.54 % (4044833)Time elapsed: 0.002 s
% 1.24/0.54 % (4044833)Peak memory usage: 10 MB
% 1.24/0.54 % (4044833)Instructions burned: 3 (million)
% 1.24/0.54 % (4044832)Instruction limit reached!
% 1.24/0.54 % (4044832)------------------------------
% 1.24/0.54 % (4044832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (4044832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (4044832)CaDiCaL version: 2.1.3
% 1.24/0.54 % (4044832)Termination reason: Instruction limit
% 1.24/0.54 % (4044832)Termination phase: shuffling
% 1.24/0.54 % (4044832)Time elapsed: 0.006 s
% 1.24/0.54 % (4044832)Peak memory usage: 10 MB
% 1.24/0.54 % (4044832)Instructions burned: 14 (million)
% 1.24/0.54 % (4044837)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1994571910:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.24/0.54 % (4044838)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2171690505:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.24/0.54 % (4044842)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.24/0.54 % (4044842)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.24/0.54 % (4044841)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1211204445:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.24/0.54 % (4044837)Instruction limit reached!
% 1.24/0.54 % (4044837)------------------------------
% 1.24/0.54 % (4044837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.24/0.54 % (4044837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.24/0.54 % (4044837)CaDiCaL version: 2.1.3
% 1.24/0.54 % (4044837)Termination reason: Instruction limit
% 1.24/0.54 % (4044837)Termination phase: shuffling
% 1.24/0.54 % (4044837)Time elapsed: 0.012 s
% 1.24/0.54 % (4044837)Peak memory usage: 10 MB
% 1.24/0.54 % (4044837)Instructions burned: 28 (million)
% 1.94/0.58 % (4044838)Instruction limit reached!
% 1.94/0.58 % (4044838)------------------------------
% 1.94/0.58 % (4044838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.58 % (4044838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.58 % (4044838)CaDiCaL version: 2.1.3
% 1.94/0.58 % (4044838)Termination reason: Instruction limit
% 1.94/0.58 % (4044838)Termination phase: shuffling
% 1.94/0.58 % (4044838)Time elapsed: 0.011 s
% 1.94/0.58 % (4044838)Peak memory usage: 10 MB
% 1.94/0.58 % (4044838)Instructions burned: 24 (million)
% 1.94/0.58 % (4044842)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=1569283737:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.94/0.58 % (4044842)Instruction limit reached!
% 1.94/0.58 % (4044842)------------------------------
% 1.94/0.58 % (4044842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.58 % (4044842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.58 % (4044842)CaDiCaL version: 2.1.3
% 1.94/0.58 % (4044842)Termination reason: Instruction limit
% 1.94/0.58 % (4044842)Termination phase: shuffling
% 1.94/0.58 % (4044842)Time elapsed: 0.007 s
% 1.94/0.58 % (4044842)Peak memory usage: 10 MB
% 1.94/0.58 % (4044842)Instructions burned: 14 (million)
% 1.94/0.58 % (4044846)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.94/0.58 % (4044846)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=1208089733:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.94/0.58 % (4044848)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=2482177961:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.94/0.58 % (4044846)Instruction limit reached!
% 1.94/0.58 % (4044846)------------------------------
% 1.94/0.58 % (4044846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.58 % (4044846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.58 % (4044846)CaDiCaL version: 2.1.3
% 1.94/0.58 % (4044846)Termination reason: Instruction limit
% 1.94/0.58 % (4044846)Termination phase: shuffling
% 1.94/0.58 % (4044846)Time elapsed: 0.004 s
% 1.94/0.58 % (4044846)Peak memory usage: 10 MB
% 1.94/0.58 % (4044846)Instructions burned: 9 (million)
% 1.94/0.58 % (4044841)Instruction limit reached!
% 1.94/0.58 % (4044841)------------------------------
% 1.94/0.58 % (4044841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.58 % (4044841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.58 % (4044841)CaDiCaL version: 2.1.3
% 1.94/0.58 % (4044841)Termination reason: Instruction limit
% 1.94/0.58 % (4044841)Termination phase: Property scanning
% 1.94/0.58 % (4044841)Time elapsed: 0.027 s
% 1.94/0.58 % (4044841)Peak memory usage: 11 MB
% 1.94/0.58 % (4044841)Instructions burned: 62 (million)
% 1.94/0.58 % (4044849)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2061403998:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.94/0.58 % (4044849)Instruction limit reached!
% 1.94/0.58 % (4044849)------------------------------
% 1.94/0.58 % (4044849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.58 % (4044849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.58 % (4044849)CaDiCaL version: 2.1.3
% 1.94/0.58 % (4044849)Termination reason: Instruction limit
% 1.94/0.58 % (4044849)Termination phase: shuffling
% 1.94/0.58 % (4044849)Time elapsed: 0.004 s
% 1.94/0.58 % (4044849)Peak memory usage: 10 MB
% 1.94/0.58 % (4044849)Instructions burned: 9 (million)
% 1.94/0.58 % (4044848)Instruction limit reached!
% 1.94/0.58 % (4044848)------------------------------
% 1.94/0.58 % (4044848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.94/0.58 % (4044848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.94/0.58 % (4044848)CaDiCaL version: 2.1.3
% 1.94/0.58 % (4044848)Termination reason: Instruction limit
% 1.94/0.58 % (4044848)Termination phase: Property scanning
% 1.94/0.58 % (4044848)Time elapsed: 0.014 s
% 1.94/0.58 % (4044848)Peak memory usage: 10 MB
% 2.35/0.66 % (4044848)Instructions burned: 32 (million)
% 2.35/0.66 % (4044830)Instruction limit reached!
% 2.35/0.66 % (4044830)------------------------------
% 2.35/0.66 % (4044830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.66 % (4044830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.66 % (4044830)CaDiCaL version: 2.1.3
% 2.35/0.66 % (4044830)Termination reason: Instruction limit
% 2.35/0.66 % (4044830)Termination phase: Saturation
% 2.35/0.66 % (4044830)Time elapsed: 0.083 s
% 2.35/0.66 % (4044830)Peak memory usage: 14 MB
% 2.35/0.66 % (4044830)Instructions burned: 329 (million)
% 2.35/0.66 % (4044852)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1058347710:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.35/0.66 % (4044853)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1250980383:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.35/0.66 % (4044857)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1458064089:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.35/0.66 % (4044855)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1932775688:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.35/0.66 % (4044852)Instruction limit reached!
% 2.35/0.66 % (4044852)------------------------------
% 2.35/0.66 % (4044852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.66 % (4044852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.66 % (4044852)CaDiCaL version: 2.1.3
% 2.35/0.66 % (4044852)Termination reason: Instruction limit
% 2.35/0.66 % (4044852)Termination phase: shuffling
% 2.35/0.66 % (4044852)Time elapsed: 0.010 s
% 2.35/0.66 % (4044852)Peak memory usage: 10 MB
% 2.35/0.66 % (4044852)Instructions burned: 24 (million)
% 2.35/0.66 % (4044856)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2455675248:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.35/0.66 % (4044853)Instruction limit reached!
% 2.35/0.66 % (4044853)------------------------------
% 2.35/0.66 % (4044853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.66 % (4044853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.66 % (4044853)CaDiCaL version: 2.1.3
% 2.35/0.66 % (4044853)Termination reason: Instruction limit
% 2.35/0.66 % (4044853)Termination phase: shuffling
% 2.35/0.66 % (4044853)Time elapsed: 0.009 s
% 2.35/0.66 % (4044853)Peak memory usage: 10 MB
% 2.35/0.66 % (4044853)Instructions burned: 20 (million)
% 2.35/0.66 % (4044864)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.35/0.66 % (4044863)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3666173381:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.35/0.66 % (4044864)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3056173160:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.35/0.66 % (4044864)Instruction limit reached!
% 2.35/0.66 % (4044864)------------------------------
% 2.35/0.66 % (4044864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.66 % (4044864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.66 % (4044864)CaDiCaL version: 2.1.3
% 2.35/0.66 % (4044864)Termination reason: Instruction limit
% 2.35/0.66 % (4044864)Termination phase: shuffling
% 2.35/0.66 % (4044864)Time elapsed: 0.004 s
% 2.35/0.66 % (4044864)Peak memory usage: 10 MB
% 2.35/0.66 % (4044864)Instructions burned: 9 (million)
% 2.35/0.66 % (4044827)Instruction limit reached!
% 2.35/0.66 % (4044827)------------------------------
% 2.35/0.66 % (4044827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.35/0.66 % (4044827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.35/0.66 % (4044827)CaDiCaL version: 2.1.3
% 2.35/0.66 % (4044827)Termination reason: Instruction limit
% 2.35/0.66 % (4044827)Termination phase: Saturation
% 2.35/0.66 % (4044827)Time elapsed: 0.121 s
% 2.35/0.66 % (4044827)Peak memory usage: 13 MB
% 2.35/0.66 % (4044827)Instructions burned: 250 (million)
% 2.35/0.66 % (4044863)Instruction limit reached!
% 2.35/0.66 % (4044863)------------------------------
% 2.63/0.73 % (4044863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.73 % (4044863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.73 % (4044863)CaDiCaL version: 2.1.3
% 2.63/0.73 % (4044863)Termination reason: Instruction limit
% 2.63/0.73 % (4044863)Termination phase: Property scanning
% 2.63/0.73 % (4044863)Time elapsed: 0.018 s
% 2.63/0.73 % (4044863)Peak memory usage: 10 MB
% 2.63/0.73 % (4044863)Instructions burned: 43 (million)
% 2.63/0.73 % (4044867)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1044891033:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.63/0.73 % (4044868)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=311143568: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.63/0.73 % (4044857)Instruction limit reached!
% 2.63/0.73 % (4044857)------------------------------
% 2.63/0.73 % (4044857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.73 % (4044857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.73 % (4044857)CaDiCaL version: 2.1.3
% 2.63/0.73 % (4044857)Termination reason: Instruction limit
% 2.63/0.73 % (4044857)Termination phase: Saturation
% 2.63/0.73 % (4044857)Time elapsed: 0.050 s
% 2.63/0.73 % (4044857)Peak memory usage: 13 MB
% 2.63/0.73 % (4044857)Instructions burned: 194 (million)
% 2.63/0.73 % (4044869)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.63/0.73 % (4044869)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=4058834918: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.63/0.73 % (4044872)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1513812378:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.63/0.73 % (4044869)Instruction limit reached!
% 2.63/0.73 % (4044869)------------------------------
% 2.63/0.73 % (4044869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.73 % (4044869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.73 % (4044869)CaDiCaL version: 2.1.3
% 2.63/0.73 % (4044869)Termination reason: Instruction limit
% 2.63/0.73 % (4044869)Termination phase: shuffling
% 2.63/0.73 % (4044869)Time elapsed: 0.004 s
% 2.63/0.73 % (4044869)Peak memory usage: 10 MB
% 2.63/0.73 % (4044869)Instructions burned: 8 (million)
% 2.63/0.73 % (4044872)Instruction limit reached!
% 2.63/0.73 % (4044872)------------------------------
% 2.63/0.73 % (4044872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.73 % (4044872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.73 % (4044872)CaDiCaL version: 2.1.3
% 2.63/0.73 % (4044872)Termination reason: Instruction limit
% 2.63/0.73 % (4044872)Termination phase: shuffling
% 2.63/0.73 % (4044872)Time elapsed: 0.006 s
% 2.63/0.73 % (4044872)Peak memory usage: 10 MB
% 2.63/0.73 % (4044872)Instructions burned: 25 (million)
% 2.63/0.73 % (4044856)Instruction limit reached!
% 2.63/0.73 % (4044856)------------------------------
% 2.63/0.73 % (4044856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.63/0.73 % (4044856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.63/0.73 % (4044856)CaDiCaL version: 2.1.3
% 2.63/0.73 % (4044856)Termination reason: Instruction limit
% 2.63/0.73 % (4044856)Termination phase: Saturation
% 2.63/0.73 % (4044856)Time elapsed: 0.066 s
% 2.63/0.73 % (4044856)Peak memory usage: 14 MB
% 2.63/0.73 % (4044856)Instructions burned: 145 (million)
% 2.63/0.73 % (4044876)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=1995908079:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.63/0.73 % (4044875)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2687350501:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.63/0.73 % (4044877)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=335640552: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.13/0.81 % (4044875)Instruction limit reached!
% 3.13/0.81 % (4044875)------------------------------
% 3.13/0.81 % (4044875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.81 % (4044875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.81 % (4044875)CaDiCaL version: 2.1.3
% 3.13/0.81 % (4044875)Termination reason: Instruction limit
% 3.13/0.81 % (4044875)Termination phase: shuffling
% 3.13/0.81 % (4044875)Time elapsed: 0.008 s
% 3.13/0.81 % (4044875)Peak memory usage: 10 MB
% 3.13/0.81 % (4044875)Instructions burned: 19 (million)
% 3.13/0.81 % (4044881)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=3802169276:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.13/0.81 % (4044881)Instruction limit reached!
% 3.13/0.81 % (4044881)------------------------------
% 3.13/0.81 % (4044881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.81 % (4044881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.81 % (4044881)CaDiCaL version: 2.1.3
% 3.13/0.81 % (4044881)Termination reason: Instruction limit
% 3.13/0.81 % (4044881)Termination phase: Property scanning
% 3.13/0.81 % (4044881)Time elapsed: 0.019 s
% 3.13/0.81 % (4044881)Peak memory usage: 10 MB
% 3.13/0.81 % (4044881)Instructions burned: 46 (million)
% 3.13/0.81 % (4044868)Instruction limit reached!
% 3.13/0.81 % (4044868)------------------------------
% 3.13/0.81 % (4044868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.81 % (4044868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.81 % (4044868)CaDiCaL version: 2.1.3
% 3.13/0.81 % (4044868)Termination reason: Instruction limit
% 3.13/0.81 % (4044868)Termination phase: Saturation
% 3.13/0.81 % (4044868)Time elapsed: 0.083 s
% 3.13/0.81 % (4044868)Peak memory usage: 14 MB
% 3.13/0.81 % (4044868)Instructions burned: 173 (million)
% 3.13/0.81 % (4044798)Instruction limit reached!
% 3.13/0.81 % (4044798)------------------------------
% 3.13/0.81 % (4044798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.81 % (4044798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.81 % (4044798)CaDiCaL version: 2.1.3
% 3.13/0.81 % (4044798)Termination reason: Instruction limit
% 3.13/0.81 % (4044798)Termination phase: Saturation
% 3.13/0.81 % (4044798)Time elapsed: 0.302 s
% 3.13/0.81 % (4044798)Peak memory usage: 15 MB
% 3.13/0.81 % (4044798)Instructions burned: 635 (million)
% 3.13/0.81 % (4044867)Instruction limit reached!
% 3.13/0.81 % (4044867)------------------------------
% 3.13/0.81 % (4044867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.81 % (4044867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.81 % (4044867)CaDiCaL version: 2.1.3
% 3.13/0.81 % (4044867)Termination reason: Instruction limit
% 3.13/0.81 % (4044867)Termination phase: Saturation
% 3.13/0.81 % (4044867)Time elapsed: 0.094 s
% 3.13/0.81 % (4044867)Peak memory usage: 14 MB
% 3.13/0.81 % (4044867)Instructions burned: 182 (million)
% 3.13/0.81 % (4044883)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1298531636:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.13/0.81 % (4044885)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.13/0.81 % (4044884)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=413819389: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.13/0.81 % (4044885)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1786190610:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.13/0.81 % (4044886)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1940637123:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.13/0.81 % (4044884)Instruction limit reached!
% 3.13/0.81 % (4044884)------------------------------
% 3.13/0.81 % (4044884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.81 % (4044884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.95 % (4044884)CaDiCaL version: 2.1.3
% 3.84/0.95 % (4044884)Termination reason: Instruction limit
% 3.84/0.95 % (4044884)Termination phase: shuffling
% 3.84/0.95 % (4044884)Time elapsed: 0.009 s
% 3.84/0.95 % (4044884)Peak memory usage: 10 MB
% 3.84/0.95 % (4044884)Instructions burned: 22 (million)
% 3.84/0.95 % (4044886)Instruction limit reached!
% 3.84/0.95 % (4044886)------------------------------
% 3.84/0.95 % (4044886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.95 % (4044886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.95 % (4044886)CaDiCaL version: 2.1.3
% 3.84/0.95 % (4044886)Termination reason: Instruction limit
% 3.84/0.95 % (4044886)Termination phase: shuffling
% 3.84/0.95 % (4044886)Time elapsed: 0.006 s
% 3.84/0.95 % (4044886)Peak memory usage: 10 MB
% 3.84/0.95 % (4044886)Instructions burned: 15 (million)
% 3.84/0.95 % (4044876)Instruction limit reached!
% 3.84/0.95 % (4044876)------------------------------
% 3.84/0.95 % (4044876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.95 % (4044876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.95 % (4044876)CaDiCaL version: 2.1.3
% 3.84/0.95 % (4044876)Termination reason: Instruction limit
% 3.84/0.95 % (4044876)Termination phase: Saturation
% 3.84/0.95 % (4044876)Time elapsed: 0.089 s
% 3.84/0.95 % (4044876)Peak memory usage: 16 MB
% 3.84/0.95 % (4044876)Instructions burned: 317 (million)
% 3.84/0.95 % (4044893)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=958167821:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.84/0.95 % (4044891)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=4201975470:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.84/0.95 % (4044892)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2249306175:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.84/0.95 % (4044893)Instruction limit reached!
% 3.84/0.95 % (4044893)------------------------------
% 3.84/0.95 % (4044893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.95 % (4044893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.95 % (4044893)CaDiCaL version: 2.1.3
% 3.84/0.95 % (4044893)Termination reason: Instruction limit
% 3.84/0.95 % (4044893)Termination phase: Property scanning
% 3.84/0.95 % (4044893)Time elapsed: 0.007 s
% 3.84/0.95 % (4044893)Peak memory usage: 10 MB
% 3.84/0.95 % (4044893)Instructions burned: 32 (million)
% 3.84/0.95 % (4044897)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1600175393:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 3.84/0.95 % (4044892)Instruction limit reached!
% 3.84/0.95 % (4044892)------------------------------
% 3.84/0.95 % (4044892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.95 % (4044892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.95 % (4044892)CaDiCaL version: 2.1.3
% 3.84/0.95 % (4044892)Termination reason: Instruction limit
% 3.84/0.95 % (4044892)Termination phase: Preprocessing 3
% 3.84/0.95 % (4044892)Time elapsed: 0.022 s
% 3.84/0.95 % (4044892)Peak memory usage: 11 MB
% 3.84/0.95 % (4044892)Instructions burned: 52 (million)
% 3.84/0.95 % (4044891)Instruction limit reached!
% 3.84/0.95 % (4044891)------------------------------
% 3.84/0.95 % (4044891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.95 % (4044891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.95 % (4044891)CaDiCaL version: 2.1.3
% 3.84/0.95 % (4044891)Termination reason: Instruction limit
% 3.84/0.95 % (4044891)Termination phase: SInE selection
% 3.84/0.95 % (4044891)Time elapsed: 0.029 s
% 3.84/0.95 % (4044891)Peak memory usage: 10 MB
% 3.84/0.95 % (4044891)Instructions burned: 67 (million)
% 3.84/0.95 % (4044899)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=1048934181:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.84/0.95 % (4044900)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4117219513:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.84/0.95 % (4044897)Instruction limit reached!
% 3.84/0.95 % (4044897)------------------------------
% 5.26/1.09 % (4044897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.09 % (4044897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.09 % (4044897)CaDiCaL version: 2.1.3
% 5.26/1.09 % (4044897)Termination reason: Instruction limit
% 5.26/1.09 % (4044897)Termination phase: Saturation
% 5.26/1.09 % (4044897)Time elapsed: 0.035 s
% 5.26/1.09 % (4044897)Peak memory usage: 13 MB
% 5.26/1.09 % (4044897)Instructions burned: 139 (million)
% 5.26/1.09 % (4044903)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.26/1.09 % (4044899)Instruction limit reached!
% 5.26/1.09 % (4044899)------------------------------
% 5.26/1.09 % (4044899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.09 % (4044899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.09 % (4044899)CaDiCaL version: 2.1.3
% 5.26/1.09 % (4044899)Termination reason: Instruction limit
% 5.26/1.09 % (4044899)Termination phase: Property scanning
% 5.26/1.09 % (4044899)Time elapsed: 0.015 s
% 5.26/1.09 % (4044903)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3357057788:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.26/1.09 % (4044899)Peak memory usage: 10 MB
% 5.26/1.09 % (4044899)Instructions burned: 34 (million)
% 5.26/1.09 % (4044885)Instruction limit reached!
% 5.26/1.09 % (4044885)------------------------------
% 5.26/1.09 % (4044885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.09 % (4044885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.09 % (4044885)CaDiCaL version: 2.1.3
% 5.26/1.09 % (4044885)Termination reason: Instruction limit
% 5.26/1.09 % (4044885)Termination phase: Saturation
% 5.26/1.09 % (4044885)Time elapsed: 0.094 s
% 5.26/1.09 % (4044885)Peak memory usage: 13 MB
% 5.26/1.09 % (4044885)Instructions burned: 201 (million)
% 5.26/1.09 % (4044900)Instruction limit reached!
% 5.26/1.09 % (4044900)------------------------------
% 5.26/1.09 % (4044900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.09 % (4044900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.09 % (4044900)CaDiCaL version: 2.1.3
% 5.26/1.09 % (4044900)Termination reason: Instruction limit
% 5.26/1.09 % (4044900)Termination phase: Property scanning
% 5.26/1.09 % (4044900)Time elapsed: 0.029 s
% 5.26/1.09 % (4044900)Peak memory usage: 11 MB
% 5.26/1.09 % (4044900)Instructions burned: 68 (million)
% 5.26/1.09 % (4044905)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3257931989:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.26/1.09 % (4044906)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=430570412:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.26/1.09 % (4044907)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1457156897:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 5.26/1.09 % (4044903)Instruction limit reached!
% 5.26/1.09 % (4044903)------------------------------
% 5.26/1.09 % (4044903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.09 % (4044903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.09 % (4044903)CaDiCaL version: 2.1.3
% 5.26/1.09 % (4044903)Termination reason: Instruction limit
% 5.26/1.09 % (4044903)Termination phase: Saturation
% 5.26/1.09 % (4044903)Time elapsed: 0.041 s
% 5.26/1.09 % (4044903)Peak memory usage: 13 MB
% 5.26/1.09 % (4044903)Instructions burned: 183 (million)
% 5.26/1.09 % (4044911)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=827919137:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.26/1.09 % (4044907)Refutation not found, incomplete strategy
% 5.26/1.09 % (4044907)------------------------------
% 5.26/1.09 % (4044907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.09 % (4044907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.09 % (4044907)CaDiCaL version: 2.1.3
% 5.26/1.09 % (4044907)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.09 % (4044907)Time elapsed: 0.033 s
% 5.26/1.09 % (4044907)Peak memory usage: 13 MB
% 5.26/1.09 % (4044907)Instructions burned: 74 (million)
% 5.26/1.09 % (4044906)Instruction limit reached!
% 5.26/1.09 % (4044906)------------------------------
% 5.26/1.09 % (4044906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.16 % (4044906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.16 % (4044906)CaDiCaL version: 2.1.3
% 5.81/1.16 % (4044906)Termination reason: Instruction limit
% 5.81/1.16 % (4044906)Termination phase: Saturation
% 5.81/1.16 % (4044906)Time elapsed: 0.042 s
% 5.81/1.16 % (4044906)Peak memory usage: 12 MB
% 5.81/1.16 % (4044906)Instructions burned: 98 (million)
% 5.81/1.16 % (4044907)------------------------------
% 5.81/1.16 % (4044907)------------------------------
% 5.81/1.16 % (4044913)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=4165341303:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.81/1.16 % (4044914)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3333073559:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.81/1.16 % (4044883)Refutation not found, incomplete strategy
% 5.81/1.16 % (4044883)------------------------------
% 5.81/1.16 % (4044883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.16 % (4044883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.16 % (4044883)CaDiCaL version: 2.1.3
% 5.81/1.16 % (4044883)Termination reason: Refutation not found, incomplete strategy
% 5.81/1.16 % (4044883)Time elapsed: 0.201 s
% 5.81/1.16 % (4044883)Peak memory usage: 14 MB
% 5.81/1.16 % (4044883)Instructions burned: 415 (million)
% 5.81/1.16 % (4044883)------------------------------
% 5.81/1.16 % (4044883)------------------------------
% 5.81/1.16 % (4044917)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3075333650:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.81/1.16 % (4044905)Instruction limit reached!
% 5.81/1.16 % (4044905)------------------------------
% 5.81/1.16 % (4044905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.16 % (4044905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.16 % (4044905)CaDiCaL version: 2.1.3
% 5.81/1.16 % (4044905)Termination reason: Instruction limit
% 5.81/1.16 % (4044905)Termination phase: Saturation
% 5.81/1.16 % (4044905)Time elapsed: 0.125 s
% 5.81/1.17 % (4044905)Peak memory usage: 14 MB
% 5.81/1.17 % (4044905)Instructions burned: 247 (million)
% 5.81/1.17 % (4044917)Instruction limit reached!
% 5.81/1.17 % (4044917)------------------------------
% 5.81/1.17 % (4044917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.17 % (4044917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.17 % (4044917)CaDiCaL version: 2.1.3
% 5.81/1.17 % (4044917)Termination reason: Instruction limit
% 5.81/1.17 % (4044917)Termination phase: Property scanning
% 5.81/1.17 % (4044917)Time elapsed: 0.019 s
% 5.81/1.17 % (4044917)Peak memory usage: 10 MB
% 5.81/1.17 % (4044917)Instructions burned: 44 (million)
% 5.81/1.17 % (4044914)Instruction limit reached!
% 5.81/1.17 % (4044914)------------------------------
% 5.81/1.17 % (4044914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.17 % (4044914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.17 % (4044914)CaDiCaL version: 2.1.3
% 5.81/1.17 % (4044914)Termination reason: Instruction limit
% 5.81/1.17 % (4044914)Termination phase: Saturation
% 5.81/1.17 % (4044914)Time elapsed: 0.062 s
% 5.81/1.17 % (4044914)Peak memory usage: 13 MB
% 5.81/1.17 % (4044914)Instructions burned: 131 (million)
% 5.81/1.17 % (4044919)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2578513737:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.81/1.17 % (4044920)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3702301091:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 5.81/1.17 % (4044921)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3365248081:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 5.81/1.17 % (4044921)Instruction limit reached!
% 5.81/1.17 % (4044921)------------------------------
% 5.81/1.17 % (4044921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.81/1.17 % (4044921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.17 % (4044921)CaDiCaL version: 2.1.3
% 5.81/1.17 % (4044921)Termination reason: Instruction limit
% 6.06/1.24 % (4044921)Termination phase: Saturation
% 6.06/1.24 % (4044921)Time elapsed: 0.040 s
% 6.06/1.24 % (4044921)Peak memory usage: 12 MB
% 6.06/1.24 % (4044921)Instructions burned: 95 (million)
% 6.06/1.24 % (4044925)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=3426516706:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 6.06/1.24 % (4044925)Instruction limit reached!
% 6.06/1.24 % (4044925)------------------------------
% 6.06/1.24 % (4044925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.06/1.24 % (4044925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.24 % (4044925)CaDiCaL version: 2.1.3
% 6.06/1.24 % (4044925)Termination reason: Instruction limit
% 6.06/1.24 % (4044925)Termination phase: Preprocessing 1
% 6.06/1.24 % (4044925)Time elapsed: 0.029 s
% 6.06/1.24 % (4044925)Peak memory usage: 10 MB
% 6.06/1.24 % (4044925)Instructions burned: 69 (million)
% 6.06/1.24 % (4044877)Instruction limit reached!
% 6.06/1.24 % (4044877)------------------------------
% 6.06/1.24 % (4044877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.06/1.24 % (4044877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.24 % (4044877)CaDiCaL version: 2.1.3
% 6.06/1.24 % (4044877)Termination reason: Instruction limit
% 6.06/1.24 % (4044877)Termination phase: Saturation
% 6.06/1.24 % (4044877)Time elapsed: 0.425 s
% 6.06/1.24 % (4044877)Peak memory usage: 16 MB
% 6.06/1.24 % (4044877)Instructions burned: 854 (million)
% 6.06/1.24 % (4044911)Instruction limit reached!
% 6.06/1.24 % (4044911)------------------------------
% 6.06/1.24 % (4044911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.06/1.24 % (4044911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.24 % (4044911)CaDiCaL version: 2.1.3
% 6.06/1.24 % (4044911)Termination reason: Instruction limit
% 6.06/1.24 % (4044911)Termination phase: Saturation
% 6.06/1.24 % (4044911)Time elapsed: 0.224 s
% 6.06/1.24 % (4044911)Peak memory usage: 15 MB
% 6.06/1.24 % (4044911)Instructions burned: 878 (million)
% 6.06/1.24 % (4044927)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=944370933: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.06/1.24 % (4044929)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=823422482:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.06/1.24 % (4044928)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=2039242076: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.06/1.24 % (4044927)Instruction limit reached!
% 6.06/1.24 % (4044927)------------------------------
% 6.06/1.24 % (4044927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.06/1.24 % (4044927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.24 % (4044927)CaDiCaL version: 2.1.3
% 6.06/1.24 % (4044927)Termination reason: Instruction limit
% 6.06/1.24 % (4044927)Termination phase: Property scanning
% 6.06/1.24 % (4044927)Time elapsed: 0.045 s
% 6.06/1.24 % (4044927)Peak memory usage: 11 MB
% 6.06/1.24 % (4044927)Instructions burned: 106 (million)
% 6.06/1.24 % (4044920)Instruction limit reached!
% 6.06/1.24 % (4044920)------------------------------
% 6.06/1.24 % (4044920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.06/1.24 % (4044920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.24 % (4044920)CaDiCaL version: 2.1.3
% 6.06/1.24 % (4044920)Termination reason: Instruction limit
% 6.06/1.24 % (4044920)Termination phase: Saturation
% 6.06/1.24 % (4044920)Time elapsed: 0.177 s
% 6.06/1.24 % (4044920)Peak memory usage: 14 MB
% 6.06/1.24 % (4044920)Instructions burned: 454 (million)
% 6.06/1.24 % (4044933)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2319392951:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.06/1.24 % (4044913)Instruction limit reached!
% 6.06/1.24 % (4044913)------------------------------
% 6.06/1.24 % (4044913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.39 % (4044913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.39 % (4044913)CaDiCaL version: 2.1.3
% 6.31/1.39 % (4044913)Termination reason: Instruction limit
% 6.31/1.39 % (4044913)Termination phase: Saturation
% 6.31/1.39 % (4044913)Time elapsed: 0.260 s
% 6.31/1.39 % (4044913)Peak memory usage: 15 MB
% 6.31/1.39 % (4044913)Instructions burned: 516 (million)
% 6.31/1.39 % (4044935)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=36671374:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.31/1.39 % (4044936)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1451698426:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 6.31/1.39 % (4044935)Instruction limit reached!
% 6.31/1.39 % (4044935)------------------------------
% 6.31/1.39 % (4044935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.39 % (4044935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.39 % (4044935)CaDiCaL version: 2.1.3
% 6.31/1.39 % (4044935)Termination reason: Instruction limit
% 6.31/1.39 % (4044935)Termination phase: Property scanning
% 6.31/1.39 % (4044935)Time elapsed: 0.015 s
% 6.31/1.39 % (4044935)Peak memory usage: 10 MB
% 6.31/1.39 % (4044935)Instructions burned: 35 (million)
% 6.31/1.39 % (4044855)Instruction limit reached!
% 6.31/1.39 % (4044855)------------------------------
% 6.31/1.39 % (4044855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.39 % (4044855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.39 % (4044855)CaDiCaL version: 2.1.3
% 6.31/1.39 % (4044855)Termination reason: Instruction limit
% 6.31/1.39 % (4044855)Termination phase: Saturation
% 6.31/1.39 % (4044855)Time elapsed: 0.629 s
% 6.31/1.39 % (4044855)Peak memory usage: 17 MB
% 6.31/1.39 % (4044855)Instructions burned: 1240 (million)
% 6.31/1.39 % (4044929)Instruction limit reached!
% 6.31/1.39 % (4044929)------------------------------
% 6.31/1.39 % (4044929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.39 % (4044929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.39 % (4044929)CaDiCaL version: 2.1.3
% 6.31/1.39 % (4044929)Termination reason: Instruction limit
% 6.31/1.39 % (4044929)Termination phase: Saturation
% 6.31/1.39 % (4044929)Time elapsed: 0.102 s
% 6.31/1.39 % (4044929)Peak memory usage: 14 MB
% 6.31/1.39 % (4044929)Instructions burned: 376 (million)
% 6.31/1.39 % (4044939)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=265859915: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)
% 6.31/1.39 % (4044941)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=1213831020:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.31/1.39 % (4044936)Instruction limit reached!
% 6.31/1.39 % (4044936)------------------------------
% 6.31/1.39 % (4044936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.39 % (4044936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.39 % (4044936)CaDiCaL version: 2.1.3
% 6.31/1.39 % (4044936)Termination reason: Instruction limit
% 6.31/1.39 % (4044936)Termination phase: Property scanning
% 6.31/1.39 % (4044936)Time elapsed: 0.040 s
% 6.31/1.39 % (4044936)Peak memory usage: 12 MB
% 6.31/1.39 % (4044936)Instructions burned: 93 (million)
% 6.31/1.39 % (4044940)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4219402476:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.31/1.39 % (4044940)Instruction limit reached!
% 6.31/1.39 % (4044940)------------------------------
% 6.31/1.39 % (4044940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.31/1.39 % (4044940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.39 % (4044940)CaDiCaL version: 2.1.3
% 6.31/1.39 % (4044940)Termination reason: Instruction limit
% 6.31/1.39 % (4044940)Termination phase: shuffling
% 6.31/1.39 % (4044940)Time elapsed: 0.010 s
% 6.31/1.39 % (4044940)Peak memory usage: 10 MB
% 6.31/1.39 % (4044940)Instructions burned: 24 (million)
% 6.31/1.39 % (4044945)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3253434340:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 7.46/1.51 % (4044939)Instruction limit reached!
% 7.46/1.51 % (4044939)------------------------------
% 7.46/1.51 % (4044939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.46/1.51 % (4044939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.51 % (4044939)CaDiCaL version: 2.1.3
% 7.46/1.51 % (4044939)Termination reason: Instruction limit
% 7.46/1.51 % (4044939)Termination phase: Property scanning
% 7.46/1.51 % (4044939)Time elapsed: 0.029 s
% 7.46/1.51 % (4044939)Peak memory usage: 11 MB
% 7.46/1.51 % (4044939)Instructions burned: 68 (million)
% 7.46/1.51 % (4044946)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.46/1.51 % (4044946)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=390923538:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.46/1.51 % (4044945)Instruction limit reached!
% 7.46/1.51 % (4044945)------------------------------
% 7.46/1.51 % (4044945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.46/1.51 % (4044945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.51 % (4044945)CaDiCaL version: 2.1.3
% 7.46/1.51 % (4044945)Termination reason: Instruction limit
% 7.46/1.51 % (4044945)Termination phase: Property scanning
% 7.46/1.51 % (4044945)Time elapsed: 0.012 s
% 7.46/1.51 % (4044945)Peak memory usage: 10 MB
% 7.46/1.51 % (4044945)Instructions burned: 29 (million)
% 7.46/1.51 % (4044948)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=2994562084:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.46/1.51 % (4044950)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=947099202:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 7.46/1.51 % (4044919)Instruction limit reached!
% 7.46/1.51 % (4044919)------------------------------
% 7.46/1.51 % (4044919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.46/1.51 % (4044919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.51 % (4044919)CaDiCaL version: 2.1.3
% 7.46/1.51 % (4044919)Termination reason: Instruction limit
% 7.46/1.51 % (4044919)Termination phase: Saturation
% 7.46/1.51 % (4044919)Time elapsed: 0.299 s
% 7.46/1.51 % (4044919)Peak memory usage: 14 MB
% 7.46/1.51 % (4044919)Instructions burned: 572 (million)
% 7.46/1.51 % (4044953)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.46/1.51 % (4044953)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=4267960190:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.46/1.51 % (4044950)Refutation not found, incomplete strategy
% 7.46/1.51 % (4044950)------------------------------
% 7.46/1.51 % (4044950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.46/1.51 % (4044950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.51 % (4044950)CaDiCaL version: 2.1.3
% 7.46/1.51 % (4044950)Termination reason: Refutation not found, incomplete strategy
% 7.46/1.51 % (4044950)Time elapsed: 0.033 s
% 7.46/1.51 % (4044950)Peak memory usage: 13 MB
% 7.46/1.51 % (4044950)Instructions burned: 75 (million)
% 7.46/1.51 % (4044950)------------------------------
% 7.46/1.51 % (4044950)------------------------------
% 7.46/1.51 % (4044941)Instruction limit reached!
% 7.46/1.51 % (4044941)------------------------------
% 7.46/1.51 % (4044941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.46/1.51 % (4044941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.46/1.51 % (4044941)CaDiCaL version: 2.1.3
% 7.46/1.51 % (4044941)Termination reason: Instruction limit
% 7.46/1.51 % (4044941)Termination phase: Saturation
% 7.46/1.51 % (4044941)Time elapsed: 0.094 s
% 7.46/1.51 % (4044941)Peak memory usage: 17 MB
% 7.46/1.51 % (4044941)Instructions burned: 341 (million)
% 7.46/1.51 % (4044946)Instruction limit reached!
% 7.46/1.51 % (4044946)------------------------------
% 7.46/1.51 % (4044946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.46/1.51 % (4044946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.21/1.71 % (4044946)CaDiCaL version: 2.1.3
% 8.21/1.71 % (4044946)Termination reason: Instruction limit
% 8.21/1.71 % (4044946)Termination phase: Saturation
% 8.21/1.71 % (4044946)Time elapsed: 0.059 s
% 8.21/1.71 % (4044946)Peak memory usage: 13 MB
% 8.21/1.71 % (4044946)Instructions burned: 138 (million)
% 8.21/1.71 % (4044956)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2262162534:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 8.21/1.71 % (4044955)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2943198518:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 8.21/1.71 % (4044957)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2992960491:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2990 on theBenchmark for (2990ds/270Mi)
% 8.21/1.71 % (4044955)Instruction limit reached!
% 8.21/1.71 % (4044955)------------------------------
% 8.21/1.71 % (4044955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.21/1.71 % (4044955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.21/1.71 % (4044955)CaDiCaL version: 2.1.3
% 8.21/1.71 % (4044955)Termination reason: Instruction limit
% 8.21/1.71 % (4044955)Termination phase: Saturation
% 8.21/1.71 % (4044955)Time elapsed: 0.052 s
% 8.21/1.71 % (4044955)Peak memory usage: 13 MB
% 8.21/1.71 % (4044955)Instructions burned: 117 (million)
% 8.21/1.71 % (4044961)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=3297377825: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)
% 8.21/1.71 % (4044933)Instruction limit reached!
% 8.21/1.71 % (4044933)------------------------------
% 8.21/1.71 % (4044933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.21/1.71 % (4044933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.21/1.71 % (4044933)CaDiCaL version: 2.1.3
% 8.21/1.71 % (4044933)Termination reason: Instruction limit
% 8.21/1.71 % (4044933)Termination phase: Saturation
% 8.21/1.71 % (4044933)Time elapsed: 0.256 s
% 8.21/1.71 % (4044933)Peak memory usage: 15 MB
% 8.21/1.71 % (4044933)Instructions burned: 496 (million)
% 8.21/1.71 % (4044948)Instruction limit reached!
% 8.21/1.71 % (4044948)------------------------------
% 8.21/1.71 % (4044948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.21/1.71 % (4044948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.21/1.71 % (4044948)CaDiCaL version: 2.1.3
% 8.21/1.71 % (4044948)Termination reason: Instruction limit
% 8.21/1.71 % (4044948)Termination phase: Saturation
% 8.21/1.71 % (4044948)Time elapsed: 0.166 s
% 8.21/1.71 % (4044948)Peak memory usage: 15 MB
% 8.21/1.71 % (4044948)Instructions burned: 340 (million)
% 8.21/1.71 % (4044963)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=802558260:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 8.21/1.71 % (4044964)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
% 8.21/1.71 % (4044964)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=3802227561:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.21/1.71 % (4044956)Instruction limit reached!
% 8.21/1.71 % (4044956)------------------------------
% 8.21/1.71 % (4044956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.21/1.71 % (4044956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.21/1.71 % (4044956)CaDiCaL version: 2.1.3
% 8.21/1.71 % (4044956)Termination reason: Instruction limit
% 8.21/1.71 % (4044956)Termination phase: Saturation
% 8.21/1.71 % (4044956)Time elapsed: 0.140 s
% 8.21/1.71 % (4044956)Peak memory usage: 15 MB
% 8.21/1.71 % (4044956)Instructions burned: 578 (million)
% 8.21/1.71 % (4044957)Instruction limit reached!
% 8.21/1.71 % (4044957)------------------------------
% 8.21/1.71 % (4044957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.21/1.71 % (4044957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.63/1.94 % (4044957)CaDiCaL version: 2.1.3
% 9.63/1.94 % (4044957)Termination reason: Instruction limit
% 9.63/1.94 % (4044957)Termination phase: Saturation
% 9.63/1.94 % (4044957)Time elapsed: 0.132 s
% 9.63/1.94 % (4044957)Peak memory usage: 14 MB
% 9.63/1.94 % (4044957)Instructions burned: 272 (million)
% 9.63/1.94 % (4044967)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1698364260:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/31Mi)
% 9.63/1.94 % (4044953)Instruction limit reached!
% 9.63/1.94 % (4044953)------------------------------
% 9.63/1.94 % (4044953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.63/1.94 % (4044953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.63/1.94 % (4044953)CaDiCaL version: 2.1.3
% 9.63/1.94 % (4044953)Termination reason: Instruction limit
% 9.63/1.94 % (4044953)Termination phase: Saturation
% 9.63/1.94 % (4044953)Time elapsed: 0.179 s
% 9.63/1.94 % (4044953)Peak memory usage: 14 MB
% 9.63/1.94 % (4044953)Instructions burned: 375 (million)
% 9.63/1.94 % (4044967)Instruction limit reached!
% 9.63/1.94 % (4044967)------------------------------
% 9.63/1.94 % (4044967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.63/1.94 % (4044967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.63/1.94 % (4044967)CaDiCaL version: 2.1.3
% 9.63/1.94 % (4044967)Termination reason: Instruction limit
% 9.63/1.94 % (4044967)Termination phase: Property scanning
% 9.63/1.94 % (4044967)Time elapsed: 0.007 s
% 9.63/1.94 % (4044967)Peak memory usage: 10 MB
% 9.63/1.94 % (4044967)Instructions burned: 32 (million)
% 9.63/1.94 % (4044968)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.63/1.94 % (4044968)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
% 9.63/1.94 % (4044968)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=3092621618:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2988 on theBenchmark for (2988ds/1440Mi)
% 9.63/1.94 % (4044971)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2515365448:i=111:add=on:fgj=on:rtra=on:fdi=1024_2988 on theBenchmark for (2988ds/111Mi)
% 9.63/1.94 % (4044970)dis+10_2_sil=128000:si=on:random_seed=2607596417:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 9.63/1.94 % (4044971)Instruction limit reached!
% 9.63/1.94 % (4044971)------------------------------
% 9.63/1.94 % (4044971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.63/1.94 % (4044971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.63/1.94 % (4044971)CaDiCaL version: 2.1.3
% 9.63/1.94 % (4044971)Termination reason: Instruction limit
% 9.63/1.94 % (4044971)Termination phase: Saturation
% 9.63/1.94 % (4044971)Time elapsed: 0.026 s
% 9.63/1.94 % (4044971)Peak memory usage: 13 MB
% 9.63/1.94 % (4044971)Instructions burned: 114 (million)
% 9.63/1.94 % (4044975)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=986993848:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2988 on theBenchmark for (2988ds/122Mi)
% 9.63/1.94 % (4044975)Instruction limit reached!
% 9.63/1.94 % (4044975)------------------------------
% 9.63/1.94 % (4044975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.63/1.94 % (4044975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.63/1.94 % (4044975)CaDiCaL version: 2.1.3
% 9.63/1.94 % (4044975)Termination reason: Instruction limit
% 9.63/1.94 % (4044975)Termination phase: Saturation
% 9.63/1.94 % (4044975)Time elapsed: 0.031 s
% 9.63/1.94 % (4044975)Peak memory usage: 13 MB
% 9.63/1.94 % (4044975)Instructions burned: 125 (million)
% 9.63/1.94 % (4044977)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=3061076341:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/136Mi)
% 9.63/1.94 % (4044964)Instruction limit reached!
% 9.63/1.94 % (4044964)------------------------------
% 9.63/1.94 % (4044964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.37/2.13 % (4044964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.37/2.13 % (4044964)CaDiCaL version: 2.1.3
% 12.37/2.13 % (4044964)Termination reason: Instruction limit
% 12.37/2.13 % (4044964)Termination phase: Saturation
% 12.37/2.13 % (4044964)Time elapsed: 0.139 s
% 12.37/2.13 % (4044964)Peak memory usage: 14 MB
% 12.37/2.13 % (4044964)Instructions burned: 271 (million)
% 12.37/2.13 % (4044977)Instruction limit reached!
% 12.37/2.13 % (4044977)------------------------------
% 12.37/2.13 % (4044977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.37/2.13 % (4044977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.37/2.13 % (4044977)CaDiCaL version: 2.1.3
% 12.37/2.13 % (4044977)Termination reason: Instruction limit
% 12.37/2.13 % (4044977)Termination phase: Saturation
% 12.37/2.13 % (4044977)Time elapsed: 0.033 s
% 12.37/2.13 % (4044977)Peak memory usage: 13 MB
% 12.37/2.13 % (4044977)Instructions burned: 137 (million)
% 12.37/2.13 % (4044979)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3373204824:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/232Mi)
% 12.37/2.13 % (4044980)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=25397222:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2987 on theBenchmark for (2987ds/1254Mi)
% 12.37/2.13 % (4044963)Instruction limit reached!
% 12.37/2.13 % (4044963)------------------------------
% 12.37/2.13 % (4044963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.37/2.13 % (4044963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.37/2.13 % (4044963)CaDiCaL version: 2.1.3
% 12.37/2.13 % (4044963)Termination reason: Instruction limit
% 12.37/2.13 % (4044963)Termination phase: Saturation
% 12.37/2.13 % (4044963)Time elapsed: 0.199 s
% 12.37/2.13 % (4044963)Peak memory usage: 14 MB
% 12.37/2.13 % (4044963)Instructions burned: 422 (million)
% 12.37/2.13 % (4044983)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 12.37/2.13 % (4044983)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=1739159779:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2987 on theBenchmark for (2987ds/281Mi)
% 12.37/2.13 % (4044970)Instruction limit reached!
% 12.37/2.13 % (4044970)------------------------------
% 12.37/2.13 % (4044970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.37/2.13 % (4044970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.37/2.13 % (4044970)CaDiCaL version: 2.1.3
% 12.37/2.13 % (4044970)Termination reason: Instruction limit
% 12.37/2.13 % (4044970)Termination phase: Saturation
% 12.37/2.13 % (4044970)Time elapsed: 0.164 s
% 12.37/2.13 % (4044970)Peak memory usage: 14 MB
% 12.37/2.13 % (4044970)Instructions burned: 339 (million)
% 12.37/2.13 % (4044985)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=36300902:i=619:add=on:rtra=on_2987 on theBenchmark for (2987ds/619Mi)
% 12.37/2.13 % (4044979)Instruction limit reached!
% 12.37/2.13 % (4044979)------------------------------
% 12.37/2.13 % (4044979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.37/2.13 % (4044979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.37/2.13 % (4044979)CaDiCaL version: 2.1.3
% 12.37/2.13 % (4044979)Termination reason: Instruction limit
% 12.37/2.13 % (4044979)Termination phase: Saturation
% 12.37/2.13 % (4044979)Time elapsed: 0.117 s
% 12.37/2.13 % (4044979)Peak memory usage: 13 MB
% 12.37/2.13 % (4044979)Instructions burned: 233 (million)
% 12.37/2.13 % (4044987)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=1858600247:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/865Mi)
% 12.37/2.13 % (4044983)Instruction limit reached!
% 12.37/2.13 % (4044983)------------------------------
% 12.37/2.13 % (4044983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.37/2.13 % (4044983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.37/2.13 % (4044983)CaDiCaL version: 2.1.3
% 12.37/2.13 % (4044983)Termination reason: Instruction limit
% 12.37/2.13 % (4044983)Termination phase: Saturation
% 12.37/2.13 % (4044983)Time elapsed: 0.130 s
% 12.37/2.13 % (4044983)Peak memory usage: 14 MB
% 13.38/2.29 % (4044983)Instructions burned: 282 (million)
% 13.38/2.29 % (4044989)lrs+10_1_sil=128000:si=on:urr=on:random_seed=520702355:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/212Mi)
% 13.38/2.29 % (4044989)Instruction limit reached!
% 13.38/2.29 % (4044989)------------------------------
% 13.38/2.29 % (4044989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.29 % (4044989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.29 % (4044989)CaDiCaL version: 2.1.3
% 13.38/2.29 % (4044989)Termination reason: Instruction limit
% 13.38/2.29 % (4044989)Termination phase: Saturation
% 13.38/2.29 % (4044989)Time elapsed: 0.098 s
% 13.38/2.29 % (4044989)Peak memory usage: 14 MB
% 13.38/2.29 % (4044989)Instructions burned: 213 (million)
% 13.38/2.29 % (4044991)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=428205266:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/130Mi)
% 13.38/2.29 % (4044980)Instruction limit reached!
% 13.38/2.29 % (4044980)------------------------------
% 13.38/2.29 % (4044980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.29 % (4044980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.29 % (4044980)CaDiCaL version: 2.1.3
% 13.38/2.29 % (4044980)Termination reason: Instruction limit
% 13.38/2.29 % (4044980)Termination phase: Saturation
% 13.38/2.29 % (4044980)Time elapsed: 0.336 s
% 13.38/2.29 % (4044980)Peak memory usage: 22 MB
% 13.38/2.29 % (4044980)Instructions burned: 1255 (million)
% 13.38/2.29 % (4044985)Instruction limit reached!
% 13.38/2.29 % (4044985)------------------------------
% 13.38/2.29 % (4044985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.29 % (4044985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.29 % (4044985)CaDiCaL version: 2.1.3
% 13.38/2.29 % (4044985)Termination reason: Instruction limit
% 13.38/2.29 % (4044985)Termination phase: Saturation
% 13.38/2.29 % (4044985)Time elapsed: 0.274 s
% 13.38/2.29 % (4044985)Peak memory usage: 17 MB
% 13.38/2.29 % (4044985)Instructions burned: 622 (million)
% 13.38/2.29 % (4044993)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2757994332:st=1.5:i=346:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/346Mi)
% 13.38/2.29 % (4044968)Instruction limit reached!
% 13.38/2.29 % (4044968)------------------------------
% 13.38/2.29 % (4044968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.29 % (4044968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.29 % (4044968)CaDiCaL version: 2.1.3
% 13.38/2.29 % (4044968)Termination reason: Instruction limit
% 13.38/2.29 % (4044968)Termination phase: Saturation
% 13.38/2.29 % (4044968)Time elapsed: 0.481 s
% 13.38/2.29 % (4044968)Peak memory usage: 14 MB
% 13.38/2.29 % (4044968)Instructions burned: 1442 (million)
% 13.38/2.29 % (4044994)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=1328748625:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/152Mi)
% 13.38/2.29 % (4044996)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3885366597:i=75:ep=R:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/75Mi)
% 13.38/2.29 % (4044991)Instruction limit reached!
% 13.38/2.29 % (4044991)------------------------------
% 13.38/2.29 % (4044991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.29 % (4044991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.29 % (4044991)CaDiCaL version: 2.1.3
% 13.38/2.29 % (4044991)Termination reason: Instruction limit
% 13.38/2.29 % (4044991)Termination phase: Saturation
% 13.38/2.29 % (4044991)Time elapsed: 0.064 s
% 13.38/2.29 % (4044991)Peak memory usage: 13 MB
% 13.38/2.29 % (4044991)Instructions burned: 131 (million)
% 13.38/2.29 % (4044999)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=566450369:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/387Mi)
% 13.38/2.29 % (4044996)Instruction limit reached!
% 13.38/2.29 % (4044996)------------------------------
% 13.38/2.29 % (4044996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.38/2.29 % (4044996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.38/2.29 % (4044996)CaDiCaL version: 2.1.3
% 13.38/2.29 % (4044996)Termination reason: Instruction limit
% 13.38/2.29 % (4044996)Termination phase: Property scanning
% 14.74/2.57 % (4044996)Time elapsed: 0.033 s
% 14.74/2.57 % (4044996)Peak memory usage: 11 MB
% 14.74/2.57 % (4044996)Instructions burned: 77 (million)
% 14.74/2.57 % (4045001)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=2359107071:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2983 on theBenchmark for (2983ds/148Mi)
% 14.74/2.57 % (4044994)Instruction limit reached!
% 14.74/2.57 % (4044994)------------------------------
% 14.74/2.57 % (4044994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.57 % (4044994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.57 % (4044994)CaDiCaL version: 2.1.3
% 14.74/2.57 % (4044994)Termination reason: Instruction limit
% 14.74/2.57 % (4044994)Termination phase: Saturation
% 14.74/2.57 % (4044994)Time elapsed: 0.069 s
% 14.74/2.57 % (4044994)Peak memory usage: 14 MB
% 14.74/2.57 % (4044994)Instructions burned: 154 (million)
% 14.74/2.57 % (4044993)Instruction limit reached!
% 14.74/2.57 % (4044993)------------------------------
% 14.74/2.57 % (4044993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.57 % (4044993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.57 % (4044993)CaDiCaL version: 2.1.3
% 14.74/2.57 % (4044993)Termination reason: Instruction limit
% 14.74/2.57 % (4044993)Termination phase: Saturation
% 14.74/2.57 % (4044993)Time elapsed: 0.095 s
% 14.74/2.57 % (4044993)Peak memory usage: 14 MB
% 14.74/2.57 % (4044993)Instructions burned: 347 (million)
% 14.74/2.57 % (4045003)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1044083664:i=161:piset=and:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/161Mi)
% 14.74/2.57 % (4045004)lrs+10_1_sil=128000:si=on:random_seed=698379211:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/888Mi)
% 14.74/2.57 % (4045001)Instruction limit reached!
% 14.74/2.57 % (4045001)------------------------------
% 14.74/2.57 % (4045001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.57 % (4045001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.57 % (4045001)CaDiCaL version: 2.1.3
% 14.74/2.57 % (4045001)Termination reason: Instruction limit
% 14.74/2.57 % (4045001)Termination phase: Saturation
% 14.74/2.57 % (4045001)Time elapsed: 0.063 s
% 14.74/2.57 % (4045001)Peak memory usage: 13 MB
% 14.74/2.57 % (4045001)Instructions burned: 149 (million)
% 14.74/2.57 % (4045007)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=2509796651:i=136:add=on:ins=4:rtra=on:sup=off_2982 on theBenchmark for (2982ds/136Mi)
% 14.74/2.57 % (4045003)Instruction limit reached!
% 14.74/2.57 % (4045003)------------------------------
% 14.74/2.57 % (4045003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.57 % (4045003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.57 % (4045003)CaDiCaL version: 2.1.3
% 14.74/2.57 % (4045003)Termination reason: Instruction limit
% 14.74/2.57 % (4045003)Termination phase: Saturation
% 14.74/2.57 % (4045003)Time elapsed: 0.079 s
% 14.74/2.57 % (4045003)Peak memory usage: 13 MB
% 14.74/2.57 % (4045003)Instructions burned: 161 (million)
% 14.74/2.57 % (4045009)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=58778777:i=88:s2at=3:nm=2:rtra=on:rawr=on_2982 on theBenchmark for (2982ds/88Mi)
% 14.74/2.57 % (4045007)Instruction limit reached!
% 14.74/2.57 % (4045007)------------------------------
% 14.74/2.57 % (4045007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.57 % (4045007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.57 % (4045007)CaDiCaL version: 2.1.3
% 14.74/2.57 % (4045007)Termination reason: Instruction limit
% 14.74/2.57 % (4045007)Termination phase: Saturation
% 14.74/2.57 % (4045007)Time elapsed: 0.062 s
% 14.74/2.57 % (4045007)Peak memory usage: 13 MB
% 14.74/2.57 % (4045007)Instructions burned: 137 (million)
% 14.74/2.57 % (4045009)Instruction limit reached!
% 14.74/2.57 % (4045009)------------------------------
% 14.74/2.57 % (4045009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.74/2.57 % (4045009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.74/2.57 % (4045009)CaDiCaL version: 2.1.3
% 14.74/2.57 % (4045009)Termination reason: Instruction limit
% 14.74/2.57 % (4045009)Termination phase: Property scanning
% 15.62/2.67 % (4045009)Time elapsed: 0.039 s
% 15.62/2.67 % (4045009)Peak memory usage: 11 MB
% 15.62/2.67 % (4045009)Instructions burned: 90 (million)
% 15.62/2.67 % (4045011)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3014615948:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2981 on theBenchmark for (2981ds/93Mi)
% 15.62/2.67 % (4044999)Instruction limit reached!
% 15.62/2.67 % (4044999)------------------------------
% 15.62/2.67 % (4044999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.67 % (4044999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.67 % (4044999)CaDiCaL version: 2.1.3
% 15.62/2.67 % (4044999)Termination reason: Instruction limit
% 15.62/2.67 % (4044999)Termination phase: Saturation
% 15.62/2.67 % (4044999)Time elapsed: 0.199 s
% 15.62/2.67 % (4044999)Peak memory usage: 14 MB
% 15.62/2.67 % (4044999)Instructions burned: 387 (million)
% 15.62/2.67 % (4044987)Instruction limit reached!
% 15.62/2.67 % (4044987)------------------------------
% 15.62/2.67 % (4044987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.67 % (4044987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.67 % (4044987)CaDiCaL version: 2.1.3
% 15.62/2.67 % (4044987)Termination reason: Instruction limit
% 15.62/2.67 % (4044987)Termination phase: Saturation
% 15.62/2.67 % (4044987)Time elapsed: 0.471 s
% 15.62/2.67 % (4044987)Peak memory usage: 23 MB
% 15.62/2.67 % (4044987)Instructions burned: 867 (million)
% 15.62/2.67 % (4045012)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3017840816:i=2186:rtra=on:ixr=off_2981 on theBenchmark for (2981ds/2186Mi)
% 15.62/2.67 % (4045014)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3312293937:s2a=on:i=240:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/240Mi)
% 15.62/2.67 % (4045015)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=260244042:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2981 on theBenchmark for (2981ds/805Mi)
% 15.62/2.67 % (4045011)Instruction limit reached!
% 15.62/2.67 % (4045011)------------------------------
% 15.62/2.67 % (4045011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.67 % (4045011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.67 % (4045011)CaDiCaL version: 2.1.3
% 15.62/2.67 % (4045011)Termination reason: Instruction limit
% 15.62/2.67 % (4045011)Termination phase: Property scanning
% 15.62/2.67 % (4045011)Time elapsed: 0.041 s
% 15.62/2.67 % (4045011)Peak memory usage: 11 MB
% 15.62/2.67 % (4045011)Instructions burned: 95 (million)
% 15.62/2.67 % (4045019)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 15.62/2.67 % (4045019)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=190434818:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2981 on theBenchmark for (2981ds/391Mi)
% 15.62/2.67 % (4045004)Instruction limit reached!
% 15.62/2.67 % (4045004)------------------------------
% 15.62/2.67 % (4045004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.67 % (4045004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.67 % (4045004)CaDiCaL version: 2.1.3
% 15.62/2.67 % (4045004)Termination reason: Instruction limit
% 15.62/2.67 % (4045004)Termination phase: Saturation
% 15.62/2.67 % (4045004)Time elapsed: 0.249 s
% 15.62/2.67 % (4045004)Peak memory usage: 17 MB
% 15.62/2.67 % (4045004)Instructions burned: 889 (million)
% 15.62/2.67 % (4045021)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=1310496942:i=355:av=off:fsr=off:rtra=on:ixr=off_2980 on theBenchmark for (2980ds/355Mi)
% 15.62/2.67 % (4045014)Instruction limit reached!
% 15.62/2.67 % (4045014)------------------------------
% 15.62/2.67 % (4045014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.67 % (4045014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.67 % (4045014)CaDiCaL version: 2.1.3
% 15.62/2.67 % (4045014)Termination reason: Instruction limit
% 15.62/2.67 % (4045014)Termination phase: Saturation
% 15.62/2.67 % (4045014)Time elapsed: 0.118 s
% 15.62/2.67 % (4045014)Peak memory usage: 14 MB
% 15.62/2.67 % (4045014)Instructions burned: 241 (million)
% 15.62/2.67 % (4045023)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=3504020164:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/314Mi)
% 16.56/2.87 % (4045021)Instruction limit reached!
% 16.56/2.87 % (4045021)------------------------------
% 16.56/2.87 % (4045021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.56/2.87 % (4045021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/2.87 % (4045021)CaDiCaL version: 2.1.3
% 16.56/2.87 % (4045021)Termination reason: Instruction limit
% 16.56/2.87 % (4045021)Termination phase: Saturation
% 16.56/2.87 % (4045021)Time elapsed: 0.099 s
% 16.56/2.87 % (4045021)Peak memory usage: 14 MB
% 16.56/2.87 % (4045021)Instructions burned: 356 (million)
% 16.56/2.87 % (4045025)lrs+10_1_sil=128000:e2e=on:si=on:cbe=off:uwa=interpreted_only:cs=on:random_seed=396324070:s2a=on:i=251:fsr=off:rtra=on_2979 on theBenchmark for (2979ds/251Mi)
% 16.56/2.87 % (4045019)Instruction limit reached!
% 16.56/2.87 % (4045019)------------------------------
% 16.56/2.87 % (4045019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.56/2.87 % (4045019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/2.87 % (4045019)CaDiCaL version: 2.1.3
% 16.56/2.87 % (4045019)Termination reason: Instruction limit
% 16.56/2.87 % (4045019)Termination phase: Saturation
% 16.56/2.87 % (4045019)Time elapsed: 0.189 s
% 16.56/2.87 % (4045019)Peak memory usage: 15 MB
% 16.56/2.87 % (4045019)Instructions burned: 391 (million)
% 16.56/2.87 % (4045027)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=1360773338:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=2470:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2979 on theBenchmark for (2979ds/2470Mi)
% 16.56/2.87 % (4045025)Instruction limit reached!
% 16.56/2.87 % (4045025)------------------------------
% 16.56/2.87 % (4045025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.56/2.87 % (4045025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/2.87 % (4045025)CaDiCaL version: 2.1.3
% 16.56/2.87 % (4045025)Termination reason: Instruction limit
% 16.56/2.87 % (4045025)Termination phase: Saturation
% 16.56/2.87 % (4045025)Time elapsed: 0.063 s
% 16.56/2.87 % (4045025)Peak memory usage: 14 MB
% 16.56/2.87 % (4045025)Instructions burned: 256 (million)
% 16.56/2.87 % (4045029)dis+10_6_sil=128000:si=on:sp=arity:bce=on:cbe=off:uwa=interpreted_only:slsqc=4:slsq=on:random_seed=3185394086:i=673:doe=on:fgj=on:piset=and:slsql=off:rtra=on:fdi=1024:ntd=on_2978 on theBenchmark for (2978ds/673Mi)
% 16.56/2.87 % (4045023)Instruction limit reached!
% 16.56/2.87 % (4045023)------------------------------
% 16.56/2.87 % (4045023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.56/2.87 % (4045023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/2.87 % (4045023)CaDiCaL version: 2.1.3
% 16.56/2.87 % (4045023)Termination reason: Instruction limit
% 16.56/2.87 % (4045023)Termination phase: Saturation
% 16.56/2.87 % (4045023)Time elapsed: 0.148 s
% 16.56/2.87 % (4045023)Peak memory usage: 15 MB
% 16.56/2.87 % (4045023)Instructions burned: 315 (million)
% 16.56/2.87 % (4045031)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2014769643:i=116:ep=RSTC:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/116Mi)
% 16.56/2.87 % (4045031)Instruction limit reached!
% 16.56/2.87 % (4045031)------------------------------
% 16.56/2.87 % (4045031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.56/2.87 % (4045031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/2.87 % (4045031)CaDiCaL version: 2.1.3
% 16.56/2.87 % (4045031)Termination reason: Instruction limit
% 16.56/2.87 % (4045031)Termination phase: Saturation
% 16.56/2.87 % (4045031)Time elapsed: 0.052 s
% 16.56/2.87 % (4045031)Peak memory usage: 13 MB
% 16.56/2.87 % (4045031)Instructions burned: 117 (million)
% 16.56/2.87 % (4045033)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2984367189:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2977 on theBenchmark for (2977ds/270Mi)
% 16.56/2.87 % (4045015)Instruction limit reached!
% 16.56/2.87 % (4045015)------------------------------
% 16.56/2.87 % (4045015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.56/2.87 % (4045015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/3.26 % (4045015)CaDiCaL version: 2.1.3
% 20.36/3.26 % (4045015)Termination reason: Instruction limit
% 20.36/3.26 % (4045015)Termination phase: Saturation
% 20.36/3.26 % (4045015)Time elapsed: 0.412 s
% 20.36/3.26 % (4045015)Peak memory usage: 16 MB
% 20.36/3.26 % (4045015)Instructions burned: 807 (million)
% 20.36/3.26 % (4045029)Instruction limit reached!
% 20.36/3.26 % (4045029)------------------------------
% 20.36/3.26 % (4045029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.36/3.26 % (4045029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/3.26 % (4045029)CaDiCaL version: 2.1.3
% 20.36/3.26 % (4045029)Termination reason: Instruction limit
% 20.36/3.26 % (4045029)Termination phase: Saturation
% 20.36/3.26 % (4045029)Time elapsed: 0.152 s
% 20.36/3.26 % (4045029)Peak memory usage: 15 MB
% 20.36/3.26 % (4045029)Instructions burned: 680 (million)
% 20.36/3.26 % (4045035)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=2489761592:hsq=on:hsqr=16,1:s2a=on:i=30:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2977 on theBenchmark for (2977ds/30Mi)
% 20.36/3.26 % (4045036)WARNING Broken Constraint: if sine_tolerance(12) has been set then sine_selection(off) is not equal to off
% 20.36/3.26 % (4045036)dis+1010_128_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=hol:nwc=2:flr=on:random_seed=2074490895:st=12:uwa_fpi=on:i=39:nm=40:ins=7:rtra=on_2976 on theBenchmark for (2976ds/39Mi)
% 20.36/3.26 % (4045035)Instruction limit reached!
% 20.36/3.26 % (4045035)------------------------------
% 20.36/3.26 % (4045035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.36/3.26 % (4045035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/3.26 % (4045035)CaDiCaL version: 2.1.3
% 20.36/3.26 % (4045035)Termination reason: Instruction limit
% 20.36/3.26 % (4045035)Termination phase: shuffling
% 20.36/3.26 % (4045035)Time elapsed: 0.015 s
% 20.36/3.26 % (4045035)Peak memory usage: 10 MB
% 20.36/3.26 % (4045035)Instructions burned: 32 (million)
% 20.36/3.26 % (4045036)Instruction limit reached!
% 20.36/3.26 % (4045036)------------------------------
% 20.36/3.26 % (4045036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.36/3.26 % (4045036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/3.26 % (4045036)CaDiCaL version: 2.1.3
% 20.36/3.26 % (4045036)Termination reason: Instruction limit
% 20.36/3.26 % (4045036)Termination phase: Property scanning
% 20.36/3.26 % (4045036)Time elapsed: 0.009 s
% 20.36/3.26 % (4045036)Peak memory usage: 10 MB
% 20.36/3.26 % (4045036)Instructions burned: 42 (million)
% 20.36/3.26 % (4045040)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=858923994:i=158:av=off:rtra=on_2976 on theBenchmark for (2976ds/158Mi)
% 20.36/3.26 % (4045039)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=394544439:i=365:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2976 on theBenchmark for (2976ds/365Mi)
% 20.36/3.26 % (4045040)Instruction limit reached!
% 20.36/3.26 % (4045040)------------------------------
% 20.36/3.26 % (4045040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.36/3.26 % (4045040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/3.26 % (4045040)CaDiCaL version: 2.1.3
% 20.36/3.26 % (4045040)Termination reason: Instruction limit
% 20.36/3.26 % (4045040)Termination phase: Saturation
% 20.36/3.26 % (4045040)Time elapsed: 0.039 s
% 20.36/3.26 % (4045040)Peak memory usage: 13 MB
% 20.36/3.26 % (4045040)Instructions burned: 161 (million)
% 20.36/3.26 % (4045033)Instruction limit reached!
% 20.36/3.26 % (4045033)------------------------------
% 20.36/3.26 % (4045033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.36/3.26 % (4045033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/3.26 % (4045033)CaDiCaL version: 2.1.3
% 20.36/3.26 % (4045033)Termination reason: Instruction limit
% 20.36/3.26 % (4045033)Termination phase: Saturation
% 20.36/3.26 % (4045033)Time elapsed: 0.134 s
% 20.36/3.26 % (4045033)Peak memory usage: 14 MB
% 20.36/3.26 % (4045033)Instructions burned: 272 (million)
% 20.36/3.26 % (4045043)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
% 20.36/3.26 % (4045043)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=3304058403:avsq=on:i=252:s2at=3:avsqr=1,16:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/252Mi)
% 21.80/3.41 % (4045044)lrs+10_1_cnfonf=off:si=on:sos=on:uwa=off:random_seed=3226708832:i=213:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/213Mi)
% 21.80/3.41 % (4045043)Instruction limit reached!
% 21.80/3.41 % (4045043)------------------------------
% 21.80/3.41 % (4045043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.80/3.41 % (4045043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/3.41 % (4045043)CaDiCaL version: 2.1.3
% 21.80/3.41 % (4045043)Termination reason: Instruction limit
% 21.80/3.41 % (4045043)Termination phase: Saturation
% 21.80/3.41 % (4045043)Time elapsed: 0.069 s
% 21.80/3.41 % (4045043)Peak memory usage: 14 MB
% 21.80/3.41 % (4045043)Instructions burned: 252 (million)
% 21.80/3.41 % (4045047)dis+1010_28_sil=128000:tgt=full:plsq=on:plsqc=1:cnfonf=off:si=on:plsqr=128,1:uwa=off:slsqc=2:sac=on:slsq=on:random_seed=2299549492:st=3:i=160:s2at=3:bd=preordered:nm=16:rtra=on:ss=axioms:ntd=on_2975 on theBenchmark for (2975ds/160Mi)
% 21.80/3.41 % (4045044)Instruction limit reached!
% 21.80/3.41 % (4045044)------------------------------
% 21.80/3.41 % (4045044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.80/3.41 % (4045044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/3.41 % (4045044)CaDiCaL version: 2.1.3
% 21.80/3.41 % (4045044)Termination reason: Instruction limit
% 21.80/3.41 % (4045044)Termination phase: Saturation
% 21.80/3.41 % (4045044)Time elapsed: 0.098 s
% 21.80/3.41 % (4045044)Peak memory usage: 14 MB
% 21.80/3.41 % (4045044)Instructions burned: 215 (million)
% 21.80/3.41 % (4045047)Instruction limit reached!
% 21.80/3.41 % (4045047)------------------------------
% 21.80/3.41 % (4045047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.80/3.41 % (4045047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/3.41 % (4045047)CaDiCaL version: 2.1.3
% 21.80/3.41 % (4045047)Termination reason: Instruction limit
% 21.80/3.41 % (4045047)Termination phase: Saturation
% 21.80/3.41 % (4045047)Time elapsed: 0.041 s
% 21.80/3.41 % (4045047)Peak memory usage: 13 MB
% 21.80/3.41 % (4045047)Instructions burned: 162 (million)
% 21.80/3.41 % (4045050)WARNING Broken Constraint: if ho_split_queue_layered_arrangement(off) has been set then ho_split_queue(off) is equal to on
% 21.80/3.41 % (4045050)ott+1010_40_sil=128000:tgt=full:plsq=on:plsqc=5:si=on:sos=all:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=1731481567:i=237:hsql=off:fgj=on:piset=all_but_not_eq:bd=preordered:av=off:rtra=on:ss=axioms:sgt=4:rawr=on_2974 on theBenchmark for (2974ds/237Mi)
% 21.80/3.41 % (4045049)lrs+1010_2:3_sil=128000:cnfonf=off:e2e=on:si=on:sp=unary_first:uwa=off:br=off:lftc=80:random_seed=1460890307:hsq=on:hsqr=16,1:i=763:kws=inv_frequency:piset=and:bd=all:rtra=on:ntd=on_2975 on theBenchmark for (2975ds/763Mi)
% 21.80/3.41 % (4045039)Instruction limit reached!
% 21.80/3.41 % (4045039)------------------------------
% 21.80/3.41 % (4045039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.80/3.41 % (4045039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/3.41 % (4045039)CaDiCaL version: 2.1.3
% 21.80/3.41 % (4045039)Termination reason: Instruction limit
% 21.80/3.41 % (4045039)Termination phase: Saturation
% 21.80/3.41 % (4045039)Time elapsed: 0.181 s
% 21.80/3.41 % (4045039)Peak memory usage: 14 MB
% 21.80/3.41 % (4045039)Instructions burned: 366 (million)
% 21.80/3.41 % (4045053)dis+1002_1_drc=ordering:cnfonf=lazy_not_gen_be_off:si=on:lma=off:cbe=off:uwa=off:random_seed=894989223:s2a=on:i=386:rtra=on:ntd=on_2974 on theBenchmark for (2974ds/386Mi)
% 21.80/3.41 % (4045050)Instruction limit reached!
% 21.80/3.41 % (4045050)------------------------------
% 21.80/3.41 % (4045050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.80/3.41 % (4045050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.80/3.41 % (4045050)CaDiCaL version: 2.1.3
% 21.80/3.41 % (4045050)Termination reason: Instruction limit
% 21.80/3.41 % (4045050)Termination phase: Saturation
% 21.80/3.41 % (4045050)Time elapsed: 0.060 s
% 21.80/3.41 % (4045050)Peak memory usage: 14 MB
% 21.80/3.41 % (4045050)Instructions burned: 240 (million)
% 21.80/3.41 % (4045055)dis+10_128_to=lpo:sil=128000:si=on:spb=intro:uwa=off:random_seed=1259825273:i=300:piset=and:nm=32:rtra=on_2974 on theBenchmark for (2974ds/300Mi)
% 22.88/3.67 % (4045055)Instruction limit reached!
% 22.88/3.67 % (4045055)------------------------------
% 22.88/3.67 % (4045055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.88/3.67 % (4045055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.88/3.67 % (4045055)CaDiCaL version: 2.1.3
% 22.88/3.67 % (4045055)Termination reason: Instruction limit
% 22.88/3.67 % (4045055)Termination phase: Saturation
% 22.88/3.67 % (4045055)Time elapsed: 0.079 s
% 22.88/3.67 % (4045055)Peak memory usage: 14 MB
% 22.88/3.67 % (4045055)Instructions burned: 302 (million)
% 22.88/3.67 % (4045057)dis+1010_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:urr=on:random_seed=80542859:st=5:s2a=on:i=567:sd=2:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/567Mi)
% 22.88/3.67 % (4045053)Instruction limit reached!
% 22.88/3.67 % (4045053)------------------------------
% 22.88/3.67 % (4045053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.88/3.67 % (4045053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.88/3.67 % (4045053)CaDiCaL version: 2.1.3
% 22.88/3.67 % (4045053)Termination reason: Instruction limit
% 22.88/3.67 % (4045053)Termination phase: Saturation
% 22.88/3.67 % (4045053)Time elapsed: 0.181 s
% 22.88/3.67 % (4045053)Peak memory usage: 15 MB
% 22.88/3.67 % (4045053)Instructions burned: 388 (million)
% 22.88/3.67 % (4045059)lrs+1010_1_si=on:uwa=one_side_interpreted:random_seed=3587467574:s2a=on:i=379:sd=1:rtra=on:ss=axioms:sgt=128_2972 on theBenchmark for (2972ds/379Mi)
% 22.88/3.67 % (4045057)Instruction limit reached!
% 22.88/3.67 % (4045057)------------------------------
% 22.88/3.67 % (4045057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.88/3.67 % (4045057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.88/3.67 % (4045057)CaDiCaL version: 2.1.3
% 22.88/3.67 % (4045057)Termination reason: Instruction limit
% 22.88/3.67 % (4045057)Termination phase: Saturation
% 22.88/3.67 % (4045057)Time elapsed: 0.150 s
% 22.88/3.67 % (4045057)Peak memory usage: 14 MB
% 22.88/3.67 % (4045057)Instructions burned: 570 (million)
% 22.88/3.67 % (4045061)dis+32_3_cha=on:sil=128000:drc=off:si=on:cbe=off:uwa=interpreted_only:nwc=3:random_seed=308638256:s2a=on:i=429:s2at=5:add=on:sd=2:ep=R:bd=preordered:rtra=on:ss=included:sgt=40_2971 on theBenchmark for (2971ds/429Mi)
% 22.88/3.67 % (4045049)Instruction limit reached!
% 22.88/3.67 % (4045049)------------------------------
% 22.88/3.67 % (4045049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.88/3.67 % (4045049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.88/3.67 % (4045049)CaDiCaL version: 2.1.3
% 22.88/3.67 % (4045049)Termination reason: Instruction limit
% 22.88/3.67 % (4045049)Termination phase: Saturation
% 22.88/3.67 % (4045049)Time elapsed: 0.336 s
% 22.88/3.67 % (4045049)Peak memory usage: 16 MB
% 22.88/3.67 % (4045049)Instructions burned: 764 (million)
% 22.88/3.67 % (4045063)ott+10_1_to=lpo:sil=128000:e2e=on:si=on:sos=on:uwa=off:sac=on:random_seed=4011402702:i=478:bd=all:rtra=on_2971 on theBenchmark for (2971ds/478Mi)
% 22.88/3.67 % (4045059)Instruction limit reached!
% 22.88/3.67 % (4045059)------------------------------
% 22.88/3.67 % (4045059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.88/3.67 % (4045059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.88/3.68 % (4045059)CaDiCaL version: 2.1.3
% 22.88/3.68 % (4045059)Termination reason: Instruction limit
% 22.88/3.68 % (4045059)Termination phase: Saturation
% 22.88/3.68 % (4045059)Time elapsed: 0.179 s
% 22.88/3.68 % (4045059)Peak memory usage: 15 MB
% 22.88/3.68 % (4045059)Instructions burned: 379 (million)
% 22.88/3.68 % (4045065)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2588786116:i=445:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2970 on theBenchmark for (2970ds/445Mi)
% 22.88/3.68 % (4045012)Instruction limit reached!
% 22.88/3.68 % (4045012)------------------------------
% 22.88/3.68 % (4045012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.88/3.68 % (4045012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.88/3.68 % (4045012)CaDiCaL version: 2.1.3
% 22.88/3.68 % (4045012)Termination reason: Instruction limit
% 22.88/3.68 % (4045012)Termination phase: Saturation
% 22.88/3.68 % (4045012)Time elapsed: 1.099 s
% 22.88/3.68 % (4045012)Peak memory usage: 20 MB
% 22.88/3.68 % (4045012)Instructions burned: 2186 (million)
% 22.88/3.68 % (4045061)Instruction limit reached!
% 22.88/3.68 % (4045061)------------------------------
% 23.99/3.85 % (4045061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.85 % (4045061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.85 % (4045061)CaDiCaL version: 2.1.3
% 23.99/3.85 % (4045061)Termination reason: Instruction limit
% 23.99/3.85 % (4045061)Termination phase: Saturation
% 23.99/3.85 % (4045061)Time elapsed: 0.124 s
% 23.99/3.85 % (4045061)Peak memory usage: 15 MB
% 23.99/3.85 % (4045061)Instructions burned: 431 (million)
% 23.99/3.85 % (4045067)ott+1003_1_to=kbo:cnfonf=lazy_pi_sigma_gen:si=on:sp=weighted_frequency:spb=units:urr=on:cbe=off:random_seed=2681793199:uwa_fpi=on:i=71:hud=10:rtra=on:ixr=off_2970 on theBenchmark for (2970ds/71Mi)
% 23.99/3.85 % (4045068)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4152973218:i=302:sd=2:bd=preordered:rtra=on:ss=axioms_2970 on theBenchmark for (2970ds/302Mi)
% 23.99/3.85 % (4045067)Instruction limit reached!
% 23.99/3.85 % (4045067)------------------------------
% 23.99/3.85 % (4045067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.85 % (4045067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.85 % (4045067)CaDiCaL version: 2.1.3
% 23.99/3.85 % (4045067)Termination reason: Instruction limit
% 23.99/3.85 % (4045067)Termination phase: Property scanning
% 23.99/3.85 % (4045067)Time elapsed: 0.030 s
% 23.99/3.85 % (4045067)Peak memory usage: 11 MB
% 23.99/3.85 % (4045067)Instructions burned: 72 (million)
% 23.99/3.85 % (4045071)lrs+10_1_sil=128000:fde=none:cnfonf=off:si=on:uwa=off:random_seed=1527183757:s2a=on:i=4980:sd=2:bd=all:rtra=on:ss=axioms:ntd=on_2969 on theBenchmark for (2969ds/4980Mi)
% 23.99/3.85 % (4045068)Instruction limit reached!
% 23.99/3.85 % (4045068)------------------------------
% 23.99/3.85 % (4045068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.85 % (4045068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.85 % (4045068)CaDiCaL version: 2.1.3
% 23.99/3.85 % (4045068)Termination reason: Instruction limit
% 23.99/3.85 % (4045068)Termination phase: Saturation
% 23.99/3.85 % (4045068)Time elapsed: 0.083 s
% 23.99/3.85 % (4045068)Peak memory usage: 14 MB
% 23.99/3.85 % (4045068)Instructions burned: 304 (million)
% 23.99/3.85 % (4045073)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
% 23.99/3.85 % (4045073)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 23.99/3.85 % (4045073)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2542403497:i=100:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2969 on theBenchmark for (2969ds/100Mi)
% 23.99/3.85 % (4045073)Instruction limit reached!
% 23.99/3.85 % (4045073)------------------------------
% 23.99/3.85 % (4045073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.85 % (4045073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.85 % (4045073)CaDiCaL version: 2.1.3
% 23.99/3.85 % (4045073)Termination reason: Instruction limit
% 23.99/3.85 % (4045073)Termination phase: Twee Goal Transformation
% 23.99/3.85 % (4045073)Time elapsed: 0.023 s
% 23.99/3.85 % (4045073)Peak memory usage: 11 MB
% 23.99/3.85 % (4045073)Instructions burned: 104 (million)
% 23.99/3.85 % (4045063)Instruction limit reached!
% 23.99/3.85 % (4045063)------------------------------
% 23.99/3.85 % (4045063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.85 % (4045063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.85 % (4045063)CaDiCaL version: 2.1.3
% 23.99/3.85 % (4045063)Termination reason: Instruction limit
% 23.99/3.85 % (4045063)Termination phase: Saturation
% 23.99/3.85 % (4045063)Time elapsed: 0.228 s
% 23.99/3.85 % (4045063)Peak memory usage: 15 MB
% 23.99/3.85 % (4045063)Instructions burned: 479 (million)
% 23.99/3.85 % (4045075)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=2998380372:i=76:piset=equals:rtra=on:ntd=on_2969 on theBenchmark for (2969ds/76Mi)
% 23.99/3.85 % (4045076)lrs+10_1_to=lpo:sil=128000:cnfonf=off:si=on:sp=unary_first:sos=all:spb=goal:uwa=off:random_seed=1066056086:i=289:rtra=on_2969 on theBenchmark for (2969ds/289Mi)
% 23.99/3.85 % (4045075)Instruction limit reached!
% 27.16/4.23 % (4045075)------------------------------
% 27.16/4.23 % (4045075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.16/4.23 % (4045075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.16/4.23 % (4045075)CaDiCaL version: 2.1.3
% 27.16/4.23 % (4045075)Termination reason: Instruction limit
% 27.16/4.23 % (4045075)Termination phase: Property scanning
% 27.16/4.23 % (4045075)Time elapsed: 0.018 s
% 27.16/4.23 % (4045075)Peak memory usage: 11 MB
% 27.16/4.23 % (4045075)Instructions burned: 80 (million)
% 27.16/4.23 % (4045079)lrs+2_64_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_first:bsr=unit_only:cbe=off:uwa=interpreted_only:nwc=0.5:slsqc=5:sac=on:slsq=on:random_seed=3626675618:i=493:s2at=5:kws=frequency:doe=on:rtra=on:er=known_2968 on theBenchmark for (2968ds/493Mi)
% 27.16/4.23 % (4045065)Instruction limit reached!
% 27.16/4.23 % (4045065)------------------------------
% 27.16/4.23 % (4045065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.16/4.23 % (4045065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.16/4.23 % (4045065)CaDiCaL version: 2.1.3
% 27.16/4.23 % (4045065)Termination reason: Instruction limit
% 27.16/4.23 % (4045065)Termination phase: Saturation
% 27.16/4.23 % (4045065)Time elapsed: 0.227 s
% 27.16/4.23 % (4045065)Peak memory usage: 15 MB
% 27.16/4.23 % (4045065)Instructions burned: 445 (million)
% 27.16/4.23 % (4045081)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=1342633486:cond=on:i=34:hud=10:nm=10:rtra=on_2968 on theBenchmark for (2968ds/34Mi)
% 27.16/4.23 % (4045081)Instruction limit reached!
% 27.16/4.23 % (4045081)------------------------------
% 27.16/4.23 % (4045081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.16/4.23 % (4045081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.16/4.23 % (4045081)CaDiCaL version: 2.1.3
% 27.16/4.23 % (4045081)Termination reason: Instruction limit
% 27.16/4.23 % (4045081)Termination phase: Property scanning
% 27.16/4.23 % (4045081)Time elapsed: 0.015 s
% 27.16/4.23 % (4045081)Peak memory usage: 10 MB
% 27.16/4.23 % (4045081)Instructions burned: 34 (million)
% 27.16/4.23 % (4045083)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 27.16/4.23 % (4045083)dis+1010_1_to=lpo:irw=on:plsq=on:drc=ordering:plsqc=4:cnfonf=lazy_simp:si=on:sp=reverse_frequency:sos=on:plsqr=32,1:cbe=off:uwa=off:rp=on:lwlo=on:random_seed=2687951434:i=372:add=off:piset=or:nm=10:fsr=off:rtra=on:c=on_2967 on theBenchmark for (2967ds/372Mi)
% 27.16/4.23 % (4045076)Instruction limit reached!
% 27.16/4.23 % (4045076)------------------------------
% 27.16/4.23 % (4045076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.16/4.23 % (4045076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.16/4.23 % (4045076)CaDiCaL version: 2.1.3
% 27.16/4.23 % (4045076)Termination reason: Instruction limit
% 27.16/4.23 % (4045076)Termination phase: Saturation
% 27.16/4.23 % (4045076)Time elapsed: 0.144 s
% 27.16/4.23 % (4045076)Peak memory usage: 14 MB
% 27.16/4.23 % (4045076)Instructions burned: 291 (million)
% 27.16/4.23 % (4045085)lrs+1002_1024_sil=128000:tgt=ground:e2e=on:si=on:uwa=interpreted_only:fd=off:nwc=1:random_seed=2845732060:cts=off:avsq=on:i=670:avsqr=1,16:nm=16:rtra=on_2967 on theBenchmark for (2967ds/670Mi)
% 27.16/4.23 % (4045027)Instruction limit reached!
% 27.16/4.23 % (4045027)------------------------------
% 27.16/4.23 % (4045027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.16/4.23 % (4045027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.16/4.23 % (4045027)CaDiCaL version: 2.1.3
% 27.16/4.23 % (4045027)Termination reason: Instruction limit
% 27.16/4.23 % (4045027)Termination phase: Saturation
% 27.16/4.23 % (4045027)Time elapsed: 1.256 s
% 27.16/4.23 % (4045027)Peak memory usage: 19 MB
% 27.16/4.23 % (4045027)Instructions burned: 2471 (million)
% 27.16/4.23 % (4045087)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3203848980:hsq=on:st=2:i=647:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2966 on theBenchmark for (2966ds/647Mi)
% 27.16/4.23 % (4045079)Instruction limit reached!
% 27.16/4.23 % (4045079)------------------------------
% 27.16/4.23 % (4045079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.16/4.23 % (4045079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.35 % (4045079)CaDiCaL version: 2.1.3
% 27.89/4.35 % (4045079)Termination reason: Instruction limit
% 27.89/4.35 % (4045079)Termination phase: Saturation
% 27.89/4.35 % (4045079)Time elapsed: 0.241 s
% 27.89/4.35 % (4045079)Peak memory usage: 15 MB
% 27.89/4.35 % (4045079)Instructions burned: 493 (million)
% 27.89/4.35 % (4045083)Instruction limit reached!
% 27.89/4.35 % (4045083)------------------------------
% 27.89/4.35 % (4045083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.35 % (4045083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.35 % (4045083)CaDiCaL version: 2.1.3
% 27.89/4.35 % (4045083)Termination reason: Instruction limit
% 27.89/4.35 % (4045083)Termination phase: Saturation
% 27.89/4.35 % (4045083)Time elapsed: 0.177 s
% 27.89/4.35 % (4045083)Peak memory usage: 16 MB
% 27.89/4.35 % (4045083)Instructions burned: 372 (million)
% 27.89/4.35 % (4045089)dis+10_128_sil=128000:tgt=full:plsq=on:plsqc=3:cnfonf=off:si=on:sp=arity:spb=goal_then_units:uwa=one_side_interpreted:nwc=1.5:random_seed=2370016381:i=857:add=off:kws=frequency:rtra=on:ntd=on_2966 on theBenchmark for (2966ds/857Mi)
% 27.89/4.35 % (4045090)dis+1010_4_anc=all_dependent:to=lpo:sil=128000:fde=unused:cnfonf=conj_eager:si=on:sp=reverse_frequency:lma=off:spb=intro:cbe=off:uwa=off:random_seed=3950581075:i=693:add=off:fsr=off:rtra=on:fe=abstraction:ntd=on_2966 on theBenchmark for (2966ds/693Mi)
% 27.89/4.35 % (4045085)Instruction limit reached!
% 27.89/4.35 % (4045085)------------------------------
% 27.89/4.35 % (4045085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.35 % (4045085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.35 % (4045085)CaDiCaL version: 2.1.3
% 27.89/4.35 % (4045085)Termination reason: Instruction limit
% 27.89/4.35 % (4045085)Termination phase: Saturation
% 27.89/4.35 % (4045085)Time elapsed: 0.161 s
% 27.89/4.35 % (4045085)Peak memory usage: 14 MB
% 27.89/4.35 % (4045085)Instructions burned: 670 (million)
% 27.89/4.35 % (4045093)dis+10_7_sil=128000:cnfonf=lazy_gen:si=on:sos=on:random_seed=1504586191:i=285:hud=10:bd=all:rtra=on:ss=axioms_2965 on theBenchmark for (2965ds/285Mi)
% 27.89/4.35 % (4045093)Instruction limit reached!
% 27.89/4.35 % (4045093)------------------------------
% 27.89/4.35 % (4045093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.35 % (4045093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.35 % (4045093)CaDiCaL version: 2.1.3
% 27.89/4.35 % (4045093)Termination reason: Instruction limit
% 27.89/4.35 % (4045093)Termination phase: Saturation
% 27.89/4.35 % (4045093)Time elapsed: 0.075 s
% 27.89/4.35 % (4045093)Peak memory usage: 14 MB
% 27.89/4.35 % (4045093)Instructions burned: 287 (million)
% 27.89/4.35 % (4045095)WARNING Broken Constraint: if ho_split_queue_ratios(23,10) has been set then ho_split_queue(off) is equal to on
% 27.89/4.35 % (4045095)dis+1002_50_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=1:si=on:sp=occurrence:plsqr=64,1:nwc=3:flr=on:chr=on:random_seed=1926055851:hsqr=23,10:uwa_fpi=on:i=52:kws=frequency:hud=15:fsr=off:rtra=on:amm=off:ntd=on:rawr=on_2964 on theBenchmark for (2964ds/52Mi)
% 27.89/4.35 % (4044928)Instruction limit reached!
% 27.89/4.35 % (4044928)------------------------------
% 27.89/4.35 % (4044928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.35 % (4044928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4044928)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4044928)Termination reason: Instruction limit
% 27.89/4.36 % (4044928)Termination phase: Saturation
% 27.89/4.36 % (4044928)Time elapsed: 2.803 s
% 27.89/4.36 % (4044928)Peak memory usage: 28 MB
% 27.89/4.36 % (4044928)Instructions burned: 5756 (million)
% 27.89/4.36 % (4045095)Instruction limit reached!
% 27.89/4.36 % (4045095)------------------------------
% 27.89/4.36 % (4045095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045095)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045095)Termination reason: Instruction limit
% 27.89/4.36 % (4045095)Termination phase: Property scanning
% 27.89/4.36 % (4045095)Time elapsed: 0.013 s
% 27.89/4.36 % (4045095)Peak memory usage: 11 MB
% 27.89/4.36 % (4045095)Instructions burned: 56 (million)
% 27.89/4.36 % (4045097)dis+10_1_si=on:random_seed=3856434500:i=407:sd=4:rtra=on:ss=axioms:sgt=20_2964 on theBenchmark for (2964ds/407Mi)
% 27.89/4.36 % (4045098)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=2627462175:i=2240:bs=unit_only:ins=25:rtra=on:ntd=on_2964 on theBenchmark for (2964ds/2240Mi)
% 27.89/4.36 % (4045097)Instruction limit reached!
% 27.89/4.36 % (4045097)------------------------------
% 27.89/4.36 % (4045097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045097)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045097)Termination reason: Instruction limit
% 27.89/4.36 % (4045097)Termination phase: Saturation
% 27.89/4.36 % (4045097)Time elapsed: 0.107 s
% 27.89/4.36 % (4045097)Peak memory usage: 14 MB
% 27.89/4.36 % (4045097)Instructions burned: 411 (million)
% 27.89/4.36 % (4045101)lrs+10_1_sil=128000:e2e=on:si=on:uwa=interpreted_only:random_seed=758569407:st=2:i=336:sd=1:rtra=on:ss=axioms:ntd=on_2963 on theBenchmark for (2963ds/336Mi)
% 27.89/4.36 % (4045087)Instruction limit reached!
% 27.89/4.36 % (4045087)------------------------------
% 27.89/4.36 % (4045087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045087)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045087)Termination reason: Instruction limit
% 27.89/4.36 % (4045087)Termination phase: Saturation
% 27.89/4.36 % (4045087)Time elapsed: 0.328 s
% 27.89/4.36 % (4045087)Peak memory usage: 15 MB
% 27.89/4.36 % (4045087)Instructions burned: 647 (million)
% 27.89/4.36 % (4045103)lrs+10_1_to=lpo:sil=128000:fde=none:cnfonf=off:si=on:sp=unary_first:urr=on:uwa=one_side_constant:random_seed=2119724666:s2a=on:i=1142:s2at=3:bd=all:rtra=on_2962 on theBenchmark for (2962ds/1142Mi)
% 27.89/4.36 % (4045090)Instruction limit reached!
% 27.89/4.36 % (4045090)------------------------------
% 27.89/4.36 % (4045090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045090)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045090)Termination reason: Instruction limit
% 27.89/4.36 % (4045090)Termination phase: Saturation
% 27.89/4.36 % (4045090)Time elapsed: 0.323 s
% 27.89/4.36 % (4045090)Peak memory usage: 16 MB
% 27.89/4.36 % (4045090)Instructions burned: 694 (million)
% 27.89/4.36 % (4045105)dis+1002_1_sil=128000:si=on:uwa=off:random_seed=2390733772:st=3:i=376:sd=4:rtra=on:ss=axioms:ntd=on_2962 on theBenchmark for (2962ds/376Mi)
% 27.89/4.36 % (4045101)Instruction limit reached!
% 27.89/4.36 % (4045101)------------------------------
% 27.89/4.36 % (4045101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045101)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045101)Termination reason: Instruction limit
% 27.89/4.36 % (4045101)Termination phase: Saturation
% 27.89/4.36 % (4045101)Time elapsed: 0.085 s
% 27.89/4.36 % (4045101)Peak memory usage: 15 MB
% 27.89/4.36 % (4045101)Instructions burned: 337 (million)
% 27.89/4.36 % (4045107)dis+1002_4:1_anc=none:sil=128000:sas=cadical:si=on:sp=weighted_frequency:sos=on:uwa=one_side_interpreted:random_seed=71421182:i=766:bd=all:rtra=on_2962 on theBenchmark for (2962ds/766Mi)
% 27.89/4.36 % (4045089)Instruction limit reached!
% 27.89/4.36 % (4045089)------------------------------
% 27.89/4.36 % (4045089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045089)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045089)Termination reason: Instruction limit
% 27.89/4.36 % (4045089)Termination phase: Saturation
% 27.89/4.36 % (4045089)Time elapsed: 0.399 s
% 27.89/4.36 % (4045089)Peak memory usage: 15 MB
% 27.89/4.36 % (4045089)Instructions burned: 857 (million)
% 27.89/4.36 % (4045109)WARNING Broken Constraint: if avatar_split_queue_cutoffs(4) has been set then avatar_split_queue(off) is equal to on
% 27.89/4.36 % (4045109)lrs+10_1_to=kbo:si=on:sp=const_frequency:sos=on:spb=non_intro:uwa=hol:avsqc=4:random_seed=2552391894:st=3:uwa_fpi=on:i=959:fgj=on:piset=pi_sigma:hud=5:nm=16:rtra=on:fe=abstraction:ss=axioms:ixr=off:ntd=on_2961 on theBenchmark for (2961ds/959Mi)
% 27.89/4.36 % (4045105)Instruction limit reached!
% 27.89/4.36 % (4045105)------------------------------
% 27.89/4.36 % (4045105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045105)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045105)Termination reason: Instruction limit
% 27.89/4.36 % (4045105)Termination phase: Saturation
% 27.89/4.36 % (4045105)Time elapsed: 0.183 s
% 27.89/4.36 % (4045105)Peak memory usage: 14 MB
% 27.89/4.36 % (4045105)Instructions burned: 377 (million)
% 27.89/4.36 % (4045111)dis+1010_1024_sil=128000:plsq=on:plsqc=1:e2e=on:si=on:lma=off:plsqr=64,1:uwa=interpreted_only:fd=off:random_seed=2680029589:i=6359:add=on:kws=inv_frequency:aac=none:rtra=on:c=on:er=filter:ntd=on_2960 on theBenchmark for (2960ds/6359Mi)
% 27.89/4.36 % (4045107)Instruction limit reached!
% 27.89/4.36 % (4045107)------------------------------
% 27.89/4.36 % (4045107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045107)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045107)Termination reason: Instruction limit
% 27.89/4.36 % (4045107)Termination phase: Saturation
% 27.89/4.36 % (4045107)Time elapsed: 0.198 s
% 27.89/4.36 % (4045107)Peak memory usage: 16 MB
% 27.89/4.36 % (4045107)Instructions burned: 768 (million)
% 27.89/4.36 % (4045113)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=570442957:st=4:i=35:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2960 on theBenchmark for (2960ds/35Mi)
% 27.89/4.36 % (4045113)Instruction limit reached!
% 27.89/4.36 % (4045113)------------------------------
% 27.89/4.36 % (4045113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045113)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045113)Termination reason: Instruction limit
% 27.89/4.36 % (4045113)Termination phase: Property scanning
% 27.89/4.36 % (4045113)Time elapsed: 0.008 s
% 27.89/4.36 % (4045113)Peak memory usage: 10 MB
% 27.89/4.36 % (4045113)Instructions burned: 38 (million)
% 27.89/4.36 % (4045115)dis+10_1_sfv=off:sil=128000:cnfonf=lazy_gen:si=on:uwa=off:nwc=1:chr=on:random_seed=1172749996:hsq=on:hsqr=1,8:i=53:hsql=off:bd=all:rtra=on:ixr=off_2960 on theBenchmark for (2960ds/53Mi)
% 27.89/4.36 % (4045115)Instruction limit reached!
% 27.89/4.36 % (4045115)------------------------------
% 27.89/4.36 % (4045115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045115)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045115)Termination reason: Instruction limit
% 27.89/4.36 % (4045115)Termination phase: Property scanning
% 27.89/4.36 % (4045115)Time elapsed: 0.013 s
% 27.89/4.36 % (4045115)Peak memory usage: 10 MB
% 27.89/4.36 % (4045115)Instructions burned: 58 (million)
% 27.89/4.36 % (4045117)dis+21_1_sil=128000:tgt=full:fde=none:e2e=on:si=on:urr=on:uwa=interpreted_only:s2agt=32:sac=on:random_seed=4267018261:s2a=on:i=876:s2at=6:nm=2:rtra=on_2959 on theBenchmark for (2959ds/876Mi)
% 27.89/4.36 % (4045103) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4044789-4045103"...
% 27.89/4.36 % (4045103)...printing done.
% 27.89/4.36 % (4045103)Refutation found. Thanks to Tanya!
% 27.89/4.36 % SZS status Theorem for theBenchmark
% 27.89/4.36 % SZS output start Proof for theBenchmark
% 27.89/4.36 thf(type_def_5, type, real: $tType).
% 27.89/4.36 thf(type_def_6, type, set: $tType > $tType).
% 27.89/4.36 thf(type_def_7, type, a: $tType).
% 27.89/4.36 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 27.89/4.36 thf(func_def_0, type, execut510477386_space: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_1, type, type: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_2, type, zero: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_3, type, order: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_4, type, group_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_5, type, monoid_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_6, type, ab_group_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_7, type, semigroup_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_8, type, comm_monoid_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_9, type, ab_semigroup_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_10, type, comm_monoid_diff: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_11, type, cancel_semigroup_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_12, type, ordered_ab_group_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_13, type, cancel1352612707id_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_14, type, cancel146912293up_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_15, type, linord219039673up_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_16, type, ordere216010020id_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_17, type, ordere779506340up_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_18, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_19, type, strict797366125id_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_20, type, ordere236663937imp_le: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_21, type, ordere223160158up_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_22, type, strict2144017051up_add: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_23, type, ordere516151231imp_le: !>[X0: $tType]:($o)).
% 27.89/4.36 thf(func_def_24, type, auto_l1112008849e_ivl0: !>[X0: $tType]:(((X0 > X0) > set @ X0 > X0 > set @ real))).
% 27.89/4.36 thf(func_def_25, type, auto_ll_on_flow0: !>[X0: $tType]:(((X0 > X0) > set @ X0 > X0 > real > X0))).
% 27.89/4.36 thf(func_def_26, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 27.89/4.36 thf(func_def_27, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 27.89/4.36 thf(func_def_28, type, uminus_uminus: !>[X0: $tType]:((X0 > X0))).
% 27.89/4.36 thf(func_def_29, type, zero_zero: !>[X0: $tType]:(X0)).
% 27.89/4.36 thf(func_def_30, type, initia826609931terval: (set @ real > $o)).
% 27.89/4.36 thf(func_def_31, type, bot_bot: !>[X0: $tType]:(X0)).
% 27.89/4.36 thf(func_def_32, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 27.89/4.36 thf(func_def_33, type, top_top: !>[X0: $tType]:(X0)).
% 27.89/4.36 thf(func_def_34, type, period385816147_orbit: !>[X0: $tType]:(((X0 > X0) > set @ X0 > X0 > $o))).
% 27.89/4.36 thf(func_def_35, type, period1153813292period: !>[X0: $tType]:(((X0 > X0) > set @ X0 > X0 > real))).
% 27.89/4.36 thf(func_def_36, type, period862636932_orbit: !>[X0: $tType]:(((X0 > X0) > set @ X0 > X0 > $o))).
% 27.89/4.36 thf(func_def_37, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 27.89/4.36 thf(func_def_38, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 27.89/4.36 thf(func_def_39, type, x: set @ a).
% 27.89/4.36 thf(func_def_40, type, d: real).
% 27.89/4.36 thf(func_def_41, type, f: (a > a)).
% 27.89/4.36 thf(func_def_42, type, i1: real).
% 27.89/4.36 thf(func_def_43, type, i2: real).
% 27.89/4.36 thf(func_def_44, type, ss: real).
% 27.89/4.36 thf(func_def_45, type, t: real).
% 27.89/4.36 thf(func_def_46, type, tt: real).
% 27.89/4.36 thf(func_def_47, type, x2: a).
% 27.89/4.36 thf(func_def_48, type, xx: a).
% 27.89/4.36 thf(func_def_52, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 27.89/4.36 thf(func_def_53, type, db0: !>[X0: $tType]:(X0)).
% 27.89/4.36 thf(func_def_54, type, db1: !>[X0: $tType]:(X0)).
% 27.89/4.36 thf(func_def_55, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 27.89/4.36 thf(func_def_56, type, vOR: ($o > $o > $o)).
% 27.89/4.36 thf(func_def_57, type, vNOT: ($o > $o)).
% 27.89/4.36 thf(func_def_58, type, vAND: ($o > $o > $o)).
% 27.89/4.36 thf(func_def_59, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 27.89/4.36 thf(func_def_60, type, sK0: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 27.89/4.36 thf(func_def_61, type, sK1: (a > real)).
% 27.89/4.36 thf(func_def_62, type, sK2: (set @ a > (a > a) > a)).
% 27.89/4.36 thf(func_def_63, type, sK3: a).
% 27.89/4.36 thf(func_def_64, type, sK4: !>[X0: $tType]:((X0 > X0 > X0))).
% 27.89/4.36 thf(func_def_65, type, sK5: (set @ a > (a > a) > a)).
% 27.89/4.36 thf(func_def_66, type, sK6: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 27.89/4.36 thf(func_def_67, type, sK7: a).
% 27.89/4.36 thf(func_def_68, type, sK8: ((a > a) > set @ a > a)).
% 27.89/4.36 thf(func_def_69, type, sK9: a).
% 27.89/4.36 thf(func_def_70, type, sK10: a).
% 27.89/4.36 thf(func_def_71, type, sK11: ((a > a) > set @ a > a)).
% 27.89/4.36 thf(func_def_72, type, sK12: (a > real)).
% 27.89/4.36 thf(f3,axiom,(
% 27.89/4.36 (((auto_ll_on_flow0 @ a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ ss)))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_eq)).
% 27.89/4.36 thf(f5,axiom,(
% 27.89/4.36 (member @ real @ tt @ (auto_l1112008849e_ivl0 @ a @ f @ x @ xx))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_tt__ex)).
% 27.89/4.36 thf(f6,axiom,(
% 27.89/4.36 (member @ real @ ss @ (auto_l1112008849e_ivl0 @ a @ f @ x @ x2))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_ss__ex)).
% 27.89/4.36 thf(f31,axiom,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0] : (((minus_minus @ X0 @ zero_zero @ X0 @ X1)) = ((uminus_uminus @ X0 @ X1))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_diff__0)).
% 27.89/4.36 thf(f34,axiom,(
% 27.89/4.36 ! [X0 : real,X1 : a] : ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1)) => (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ (minus_minus @ real @ zero_zero @ real @ X0))) = X1))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_local_Oflows__reverse)).
% 27.89/4.36 thf(f35,axiom,(
% 27.89/4.36 ! [X1 : a,X0 : real] : ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1)) => (member @ real @ (minus_minus @ real @ zero_zero @ real @ X0) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_local_Oexistence__ivl__reverse)).
% 27.89/4.36 thf(f42,axiom,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0] : (((uminus_uminus @ X0 @ (uminus_uminus @ X0 @ X1))) = X1))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_add_Oinverse__inverse)).
% 27.89/4.36 thf(f104,axiom,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X2 : X0,X1 : X0] : (((uminus_uminus @ X0 @ (minus_minus @ X0 @ X1 @ X2))) = ((minus_minus @ X0 @ X2 @ X1))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_minus__diff__eq)).
% 27.89/4.36 thf(f140,axiom,(
% 27.89/4.36 ! [X0 : real,X2 : real,X1 : a] : ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1)) => ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0))) => (((auto_ll_on_flow0 @ a @ f @ x @ X1 @ (plus_plus @ real @ X0 @ X2))) = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ X2)))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_local_Oflow__trans)).
% 27.89/4.36 thf(f142,axiom,(
% 27.89/4.36 ! [X1 : a,X2 : real,X0 : real] : ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1)) => ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0))) => (member @ real @ (plus_plus @ real @ X0 @ X2) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_local_Oexistence__ivl__trans)).
% 27.89/4.36 thf(f197,axiom,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0,X2 : X0] : (((minus_minus @ X0 @ X1 @ (uminus_uminus @ X0 @ X2))) = ((plus_plus @ X0 @ X1 @ X2))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_diff__minus__eq__add)).
% 27.89/4.36 thf(f301,axiom,(
% 27.89/4.36 group_add @ real),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ogroup__add)).
% 27.89/4.36 thf(f305,conjecture,(
% 27.89/4.36 (xx = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (minus_minus @ real @ ss @ tt))))),
% 27.89/4.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 27.89/4.36 thf(f306,negated_conjecture,(
% 27.89/4.36 ~ (xx = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (minus_minus @ real @ ss @ tt))))),
% 27.89/4.36 inference(negated_conjecture,[status(cth)],[f305])).
% 27.89/4.36 thf(f378,plain,(
% 27.89/4.36 (member @ real @ tt @ (auto_l1112008849e_ivl0 @ a @ f @ x @ xx))),
% 27.89/4.36 inference(rectify,[],[f5])).
% 27.89/4.36 thf(f379,plain,(
% 27.89/4.36 (((member @ real @ tt @ (auto_l1112008849e_ivl0 @ a @ f @ x @ xx))) = $true)),
% 27.89/4.36 inference(fool_elimination,[],[f378])).
% 27.89/4.36 thf(f407,plain,(
% 27.89/4.36 ! [X0 : a,X1 : real] : ((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)) => (member @ real @ (minus_minus @ real @ zero_zero @ real @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X1))))),
% 27.89/4.36 inference(rectify,[],[f35])).
% 27.89/4.36 thf(f408,plain,(
% 27.89/4.36 ! [X1 : real,X0 : a] : ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) = $true) => ($true = ((member @ real @ (minus_minus @ real @ zero_zero @ real @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X1))))))),
% 27.89/4.36 inference(fool_elimination,[],[f407])).
% 27.89/4.36 thf(f427,plain,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0] : (((minus_minus @ X0 @ zero_zero @ X0 @ X1)) = ((uminus_uminus @ X0 @ X1))))),
% 27.89/4.36 inference(rectify,[],[f31])).
% 27.89/4.36 thf(f428,plain,(
% 27.89/4.36 ! [X0 : $tType] : ((group_add @ X0 = $true) => ! [X1 : X0] : (((minus_minus @ X0 @ zero_zero @ X0 @ X1)) = ((uminus_uminus @ X0 @ X1))))),
% 27.89/4.36 inference(fool_elimination,[],[f427])).
% 27.89/4.36 thf(f556,plain,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0,X2 : X0] : (((minus_minus @ X0 @ X1 @ X2)) = ((uminus_uminus @ X0 @ (minus_minus @ X0 @ X2 @ X1)))))),
% 27.89/4.36 inference(rectify,[],[f104])).
% 27.89/4.36 thf(f557,plain,(
% 27.89/4.36 ! [X0 : $tType] : ((group_add @ X0 = $true) => ! [X2 : X0,X1 : X0] : (((minus_minus @ X0 @ X1 @ X2)) = ((uminus_uminus @ X0 @ (minus_minus @ X0 @ X2 @ X1)))))),
% 27.89/4.36 inference(fool_elimination,[],[f556])).
% 27.89/4.36 thf(f594,plain,(
% 27.89/4.36 ! [X0 : real,X1 : a] : ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1)) => (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ (minus_minus @ real @ zero_zero @ real @ X0))) = X1))),
% 27.89/4.36 inference(rectify,[],[f34])).
% 27.89/4.36 thf(f595,plain,(
% 27.89/4.36 ! [X1 : a,X0 : real] : ((((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1))) = $true) => (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ (minus_minus @ real @ zero_zero @ real @ X0))) = X1))),
% 27.89/4.36 inference(fool_elimination,[],[f594])).
% 27.89/4.36 thf(f674,plain,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0] : (((uminus_uminus @ X0 @ (uminus_uminus @ X0 @ X1))) = X1))),
% 27.89/4.36 inference(rectify,[],[f42])).
% 27.89/4.36 thf(f675,plain,(
% 27.89/4.36 ! [X0 : $tType] : ((group_add @ X0 = $true) => ! [X1 : X0] : (((uminus_uminus @ X0 @ (uminus_uminus @ X0 @ X1))) = X1))),
% 27.89/4.36 inference(fool_elimination,[],[f674])).
% 27.89/4.36 thf(f676,plain,(
% 27.89/4.36 ~ (xx = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (minus_minus @ real @ ss @ tt))))),
% 27.89/4.36 inference(fool_elimination,[],[f306])).
% 27.89/4.36 thf(f703,plain,(
% 27.89/4.36 ! [X0 : real,X1 : real,X2 : a] : ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2)) => ((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0))) => (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0) @ X1)) = ((auto_ll_on_flow0 @ a @ f @ x @ X2 @ (plus_plus @ real @ X0 @ X1))))))),
% 27.89/4.36 inference(rectify,[],[f140])).
% 27.89/4.36 thf(f704,plain,(
% 27.89/4.36 ! [X1 : real,X0 : real,X2 : a] : ((((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) = $true) => ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0)))) = $true) => (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0) @ X1)) = ((auto_ll_on_flow0 @ a @ f @ x @ X2 @ (plus_plus @ real @ X0 @ X1))))))),
% 27.89/4.36 inference(fool_elimination,[],[f703])).
% 27.89/4.36 thf(f735,plain,(
% 27.89/4.36 (((auto_ll_on_flow0 @ a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ ss)))),
% 27.89/4.36 inference(fool_elimination,[],[f3])).
% 27.89/4.36 thf(f756,plain,(
% 27.89/4.36 group_add @ real),
% 27.89/4.36 inference(rectify,[],[f301])).
% 27.89/4.36 thf(f757,plain,(
% 27.89/4.36 (group_add @ real = $true)),
% 27.89/4.36 inference(fool_elimination,[],[f756])).
% 27.89/4.36 thf(f774,plain,(
% 27.89/4.36 (member @ real @ ss @ (auto_l1112008849e_ivl0 @ a @ f @ x @ x2))),
% 27.89/4.36 inference(rectify,[],[f6])).
% 27.89/4.36 thf(f775,plain,(
% 27.89/4.36 (((member @ real @ ss @ (auto_l1112008849e_ivl0 @ a @ f @ x @ x2))) = $true)),
% 27.89/4.36 inference(fool_elimination,[],[f774])).
% 27.89/4.36 thf(f808,plain,(
% 27.89/4.36 ! [X0 : $tType] : (group_add @ X0 => ! [X1 : X0,X2 : X0] : (((minus_minus @ X0 @ X1 @ (uminus_uminus @ X0 @ X2))) = ((plus_plus @ X0 @ X1 @ X2))))),
% 27.89/4.36 inference(rectify,[],[f197])).
% 27.89/4.36 thf(f809,plain,(
% 27.89/4.36 ! [X0 : $tType] : ((group_add @ X0 = $true) => ! [X2 : X0,X1 : X0] : (((plus_plus @ X0 @ X1 @ X2)) = ((minus_minus @ X0 @ X1 @ (uminus_uminus @ X0 @ X2)))))),
% 27.89/4.36 inference(fool_elimination,[],[f808])).
% 27.89/4.36 thf(f878,plain,(
% 27.89/4.36 ! [X0 : a,X1 : real,X2 : real] : ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)) => ((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2))) => (member @ real @ (plus_plus @ real @ X2 @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))))),
% 27.89/4.36 inference(rectify,[],[f142])).
% 27.89/4.36 thf(f879,plain,(
% 27.89/4.36 ! [X1 : real,X0 : a,X2 : real] : (($true = ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)))) => ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2)))) = $true) => (((member @ real @ (plus_plus @ real @ X2 @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) = $true)))),
% 27.89/4.36 inference(fool_elimination,[],[f878])).
% 27.89/4.36 thf(f919,plain,(
% 27.89/4.36 (xx != ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (minus_minus @ real @ ss @ tt))))),
% 27.89/4.36 inference(flattening,[],[f676])).
% 27.89/4.36 thf(f926,plain,(
% 27.89/4.36 ! [X0 : $tType] : (! [X1 : X0] : (((uminus_uminus @ X0 @ (uminus_uminus @ X0 @ X1))) = X1) | (group_add @ X0 != $true))),
% 27.89/4.36 inference(ennf_transformation,[],[f675])).
% 27.89/4.36 thf(f1024,plain,(
% 27.89/4.36 ! [X0 : $tType] : (! [X2 : X0,X1 : X0] : (((plus_plus @ X0 @ X1 @ X2)) = ((minus_minus @ X0 @ X1 @ (uminus_uminus @ X0 @ X2)))) | (group_add @ X0 != $true))),
% 27.89/4.36 inference(ennf_transformation,[],[f809])).
% 27.89/4.36 thf(f1074,plain,(
% 27.89/4.36 ! [X0 : real,X1 : a] : ((((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1))) != $true) | (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ (minus_minus @ real @ zero_zero @ real @ X0))) = X1))),
% 27.89/4.36 inference(ennf_transformation,[],[f595])).
% 27.89/4.36 thf(f1173,plain,(
% 27.89/4.36 ! [X0 : $tType] : ((group_add @ X0 != $true) | ! [X2 : X0,X1 : X0] : (((minus_minus @ X0 @ X1 @ X2)) = ((uminus_uminus @ X0 @ (minus_minus @ X0 @ X2 @ X1)))))),
% 27.89/4.36 inference(ennf_transformation,[],[f557])).
% 27.89/4.36 thf(f1202,plain,(
% 27.89/4.36 ! [X1 : real,X0 : a,X2 : real] : (((((member @ real @ (plus_plus @ real @ X2 @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) = $true) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2)))) != $true)) | ($true != ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)))))),
% 27.89/4.36 inference(ennf_transformation,[],[f879])).
% 27.89/4.36 thf(f1203,plain,(
% 27.89/4.36 ! [X1 : real,X2 : real,X0 : a] : ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2)))) != $true) | ($true != ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)))) | (((member @ real @ (plus_plus @ real @ X2 @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) = $true))),
% 27.89/4.36 inference(flattening,[],[f1202])).
% 27.89/4.36 thf(f1213,plain,(
% 27.89/4.36 ! [X0 : $tType] : (! [X1 : X0] : (((minus_minus @ X0 @ zero_zero @ X0 @ X1)) = ((uminus_uminus @ X0 @ X1))) | (group_add @ X0 != $true))),
% 27.89/4.36 inference(ennf_transformation,[],[f428])).
% 27.89/4.36 thf(f1223,plain,(
% 27.89/4.36 ! [X0 : a,X1 : real] : ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) != $true) | ($true = ((member @ real @ (minus_minus @ real @ zero_zero @ real @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X1))))))),
% 27.89/4.36 inference(ennf_transformation,[],[f408])).
% 27.89/4.36 thf(f1229,plain,(
% 27.89/4.36 ! [X1 : real,X0 : real,X2 : a] : (((((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0) @ X1)) = ((auto_ll_on_flow0 @ a @ f @ x @ X2 @ (plus_plus @ real @ X0 @ X1)))) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0)))) != $true)) | (((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) != $true))),
% 27.89/4.36 inference(ennf_transformation,[],[f704])).
% 27.89/4.36 thf(f1230,plain,(
% 27.89/4.36 ! [X2 : a,X1 : real,X0 : real] : ((((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0) @ X1)) = ((auto_ll_on_flow0 @ a @ f @ x @ X2 @ (plus_plus @ real @ X0 @ X1)))) | (((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) != $true) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X0)))) != $true))),
% 27.89/4.36 inference(flattening,[],[f1229])).
% 27.89/4.36 thf(f1251,plain,(
% 27.89/4.36 ! [X0 : $tType] : ((group_add @ X0 != $true) | ! [X1 : X0,X2 : X0] : (((uminus_uminus @ X0 @ (minus_minus @ X0 @ X1 @ X2))) = ((minus_minus @ X0 @ X2 @ X1))))),
% 27.89/4.36 inference(rectify,[],[f1173])).
% 27.89/4.36 thf(f1255,plain,(
% 27.89/4.36 ! [X0 : a,X1 : real,X2 : real] : ((((auto_ll_on_flow0 @ a @ f @ x @ X0 @ (plus_plus @ real @ X2 @ X1))) = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2) @ X1))) | ($true != ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)))) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2)))) != $true))),
% 27.89/4.36 inference(rectify,[],[f1230])).
% 27.89/4.36 thf(f1261,plain,(
% 27.89/4.36 ! [X0 : real,X1 : real,X2 : a] : (($true != ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X1))))) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) != $true) | (((member @ real @ (plus_plus @ real @ X1 @ X0) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) = $true))),
% 27.89/4.36 inference(rectify,[],[f1203])).
% 27.89/4.36 thf(f1352,plain,(
% 27.89/4.36 ! [X0 : $tType] : (! [X1 : X0,X2 : X0] : (((plus_plus @ X0 @ X2 @ X1)) = ((minus_minus @ X0 @ X2 @ (uminus_uminus @ X0 @ X1)))) | (group_add @ X0 != $true))),
% 27.89/4.36 inference(rectify,[],[f1024])).
% 27.89/4.36 thf(f1383,plain,(
% 27.89/4.36 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((group_add @ X0 != $true) | (((uminus_uminus @ X0 @ (minus_minus @ X0 @ X1 @ X2))) = ((minus_minus @ X0 @ X2 @ X1)))) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1251])).
% 27.89/4.36 thf(f1392,plain,(
% 27.89/4.36 ( ! [X2 : real,X0 : a,X1 : real] : ((((auto_ll_on_flow0 @ a @ f @ x @ X0 @ (plus_plus @ real @ X2 @ X1))) = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2) @ X1))) | ($true != ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0)))) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2)))) != $true)) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1255])).
% 27.89/4.36 thf(f1405,plain,(
% 27.89/4.36 ( ! [X2 : a,X0 : real,X1 : real] : (($true != ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X1))))) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) != $true) | (((member @ real @ (plus_plus @ real @ X1 @ X0) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) = $true)) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1261])).
% 27.89/4.36 thf(f1443,plain,(
% 27.89/4.36 ( ! [X0 : real,X1 : a] : ((((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ (minus_minus @ real @ zero_zero @ real @ X0))) = X1) | (((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1))) != $true)) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1074])).
% 27.89/4.36 thf(f1492,plain,(
% 27.89/4.36 (((member @ real @ tt @ (auto_l1112008849e_ivl0 @ a @ f @ x @ xx))) = $true)),
% 27.89/4.36 inference(cnf_transformation,[],[f379])).
% 27.89/4.36 thf(f1503,plain,(
% 27.89/4.36 ( ! [X0 : $tType,X1 : X0] : ((group_add @ X0 != $true) | (((uminus_uminus @ X0 @ (uminus_uminus @ X0 @ X1))) = X1)) )),
% 27.89/4.36 inference(cnf_transformation,[],[f926])).
% 27.89/4.36 thf(f1523,plain,(
% 27.89/4.36 ( ! [X0 : a,X1 : real] : ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) != $true) | ($true = ((member @ real @ (minus_minus @ real @ zero_zero @ real @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X1)))))) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1223])).
% 27.89/4.36 thf(f1587,plain,(
% 27.89/4.36 (group_add @ real = $true)),
% 27.89/4.36 inference(cnf_transformation,[],[f757])).
% 27.89/4.36 thf(f1589,plain,(
% 27.89/4.36 (xx != ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (minus_minus @ real @ ss @ tt))))),
% 27.89/4.36 inference(cnf_transformation,[],[f919])).
% 27.89/4.36 thf(f1607,plain,(
% 27.89/4.36 ( ! [X0 : $tType,X1 : X0] : ((group_add @ X0 != $true) | (((minus_minus @ X0 @ zero_zero @ X0 @ X1)) = ((uminus_uminus @ X0 @ X1)))) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1213])).
% 27.89/4.36 thf(f1639,plain,(
% 27.89/4.36 (((auto_ll_on_flow0 @ a @ f @ x @ xx @ tt)) = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ ss)))),
% 27.89/4.36 inference(cnf_transformation,[],[f735])).
% 27.89/4.36 thf(f1652,plain,(
% 27.89/4.36 (((member @ real @ ss @ (auto_l1112008849e_ivl0 @ a @ f @ x @ x2))) = $true)),
% 27.89/4.36 inference(cnf_transformation,[],[f775])).
% 27.89/4.36 thf(f1660,plain,(
% 27.89/4.36 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((group_add @ X0 != $true) | (((plus_plus @ X0 @ X2 @ X1)) = ((minus_minus @ X0 @ X2 @ (uminus_uminus @ X0 @ X1))))) )),
% 27.89/4.36 inference(cnf_transformation,[],[f1352])).
% 27.89/4.36 thf(f1797,plain,(
% 27.89/4.36 ( ! [X0 : real] : ((((uminus_uminus @ real @ X0)) = ((minus_minus @ real @ zero_zero @ real @ X0)))) )),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1607,f1587])).
% 27.89/4.36 thf(f1799,plain,(
% 27.89/4.36 ( ! [X0 : a,X1 : real] : ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))) != $true) | ($true = ((member @ real @ (uminus_uminus @ real @ X1) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X1)))))) )),
% 27.89/4.36 inference(backward_demodulation,[],[f1523,f1797])).
% 27.89/4.36 thf(f1800,plain,(
% 27.89/4.36 ( ! [X0 : real,X1 : a] : ((((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X1))) != $true) | (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X1 @ X0) @ (uminus_uminus @ real @ X0))) = X1)) )),
% 27.89/4.36 inference(backward_demodulation,[],[f1443,f1797])).
% 27.89/4.36 thf(f1807,plain,(
% 27.89/4.36 ( ! [X0 : real,X1 : real] : ((((minus_minus @ real @ X0 @ X1)) = ((uminus_uminus @ real @ (minus_minus @ real @ X1 @ X0))))) )),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1383,f1587])).
% 27.89/4.36 thf(f1810,plain,(
% 27.89/4.36 (xx != ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (uminus_uminus @ real @ (minus_minus @ real @ tt @ ss)))))),
% 27.89/4.36 inference(backward_demodulation,[],[f1589,f1807])).
% 27.89/4.36 thf(f1812,plain,(
% 27.89/4.36 ( ! [X0 : real,X1 : real] : ((((plus_plus @ real @ X0 @ X1)) = ((minus_minus @ real @ X0 @ (uminus_uminus @ real @ X1))))) )),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1660,f1587])).
% 27.89/4.36 thf(f1818,plain,(
% 27.89/4.36 ( ! [X2 : real,X0 : a,X1 : real] : ((((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2)))) != $true) | (((auto_ll_on_flow0 @ a @ f @ x @ X0 @ (minus_minus @ real @ X2 @ (uminus_uminus @ real @ X1)))) = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X0 @ X2) @ X1))) | ($true != ((member @ real @ X2 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X0))))) )),
% 27.89/4.36 inference(backward_demodulation,[],[f1392,f1812])).
% 27.89/4.36 thf(f1820,plain,(
% 27.89/4.36 ( ! [X2 : a,X0 : real,X1 : real] : (($true != ((member @ real @ X0 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ X2 @ X1))))) | (((member @ real @ X1 @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))) != $true) | ($true = ((member @ real @ (minus_minus @ real @ X1 @ (uminus_uminus @ real @ X0)) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ X2))))) )),
% 27.89/4.36 inference(backward_demodulation,[],[f1405,f1812])).
% 27.89/4.36 thf(f2452,plain,(
% 27.89/4.36 (x2 = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ x2 @ ss) @ (uminus_uminus @ real @ ss))))),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1800,f1652])).
% 27.89/4.36 thf(f2458,plain,(
% 27.89/4.36 (x2 = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ xx @ tt) @ (uminus_uminus @ real @ ss))))),
% 27.89/4.36 inference(forward_demodulation,[],[f2452,f1639])).
% 27.89/4.36 thf(f2465,plain,(
% 27.89/4.36 ($true = ((member @ real @ (uminus_uminus @ real @ ss) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ x2 @ ss)))))),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1799,f1652])).
% 27.89/4.36 thf(f2470,plain,(
% 27.89/4.36 ($true = ((member @ real @ (uminus_uminus @ real @ ss) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ xx @ tt)))))),
% 27.89/4.36 inference(forward_demodulation,[],[f2465,f1639])).
% 27.89/4.36 thf(f2568,plain,(
% 27.89/4.36 ( ! [X0 : real] : ((((uminus_uminus @ real @ (uminus_uminus @ real @ X0))) = X0)) )),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1503,f1587])).
% 27.89/4.36 thf(f3118,plain,(
% 27.89/4.36 (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ xx @ tt) @ (uminus_uminus @ real @ ss))) = ((auto_ll_on_flow0 @ a @ f @ x @ xx @ (minus_minus @ real @ tt @ (uminus_uminus @ real @ (uminus_uminus @ real @ ss))))))),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1818,f1492,f2470])).
% 27.89/4.36 thf(f3119,plain,(
% 27.89/4.36 ($true = ((member @ real @ (minus_minus @ real @ tt @ (uminus_uminus @ real @ (uminus_uminus @ real @ ss))) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ xx))))),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1820,f1492,f2470])).
% 27.89/4.36 thf(f3134,plain,(
% 27.89/4.36 ($true = ((member @ real @ (minus_minus @ real @ tt @ ss) @ (auto_l1112008849e_ivl0 @ a @ f @ x @ xx))))),
% 27.89/4.36 inference(forward_demodulation,[],[f3119,f2568])).
% 27.89/4.36 thf(f3136,plain,(
% 27.89/4.36 (((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ xx @ tt) @ (uminus_uminus @ real @ ss))) = ((auto_ll_on_flow0 @ a @ f @ x @ xx @ (minus_minus @ real @ tt @ ss))))),
% 27.89/4.36 inference(forward_demodulation,[],[f3118,f2568])).
% 27.89/4.36 thf(f3143,plain,(
% 27.89/4.36 (x2 = ((auto_ll_on_flow0 @ a @ f @ x @ xx @ (minus_minus @ real @ tt @ ss))))),
% 27.89/4.36 inference(forward_demodulation,[],[f3136,f2458])).
% 27.89/4.36 thf(f4340,plain,(
% 27.89/4.36 (xx = ((auto_ll_on_flow0 @ a @ f @ x @ (auto_ll_on_flow0 @ a @ f @ x @ xx @ (minus_minus @ real @ tt @ ss)) @ (uminus_uminus @ real @ (minus_minus @ real @ tt @ ss)))))),
% 27.89/4.36 inference(unit_resulting_resolution,[],[f1800,f3134])).
% 27.89/4.36 thf(f4346,plain,(
% 27.89/4.36 (xx = ((auto_ll_on_flow0 @ a @ f @ x @ x2 @ (uminus_uminus @ real @ (minus_minus @ real @ tt @ ss)))))),
% 27.89/4.36 inference(forward_demodulation,[],[f4340,f3143])).
% 27.89/4.36 thf(f4354,plain,(
% 27.89/4.36 $false),
% 27.89/4.36 inference(forward_subsumption_resolution,[],[f4346,f1810])).
% 27.89/4.36 % SZS output end Proof for theBenchmark
% 27.89/4.36 % (4045103)------------------------------
% 27.89/4.36 % (4045103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.89/4.36 % (4045103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.89/4.36 % (4045103)CaDiCaL version: 2.1.3
% 27.89/4.36 % (4045103)Termination reason: Refutation
% 27.89/4.36 % (4045103)Time elapsed: 0.325 s
% 27.89/4.36 % (4045103)Peak memory usage: 16 MB
% 27.89/4.36 % (4045103)Instructions burned: 613 (million)
% 27.89/4.36 % (4044789)Success in time 4.068 s
% 27.89/4.36 % Vampire exiting
%------------------------------------------------------------------------------