%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT231^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 07:48:35 AM UTC 2026
% Result : Theorem 15.94s 2.98s
% Output : Refutation 15.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT231^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 % Computer : n014.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 18:12:45 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.28 Running higher-order theorem proving
% 0.27/0.34 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.10/0.54 % (3021809)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.10/0.54 % (3021814)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2783292730:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 1.10/0.54 % (3021816)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4039397684:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 1.10/0.54 % (3021816)Instruction limit reached!
% 1.10/0.54 % (3021816)------------------------------
% 1.10/0.54 % (3021816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.54 % (3021816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.54 % (3021816)CaDiCaL version: 2.1.3
% 1.10/0.54 % (3021816)Termination reason: Instruction limit
% 1.10/0.54 % (3021816)Termination phase: shuffling
% 1.10/0.54 % (3021816)Time elapsed: 0.004 s
% 1.10/0.54 % (3021816)Peak memory usage: 10 MB
% 1.10/0.54 % (3021816)Instructions burned: 6 (million)
% 1.10/0.54 % (3021820)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.10/0.54 % (3021820)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
% 1.10/0.54 % (3021815)lrs+10_16_si=on:nwc=1.5:random_seed=469086435:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 1.10/0.54 % (3021818)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4164239908:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 1.10/0.54 % (3021817)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=1263893398: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)
% 1.10/0.54 % (3021820)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=1131451106:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 1.10/0.54 % (3021819)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=302818107:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 1.10/0.54 % (3021823)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2146957195:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.10/0.54 % (3021815)Instruction limit reached!
% 1.10/0.54 % (3021815)------------------------------
% 1.10/0.54 % (3021815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.54 % (3021815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.54 % (3021815)CaDiCaL version: 2.1.3
% 1.10/0.54 % (3021815)Termination reason: Instruction limit
% 1.10/0.54 % (3021815)Termination phase: shuffling
% 1.10/0.54 % (3021815)Time elapsed: 0.017 s
% 1.10/0.54 % (3021815)Peak memory usage: 10 MB
% 1.10/0.54 % (3021815)Instructions burned: 19 (million)
% 1.10/0.54 % (3021823)Instruction limit reached!
% 1.10/0.54 % (3021823)------------------------------
% 1.10/0.54 % (3021823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.54 % (3021823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.54 % (3021823)CaDiCaL version: 2.1.3
% 1.10/0.54 % (3021823)Termination reason: Instruction limit
% 1.10/0.54 % (3021823)Termination phase: shuffling
% 1.10/0.54 % (3021823)Time elapsed: 0.002 s
% 1.10/0.54 % (3021823)Peak memory usage: 10 MB
% 1.10/0.54 % (3021823)Instructions burned: 3 (million)
% 1.10/0.54 % (3021818)Instruction limit reached!
% 1.10/0.54 % (3021818)------------------------------
% 1.10/0.54 % (3021818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.10/0.54 % (3021818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.10/0.54 % (3021818)CaDiCaL version: 2.1.3
% 1.10/0.54 % (3021818)Termination reason: Instruction limit
% 1.10/0.54 % (3021818)Termination phase: Property scanning
% 1.10/0.54 % (3021818)Time elapsed: 0.022 s
% 1.10/0.54 % (3021818)Peak memory usage: 10 MB
% 1.10/0.54 % (3021818)Instructions burned: 26 (million)
% 1.10/0.54 % (3021814)Instruction limit reached!
% 1.10/0.54 % (3021814)------------------------------
% 1.10/0.54 % (3021814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.60 % (3021814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.60 % (3021814)CaDiCaL version: 2.1.3
% 1.69/0.60 % (3021814)Termination reason: Instruction limit
% 1.69/0.60 % (3021814)Termination phase: Property scanning
% 1.69/0.60 % (3021814)Time elapsed: 0.040 s
% 1.69/0.60 % (3021814)Peak memory usage: 12 MB
% 1.69/0.60 % (3021814)Instructions burned: 88 (million)
% 1.69/0.60 % (3021833)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
% 1.69/0.60 % (3021833)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.69/0.60 % (3021831)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.69/0.60 % (3021830)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2740160397:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.69/0.60 % (3021833)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=424471371:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.69/0.60 % (3021831)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=370868947:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.69/0.60 % (3021830)Instruction limit reached!
% 1.69/0.60 % (3021830)------------------------------
% 1.69/0.60 % (3021830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.60 % (3021830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.60 % (3021830)CaDiCaL version: 2.1.3
% 1.69/0.60 % (3021830)Termination reason: Instruction limit
% 1.69/0.60 % (3021830)Termination phase: shuffling
% 1.69/0.60 % (3021830)Time elapsed: 0.005 s
% 1.69/0.60 % (3021830)Peak memory usage: 10 MB
% 1.69/0.60 % (3021830)Instructions burned: 5 (million)
% 1.69/0.60 % (3021832)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=861865437:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.69/0.60 % (3021831)Instruction limit reached!
% 1.69/0.60 % (3021831)------------------------------
% 1.69/0.60 % (3021831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.60 % (3021831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.60 % (3021831)CaDiCaL version: 2.1.3
% 1.69/0.60 % (3021831)Termination reason: Instruction limit
% 1.69/0.60 % (3021831)Termination phase: shuffling
% 1.69/0.60 % (3021831)Time elapsed: 0.010 s
% 1.69/0.60 % (3021831)Peak memory usage: 10 MB
% 1.69/0.60 % (3021831)Instructions burned: 11 (million)
% 1.69/0.60 % (3021819)Instruction limit reached!
% 1.69/0.60 % (3021819)------------------------------
% 1.69/0.60 % (3021819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.60 % (3021819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.60 % (3021819)CaDiCaL version: 2.1.3
% 1.69/0.60 % (3021819)Termination reason: Instruction limit
% 1.69/0.60 % (3021819)Termination phase: Property scanning
% 1.69/0.60 % (3021819)Time elapsed: 0.065 s
% 1.69/0.60 % (3021819)Peak memory usage: 12 MB
% 1.69/0.60 % (3021819)Instructions burned: 75 (million)
% 1.69/0.60 % (3021832)Instruction limit reached!
% 1.69/0.60 % (3021832)------------------------------
% 1.69/0.60 % (3021832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.69/0.60 % (3021832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.69/0.60 % (3021832)CaDiCaL version: 2.1.3
% 1.69/0.60 % (3021832)Termination reason: Instruction limit
% 1.69/0.60 % (3021832)Termination phase: shuffling
% 1.69/0.60 % (3021832)Time elapsed: 0.011 s
% 1.69/0.60 % (3021832)Peak memory usage: 10 MB
% 1.69/0.60 % (3021832)Instructions burned: 12 (million)
% 1.69/0.60 % (3021837)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=1259790217:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.69/0.60 % (3021833)Instruction limit reached!
% 1.69/0.60 % (3021833)------------------------------
% 1.69/0.60 % (3021833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.08/0.67 % (3021833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.08/0.67 % (3021833)CaDiCaL version: 2.1.3
% 2.08/0.67 % (3021833)Termination reason: Instruction limit
% 2.08/0.67 % (3021833)Termination phase: shuffling
% 2.08/0.67 % (3021833)Time elapsed: 0.024 s
% 2.08/0.67 % (3021833)Peak memory usage: 10 MB
% 2.08/0.67 % (3021833)Instructions burned: 28 (million)
% 2.08/0.67 % (3021840)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 2.08/0.67 % (3021839)lrs+10_1_si=on:cs=on:random_seed=1269000616:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.08/0.67 % (3021841)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4275883735:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.08/0.67 % (3021840)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=3271830572:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.08/0.67 % (3021840)Instruction limit reached!
% 2.08/0.67 % (3021840)------------------------------
% 2.08/0.67 % (3021840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.08/0.67 % (3021840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.08/0.67 % (3021840)CaDiCaL version: 2.1.3
% 2.08/0.67 % (3021840)Termination reason: Instruction limit
% 2.08/0.67 % (3021840)Termination phase: shuffling
% 2.08/0.67 % (3021840)Time elapsed: 0.003 s
% 2.08/0.67 % (3021840)Peak memory usage: 10 MB
% 2.08/0.67 % (3021840)Instructions burned: 2 (million)
% 2.08/0.67 % (3021839)Instruction limit reached!
% 2.08/0.67 % (3021839)------------------------------
% 2.08/0.67 % (3021839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.08/0.67 % (3021839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.08/0.67 % (3021839)CaDiCaL version: 2.1.3
% 2.08/0.67 % (3021839)Termination reason: Instruction limit
% 2.08/0.67 % (3021839)Termination phase: shuffling
% 2.08/0.67 % (3021839)Time elapsed: 0.008 s
% 2.08/0.67 % (3021839)Peak memory usage: 10 MB
% 2.08/0.67 % (3021839)Instructions burned: 8 (million)
% 2.08/0.67 % (3021843)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3495004947:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.08/0.67 % (3021837)Instruction limit reached!
% 2.08/0.67 % (3021837)------------------------------
% 2.08/0.67 % (3021837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.08/0.67 % (3021837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.08/0.67 % (3021837)CaDiCaL version: 2.1.3
% 2.08/0.67 % (3021837)Termination reason: Instruction limit
% 2.08/0.67 % (3021837)Termination phase: Preprocessing 1
% 2.08/0.67 % (3021837)Time elapsed: 0.037 s
% 2.08/0.67 % (3021837)Peak memory usage: 11 MB
% 2.08/0.67 % (3021837)Instructions burned: 87 (million)
% 2.08/0.67 % (3021847)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1328727011:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.08/0.67 % (3021850)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1633528371:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.08/0.67 % (3021841)Instruction limit reached!
% 2.08/0.67 % (3021841)------------------------------
% 2.08/0.67 % (3021841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.08/0.67 % (3021841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.08/0.67 % (3021841)CaDiCaL version: 2.1.3
% 2.08/0.67 % (3021841)Termination reason: Instruction limit
% 2.08/0.67 % (3021841)Termination phase: Preprocessing 2
% 2.08/0.67 % (3021841)Time elapsed: 0.033 s
% 2.08/0.67 % (3021841)Peak memory usage: 11 MB
% 2.08/0.67 % (3021841)Instructions burned: 38 (million)
% 2.08/0.67 % (3021820)Instruction limit reached!
% 2.08/0.67 % (3021820)------------------------------
% 2.08/0.67 % (3021820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.08/0.67 % (3021820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.08/0.67 % (3021820)CaDiCaL version: 2.1.3
% 2.08/0.67 % (3021820)Termination reason: Instruction limit
% 2.08/0.67 % (3021820)Termination phase: Saturation
% 2.08/0.67 % (3021820)Time elapsed: 0.132 s
% 2.08/0.67 % (3021820)Peak memory usage: 14 MB
% 2.49/0.75 % (3021820)Instructions burned: 157 (million)
% 2.49/0.75 % (3021847)Instruction limit reached!
% 2.49/0.75 % (3021847)------------------------------
% 2.49/0.75 % (3021847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.75 % (3021847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.75 % (3021847)CaDiCaL version: 2.1.3
% 2.49/0.75 % (3021847)Termination reason: Instruction limit
% 2.49/0.75 % (3021847)Termination phase: Property scanning
% 2.49/0.75 % (3021847)Time elapsed: 0.012 s
% 2.49/0.75 % (3021847)Peak memory usage: 10 MB
% 2.49/0.75 % (3021847)Instructions burned: 25 (million)
% 2.49/0.75 % (3021849)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3864457158:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.49/0.75 % (3021849)Instruction limit reached!
% 2.49/0.75 % (3021849)------------------------------
% 2.49/0.75 % (3021849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.75 % (3021849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.75 % (3021849)CaDiCaL version: 2.1.3
% 2.49/0.75 % (3021849)Termination reason: Instruction limit
% 2.49/0.75 % (3021849)Termination phase: shuffling
% 2.49/0.75 % (3021849)Time elapsed: 0.013 s
% 2.49/0.75 % (3021849)Peak memory usage: 11 MB
% 2.49/0.75 % (3021849)Instructions burned: 15 (million)
% 2.49/0.75 % (3021853)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2603673017:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.49/0.75 % (3021854)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3656578054: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)
% 2.49/0.75 % (3021855)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1313163796:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.49/0.75 % (3021854)Instruction limit reached!
% 2.49/0.75 % (3021854)------------------------------
% 2.49/0.75 % (3021854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.75 % (3021854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.75 % (3021854)CaDiCaL version: 2.1.3
% 2.49/0.75 % (3021854)Termination reason: Instruction limit
% 2.49/0.75 % (3021854)Termination phase: shuffling
% 2.49/0.75 % (3021854)Time elapsed: 0.003 s
% 2.49/0.75 % (3021854)Peak memory usage: 10 MB
% 2.49/0.75 % (3021854)Instructions burned: 2 (million)
% 2.49/0.75 % (3021853)Instruction limit reached!
% 2.49/0.75 % (3021853)------------------------------
% 2.49/0.75 % (3021853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.75 % (3021853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.75 % (3021853)CaDiCaL version: 2.1.3
% 2.49/0.75 % (3021853)Termination reason: Instruction limit
% 2.49/0.75 % (3021853)Termination phase: shuffling
% 2.49/0.75 % (3021853)Time elapsed: 0.014 s
% 2.49/0.75 % (3021853)Peak memory usage: 10 MB
% 2.49/0.75 % (3021853)Instructions burned: 15 (million)
% 2.49/0.75 % (3021857)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1573619597:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.49/0.75 % (3021855)Instruction limit reached!
% 2.49/0.75 % (3021855)------------------------------
% 2.49/0.75 % (3021855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.75 % (3021855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.75 % (3021855)CaDiCaL version: 2.1.3
% 2.49/0.75 % (3021855)Termination reason: Instruction limit
% 2.49/0.75 % (3021855)Termination phase: shuffling
% 2.49/0.75 % (3021855)Time elapsed: 0.022 s
% 2.49/0.75 % (3021855)Peak memory usage: 10 MB
% 2.49/0.75 % (3021855)Instructions burned: 26 (million)
% 2.49/0.75 % (3021863)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
% 2.49/0.75 % (3021863)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.49/0.75 % (3021863)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=3794431434:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.89/0.84 % (3021862)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3184554886:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.89/0.84 % (3021857)Instruction limit reached!
% 2.89/0.84 % (3021857)------------------------------
% 2.89/0.84 % (3021857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.89/0.84 % (3021857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.89/0.84 % (3021857)CaDiCaL version: 2.1.3
% 2.89/0.84 % (3021857)Termination reason: Instruction limit
% 2.89/0.84 % (3021857)Termination phase: Property scanning
% 2.89/0.84 % (3021857)Time elapsed: 0.020 s
% 2.89/0.84 % (3021857)Peak memory usage: 11 MB
% 2.89/0.84 % (3021857)Instructions burned: 23 (million)
% 2.89/0.84 % (3021863)Instruction limit reached!
% 2.89/0.84 % (3021863)------------------------------
% 2.89/0.84 % (3021863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.89/0.84 % (3021863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.89/0.84 % (3021863)CaDiCaL version: 2.1.3
% 2.89/0.84 % (3021863)Termination reason: Instruction limit
% 2.89/0.84 % (3021863)Termination phase: shuffling
% 2.89/0.84 % (3021863)Time elapsed: 0.008 s
% 2.89/0.84 % (3021863)Peak memory usage: 10 MB
% 2.89/0.84 % (3021863)Instructions burned: 15 (million)
% 2.89/0.84 % (3021865)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.89/0.84 % (3021865)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=2422630759:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.89/0.84 % (3021865)Instruction limit reached!
% 2.89/0.84 % (3021865)------------------------------
% 2.89/0.84 % (3021865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.89/0.84 % (3021865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.89/0.84 % (3021865)CaDiCaL version: 2.1.3
% 2.89/0.84 % (3021865)Termination reason: Instruction limit
% 2.89/0.84 % (3021865)Termination phase: shuffling
% 2.89/0.84 % (3021865)Time elapsed: 0.008 s
% 2.89/0.84 % (3021865)Peak memory usage: 10 MB
% 2.89/0.84 % (3021865)Instructions burned: 8 (million)
% 2.89/0.84 % (3021869)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=622177309:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.89/0.84 % (3021870)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3508011449:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.89/0.84 % (3021870)Instruction limit reached!
% 2.89/0.84 % (3021870)------------------------------
% 2.89/0.84 % (3021870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.89/0.84 % (3021870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.89/0.84 % (3021870)CaDiCaL version: 2.1.3
% 2.89/0.84 % (3021870)Termination reason: Instruction limit
% 2.89/0.84 % (3021870)Termination phase: shuffling
% 2.89/0.84 % (3021870)Time elapsed: 0.007 s
% 2.89/0.84 % (3021870)Peak memory usage: 10 MB
% 2.89/0.84 % (3021870)Instructions burned: 8 (million)
% 2.89/0.84 % (3021862)Instruction limit reached!
% 2.89/0.84 % (3021862)------------------------------
% 2.89/0.84 % (3021862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.89/0.84 % (3021862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.89/0.84 % (3021862)CaDiCaL version: 2.1.3
% 2.89/0.84 % (3021862)Termination reason: Instruction limit
% 2.89/0.84 % (3021862)Termination phase: Property scanning
% 2.89/0.84 % (3021862)Time elapsed: 0.052 s
% 2.89/0.84 % (3021862)Peak memory usage: 11 MB
% 2.89/0.84 % (3021862)Instructions burned: 60 (million)
% 2.89/0.84 % (3021869)Instruction limit reached!
% 2.89/0.84 % (3021869)------------------------------
% 2.89/0.84 % (3021869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.89/0.84 % (3021869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.89/0.84 % (3021869)CaDiCaL version: 2.1.3
% 2.89/0.84 % (3021869)Termination reason: Instruction limit
% 2.89/0.84 % (3021869)Termination phase: shuffling
% 2.89/0.84 % (3021869)Time elapsed: 0.029 s
% 2.89/0.84 % (3021869)Peak memory usage: 10 MB
% 3.24/0.96 % (3021869)Instructions burned: 32 (million)
% 3.24/0.96 % (3021872)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=428924669:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.24/0.96 % (3021872)Instruction limit reached!
% 3.24/0.96 % (3021872)------------------------------
% 3.24/0.96 % (3021872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.96 % (3021872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.96 % (3021872)CaDiCaL version: 2.1.3
% 3.24/0.96 % (3021872)Termination reason: Instruction limit
% 3.24/0.96 % (3021872)Termination phase: shuffling
% 3.24/0.96 % (3021872)Time elapsed: 0.020 s
% 3.24/0.96 % (3021872)Peak memory usage: 10 MB
% 3.24/0.96 % (3021872)Instructions burned: 24 (million)
% 3.24/0.96 % (3021850)Instruction limit reached!
% 3.24/0.96 % (3021850)------------------------------
% 3.24/0.96 % (3021850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.96 % (3021850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.96 % (3021850)CaDiCaL version: 2.1.3
% 3.24/0.96 % (3021850)Termination reason: Instruction limit
% 3.24/0.96 % (3021850)Termination phase: Saturation
% 3.24/0.96 % (3021850)Time elapsed: 0.153 s
% 3.24/0.96 % (3021850)Peak memory usage: 14 MB
% 3.24/0.96 % (3021850)Instructions burned: 329 (million)
% 3.24/0.96 % (3021876)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=351658266:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/20Mi)
% 3.24/0.96 % (3021877)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3837289747:i=1240:rtra=on:ixr=off_2996 on theBenchmark for (2996ds/1240Mi)
% 3.24/0.96 % (3021879)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1239668211:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.24/0.96 % (3021876)Instruction limit reached!
% 3.24/0.96 % (3021876)------------------------------
% 3.24/0.96 % (3021876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.96 % (3021876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.96 % (3021876)CaDiCaL version: 2.1.3
% 3.24/0.96 % (3021876)Termination reason: Instruction limit
% 3.24/0.96 % (3021876)Termination phase: shuffling
% 3.24/0.96 % (3021876)Time elapsed: 0.018 s
% 3.24/0.96 % (3021876)Peak memory usage: 10 MB
% 3.24/0.96 % (3021876)Instructions burned: 20 (million)
% 3.24/0.96 % (3021880)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2130062951:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.24/0.96 % (3021843)Instruction limit reached!
% 3.24/0.96 % (3021843)------------------------------
% 3.24/0.96 % (3021843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.96 % (3021843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.96 % (3021843)CaDiCaL version: 2.1.3
% 3.24/0.96 % (3021843)Termination reason: Instruction limit
% 3.24/0.96 % (3021843)Termination phase: Saturation
% 3.24/0.96 % (3021843)Time elapsed: 0.208 s
% 3.24/0.96 % (3021843)Peak memory usage: 14 MB
% 3.24/0.96 % (3021843)Instructions burned: 249 (million)
% 3.24/0.96 % (3021881)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=126080215:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.24/0.97 % (3021887)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.24/0.97 % (3021887)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3426250868:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.24/0.97 % (3021887)Instruction limit reached!
% 3.24/0.97 % (3021887)------------------------------
% 3.24/0.97 % (3021887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.24/0.97 % (3021887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.24/0.97 % (3021887)CaDiCaL version: 2.1.3
% 3.24/0.97 % (3021887)Termination reason: Instruction limit
% 3.24/0.97 % (3021887)Termination phase: shuffling
% 3.24/0.97 % (3021887)Time elapsed: 0.005 s
% 3.24/0.97 % (3021887)Peak memory usage: 10 MB
% 3.24/0.97 % (3021887)Instructions burned: 8 (million)
% 3.24/0.97 % (3021888)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2108688827:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 5.14/1.12 % (3021881)Instruction limit reached!
% 5.14/1.12 % (3021881)------------------------------
% 5.14/1.12 % (3021881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.12 % (3021881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.12 % (3021881)CaDiCaL version: 2.1.3
% 5.14/1.12 % (3021881)Termination reason: Instruction limit
% 5.14/1.12 % (3021881)Termination phase: Naming
% 5.14/1.12 % (3021881)Time elapsed: 0.033 s
% 5.14/1.12 % (3021881)Peak memory usage: 11 MB
% 5.14/1.12 % (3021881)Instructions burned: 43 (million)
% 5.14/1.12 % (3021891)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=2286664667:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 5.14/1.12 % (3021894)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 5.14/1.12 % (3021894)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1171013132:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 5.14/1.12 % (3021894)Instruction limit reached!
% 5.14/1.12 % (3021894)------------------------------
% 5.14/1.12 % (3021894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.12 % (3021894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.12 % (3021894)CaDiCaL version: 2.1.3
% 5.14/1.12 % (3021894)Termination reason: Instruction limit
% 5.14/1.12 % (3021894)Termination phase: shuffling
% 5.14/1.12 % (3021894)Time elapsed: 0.004 s
% 5.14/1.12 % (3021894)Peak memory usage: 10 MB
% 5.14/1.12 % (3021894)Instructions burned: 8 (million)
% 5.14/1.12 % (3021880)Instruction limit reached!
% 5.14/1.12 % (3021880)------------------------------
% 5.14/1.12 % (3021880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.12 % (3021880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.12 % (3021880)CaDiCaL version: 2.1.3
% 5.14/1.12 % (3021880)Termination reason: Instruction limit
% 5.14/1.12 % (3021880)Termination phase: Saturation
% 5.14/1.12 % (3021880)Time elapsed: 0.089 s
% 5.14/1.12 % (3021880)Peak memory usage: 14 MB
% 5.14/1.12 % (3021880)Instructions burned: 193 (million)
% 5.14/1.12 % (3021897)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3854343186:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 5.14/1.12 % (3021897)Instruction limit reached!
% 5.14/1.12 % (3021897)------------------------------
% 5.14/1.12 % (3021897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.12 % (3021897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.12 % (3021897)CaDiCaL version: 2.1.3
% 5.14/1.12 % (3021897)Termination reason: Instruction limit
% 5.14/1.12 % (3021897)Termination phase: Property scanning
% 5.14/1.12 % (3021897)Time elapsed: 0.013 s
% 5.14/1.12 % (3021897)Peak memory usage: 10 MB
% 5.14/1.12 % (3021897)Instructions burned: 23 (million)
% 5.14/1.12 % (3021879)Instruction limit reached!
% 5.14/1.12 % (3021879)------------------------------
% 5.14/1.12 % (3021879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.14/1.12 % (3021879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.14/1.12 % (3021879)CaDiCaL version: 2.1.3
% 5.14/1.12 % (3021879)Termination reason: Instruction limit
% 5.14/1.12 % (3021879)Termination phase: Saturation
% 5.14/1.12 % (3021879)Time elapsed: 0.120 s
% 5.14/1.12 % (3021879)Peak memory usage: 13 MB
% 5.14/1.12 % (3021879)Instructions burned: 144 (million)
% 5.14/1.12 % (3021899)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1314856232:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 5.14/1.12 % (3021901)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=3622767564:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 5.14/1.12 % (3021902)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=1577343523:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.75/1.26 % (3021899)Instruction limit reached!
% 5.75/1.26 % (3021899)------------------------------
% 5.75/1.26 % (3021899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.26 % (3021899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.26 % (3021899)CaDiCaL version: 2.1.3
% 5.75/1.26 % (3021899)Termination reason: Instruction limit
% 5.75/1.26 % (3021899)Termination phase: shuffling
% 5.75/1.26 % (3021899)Time elapsed: 0.017 s
% 5.75/1.26 % (3021899)Peak memory usage: 10 MB
% 5.75/1.26 % (3021899)Instructions burned: 19 (million)
% 5.75/1.26 % (3021907)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=2936794572:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 5.75/1.26 % (3021891)Instruction limit reached!
% 5.75/1.26 % (3021891)------------------------------
% 5.75/1.26 % (3021891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.26 % (3021891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.26 % (3021891)CaDiCaL version: 2.1.3
% 5.75/1.26 % (3021891)Termination reason: Instruction limit
% 5.75/1.26 % (3021891)Termination phase: Saturation
% 5.75/1.26 % (3021891)Time elapsed: 0.145 s
% 5.75/1.26 % (3021891)Peak memory usage: 14 MB
% 5.75/1.26 % (3021891)Instructions burned: 169 (million)
% 5.75/1.26 % (3021888)Instruction limit reached!
% 5.75/1.26 % (3021888)------------------------------
% 5.75/1.26 % (3021888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.26 % (3021888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.26 % (3021888)CaDiCaL version: 2.1.3
% 5.75/1.26 % (3021888)Termination reason: Instruction limit
% 5.75/1.26 % (3021888)Termination phase: Saturation
% 5.75/1.26 % (3021888)Time elapsed: 0.160 s
% 5.75/1.26 % (3021888)Peak memory usage: 14 MB
% 5.75/1.26 % (3021888)Instructions burned: 181 (million)
% 5.75/1.26 % (3021817)Instruction limit reached!
% 5.75/1.26 % (3021817)------------------------------
% 5.75/1.26 % (3021817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.26 % (3021817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.26 % (3021817)CaDiCaL version: 2.1.3
% 5.75/1.26 % (3021817)Termination reason: Instruction limit
% 5.75/1.26 % (3021817)Termination phase: Saturation
% 5.75/1.26 % (3021817)Time elapsed: 0.515 s
% 5.75/1.26 % (3021817)Peak memory usage: 15 MB
% 5.75/1.26 % (3021817)Instructions burned: 635 (million)
% 5.75/1.26 % (3021907)Instruction limit reached!
% 5.75/1.26 % (3021907)------------------------------
% 5.75/1.26 % (3021907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.26 % (3021907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.26 % (3021907)CaDiCaL version: 2.1.3
% 5.75/1.26 % (3021907)Termination reason: Instruction limit
% 5.75/1.26 % (3021907)Termination phase: Property scanning
% 5.75/1.26 % (3021907)Time elapsed: 0.038 s
% 5.75/1.26 % (3021907)Peak memory usage: 10 MB
% 5.75/1.26 % (3021907)Instructions burned: 45 (million)
% 5.75/1.26 % (3021910)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1073739671:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 5.75/1.26 % (3021911)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=966901498:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.75/1.26 % (3021912)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.75/1.26 % (3021912)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2072671262:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 5.75/1.26 % (3021914)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2417595247:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 5.75/1.26 % (3021911)Instruction limit reached!
% 5.75/1.26 % (3021911)------------------------------
% 5.75/1.26 % (3021911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.26 % (3021911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.42 % (3021911)CaDiCaL version: 2.1.3
% 6.88/1.42 % (3021911)Termination reason: Instruction limit
% 6.88/1.42 % (3021911)Termination phase: shuffling
% 6.88/1.42 % (3021911)Time elapsed: 0.019 s
% 6.88/1.42 % (3021911)Peak memory usage: 11 MB
% 6.88/1.42 % (3021911)Instructions burned: 22 (million)
% 6.88/1.42 % (3021914)Instruction limit reached!
% 6.88/1.42 % (3021914)------------------------------
% 6.88/1.42 % (3021914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.42 % (3021914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.42 % (3021914)CaDiCaL version: 2.1.3
% 6.88/1.42 % (3021914)Termination reason: Instruction limit
% 6.88/1.42 % (3021914)Termination phase: shuffling
% 6.88/1.42 % (3021914)Time elapsed: 0.013 s
% 6.88/1.42 % (3021914)Peak memory usage: 10 MB
% 6.88/1.42 % (3021914)Instructions burned: 13 (million)
% 6.88/1.42 % (3021918)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=3808738459:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 6.88/1.42 % (3021919)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=455602857:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 6.88/1.42 % (3021919)Instruction limit reached!
% 6.88/1.42 % (3021919)------------------------------
% 6.88/1.42 % (3021919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.42 % (3021919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.42 % (3021919)CaDiCaL version: 2.1.3
% 6.88/1.42 % (3021919)Termination reason: Instruction limit
% 6.88/1.42 % (3021919)Termination phase: Preprocessing 3
% 6.88/1.42 % (3021919)Time elapsed: 0.044 s
% 6.88/1.42 % (3021919)Peak memory usage: 11 MB
% 6.88/1.42 % (3021919)Instructions burned: 52 (million)
% 6.88/1.42 % (3021918)Instruction limit reached!
% 6.88/1.42 % (3021918)------------------------------
% 6.88/1.42 % (3021918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.42 % (3021918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.42 % (3021918)CaDiCaL version: 2.1.3
% 6.88/1.42 % (3021918)Termination reason: Instruction limit
% 6.88/1.42 % (3021918)Termination phase: Property scanning
% 6.88/1.42 % (3021918)Time elapsed: 0.055 s
% 6.88/1.42 % (3021918)Peak memory usage: 11 MB
% 6.88/1.42 % (3021918)Instructions burned: 67 (million)
% 6.88/1.42 % (3021901)Instruction limit reached!
% 6.88/1.42 % (3021901)------------------------------
% 6.88/1.42 % (3021901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.42 % (3021901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.42 % (3021901)CaDiCaL version: 2.1.3
% 6.88/1.42 % (3021901)Termination reason: Instruction limit
% 6.88/1.42 % (3021901)Termination phase: Saturation
% 6.88/1.42 % (3021901)Time elapsed: 0.234 s
% 6.88/1.42 % (3021901)Peak memory usage: 16 MB
% 6.88/1.42 % (3021901)Instructions burned: 316 (million)
% 6.88/1.42 % (3021922)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2497865103:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 6.88/1.42 % (3021923)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3016071405:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2992 on theBenchmark for (2992ds/137Mi)
% 6.88/1.42 % (3021924)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=3643692509:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.88/1.42 % (3021922)Instruction limit reached!
% 6.88/1.42 % (3021922)------------------------------
% 6.88/1.42 % (3021922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.42 % (3021922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.42 % (3021922)CaDiCaL version: 2.1.3
% 6.88/1.42 % (3021922)Termination reason: Instruction limit
% 6.88/1.42 % (3021922)Termination phase: shuffling
% 6.88/1.42 % (3021922)Time elapsed: 0.028 s
% 6.88/1.42 % (3021922)Peak memory usage: 11 MB
% 6.88/1.42 % (3021922)Instructions burned: 32 (million)
% 6.88/1.42 % (3021912)Instruction limit reached!
% 6.88/1.42 % (3021912)------------------------------
% 6.88/1.42 % (3021912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.88/1.42 % (3021912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.71 % (3021912)CaDiCaL version: 2.1.3
% 7.87/1.71 % (3021912)Termination reason: Instruction limit
% 7.87/1.71 % (3021912)Termination phase: Saturation
% 7.87/1.71 % (3021912)Time elapsed: 0.164 s
% 7.87/1.71 % (3021912)Peak memory usage: 13 MB
% 7.87/1.71 % (3021912)Instructions burned: 200 (million)
% 7.87/1.71 % (3021924)Instruction limit reached!
% 7.87/1.71 % (3021924)------------------------------
% 7.87/1.71 % (3021924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.87/1.71 % (3021924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.71 % (3021924)CaDiCaL version: 2.1.3
% 7.87/1.71 % (3021924)Termination reason: Instruction limit
% 7.87/1.71 % (3021924)Termination phase: shuffling
% 7.87/1.71 % (3021924)Time elapsed: 0.030 s
% 7.87/1.71 % (3021924)Peak memory usage: 10 MB
% 7.87/1.71 % (3021924)Instructions burned: 34 (million)
% 7.87/1.71 % (3021930)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 7.87/1.71 % (3021930)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1498852284:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 7.87/1.71 % (3021928)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3619346980:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 7.87/1.71 % (3021932)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1575631365:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 7.87/1.71 % (3021928)Instruction limit reached!
% 7.87/1.71 % (3021928)------------------------------
% 7.87/1.71 % (3021928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.87/1.71 % (3021928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.71 % (3021928)CaDiCaL version: 2.1.3
% 7.87/1.71 % (3021928)Termination reason: Instruction limit
% 7.87/1.71 % (3021928)Termination phase: Property scanning
% 7.87/1.71 % (3021928)Time elapsed: 0.058 s
% 7.87/1.71 % (3021928)Peak memory usage: 12 MB
% 7.87/1.71 % (3021928)Instructions burned: 67 (million)
% 7.87/1.71 % (3021923)Instruction limit reached!
% 7.87/1.71 % (3021923)------------------------------
% 7.87/1.71 % (3021923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.87/1.71 % (3021923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.71 % (3021923)CaDiCaL version: 2.1.3
% 7.87/1.71 % (3021923)Termination reason: Instruction limit
% 7.87/1.71 % (3021923)Termination phase: Saturation
% 7.87/1.71 % (3021923)Time elapsed: 0.119 s
% 7.87/1.71 % (3021923)Peak memory usage: 13 MB
% 7.87/1.71 % (3021923)Instructions burned: 137 (million)
% 7.87/1.71 % (3021902)Instruction limit reached!
% 7.87/1.71 % (3021902)------------------------------
% 7.87/1.71 % (3021902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.87/1.71 % (3021902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.71 % (3021902)CaDiCaL version: 2.1.3
% 7.87/1.71 % (3021902)Termination reason: Instruction limit
% 7.87/1.71 % (3021902)Termination phase: Saturation
% 7.87/1.71 % (3021902)Time elapsed: 0.384 s
% 7.87/1.71 % (3021902)Peak memory usage: 16 MB
% 7.87/1.71 % (3021902)Instructions burned: 854 (million)
% 7.87/1.71 % (3021910)Instruction limit reached!
% 7.87/1.71 % (3021910)------------------------------
% 7.87/1.72 % (3021910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.87/1.72 % (3021910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.87/1.72 % (3021910)CaDiCaL version: 2.1.3
% 7.87/1.72 % (3021910)Termination reason: Instruction limit
% 7.87/1.72 % (3021910)Termination phase: Saturation
% 7.87/1.72 % (3021910)Time elapsed: 0.302 s
% 7.87/1.72 % (3021910)Peak memory usage: 16 MB
% 7.87/1.72 % (3021910)Instructions burned: 480 (million)
% 7.87/1.72 % (3021936)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=298283712:cond=on:i=96:bd=all:rtra=on_2991 on theBenchmark for (2991ds/96Mi)
% 7.87/1.72 % (3021937)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3814048746:i=427:sd=1:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/427Mi)
% 7.87/1.72 % (3021938)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2876971690:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/874Mi)
% 7.87/1.72 % (3021937)Refutation not found, incomplete strategy
% 7.87/1.72 % (3021937)------------------------------
% 8.89/1.88 % (3021937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.88 % (3021937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.88 % (3021937)CaDiCaL version: 2.1.3
% 8.89/1.88 % (3021937)Termination reason: Refutation not found, incomplete strategy
% 8.89/1.88 % (3021937)Time elapsed: 0.019 s
% 8.89/1.88 % (3021937)Peak memory usage: 13 MB
% 8.89/1.88 % (3021937)Instructions burned: 40 (million)
% 8.89/1.88 % (3021937)------------------------------
% 8.89/1.88 % (3021937)------------------------------
% 8.89/1.88 % (3021940)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2256310258:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/515Mi)
% 8.89/1.88 % (3021930)Instruction limit reached!
% 8.89/1.88 % (3021930)------------------------------
% 8.89/1.88 % (3021930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.88 % (3021930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.88 % (3021930)CaDiCaL version: 2.1.3
% 8.89/1.88 % (3021930)Termination reason: Instruction limit
% 8.89/1.88 % (3021930)Termination phase: Saturation
% 8.89/1.88 % (3021930)Time elapsed: 0.146 s
% 8.89/1.88 % (3021930)Peak memory usage: 13 MB
% 8.89/1.88 % (3021930)Instructions burned: 181 (million)
% 8.89/1.88 % (3021944)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=981052245:st=1.5:i=130:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/130Mi)
% 8.89/1.88 % (3021948)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2553323546:i=44:ep=R:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/44Mi)
% 8.89/1.88 % (3021936)Instruction limit reached!
% 8.89/1.88 % (3021936)------------------------------
% 8.89/1.88 % (3021936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.88 % (3021936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.88 % (3021936)CaDiCaL version: 2.1.3
% 8.89/1.88 % (3021936)Termination reason: Instruction limit
% 8.89/1.88 % (3021936)Termination phase: Property scanning
% 8.89/1.88 % (3021936)Time elapsed: 0.081 s
% 8.89/1.88 % (3021936)Peak memory usage: 12 MB
% 8.89/1.88 % (3021936)Instructions burned: 96 (million)
% 8.89/1.88 % (3021948)Instruction limit reached!
% 8.89/1.88 % (3021948)------------------------------
% 8.89/1.88 % (3021948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.88 % (3021948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.88 % (3021948)CaDiCaL version: 2.1.3
% 8.89/1.88 % (3021948)Termination reason: Instruction limit
% 8.89/1.88 % (3021948)Termination phase: Property scanning
% 8.89/1.88 % (3021948)Time elapsed: 0.020 s
% 8.89/1.88 % (3021948)Peak memory usage: 11 MB
% 8.89/1.88 % (3021948)Instructions burned: 46 (million)
% 8.89/1.88 % (3021950)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2068199868:s2a=on:i=571:nm=16:rtra=on_2990 on theBenchmark for (2990ds/571Mi)
% 8.89/1.88 % (3021951)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3700347275:i=450:rtra=on:ixr=off:ntd=on_2990 on theBenchmark for (2990ds/450Mi)
% 8.89/1.88 % (3021932)Instruction limit reached!
% 8.89/1.88 % (3021932)------------------------------
% 8.89/1.88 % (3021932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.88 % (3021932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.88 % (3021932)CaDiCaL version: 2.1.3
% 8.89/1.88 % (3021932)Termination reason: Instruction limit
% 8.89/1.88 % (3021932)Termination phase: Saturation
% 8.89/1.88 % (3021932)Time elapsed: 0.208 s
% 8.89/1.88 % (3021932)Peak memory usage: 14 MB
% 8.89/1.88 % (3021932)Instructions burned: 246 (million)
% 8.89/1.88 % (3021944)Instruction limit reached!
% 8.89/1.88 % (3021944)------------------------------
% 8.89/1.88 % (3021944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.89/1.88 % (3021944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.89/1.88 % (3021944)CaDiCaL version: 2.1.3
% 8.89/1.88 % (3021944)Termination reason: Instruction limit
% 8.89/1.88 % (3021944)Termination phase: Saturation
% 8.89/1.88 % (3021944)Time elapsed: 0.108 s
% 8.89/1.88 % (3021944)Peak memory usage: 13 MB
% 8.89/1.88 % (3021944)Instructions burned: 130 (million)
% 8.89/1.88 % (3021954)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=160417014:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/95Mi)
% 9.18/2.04 % (3021955)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=3092951088:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2989 on theBenchmark for (2989ds/65Mi)
% 9.18/2.04 % (3021955)Instruction limit reached!
% 9.18/2.04 % (3021955)------------------------------
% 9.18/2.04 % (3021955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/2.04 % (3021955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.04 % (3021955)CaDiCaL version: 2.1.3
% 9.18/2.04 % (3021955)Termination reason: Instruction limit
% 9.18/2.04 % (3021955)Termination phase: Property scanning
% 9.18/2.04 % (3021955)Time elapsed: 0.054 s
% 9.18/2.04 % (3021955)Peak memory usage: 11 MB
% 9.18/2.04 % (3021955)Instructions burned: 66 (million)
% 9.18/2.04 % (3021954)Instruction limit reached!
% 9.18/2.04 % (3021954)------------------------------
% 9.18/2.04 % (3021954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/2.04 % (3021954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.04 % (3021954)CaDiCaL version: 2.1.3
% 9.18/2.04 % (3021954)Termination reason: Instruction limit
% 9.18/2.04 % (3021954)Termination phase: Property scanning
% 9.18/2.04 % (3021954)Time elapsed: 0.083 s
% 9.18/2.04 % (3021954)Peak memory usage: 12 MB
% 9.18/2.04 % (3021954)Instructions burned: 95 (million)
% 9.18/2.04 % (3021959)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=3811056392:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2988 on theBenchmark for (2988ds/5755Mi)
% 9.18/2.04 % (3021958)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=3568372727: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_2988 on theBenchmark for (2988ds/105Mi)
% 9.18/2.04 % (3021951)Instruction limit reached!
% 9.18/2.04 % (3021951)------------------------------
% 9.18/2.04 % (3021951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/2.04 % (3021951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.04 % (3021951)CaDiCaL version: 2.1.3
% 9.18/2.04 % (3021951)Termination reason: Instruction limit
% 9.18/2.04 % (3021951)Termination phase: Saturation
% 9.18/2.04 % (3021951)Time elapsed: 0.186 s
% 9.18/2.04 % (3021951)Peak memory usage: 14 MB
% 9.18/2.04 % (3021951)Instructions burned: 452 (million)
% 9.18/2.04 % (3021962)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1879440108:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/375Mi)
% 9.18/2.04 % (3021958)Instruction limit reached!
% 9.18/2.04 % (3021958)------------------------------
% 9.18/2.04 % (3021958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/2.04 % (3021958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.04 % (3021958)CaDiCaL version: 2.1.3
% 9.18/2.04 % (3021958)Termination reason: Instruction limit
% 9.18/2.04 % (3021958)Termination phase: Preprocessing 3
% 9.18/2.04 % (3021958)Time elapsed: 0.087 s
% 9.18/2.04 % (3021958)Peak memory usage: 11 MB
% 9.18/2.04 % (3021958)Instructions burned: 105 (million)
% 9.18/2.04 % (3021964)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1064546055:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2987 on theBenchmark for (2987ds/495Mi)
% 9.18/2.04 % (3021940)Instruction limit reached!
% 9.18/2.04 % (3021940)------------------------------
% 9.18/2.04 % (3021940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/2.04 % (3021940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.04 % (3021940)CaDiCaL version: 2.1.3
% 9.18/2.04 % (3021940)Termination reason: Instruction limit
% 9.18/2.04 % (3021940)Termination phase: Saturation
% 9.18/2.04 % (3021940)Time elapsed: 0.450 s
% 9.18/2.04 % (3021940)Peak memory usage: 16 MB
% 9.18/2.04 % (3021940)Instructions burned: 516 (million)
% 9.18/2.04 % (3021950)Instruction limit reached!
% 9.18/2.04 % (3021950)------------------------------
% 9.18/2.04 % (3021950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.18/2.04 % (3021950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.30 % (3021950)CaDiCaL version: 2.1.3
% 12.63/2.30 % (3021950)Termination reason: Instruction limit
% 12.63/2.30 % (3021950)Termination phase: Saturation
% 12.63/2.30 % (3021950)Time elapsed: 0.382 s
% 12.63/2.30 % (3021950)Peak memory usage: 17 MB
% 12.63/2.30 % (3021950)Instructions burned: 576 (million)
% 12.63/2.30 % (3021966)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=538753568:cond=on:i=34:hud=10:nm=10:rtra=on_2986 on theBenchmark for (2986ds/34Mi)
% 12.63/2.30 % (3021967)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2086588152:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2986 on theBenchmark for (2986ds/91Mi)
% 12.63/2.30 % (3021966)Instruction limit reached!
% 12.63/2.30 % (3021966)------------------------------
% 12.63/2.30 % (3021966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.30 % (3021966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.30 % (3021966)CaDiCaL version: 2.1.3
% 12.63/2.30 % (3021966)Termination reason: Instruction limit
% 12.63/2.30 % (3021966)Termination phase: shuffling
% 12.63/2.30 % (3021966)Time elapsed: 0.021 s
% 12.63/2.30 % (3021966)Peak memory usage: 10 MB
% 12.63/2.30 % (3021966)Instructions burned: 35 (million)
% 12.63/2.30 % (3021877)Instruction limit reached!
% 12.63/2.30 % (3021877)------------------------------
% 12.63/2.30 % (3021877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.30 % (3021877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.30 % (3021877)CaDiCaL version: 2.1.3
% 12.63/2.30 % (3021877)Termination reason: Instruction limit
% 12.63/2.30 % (3021877)Termination phase: Saturation
% 12.63/2.30 % (3021877)Time elapsed: 1.066 s
% 12.63/2.30 % (3021877)Peak memory usage: 18 MB
% 12.63/2.30 % (3021877)Instructions burned: 1240 (million)
% 12.63/2.30 % (3021971)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2007432040:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2985 on theBenchmark for (2985ds/22Mi)
% 12.63/2.30 % (3021970)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1373371069:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2985 on theBenchmark for (2985ds/66Mi)
% 12.63/2.30 % (3021971)Instruction limit reached!
% 12.63/2.30 % (3021971)------------------------------
% 12.63/2.30 % (3021971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.30 % (3021971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.30 % (3021971)CaDiCaL version: 2.1.3
% 12.63/2.30 % (3021971)Termination reason: Instruction limit
% 12.63/2.30 % (3021971)Termination phase: Property scanning
% 12.63/2.30 % (3021971)Time elapsed: 0.014 s
% 12.63/2.30 % (3021971)Peak memory usage: 10 MB
% 12.63/2.30 % (3021971)Instructions burned: 23 (million)
% 12.63/2.30 % (3021974)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=176988723:i=338:bd=all:ins=4:rtra=on_2985 on theBenchmark for (2985ds/338Mi)
% 12.63/2.30 % (3021967)Instruction limit reached!
% 12.63/2.30 % (3021967)------------------------------
% 12.63/2.30 % (3021967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.30 % (3021967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.30 % (3021967)CaDiCaL version: 2.1.3
% 12.63/2.30 % (3021967)Termination reason: Instruction limit
% 12.63/2.30 % (3021967)Termination phase: Property scanning
% 12.63/2.30 % (3021967)Time elapsed: 0.077 s
% 12.63/2.30 % (3021967)Peak memory usage: 12 MB
% 12.63/2.30 % (3021967)Instructions burned: 91 (million)
% 12.63/2.30 % (3021970)Instruction limit reached!
% 12.63/2.30 % (3021970)------------------------------
% 12.63/2.30 % (3021970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.63/2.30 % (3021970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.63/2.30 % (3021970)CaDiCaL version: 2.1.3
% 12.63/2.30 % (3021970)Termination reason: Instruction limit
% 12.63/2.30 % (3021970)Termination phase: Saturation
% 12.63/2.30 % (3021970)Time elapsed: 0.058 s
% 12.63/2.30 % (3021970)Peak memory usage: 13 MB
% 12.63/2.30 % (3021970)Instructions burned: 67 (million)
% 12.63/2.30 % (3021976)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3248018176:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/28Mi)
% 12.63/2.30 % (3021977)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 13.94/2.53 % (3021976)Instruction limit reached!
% 13.94/2.53 % (3021976)------------------------------
% 13.94/2.53 % (3021976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.94/2.53 % (3021976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.94/2.53 % (3021976)CaDiCaL version: 2.1.3
% 13.94/2.53 % (3021976)Termination reason: Instruction limit
% 13.94/2.53 % (3021976)Termination phase: Property scanning
% 13.94/2.53 % (3021976)Time elapsed: 0.024 s
% 13.94/2.53 % (3021976)Peak memory usage: 11 MB
% 13.94/2.53 % (3021976)Instructions burned: 28 (million)
% 13.94/2.53 % (3021977)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=37600472:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2984 on theBenchmark for (2984ds/137Mi)
% 13.94/2.53 % (3021938)Instruction limit reached!
% 13.94/2.53 % (3021938)------------------------------
% 13.94/2.53 % (3021938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.94/2.53 % (3021938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.94/2.53 % (3021938)CaDiCaL version: 2.1.3
% 13.94/2.53 % (3021938)Termination reason: Instruction limit
% 13.94/2.53 % (3021938)Termination phase: Saturation
% 13.94/2.53 % (3021938)Time elapsed: 0.665 s
% 13.94/2.53 % (3021938)Peak memory usage: 15 MB
% 13.94/2.53 % (3021938)Instructions burned: 875 (million)
% 13.94/2.53 % (3021962)Instruction limit reached!
% 13.94/2.53 % (3021962)------------------------------
% 13.94/2.53 % (3021962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.94/2.53 % (3021962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.94/2.53 % (3021962)CaDiCaL version: 2.1.3
% 13.94/2.53 % (3021962)Termination reason: Instruction limit
% 13.94/2.53 % (3021962)Termination phase: Saturation
% 13.94/2.53 % (3021962)Time elapsed: 0.346 s
% 13.94/2.53 % (3021962)Peak memory usage: 16 MB
% 13.94/2.53 % (3021962)Instructions burned: 375 (million)
% 13.94/2.53 % (3021980)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=731364853:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2984 on theBenchmark for (2984ds/340Mi)
% 13.94/2.53 % (3021981)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3216361159:i=227:sd=1:bd=all:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/227Mi)
% 13.94/2.53 % (3021982)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 13.94/2.53 % (3021982)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2855755708:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/373Mi)
% 13.94/2.53 % (3021981)Refutation not found, incomplete strategy
% 13.94/2.53 % (3021981)------------------------------
% 13.94/2.53 % (3021981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.94/2.53 % (3021981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.94/2.53 % (3021981)CaDiCaL version: 2.1.3
% 13.94/2.53 % (3021981)Termination reason: Refutation not found, incomplete strategy
% 13.94/2.53 % (3021981)Time elapsed: 0.035 s
% 13.94/2.53 % (3021981)Peak memory usage: 13 MB
% 13.94/2.53 % (3021981)Instructions burned: 40 (million)
% 13.94/2.53 % (3021981)------------------------------
% 13.94/2.53 % (3021981)------------------------------
% 13.94/2.53 % (3021977)Instruction limit reached!
% 13.94/2.53 % (3021977)------------------------------
% 13.94/2.53 % (3021977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.94/2.53 % (3021977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.94/2.53 % (3021977)CaDiCaL version: 2.1.3
% 13.94/2.53 % (3021977)Termination reason: Instruction limit
% 13.94/2.53 % (3021977)Termination phase: Saturation
% 13.94/2.53 % (3021977)Time elapsed: 0.113 s
% 13.94/2.53 % (3021977)Peak memory usage: 13 MB
% 13.94/2.53 % (3021977)Instructions burned: 137 (million)
% 13.94/2.53 % (3021986)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1908427026:i=116:ep=RSTC:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/116Mi)
% 13.94/2.53 % (3021987)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=205767386:i=575:rtra=on_2983 on theBenchmark for (2983ds/575Mi)
% 15.62/2.87 % (3021974)Instruction limit reached!
% 15.62/2.87 % (3021974)------------------------------
% 15.62/2.87 % (3021974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.87 % (3021974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.87 % (3021974)CaDiCaL version: 2.1.3
% 15.62/2.87 % (3021974)Termination reason: Instruction limit
% 15.62/2.87 % (3021974)Termination phase: Saturation
% 15.62/2.87 % (3021974)Time elapsed: 0.226 s
% 15.62/2.87 % (3021974)Peak memory usage: 17 MB
% 15.62/2.87 % (3021974)Instructions burned: 339 (million)
% 15.62/2.87 % (3021990)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=2379134173:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2982 on theBenchmark for (2982ds/270Mi)
% 15.62/2.87 % (3021964)Instruction limit reached!
% 15.62/2.87 % (3021964)------------------------------
% 15.62/2.87 % (3021964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.87 % (3021964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.87 % (3021964)CaDiCaL version: 2.1.3
% 15.62/2.87 % (3021964)Termination reason: Instruction limit
% 15.62/2.87 % (3021964)Termination phase: Saturation
% 15.62/2.87 % (3021964)Time elapsed: 0.440 s
% 15.62/2.87 % (3021964)Peak memory usage: 17 MB
% 15.62/2.87 % (3021964)Instructions burned: 496 (million)
% 15.62/2.87 % (3021992)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=416184482: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_2982 on theBenchmark for (2982ds/9840Mi)
% 15.62/2.87 % (3021986)Instruction limit reached!
% 15.62/2.87 % (3021986)------------------------------
% 15.62/2.87 % (3021986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.87 % (3021986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.87 % (3021986)CaDiCaL version: 2.1.3
% 15.62/2.87 % (3021986)Termination reason: Instruction limit
% 15.62/2.87 % (3021986)Termination phase: Property scanning
% 15.62/2.87 % (3021986)Time elapsed: 0.109 s
% 15.62/2.87 % (3021986)Peak memory usage: 12 MB
% 15.62/2.87 % (3021986)Instructions burned: 116 (million)
% 15.62/2.87 % (3021994)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3501330881:i=421:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/421Mi)
% 15.62/2.87 % (3021980)Instruction limit reached!
% 15.62/2.87 % (3021980)------------------------------
% 15.62/2.87 % (3021980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.87 % (3021980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.87 % (3021980)CaDiCaL version: 2.1.3
% 15.62/2.87 % (3021980)Termination reason: Instruction limit
% 15.62/2.87 % (3021980)Termination phase: Saturation
% 15.62/2.87 % (3021980)Time elapsed: 0.298 s
% 15.62/2.87 % (3021980)Peak memory usage: 15 MB
% 15.62/2.87 % (3021980)Instructions burned: 341 (million)
% 15.62/2.87 % (3021996)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
% 15.62/2.87 % (3021996)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=691721332:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2981 on theBenchmark for (2981ds/270Mi)
% 15.62/2.87 % (3021982)Instruction limit reached!
% 15.62/2.87 % (3021982)------------------------------
% 15.62/2.87 % (3021982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.87 % (3021982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.87 % (3021982)CaDiCaL version: 2.1.3
% 15.62/2.87 % (3021982)Termination reason: Instruction limit
% 15.62/2.87 % (3021982)Termination phase: Saturation
% 15.62/2.87 % (3021982)Time elapsed: 0.323 s
% 15.62/2.87 % (3021982)Peak memory usage: 14 MB
% 15.62/2.87 % (3021982)Instructions burned: 374 (million)
% 15.62/2.87 % (3021990)Instruction limit reached!
% 15.62/2.87 % (3021990)------------------------------
% 15.62/2.87 % (3021990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.62/2.87 % (3021990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.62/2.87 % (3021990)CaDiCaL version: 2.1.3
% 15.62/2.87 % (3021990)Termination reason: Instruction limit
% 15.94/2.98 % (3021990)Termination phase: Saturation
% 15.94/2.98 % (3021990)Time elapsed: 0.226 s
% 15.94/2.98 % (3021990)Peak memory usage: 14 MB
% 15.94/2.98 % (3021990)Instructions burned: 271 (million)
% 15.94/2.98 % (3021998)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=955475133:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2980 on theBenchmark for (2980ds/31Mi)
% 15.94/2.98 % (3021999)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 15.94/2.98 % (3021999)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
% 15.94/2.98 % (3021999)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=2284860241:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2980 on theBenchmark for (2980ds/1440Mi)
% 15.94/2.98 % (3021998)Instruction limit reached!
% 15.94/2.98 % (3021998)------------------------------
% 15.94/2.98 % (3021998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3021998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3021998)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3021998)Termination reason: Instruction limit
% 15.94/2.98 % (3021998)Termination phase: shuffling
% 15.94/2.98 % (3021998)Time elapsed: 0.028 s
% 15.94/2.98 % (3021998)Peak memory usage: 10 MB
% 15.94/2.98 % (3021998)Instructions burned: 31 (million)
% 15.94/2.98 % (3022002)dis+10_2_sil=128000:si=on:random_seed=874769179:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2980 on theBenchmark for (2980ds/339Mi)
% 15.94/2.98 % (3021996)Instruction limit reached!
% 15.94/2.98 % (3021996)------------------------------
% 15.94/2.98 % (3021996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3021996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3021996)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3021996)Termination reason: Instruction limit
% 15.94/2.98 % (3021996)Termination phase: Saturation
% 15.94/2.98 % (3021996)Time elapsed: 0.186 s
% 15.94/2.98 % (3021996)Peak memory usage: 14 MB
% 15.94/2.98 % (3021996)Instructions burned: 271 (million)
% 15.94/2.98 % (3022004)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=146442494:i=111:add=on:fgj=on:rtra=on:fdi=1024_2979 on theBenchmark for (2979ds/111Mi)
% 15.94/2.98 % (3021994)Instruction limit reached!
% 15.94/2.98 % (3021994)------------------------------
% 15.94/2.98 % (3021994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3021994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3021994)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3021994)Termination reason: Instruction limit
% 15.94/2.98 % (3021994)Termination phase: Saturation
% 15.94/2.98 % (3021994)Time elapsed: 0.326 s
% 15.94/2.98 % (3021994)Peak memory usage: 15 MB
% 15.94/2.98 % (3021994)Instructions burned: 421 (million)
% 15.94/2.98 % (3021987)Instruction limit reached!
% 15.94/2.98 % (3021987)------------------------------
% 15.94/2.98 % (3021987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3021987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3021987)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3021987)Termination reason: Instruction limit
% 15.94/2.98 % (3021987)Termination phase: Saturation
% 15.94/2.98 % (3021987)Time elapsed: 0.481 s
% 15.94/2.98 % (3021987)Peak memory usage: 18 MB
% 15.94/2.98 % (3021987)Instructions burned: 576 (million)
% 15.94/2.98 % (3022004)Instruction limit reached!
% 15.94/2.98 % (3022004)------------------------------
% 15.94/2.98 % (3022004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022004)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022004)Termination reason: Instruction limit
% 15.94/2.98 % (3022004)Termination phase: Saturation
% 15.94/2.98 % (3022004)Time elapsed: 0.070 s
% 15.94/2.98 % (3022004)Peak memory usage: 13 MB
% 15.94/2.98 % (3022004)Instructions burned: 111 (million)
% 15.94/2.98 % (3022006)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=632943318:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/122Mi)
% 15.94/2.98 % (3022009)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1172069464:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2978 on theBenchmark for (2978ds/232Mi)
% 15.94/2.98 % (3022007)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=3759767534:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/136Mi)
% 15.94/2.98 % (3022006)Instruction limit reached!
% 15.94/2.98 % (3022006)------------------------------
% 15.94/2.98 % (3022006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022006)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022006)Termination reason: Instruction limit
% 15.94/2.98 % (3022006)Termination phase: Saturation
% 15.94/2.98 % (3022006)Time elapsed: 0.106 s
% 15.94/2.98 % (3022006)Peak memory usage: 14 MB
% 15.94/2.98 % (3022006)Instructions burned: 122 (million)
% 15.94/2.98 % (3022002)Instruction limit reached!
% 15.94/2.98 % (3022002)------------------------------
% 15.94/2.98 % (3022002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022002)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022002)Termination reason: Instruction limit
% 15.94/2.98 % (3022002)Termination phase: Saturation
% 15.94/2.98 % (3022002)Time elapsed: 0.274 s
% 15.94/2.98 % (3022002)Peak memory usage: 15 MB
% 15.94/2.98 % (3022002)Instructions burned: 339 (million)
% 15.94/2.98 % (3022013)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 15.94/2.98 % (3022007)Instruction limit reached!
% 15.94/2.98 % (3022007)------------------------------
% 15.94/2.98 % (3022007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022007)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022007)Termination reason: Instruction limit
% 15.94/2.98 % (3022007)Termination phase: Saturation
% 15.94/2.98 % (3022007)Time elapsed: 0.115 s
% 15.94/2.98 % (3022007)Peak memory usage: 13 MB
% 15.94/2.98 % (3022007)Instructions burned: 136 (million)
% 15.94/2.98 % (3022012)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=825901351:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2977 on theBenchmark for (2977ds/1254Mi)
% 15.94/2.98 % (3022013)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=4286221599:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2977 on theBenchmark for (2977ds/281Mi)
% 15.94/2.98 % (3022014)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=631832033:i=619:add=on:rtra=on_2976 on theBenchmark for (2976ds/619Mi)
% 15.94/2.98 % (3022009)Instruction limit reached!
% 15.94/2.98 % (3022009)------------------------------
% 15.94/2.98 % (3022009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022009)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022009)Termination reason: Instruction limit
% 15.94/2.98 % (3022009)Termination phase: Saturation
% 15.94/2.98 % (3022009)Time elapsed: 0.174 s
% 15.94/2.98 % (3022009)Peak memory usage: 14 MB
% 15.94/2.98 % (3022009)Instructions burned: 232 (million)
% 15.94/2.98 % (3022018)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=4257027579:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2976 on theBenchmark for (2976ds/865Mi)
% 15.94/2.98 % (3022014)Refutation not found, incomplete strategy
% 15.94/2.98 % (3022014)------------------------------
% 15.94/2.98 % (3022014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022014)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022014)Termination reason: Refutation not found, incomplete strategy
% 15.94/2.98 % (3022014)Time elapsed: 0.169 s
% 15.94/2.98 % (3022014)Peak memory usage: 16 MB
% 15.94/2.98 % (3022014)Instructions burned: 203 (million)
% 15.94/2.98 % (3022014)------------------------------
% 15.94/2.98 % (3022014)------------------------------
% 15.94/2.98 % (3022013)Instruction limit reached!
% 15.94/2.98 % (3022013)------------------------------
% 15.94/2.98 % (3022013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022013)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022013)Termination reason: Instruction limit
% 15.94/2.98 % (3022013)Termination phase: Saturation
% 15.94/2.98 % (3022013)Time elapsed: 0.231 s
% 15.94/2.98 % (3022013)Peak memory usage: 14 MB
% 15.94/2.98 % (3022013)Instructions burned: 281 (million)
% 15.94/2.98 % (3022020)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2041740499:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/212Mi)
% 15.94/2.98 % (3022012)Refutation not found, incomplete strategy
% 15.94/2.98 % (3022012)------------------------------
% 15.94/2.98 % (3022012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022012)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022012)Termination reason: Refutation not found, incomplete strategy
% 15.94/2.98 % (3022012)Time elapsed: 0.246 s
% 15.94/2.98 % (3022012)Peak memory usage: 16 MB
% 15.94/2.98 % (3022012)Instructions burned: 294 (million)
% 15.94/2.98 % (3022012)------------------------------
% 15.94/2.98 % (3022012)------------------------------
% 15.94/2.98 % (3022021)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=2140141569:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/130Mi)
% 15.94/2.98 % (3022023)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2128963581:st=1.5:i=346:rtra=on:ss=axioms_2974 on theBenchmark for (2974ds/346Mi)
% 15.94/2.98 % (3022021) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3021809-3022021"...
% 15.94/2.98 % (3022021)...printing done.
% 15.94/2.98 % (3022021)Refutation found. Thanks to Tanya!
% 15.94/2.98 % SZS status Theorem for theBenchmark
% 15.94/2.98 % SZS output start Proof for theBenchmark
% 15.94/2.98 thf(type_def_5, type, rBT_Im1923302023_color: $tType).
% 15.94/2.98 thf(type_def_6, type, rBT_Im246033960le_rbt: ($tType * $tType) > $tType).
% 15.94/2.98 thf(type_def_7, type, set: $tType > $tType).
% 15.94/2.98 thf(type_def_8, type, nat: $tType).
% 15.94/2.98 thf(type_def_9, type, itself: $tType > $tType).
% 15.94/2.98 thf(type_def_10, type, b: $tType).
% 15.94/2.98 thf(type_def_11, type, a: $tType).
% 15.94/2.98 thf(type_def_12, type, sTfun: ($tType * $tType) > $tType).
% 15.94/2.98 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_1, type, ord: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_2, type, order: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_3, type, no_bot: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_4, type, no_top: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_5, type, linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_6, type, preorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_7, type, zero_neq_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_8, type, wellorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_9, type, zero_less_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_10, type, dense_order: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_11, type, linordered_idom: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_12, type, linordered_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_13, type, dense_linorder: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_14, type, linordered_semidom: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_15, type, ordered_ab_group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_16, type, linord219039673up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_17, type, ordere216010020id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_18, type, ordere142940540dd_abs: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_19, type, linord1659791738miring: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_20, type, canoni770627133id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_21, type, strict797366125id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_22, type, ordere236663937imp_le: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_23, type, ordere223160158up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_24, type, strict2144017051up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_25, type, ordere516151231imp_le: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_26, type, condit1656338222tinuum: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_27, type, condit1037483654norder: !>[X0: $tType]:((itself @ X0 > $o))).
% 15.94/2.98 thf(func_def_28, type, bNF_eq_onp: !>[X0: $tType]:(((X0 > $o) > X0 > X0 > $o))).
% 15.94/2.98 thf(func_def_29, type, abs_abs: !>[X0: $tType]:((X0 > X0))).
% 15.94/2.98 thf(func_def_30, type, one_one: !>[X0: $tType]:(X0)).
% 15.94/2.98 thf(func_def_31, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 15.94/2.98 thf(func_def_32, type, sgn_sgn: !>[X0: $tType]:((X0 > X0))).
% 15.94/2.98 thf(func_def_33, type, uminus_uminus: !>[X0: $tType]:((X0 > X0))).
% 15.94/2.98 thf(func_def_34, type, zero_zero: !>[X0: $tType]:(X0)).
% 15.94/2.98 thf(func_def_35, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 15.94/2.98 thf(func_def_36, type, suc: (nat > nat)).
% 15.94/2.98 thf(func_def_37, type, semiring_1_of_nat: !>[X0: $tType]:((nat > X0))).
% 15.94/2.98 thf(func_def_38, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 15.94/2.98 thf(func_def_39, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 15.94/2.98 thf(func_def_40, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 15.94/2.98 thf(func_def_41, type, order_strict_mono: !>[X0: $tType, X1: $tType]:(((X0 > X1) > $o))).
% 15.94/2.98 thf(func_def_42, type, power_power: !>[X0: $tType]:((X0 > nat > X0))).
% 15.94/2.98 thf(func_def_43, type, type2: !>[X0: $tType]:(itself @ X0)).
% 15.94/2.98 thf(func_def_44, type, rBT_Im315265182height: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > nat))).
% 15.94/2.98 thf(func_def_45, type, rBT_Impl_Mirabelle_B: rBT_Im1923302023_color).
% 15.94/2.98 thf(func_def_46, type, rBT_Impl_Mirabelle_R: rBT_Im1923302023_color).
% 15.94/2.98 thf(func_def_47, type, rBT_Im1975547051_color: !>[X0: $tType]:((X0 > X0 > rBT_Im1923302023_color > X0))).
% 15.94/2.98 thf(func_def_48, type, rBT_Im1059957627_color: !>[X0: $tType]:((X0 > X0 > rBT_Im1923302023_color > X0))).
% 15.94/2.98 thf(func_def_49, type, rBT_Im800559290_color: (rBT_Im1923302023_color > nat)).
% 15.94/2.98 thf(func_def_50, type, rBT_Im1805589839lor_of: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > rBT_Im1923302023_color))).
% 15.94/2.98 thf(func_def_51, type, rBT_Im1040612427e_inv1: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_52, type, rBT_Im1071879905_inv1l: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_53, type, rBT_Im1259024060reater: !>[X0: $tType, X1: $tType]:(((X0 > X0 > $o) > X0 > rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_54, type, rBT_Im2075124343t_less: !>[X0: $tType, X1: $tType]:(((X0 > X0 > $o) > X0 > rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_55, type, rBT_Im759614907sorted: !>[X0: $tType, X1: $tType]:(((X0 > X0 > $o) > rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_56, type, rBT_Im1332541288reater: !>[X0: $tType, X1: $tType]:((X0 > rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_57, type, rBT_Im903026891t_less: !>[X0: $tType, X1: $tType]:((X0 > rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_58, type, rBT_Im1183586831sorted: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_59, type, rBT_Im480247531Branch: !>[X0: $tType, X1: $tType]:((rBT_Im1923302023_color > rBT_Im246033960le_rbt @ X0 @ X1 > X0 > X1 > rBT_Im246033960le_rbt @ X0 @ X1 > rBT_Im246033960le_rbt @ X0 @ X1))).
% 15.94/2.98 thf(func_def_60, type, rBT_Im418718756_Empty: !>[X0: $tType, X1: $tType]:(rBT_Im246033960le_rbt @ X0 @ X1)).
% 15.94/2.98 thf(func_def_61, type, rBT_Im858806507se_rbt: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > (rBT_Im1923302023_color > rBT_Im246033960le_rbt @ X1 @ X2 > X1 > X2 > rBT_Im246033960le_rbt @ X1 @ X2 > X0) > rBT_Im246033960le_rbt @ X1 @ X2 > X0))).
% 15.94/2.98 thf(func_def_62, type, rBT_Im1931894874ed_rbt: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X1 > $o) > rBT_Im246033960le_rbt @ X0 @ X1 > $o))).
% 15.94/2.98 thf(func_def_63, type, rBT_Im1947144893ec_rbt: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > (rBT_Im1923302023_color > rBT_Im246033960le_rbt @ X1 @ X2 > X1 > X2 > rBT_Im246033960le_rbt @ X1 @ X2 > X0 > X0 > X0) > rBT_Im246033960le_rbt @ X1 @ X2 > X0))).
% 15.94/2.98 thf(func_def_64, type, rBT_Im1000242676el_rbt: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X0 > X1 > $o) > (X2 > X3 > $o) > rBT_Im246033960le_rbt @ X0 @ X2 > rBT_Im246033960le_rbt @ X1 @ X3 > $o))).
% 15.94/2.98 thf(func_def_65, type, rBT_Im1178217900t1_rbt: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > set @ X0))).
% 15.94/2.98 thf(func_def_66, type, rBT_Im1550225131t2_rbt: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > set @ X1))).
% 15.94/2.98 thf(func_def_67, type, rBT_Im1485196410ze_rbt: !>[X0: $tType, X1: $tType]:(((X0 > nat) > (X1 > nat) > rBT_Im246033960le_rbt @ X0 @ X1 > nat))).
% 15.94/2.98 thf(func_def_68, type, zero_neq_one_of_bool: !>[X0: $tType]:(($o > X0))).
% 15.94/2.98 thf(func_def_69, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 15.94/2.98 thf(func_def_70, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 15.94/2.98 thf(func_def_71, type, t: rBT_Im246033960le_rbt @ a @ b).
% 15.94/2.98 thf(func_def_75, type, vAND: ($o > $o > $o)).
% 15.94/2.98 thf(func_def_76, type, db0: !>[X0: $tType]:(X0)).
% 15.94/2.98 thf(func_def_77, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 15.94/2.98 thf(func_def_78, type, db1: !>[X0: $tType]:(X0)).
% 15.94/2.98 thf(func_def_79, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 15.94/2.98 thf(func_def_80, type, vNOT: ($o > $o)).
% 15.94/2.98 thf(func_def_81, type, vOR: ($o > $o > $o)).
% 15.94/2.98 thf(func_def_82, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 15.94/2.98 thf(func_def_83, type, vIMP: ($o > $o > $o)).
% 15.94/2.98 thf(func_def_84, type, db2: !>[X0: $tType]:(X0)).
% 15.94/2.98 thf(func_def_85, type, db3: !>[X0: $tType]:(X0)).
% 15.94/2.98 thf(func_def_86, type, sK0: !>[X0: $tType, X1: $tType]:(((rBT_Im246033960le_rbt @ X0 @ X1 > $o) > X0))).
% 15.94/2.98 thf(func_def_87, type, sK1: !>[X0: $tType, X1: $tType]:(((rBT_Im246033960le_rbt @ X0 @ X1 > $o) > X1))).
% 15.94/2.98 thf(func_def_88, type, sK2: !>[X0: $tType, X1: $tType]:(((rBT_Im246033960le_rbt @ X0 @ X1 > $o) > rBT_Im246033960le_rbt @ X0 @ X1))).
% 15.94/2.98 thf(func_def_89, type, sK3: !>[X0: $tType, X1: $tType]:(((rBT_Im246033960le_rbt @ X0 @ X1 > $o) > rBT_Im1923302023_color))).
% 15.94/2.98 thf(func_def_90, type, sK4: !>[X0: $tType, X1: $tType]:(((rBT_Im246033960le_rbt @ X0 @ X1 > $o) > rBT_Im246033960le_rbt @ X0 @ X1))).
% 15.94/2.98 thf(func_def_91, type, sK5: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 15.94/2.98 thf(func_def_92, type, sK6: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > rBT_Im246033960le_rbt @ X0 @ X1))).
% 15.94/2.98 thf(func_def_93, type, sK7: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > X1))).
% 15.94/2.98 thf(func_def_94, type, sK8: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > rBT_Im246033960le_rbt @ X0 @ X1))).
% 15.94/2.98 thf(func_def_95, type, sK9: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > rBT_Im1923302023_color))).
% 15.94/2.98 thf(func_def_96, type, sK10: !>[X0: $tType, X1: $tType]:((rBT_Im246033960le_rbt @ X0 @ X1 > X0))).
% 15.94/2.98 thf(f1,axiom,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X7 : X0,X8 : X1,X5 : rBT_Im1923302023_color,X9 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : rBT_Im246033960le_rbt @ X0 @ X1] : ((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X6) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X9) = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X6 @ X7 @ X8 @ X9))))),
% 15.94/2.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_inv1l_Osimps_I2_J)).
% 15.94/2.98 thf(f2,axiom,(
% 15.94/2.98 ! [X1 : $tType,X0 : $tType] : (rBT_Im1071879905_inv1l @ X1 @ X0 @ rBT_Im418718756_Empty @ X1 @ X0)),
% 15.94/2.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_inv1l_Osimps_I1_J)).
% 15.94/2.98 thf(f4,axiom,(
% 15.94/2.98 ! [X1 : $tType,X0 : $tType,X5 : X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X4 : X0,X2 : rBT_Im1923302023_color,X6 : rBT_Im246033960le_rbt @ X0 @ X1] : ((((((rBT_Im1805589839lor_of @ X0 @ X1 @ X3)) = rBT_Impl_Mirabelle_B) & (((rBT_Im1805589839lor_of @ X0 @ X1 @ X6)) = rBT_Impl_Mirabelle_B)) | (X2 = rBT_Impl_Mirabelle_B)) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X6) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3) = ((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6))))),
% 15.94/2.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_inv1_Osimps_I2_J)).
% 15.94/2.98 thf(f12,axiom,(
% 15.94/2.98 ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X1 @ X0] : ((X2 != rBT_Im418718756_Empty @ X1 @ X0) => ~ ! [X3 : rBT_Im1923302023_color,X4 : rBT_Im246033960le_rbt @ X1 @ X0,X6 : X0,X7 : rBT_Im246033960le_rbt @ X1 @ X0,X5 : X1] : (X2 != ((rBT_Im480247531Branch @ X1 @ X0 @ X3 @ X4 @ X5 @ X6 @ X7))))),
% 15.94/2.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_rbt_Oexhaust)).
% 15.94/2.98 thf(f288,axiom,(
% 15.94/2.98 (rBT_Im1040612427e_inv1 @ a @ b @ t)),
% 15.94/2.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 15.94/2.98 thf(f289,conjecture,(
% 15.94/2.98 (rBT_Im1071879905_inv1l @ a @ b @ t)),
% 15.94/2.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1)).
% 15.94/2.98 thf(f290,negated_conjecture,(
% 15.94/2.98 ~(rBT_Im1071879905_inv1l @ a @ b @ t)),
% 15.94/2.98 inference(negated_conjecture,[status(cth)],[f289])).
% 15.94/2.98 thf(f335,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X1,X4 : rBT_Im1923302023_color,X5 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : rBT_Im246033960le_rbt @ X0 @ X1] : ((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X6) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X5) = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X4 @ X6 @ X2 @ X3 @ X5))))),
% 15.94/2.98 inference(rectify,[],[f1])).
% 15.94/2.98 thf(f336,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : X0,X5 : rBT_Im246033960le_rbt @ X0 @ X1,X4 : rBT_Im1923302023_color,X6 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : X1] : (((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X4 @ X6 @ X2 @ X3 @ X5))) = (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X5) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X6))))),
% 15.94/2.98 inference(fool_elimination,[],[f335])).
% 15.94/2.98 thf(f429,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType] : (rBT_Im1071879905_inv1l @ X0 @ X1 @ rBT_Im418718756_Empty @ X0 @ X1)),
% 15.94/2.98 inference(rectify,[],[f2])).
% 15.94/2.98 thf(f430,plain,(
% 15.94/2.98 ! [X1 : $tType,X0 : $tType] : ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ rBT_Im418718756_Empty @ X0 @ X1)))),
% 15.94/2.98 inference(fool_elimination,[],[f429])).
% 15.94/2.98 thf(f670,plain,(
% 15.94/2.98 (rBT_Im1040612427e_inv1 @ a @ b @ t)),
% 15.94/2.98 inference(rectify,[],[f288])).
% 15.94/2.98 thf(f671,plain,(
% 15.94/2.98 (((rBT_Im1040612427e_inv1 @ a @ b @ t)) = $true)),
% 15.94/2.98 inference(fool_elimination,[],[f670])).
% 15.94/2.98 thf(f732,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : rBT_Im246033960le_rbt @ X1 @ X0,X4 : X1,X5 : rBT_Im1923302023_color,X6 : rBT_Im246033960le_rbt @ X1 @ X0] : ((((rBT_Impl_Mirabelle_B = ((rBT_Im1805589839lor_of @ X1 @ X0 @ X3))) & (rBT_Impl_Mirabelle_B = ((rBT_Im1805589839lor_of @ X1 @ X0 @ X6)))) | (rBT_Impl_Mirabelle_B = X5)) & (rBT_Im1040612427e_inv1 @ X1 @ X0 @ X6) & (rBT_Im1040612427e_inv1 @ X1 @ X0 @ X3) = ((rBT_Im1040612427e_inv1 @ X1 @ X0 @ (rBT_Im480247531Branch @ X1 @ X0 @ X5 @ X3 @ X4 @ X2 @ X6))))),
% 15.94/2.98 inference(rectify,[],[f4])).
% 15.94/2.98 thf(f733,plain,(
% 15.94/2.98 ! [X1 : $tType,X0 : $tType,X3 : rBT_Im246033960le_rbt @ X1 @ X0,X6 : rBT_Im246033960le_rbt @ X1 @ X0,X4 : X1,X5 : rBT_Im1923302023_color,X2 : X0] : (((rBT_Im1040612427e_inv1 @ X1 @ X0 @ (rBT_Im480247531Branch @ X1 @ X0 @ X5 @ X3 @ X4 @ X2 @ X6))) = ((((rBT_Im1040612427e_inv1 @ X1 @ X0 @ X3) & (rBT_Im1040612427e_inv1 @ X1 @ X0 @ X6)) & ((rBT_Impl_Mirabelle_B = X5) | ((rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X1 @ X0 @ X6)) & (rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X1 @ X0 @ X3)))))))),
% 15.94/2.98 inference(fool_elimination,[],[f732])).
% 15.94/2.98 thf(f794,plain,(
% 15.94/2.98 ~(rBT_Im1071879905_inv1l @ a @ b @ t)),
% 15.94/2.98 inference(rectify,[],[f290])).
% 15.94/2.98 thf(f795,plain,(
% 15.94/2.98 ~ (((rBT_Im1071879905_inv1l @ a @ b @ t)) = $true)),
% 15.94/2.98 inference(fool_elimination,[],[f794])).
% 15.94/2.98 thf(f810,plain,(
% 15.94/2.98 (((rBT_Im1071879905_inv1l @ a @ b @ t)) != $true)),
% 15.94/2.98 inference(flattening,[],[f795])).
% 15.94/2.98 thf(f812,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((rBT_Im418718756_Empty @ X0 @ X1 != X2) => ~ ! [X5 : X1,X3 : rBT_Im1923302023_color,X6 : rBT_Im246033960le_rbt @ X0 @ X1,X7 : X0,X4 : rBT_Im246033960le_rbt @ X0 @ X1] : (((rBT_Im480247531Branch @ X0 @ X1 @ X3 @ X4 @ X7 @ X5 @ X6)) != X2))),
% 15.94/2.98 inference(rectify,[],[f12])).
% 15.94/2.98 thf(f817,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : (? [X4 : rBT_Im246033960le_rbt @ X0 @ X1,X5 : X1,X6 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im1923302023_color,X7 : X0] : (((rBT_Im480247531Branch @ X0 @ X1 @ X3 @ X4 @ X7 @ X5 @ X6)) = X2) | (rBT_Im418718756_Empty @ X0 @ X1 = X2))),
% 15.94/2.98 inference(ennf_transformation,[],[f812])).
% 15.94/2.98 thf(f821,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X4 : rBT_Im1923302023_color,X5 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1] : ((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X5))) = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X4 @ X5 @ X2 @ X6 @ X3))))),
% 15.94/2.98 inference(rectify,[],[f336])).
% 15.94/2.98 thf(f824,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X4 : X0,X5 : rBT_Im1923302023_color,X6 : X1] : (((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3)) & ((rBT_Impl_Mirabelle_B = X5) | ((rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X0 @ X1 @ X3)) & (rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X0 @ X1 @ X2)))))) = ((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X2 @ X4 @ X6 @ X3))))),
% 15.94/2.98 inference(rectify,[],[f733])).
% 15.94/2.98 thf(f826,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : (? [X3 : rBT_Im246033960le_rbt @ X0 @ X1,X4 : X1,X5 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : rBT_Im1923302023_color,X7 : X0] : (((rBT_Im480247531Branch @ X0 @ X1 @ X6 @ X3 @ X7 @ X4 @ X5)) = X2) | (rBT_Im418718756_Empty @ X0 @ X1 = X2))),
% 15.94/2.98 inference(rectify,[],[f817])).
% 15.94/2.98 thf(f827,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((((rBT_Im480247531Branch @ X0 @ X1 @ (sK9 @ X0 @ X1 @ X2) @ (sK6 @ X0 @ X1 @ X2) @ (sK10 @ X0 @ X1 @ X2) @ (sK7 @ X0 @ X1 @ X2) @ (sK8 @ X0 @ X1 @ X2))) = X2) | (rBT_Im418718756_Empty @ X0 @ X1 = X2))),
% 15.94/2.98 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X8,sK4 @ X0 @ X1 @ X3),skolemize(X8,sK4 @ X0 @ X1 @ X3),skolemize(X8,sK4 @ X0 @ X1 @ X3),skolemize(X8,sK4 @ X0 @ X1 @ X3),skolemize(X8,sK4 @ X0 @ X1 @ X3)],[f826])).
% 15.94/2.98 thf(f828,plain,(
% 15.94/2.98 ! [X0 : $tType,X1 : $tType] : (((rBT_Im1071879905_inv1l @ X1 @ X0 @ rBT_Im418718756_Empty @ X1 @ X0)) = $true)),
% 15.94/2.98 inference(rectify,[],[f430])).
% 15.94/2.98 thf(f830,plain,(
% 15.94/2.98 (((rBT_Im1040612427e_inv1 @ a @ b @ t)) = $true)),
% 15.94/2.98 inference(cnf_transformation,[],[f671])).
% 15.94/2.98 thf(f835,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : rBT_Im1923302023_color,X5 : rBT_Im246033960le_rbt @ X0 @ X1] : (((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X5))) = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X4 @ X5 @ X2 @ X6 @ X3))))) )),
% 15.94/2.98 inference(cnf_transformation,[],[f821])).
% 15.94/2.98 thf(f837,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : X0,X5 : rBT_Im1923302023_color] : ((((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3)) & ((rBT_Impl_Mirabelle_B = X5) | ((rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X0 @ X1 @ X3)) & (rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X0 @ X1 @ X2)))))) = ((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X2 @ X4 @ X6 @ X3))))) )),
% 15.94/2.98 inference(cnf_transformation,[],[f824])).
% 15.94/2.98 thf(f839,plain,(
% 15.94/2.98 (((rBT_Im1071879905_inv1l @ a @ b @ t)) != $true)),
% 15.94/2.98 inference(cnf_transformation,[],[f810])).
% 15.94/2.98 thf(f840,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((((rBT_Im480247531Branch @ X0 @ X1 @ (sK9 @ X0 @ X1 @ X2) @ (sK6 @ X0 @ X1 @ X2) @ (sK10 @ X0 @ X1 @ X2) @ (sK7 @ X0 @ X1 @ X2) @ (sK8 @ X0 @ X1 @ X2))) = X2) | (rBT_Im418718756_Empty @ X0 @ X1 = X2)) )),
% 15.94/2.98 inference(cnf_transformation,[],[f827])).
% 15.94/2.98 thf(f841,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType] : ((((rBT_Im1071879905_inv1l @ X1 @ X0 @ rBT_Im418718756_Empty @ X1 @ X0)) = $true)) )),
% 15.94/2.98 inference(cnf_transformation,[],[f828])).
% 15.94/2.98 thf(f844,definition,(
% 15.94/2.98 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 15.94/2.98 introduced(theory,[fool_exhaustiveness_axiom])).
% 15.94/2.98 thf(f845,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : X0,X5 : rBT_Im1923302023_color] : ((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X2 @ X4 @ X6 @ X3))) = $false) | (((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3)) & ((rBT_Impl_Mirabelle_B = X5) | ((rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X0 @ X1 @ X3)) & (rBT_Impl_Mirabelle_B = (rBT_Im1805589839lor_of @ X0 @ X1 @ X2)))))) = $true)) )),
% 15.94/2.98 inference(iff_proxy_clausification,[],[f837])).
% 15.94/2.98 thf(f856,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : X0,X5 : rBT_Im1923302023_color] : (($true = (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3)))) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X2 @ X4 @ X6 @ X3))) = $false)) )),
% 15.94/2.98 inference(and_proxy_clausification,[],[f845])).
% 15.94/2.98 thf(f857,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : X0,X5 : rBT_Im1923302023_color] : ((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X2 @ X4 @ X6 @ X3))) = $false) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3)) = $true)) )),
% 15.94/2.98 inference(and_proxy_clausification,[],[f856])).
% 15.94/2.98 thf(f858,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : X0,X5 : rBT_Im1923302023_color] : ((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X5 @ X2 @ X4 @ X6 @ X3))) = $false) | ($true = ((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)))) )),
% 15.94/2.98 inference(and_proxy_clausification,[],[f856])).
% 15.94/2.98 thf(f867,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : rBT_Im1923302023_color,X5 : rBT_Im246033960le_rbt @ X0 @ X1] : (((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3) & (rBT_Im1040612427e_inv1 @ X0 @ X1 @ X5))) = $false) | ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X4 @ X5 @ X2 @ X6 @ X3))))) )),
% 15.94/2.98 inference(iff_proxy_clausification,[],[f835])).
% 15.94/2.98 thf(f868,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : rBT_Im246033960le_rbt @ X0 @ X1,X6 : X1,X4 : rBT_Im1923302023_color,X5 : rBT_Im246033960le_rbt @ X0 @ X1] : (($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ (rBT_Im480247531Branch @ X0 @ X1 @ X4 @ X5 @ X2 @ X6 @ X3)))) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X5)) = $false) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X3)) = $false)) )),
% 15.94/2.98 inference(and_proxy_clausification,[],[f867])).
% 15.94/2.98 thf(f899,plain,(
% 15.94/2.98 ($true != $true) | (((rBT_Im1071879905_inv1l @ a @ b @ t)) = $false)),
% 15.94/2.98 inference(superposition,[],[f839,f844])).
% 15.94/2.98 thf(f901,plain,(
% 15.94/2.98 (((rBT_Im1071879905_inv1l @ a @ b @ t)) = $false)),
% 15.94/2.98 inference(trivial_inequality_removal,[],[f899])).
% 15.94/2.98 thf(f1109,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X2 : $tType,X0 : rBT_Im246033960le_rbt @ X1 @ X2] : ((((rBT_Im1040612427e_inv1 @ X1 @ X2 @ (sK6 @ X1 @ X2 @ X0))) = $true) | (((rBT_Im1040612427e_inv1 @ X1 @ X2 @ X0)) = $false) | (rBT_Im418718756_Empty @ X1 @ X2 = X0)) )),
% 15.94/2.98 inference(superposition,[],[f858,f840])).
% 15.94/2.98 thf(f1110,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X2 : $tType,X0 : rBT_Im246033960le_rbt @ X1 @ X2] : (($true = ((rBT_Im1040612427e_inv1 @ X1 @ X2 @ (sK8 @ X1 @ X2 @ X0)))) | (rBT_Im418718756_Empty @ X1 @ X2 = X0) | (((rBT_Im1040612427e_inv1 @ X1 @ X2 @ X0)) = $false)) )),
% 15.94/2.98 inference(superposition,[],[f857,f840])).
% 15.94/2.98 thf(f1126,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X2 : $tType,X0 : rBT_Im246033960le_rbt @ X1 @ X2] : ((((rBT_Im1040612427e_inv1 @ X1 @ X2 @ (sK8 @ X1 @ X2 @ X0))) = $false) | (rBT_Im418718756_Empty @ X1 @ X2 = X0) | ($true = ((rBT_Im1071879905_inv1l @ X1 @ X2 @ X0))) | (((rBT_Im1040612427e_inv1 @ X1 @ X2 @ (sK6 @ X1 @ X2 @ X0))) = $false)) )),
% 15.94/2.98 inference(superposition,[],[f868,f840])).
% 15.94/2.98 thf(f1136,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((rBT_Im418718756_Empty @ X0 @ X1 = X2) | (rBT_Im418718756_Empty @ X0 @ X1 = X2) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (sK6 @ X0 @ X1 @ X2))) = $false) | ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ X2))) | ($true = $false)) )),
% 15.94/2.98 inference(superposition,[],[f1126,f1110])).
% 15.94/2.98 thf(f1141,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : (($true = $false) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (sK6 @ X0 @ X1 @ X2))) = $false) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false) | ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ X2))) | (rBT_Im418718756_Empty @ X0 @ X1 = X2)) )),
% 15.94/2.98 inference(duplicate_literal_removal,[],[f1136])).
% 15.94/2.98 thf(f1142,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((((rBT_Im1040612427e_inv1 @ X0 @ X1 @ (sK6 @ X0 @ X1 @ X2))) = $false) | (rBT_Im418718756_Empty @ X0 @ X1 = X2) | ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ X2))) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false)) )),
% 15.94/2.98 inference(trivial_inequality_removal,[],[f1141])).
% 15.94/2.98 thf(f1150,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((rBT_Im418718756_Empty @ X0 @ X1 = X2) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false) | ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ X2))) | (rBT_Im418718756_Empty @ X0 @ X1 = X2) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false) | ($true = $false)) )),
% 15.94/2.98 inference(superposition,[],[f1142,f1109])).
% 15.94/2.98 thf(f1155,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : ((rBT_Im418718756_Empty @ X0 @ X1 = X2) | ($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ X2))) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false) | ($true = $false)) )),
% 15.94/2.98 inference(duplicate_literal_removal,[],[f1150])).
% 15.94/2.98 thf(f1156,plain,(
% 15.94/2.98 ( ! [X1 : $tType,X0 : $tType,X2 : rBT_Im246033960le_rbt @ X0 @ X1] : (($true = ((rBT_Im1071879905_inv1l @ X0 @ X1 @ X2))) | (((rBT_Im1040612427e_inv1 @ X0 @ X1 @ X2)) = $false) | (rBT_Im418718756_Empty @ X0 @ X1 = X2)) )),
% 15.94/2.98 inference(trivial_inequality_removal,[],[f1155])).
% 15.94/2.98 thf(f1169,plain,(
% 15.94/2.98 (t = rBT_Im418718756_Empty @ a @ b) | ($true = $false) | (((rBT_Im1040612427e_inv1 @ a @ b @ t)) = $false)),
% 15.94/2.98 inference(superposition,[],[f901,f1156])).
% 15.94/2.98 thf(f1176,plain,(
% 15.94/2.98 (t = rBT_Im418718756_Empty @ a @ b) | (((rBT_Im1040612427e_inv1 @ a @ b @ t)) = $false)),
% 15.94/2.98 inference(trivial_inequality_removal,[],[f1169])).
% 15.94/2.98 thf(f1186,plain,(
% 15.94/2.98 (t = rBT_Im418718756_Empty @ a @ b) | ($true = $false)),
% 15.94/2.98 inference(forward_demodulation,[],[f1176,f830])).
% 15.94/2.98 thf(f1187,plain,(
% 15.94/2.98 (t = rBT_Im418718756_Empty @ a @ b)),
% 15.94/2.98 inference(trivial_inequality_removal,[],[f1186])).
% 15.94/2.98 thf(f1195,plain,(
% 15.94/2.98 (((rBT_Im1071879905_inv1l @ a @ b @ t)) = $true)),
% 15.94/2.98 inference(superposition,[],[f841,f1187])).
% 15.94/2.98 thf(f1214,plain,(
% 15.94/2.98 $false),
% 15.94/2.98 inference(forward_subsumption_resolution,[],[f1195,f839])).
% 15.94/2.98 % SZS output end Proof for theBenchmark
% 15.94/2.98 % (3022021)------------------------------
% 15.94/2.98 % (3022021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.94/2.98 % (3022021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.94/2.98 % (3022021)CaDiCaL version: 2.1.3
% 15.94/2.98 % (3022021)Termination reason: Refutation
% 15.94/2.98 % (3022021)Time elapsed: 0.048 s
% 15.94/2.98 % (3022021)Peak memory usage: 14 MB
% 15.94/2.98 % (3022021)Instructions burned: 80 (million)
% 15.94/2.98 % (3021809)Success in time 2.63 s
% 15.94/2.98 % Vampire exiting
%------------------------------------------------------------------------------