%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT226^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 : n018.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 13.90s 2.35s
% Output : Refutation 13.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT226^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n018.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 18:15:09 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.20/0.27 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
% 0.51/0.40 % (449081)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.51/0.40 % (449086)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1038199494:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.51/0.40 % (449092)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.51/0.40 % (449092)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.51/0.40 % (449087)lrs+10_16_si=on:nwc=1.5:random_seed=1493825320:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.51/0.40 % (449088)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3099005230:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.51/0.40 % (449090)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2298929274:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.51/0.40 % (449089)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=2926431707:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.51/0.40 % (449091)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=281381473:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.51/0.40 % (449092)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=4008206294:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.51/0.40 % (449088)Instruction limit reached!
% 0.51/0.40 % (449088)------------------------------
% 0.51/0.40 % (449088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.40 % (449088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.40 % (449088)CaDiCaL version: 2.1.3
% 0.51/0.40 % (449088)Termination reason: Instruction limit
% 0.51/0.40 % (449088)Termination phase: shuffling
% 0.51/0.40 % (449088)Time elapsed: 0.002 s
% 0.51/0.40 % (449088)Peak memory usage: 10 MB
% 0.51/0.40 % (449088)Instructions burned: 3 (million)
% 0.51/0.40 % (449087)Instruction limit reached!
% 0.51/0.40 % (449087)------------------------------
% 0.51/0.40 % (449087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.40 % (449087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.40 % (449087)CaDiCaL version: 2.1.3
% 0.51/0.40 % (449087)Termination reason: Instruction limit
% 0.51/0.40 % (449087)Termination phase: Property scanning
% 0.51/0.40 % (449087)Time elapsed: 0.010 s
% 0.51/0.40 % (449087)Peak memory usage: 10 MB
% 0.51/0.40 % (449087)Instructions burned: 21 (million)
% 0.51/0.40 % (449090)Instruction limit reached!
% 0.51/0.40 % (449090)------------------------------
% 0.51/0.40 % (449090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.40 % (449090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.40 % (449090)CaDiCaL version: 2.1.3
% 0.51/0.40 % (449090)Termination reason: Instruction limit
% 0.51/0.40 % (449090)Termination phase: Preprocessing 1
% 0.51/0.40 % (449090)Time elapsed: 0.012 s
% 0.51/0.40 % (449090)Peak memory usage: 10 MB
% 0.51/0.40 % (449090)Instructions burned: 25 (million)
% 0.51/0.40 % (449086)Instruction limit reached!
% 0.51/0.40 % (449086)------------------------------
% 0.51/0.40 % (449086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.40 % (449086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.40 % (449086)CaDiCaL version: 2.1.3
% 0.51/0.40 % (449086)Termination reason: Instruction limit
% 0.51/0.40 % (449086)Termination phase: Saturation
% 0.51/0.40 % (449086)Time elapsed: 0.023 s
% 0.51/0.40 % (449086)Peak memory usage: 13 MB
% 0.51/0.40 % (449086)Instructions burned: 89 (million)
% 0.51/0.40 % (449100)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3613513407:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.51/0.40 % (449103)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3667027409:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.51/0.40 % (449100)Instruction limit reached!
% 0.51/0.44 % (449100)------------------------------
% 0.51/0.44 % (449100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (449100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (449100)CaDiCaL version: 2.1.3
% 0.51/0.44 % (449100)Termination reason: Instruction limit
% 0.51/0.44 % (449100)Termination phase: shuffling
% 0.51/0.44 % (449100)Time elapsed: 0.002 s
% 0.51/0.44 % (449100)Peak memory usage: 10 MB
% 0.51/0.44 % (449100)Instructions burned: 3 (million)
% 0.51/0.44 % (449102)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.51/0.44 % (449101)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2551892317:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.51/0.44 % (449102)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3904326642:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.51/0.44 % (449103)Instruction limit reached!
% 0.51/0.44 % (449103)------------------------------
% 0.51/0.44 % (449103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (449103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (449101)Instruction limit reached!
% 0.51/0.44 % (449101)------------------------------
% 0.51/0.44 % (449101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (449103)CaDiCaL version: 2.1.3
% 0.51/0.44 % (449103)Termination reason: Instruction limit
% 0.51/0.44 % (449103)Termination phase: SInE selection
% 0.51/0.44 % (449103)Time elapsed: 0.008 s
% 0.51/0.44 % (449103)Peak memory usage: 11 MB
% 0.51/0.44 % (449103)Instructions burned: 30 (million)
% 0.51/0.44 % (449101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (449101)CaDiCaL version: 2.1.3
% 0.51/0.44 % (449101)Termination reason: Instruction limit
% 0.51/0.44 % (449101)Termination phase: shuffling
% 0.51/0.44 % (449101)Time elapsed: 0.003 s
% 0.51/0.44 % (449101)Peak memory usage: 10 MB
% 0.51/0.44 % (449101)Instructions burned: 6 (million)
% 0.51/0.44 % (449102)Instruction limit reached!
% 0.51/0.44 % (449102)------------------------------
% 0.51/0.44 % (449102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (449102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (449102)CaDiCaL version: 2.1.3
% 0.51/0.44 % (449102)Termination reason: Instruction limit
% 0.51/0.44 % (449102)Termination phase: shuffling
% 0.51/0.44 % (449102)Time elapsed: 0.004 s
% 0.51/0.44 % (449102)Peak memory usage: 10 MB
% 0.51/0.44 % (449102)Instructions burned: 7 (million)
% 0.51/0.44 % (449091)Instruction limit reached!
% 0.51/0.44 % (449091)------------------------------
% 0.51/0.44 % (449091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.51/0.44 % (449091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.51/0.44 % (449091)CaDiCaL version: 2.1.3
% 0.51/0.44 % (449091)Termination reason: Instruction limit
% 0.51/0.44 % (449091)Termination phase: Property scanning
% 0.51/0.44 % (449091)Time elapsed: 0.037 s
% 0.51/0.44 % (449091)Peak memory usage: 12 MB
% 0.51/0.44 % (449091)Instructions burned: 76 (million)
% 0.51/0.44 % (449106)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.51/0.44 % (449106)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.51/0.44 % (449109)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=1597220946:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.51/0.44 % (449106)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1500021016:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.51/0.44 % (449111)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.51/0.44 % (449110)lrs+10_1_si=on:cs=on:random_seed=4205688537:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 1.23/0.47 % (449111)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=682869796:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.23/0.47 % (449112)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2036450998:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 1.23/0.47 % (449111)Instruction limit reached!
% 1.23/0.47 % (449111)------------------------------
% 1.23/0.47 % (449111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.47 % (449111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.47 % (449111)CaDiCaL version: 2.1.3
% 1.23/0.47 % (449111)Termination reason: Instruction limit
% 1.23/0.47 % (449111)Termination phase: shuffling
% 1.23/0.47 % (449111)Time elapsed: 0.002 s
% 1.23/0.47 % (449111)Peak memory usage: 10 MB
% 1.23/0.47 % (449111)Instructions burned: 3 (million)
% 1.23/0.47 % (449110)Instruction limit reached!
% 1.23/0.47 % (449110)------------------------------
% 1.23/0.47 % (449110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.47 % (449110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.47 % (449110)CaDiCaL version: 2.1.3
% 1.23/0.47 % (449110)Termination reason: Instruction limit
% 1.23/0.47 % (449110)Termination phase: shuffling
% 1.23/0.47 % (449110)Time elapsed: 0.005 s
% 1.23/0.47 % (449110)Peak memory usage: 10 MB
% 1.23/0.47 % (449110)Instructions burned: 10 (million)
% 1.23/0.47 % (449106)Instruction limit reached!
% 1.23/0.47 % (449106)------------------------------
% 1.23/0.47 % (449106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.47 % (449106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.47 % (449106)CaDiCaL version: 2.1.3
% 1.23/0.47 % (449106)Termination reason: Instruction limit
% 1.23/0.47 % (449106)Termination phase: Property scanning
% 1.23/0.47 % (449106)Time elapsed: 0.014 s
% 1.23/0.47 % (449106)Peak memory usage: 11 MB
% 1.23/0.47 % (449106)Instructions burned: 30 (million)
% 1.23/0.47 % (449109)Instruction limit reached!
% 1.23/0.47 % (449109)------------------------------
% 1.23/0.47 % (449109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.47 % (449109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.47 % (449109)CaDiCaL version: 2.1.3
% 1.23/0.47 % (449109)Termination reason: Instruction limit
% 1.23/0.47 % (449109)Termination phase: Property scanning
% 1.23/0.47 % (449109)Time elapsed: 0.020 s
% 1.23/0.47 % (449109)Peak memory usage: 11 MB
% 1.23/0.47 % (449109)Instructions burned: 87 (million)
% 1.23/0.47 % (449121)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=928781530:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.23/0.47 % (449112)Instruction limit reached!
% 1.23/0.47 % (449112)------------------------------
% 1.23/0.47 % (449112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.47 % (449112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.47 % (449112)CaDiCaL version: 2.1.3
% 1.23/0.47 % (449112)Termination reason: Instruction limit
% 1.23/0.47 % (449112)Termination phase: Property scanning
% 1.23/0.47 % (449112)Time elapsed: 0.019 s
% 1.23/0.47 % (449112)Peak memory usage: 11 MB
% 1.23/0.47 % (449112)Instructions burned: 38 (million)
% 1.23/0.47 % (449119)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1988323961:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.23/0.47 % (449118)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2074853529:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.23/0.47 % (449120)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3522782550:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.23/0.47 % (449092)Instruction limit reached!
% 1.23/0.47 % (449092)------------------------------
% 1.23/0.47 % (449092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.47 % (449092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.47 % (449092)CaDiCaL version: 2.1.3
% 1.23/0.47 % (449092)Termination reason: Instruction limit
% 1.23/0.47 % (449092)Termination phase: Saturation
% 1.23/0.52 % (449092)Time elapsed: 0.079 s
% 1.23/0.52 % (449092)Peak memory usage: 13 MB
% 1.23/0.52 % (449092)Instructions burned: 157 (million)
% 1.23/0.52 % (449120)Instruction limit reached!
% 1.23/0.52 % (449120)------------------------------
% 1.23/0.52 % (449120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.52 % (449120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.52 % (449120)CaDiCaL version: 2.1.3
% 1.23/0.52 % (449120)Termination reason: Instruction limit
% 1.23/0.52 % (449120)Termination phase: shuffling
% 1.23/0.52 % (449120)Time elapsed: 0.007 s
% 1.23/0.52 % (449120)Peak memory usage: 10 MB
% 1.23/0.52 % (449120)Instructions burned: 15 (million)
% 1.23/0.52 % (449119)Instruction limit reached!
% 1.23/0.52 % (449119)------------------------------
% 1.23/0.52 % (449119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.52 % (449119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.52 % (449119)CaDiCaL version: 2.1.3
% 1.23/0.52 % (449119)Termination reason: Instruction limit
% 1.23/0.52 % (449119)Termination phase: SInE selection
% 1.23/0.52 % (449119)Time elapsed: 0.012 s
% 1.23/0.52 % (449119)Peak memory usage: 11 MB
% 1.23/0.52 % (449119)Instructions burned: 26 (million)
% 1.23/0.52 % (449123)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1745700922:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.23/0.52 % (449127)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3167260064:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.23/0.52 % (449127)Instruction limit reached!
% 1.23/0.52 % (449127)------------------------------
% 1.23/0.52 % (449127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.52 % (449127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.52 % (449127)CaDiCaL version: 2.1.3
% 1.23/0.52 % (449127)Termination reason: Instruction limit
% 1.23/0.52 % (449127)Termination phase: shuffling
% 1.23/0.52 % (449127)Time elapsed: 0.002 s
% 1.23/0.52 % (449127)Peak memory usage: 10 MB
% 1.23/0.52 % (449127)Instructions burned: 3 (million)
% 1.23/0.52 % (449123)Instruction limit reached!
% 1.23/0.53 % (449123)------------------------------
% 1.23/0.53 % (449123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.53 % (449123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.53 % (449123)CaDiCaL version: 2.1.3
% 1.23/0.53 % (449123)Termination reason: Instruction limit
% 1.23/0.53 % (449123)Termination phase: shuffling
% 1.23/0.53 % (449123)Time elapsed: 0.007 s
% 1.23/0.53 % (449123)Peak memory usage: 10 MB
% 1.23/0.53 % (449123)Instructions burned: 15 (million)
% 1.23/0.53 % (449118)Refutation not found, incomplete strategy
% 1.23/0.53 % (449118)------------------------------
% 1.23/0.53 % (449118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.53 % (449118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.53 % (449118)CaDiCaL version: 2.1.3
% 1.23/0.53 % (449118)Termination reason: Refutation not found, incomplete strategy
% 1.23/0.53 % (449118)Time elapsed: 0.027 s
% 1.23/0.53 % (449118)Peak memory usage: 13 MB
% 1.23/0.53 % (449118)Instructions burned: 52 (million)
% 1.23/0.53 % (449128)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2481886868:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.23/0.53 % (449118)------------------------------
% 1.23/0.53 % (449118)------------------------------
% 1.23/0.53 % (449129)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=869939066:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.23/0.53 % (449128)Instruction limit reached!
% 1.23/0.53 % (449128)------------------------------
% 1.23/0.53 % (449128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.23/0.53 % (449128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.23/0.53 % (449128)CaDiCaL version: 2.1.3
% 1.23/0.53 % (449128)Termination reason: Instruction limit
% 1.23/0.53 % (449128)Termination phase: shuffling
% 1.23/0.53 % (449128)Time elapsed: 0.013 s
% 1.23/0.53 % (449128)Peak memory usage: 10 MB
% 1.23/0.53 % (449128)Instructions burned: 26 (million)
% 1.23/0.53 % (449133)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.89/0.58 % (449133)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.89/0.58 % (449132)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2533264825:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.89/0.58 % (449129)Instruction limit reached!
% 1.89/0.58 % (449129)------------------------------
% 1.89/0.58 % (449129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.58 % (449135)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.89/0.58 % (449129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.58 % (449129)CaDiCaL version: 2.1.3
% 1.89/0.58 % (449129)Termination reason: Instruction limit
% 1.89/0.58 % (449129)Termination phase: Property scanning
% 1.89/0.58 % (449129)Time elapsed: 0.012 s
% 1.89/0.58 % (449129)Peak memory usage: 10 MB
% 1.89/0.58 % (449129)Instructions burned: 24 (million)
% 1.89/0.58 % (449133)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=517603585:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.89/0.58 % (449135)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=4145093969:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.89/0.58 % (449133)Instruction limit reached!
% 1.89/0.58 % (449133)------------------------------
% 1.89/0.58 % (449133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.58 % (449133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.58 % (449133)CaDiCaL version: 2.1.3
% 1.89/0.58 % (449133)Termination reason: Instruction limit
% 1.89/0.58 % (449133)Termination phase: shuffling
% 1.89/0.58 % (449133)Time elapsed: 0.007 s
% 1.89/0.58 % (449133)Peak memory usage: 10 MB
% 1.89/0.58 % (449133)Instructions burned: 15 (million)
% 1.89/0.58 % (449135)Instruction limit reached!
% 1.89/0.58 % (449135)------------------------------
% 1.89/0.58 % (449135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.58 % (449135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.58 % (449135)CaDiCaL version: 2.1.3
% 1.89/0.58 % (449135)Termination reason: Instruction limit
% 1.89/0.58 % (449135)Termination phase: Property scanning
% 1.89/0.58 % (449135)Time elapsed: 0.008 s
% 1.89/0.58 % (449135)Peak memory usage: 10 MB
% 1.89/0.58 % (449135)Instructions burned: 17 (million)
% 1.89/0.58 % (449137)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=71340620:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.89/0.58 % (449140)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=380819043:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.89/0.58 % (449142)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4217973000:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.89/0.58 % (449140)Instruction limit reached!
% 1.89/0.58 % (449140)------------------------------
% 1.89/0.58 % (449140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.58 % (449140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.58 % (449140)CaDiCaL version: 2.1.3
% 1.89/0.58 % (449140)Termination reason: Instruction limit
% 1.89/0.58 % (449140)Termination phase: shuffling
% 1.89/0.58 % (449140)Time elapsed: 0.004 s
% 1.89/0.58 % (449140)Peak memory usage: 10 MB
% 1.89/0.58 % (449140)Instructions burned: 8 (million)
% 1.89/0.58 % (449132)Instruction limit reached!
% 1.89/0.58 % (449132)------------------------------
% 1.89/0.58 % (449132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.58 % (449132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.58 % (449132)CaDiCaL version: 2.1.3
% 1.89/0.58 % (449132)Termination reason: Instruction limit
% 1.89/0.58 % (449132)Termination phase: Property scanning
% 1.89/0.58 % (449132)Time elapsed: 0.029 s
% 1.89/0.58 % (449132)Peak memory usage: 11 MB
% 1.89/0.63 % (449132)Instructions burned: 60 (million)
% 1.89/0.63 % (449143)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2277319179:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 1.89/0.63 % (449137)Instruction limit reached!
% 1.89/0.63 % (449137)------------------------------
% 1.89/0.63 % (449137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.63 % (449137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.63 % (449137)CaDiCaL version: 2.1.3
% 1.89/0.63 % (449137)Termination reason: Instruction limit
% 1.89/0.63 % (449137)Termination phase: Property scanning
% 1.89/0.63 % (449137)Time elapsed: 0.015 s
% 1.89/0.63 % (449137)Peak memory usage: 11 MB
% 1.89/0.63 % (449137)Instructions burned: 32 (million)
% 1.89/0.63 % (449142)Instruction limit reached!
% 1.89/0.63 % (449142)------------------------------
% 1.89/0.63 % (449142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.63 % (449142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.63 % (449142)CaDiCaL version: 2.1.3
% 1.89/0.63 % (449142)Termination reason: Instruction limit
% 1.89/0.63 % (449142)Termination phase: shuffling
% 1.89/0.63 % (449142)Time elapsed: 0.011 s
% 1.89/0.63 % (449142)Peak memory usage: 10 MB
% 1.89/0.63 % (449142)Instructions burned: 24 (million)
% 1.89/0.63 % (449143)Instruction limit reached!
% 1.89/0.63 % (449143)------------------------------
% 1.89/0.63 % (449143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.63 % (449143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.63 % (449143)CaDiCaL version: 2.1.3
% 1.89/0.63 % (449143)Termination reason: Instruction limit
% 1.89/0.63 % (449143)Termination phase: Property scanning
% 1.89/0.63 % (449143)Time elapsed: 0.011 s
% 1.89/0.63 % (449143)Peak memory usage: 10 MB
% 1.89/0.63 % (449143)Instructions burned: 22 (million)
% 1.89/0.63 % (449147)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2030679119:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.89/0.63 % (449148)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2240338071:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 1.89/0.63 % (449121)Instruction limit reached!
% 1.89/0.63 % (449121)------------------------------
% 1.89/0.63 % (449121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.63 % (449121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.63 % (449121)CaDiCaL version: 2.1.3
% 1.89/0.63 % (449121)Termination reason: Instruction limit
% 1.89/0.63 % (449121)Termination phase: Saturation
% 1.89/0.63 % (449121)Time elapsed: 0.096 s
% 1.89/0.63 % (449121)Peak memory usage: 15 MB
% 1.89/0.63 % (449121)Instructions burned: 330 (million)
% 1.89/0.63 % (449150)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=364461902:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 1.89/0.63 % (449152)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.89/0.63 % (449151)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=126916416:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 1.89/0.63 % (449155)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=505939193:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 1.89/0.63 % (449152)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2457661063:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.89/0.63 % (449152)Instruction limit reached!
% 1.89/0.63 % (449152)------------------------------
% 1.89/0.63 % (449152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.63 % (449152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.63 % (449152)CaDiCaL version: 2.1.3
% 1.89/0.63 % (449152)Termination reason: Instruction limit
% 1.89/0.63 % (449152)Termination phase: shuffling
% 1.89/0.63 % (449152)Time elapsed: 0.004 s
% 1.89/0.63 % (449152)Peak memory usage: 10 MB
% 1.89/0.63 % (449152)Instructions burned: 8 (million)
% 1.89/0.63 % (449151)Instruction limit reached!
% 1.89/0.63 % (449151)------------------------------
% 1.89/0.63 % (449151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.70 % (449151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.70 % (449151)CaDiCaL version: 2.1.3
% 2.57/0.70 % (449151)Termination reason: Instruction limit
% 2.57/0.70 % (449151)Termination phase: Property scanning
% 2.57/0.70 % (449151)Time elapsed: 0.021 s
% 2.57/0.70 % (449151)Peak memory usage: 11 MB
% 2.57/0.70 % (449151)Instructions burned: 43 (million)
% 2.57/0.70 % (449160)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=1642920922:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.57/0.70 % (449161)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.57/0.70 % (449161)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2199410671:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.57/0.70 % (449161)Instruction limit reached!
% 2.57/0.70 % (449161)------------------------------
% 2.57/0.70 % (449161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.70 % (449161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.70 % (449161)CaDiCaL version: 2.1.3
% 2.57/0.70 % (449161)Termination reason: Instruction limit
% 2.57/0.70 % (449161)Termination phase: shuffling
% 2.57/0.70 % (449161)Time elapsed: 0.004 s
% 2.57/0.70 % (449161)Peak memory usage: 10 MB
% 2.57/0.70 % (449161)Instructions burned: 7 (million)
% 2.57/0.70 % (449155)Instruction limit reached!
% 2.57/0.70 % (449155)------------------------------
% 2.57/0.70 % (449155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.70 % (449155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.70 % (449155)CaDiCaL version: 2.1.3
% 2.57/0.70 % (449155)Termination reason: Instruction limit
% 2.57/0.70 % (449155)Termination phase: Saturation
% 2.57/0.70 % (449155)Time elapsed: 0.052 s
% 2.57/0.70 % (449155)Peak memory usage: 14 MB
% 2.57/0.70 % (449155)Instructions burned: 181 (million)
% 2.57/0.70 % (449148)Instruction limit reached!
% 2.57/0.70 % (449148)------------------------------
% 2.57/0.70 % (449148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.70 % (449148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.70 % (449148)CaDiCaL version: 2.1.3
% 2.57/0.70 % (449148)Termination reason: Instruction limit
% 2.57/0.70 % (449148)Termination phase: Saturation
% 2.57/0.70 % (449148)Time elapsed: 0.072 s
% 2.57/0.70 % (449148)Peak memory usage: 14 MB
% 2.57/0.70 % (449148)Instructions burned: 143 (million)
% 2.57/0.70 % (449164)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3607160571:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.57/0.70 % (449160)Refutation not found, incomplete strategy
% 2.57/0.70 % (449160)------------------------------
% 2.57/0.70 % (449160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.70 % (449160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.70 % (449160)CaDiCaL version: 2.1.3
% 2.57/0.70 % (449160)Termination reason: Refutation not found, incomplete strategy
% 2.57/0.70 % (449160)Time elapsed: 0.038 s
% 2.57/0.70 % (449160)Peak memory usage: 13 MB
% 2.57/0.70 % (449160)Instructions burned: 72 (million)
% 2.57/0.70 % (449165)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2961652158:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.57/0.70 % (449160)------------------------------
% 2.57/0.70 % (449160)------------------------------
% 2.57/0.70 % (449165)Instruction limit reached!
% 2.57/0.70 % (449165)------------------------------
% 2.57/0.70 % (449165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.70 % (449165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.70 % (449165)CaDiCaL version: 2.1.3
% 2.57/0.70 % (449165)Termination reason: Instruction limit
% 2.57/0.70 % (449165)Termination phase: shuffling
% 2.57/0.70 % (449165)Time elapsed: 0.005 s
% 2.57/0.70 % (449165)Peak memory usage: 10 MB
% 2.57/0.70 % (449165)Instructions burned: 20 (million)
% 2.57/0.70 % (449164)Instruction limit reached!
% 2.57/0.70 % (449164)------------------------------
% 2.57/0.70 % (449164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.80 % (449164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.80 % (449164)CaDiCaL version: 2.1.3
% 3.19/0.80 % (449164)Termination reason: Instruction limit
% 3.19/0.80 % (449164)Termination phase: Property scanning
% 3.19/0.80 % (449164)Time elapsed: 0.011 s
% 3.19/0.80 % (449164)Peak memory usage: 10 MB
% 3.19/0.80 % (449164)Instructions burned: 22 (million)
% 3.19/0.80 % (449170)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=4258558306:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 3.19/0.80 % (449166)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=4183322547:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.19/0.80 % (449169)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=147376358:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 3.19/0.80 % (449170)Instruction limit reached!
% 3.19/0.80 % (449170)------------------------------
% 3.19/0.80 % (449170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.80 % (449170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.80 % (449170)CaDiCaL version: 2.1.3
% 3.19/0.80 % (449170)Termination reason: Instruction limit
% 3.19/0.80 % (449170)Termination phase: Preprocessing 3
% 3.19/0.80 % (449170)Time elapsed: 0.012 s
% 3.19/0.80 % (449170)Peak memory usage: 11 MB
% 3.19/0.80 % (449170)Instructions burned: 47 (million)
% 3.19/0.80 % (449171)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=1729566417:i=480:rtra=on_2997 on theBenchmark for (2997ds/480Mi)
% 3.19/0.80 % (449150)Instruction limit reached!
% 3.19/0.80 % (449150)------------------------------
% 3.19/0.80 % (449150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.80 % (449150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.80 % (449150)CaDiCaL version: 2.1.3
% 3.19/0.80 % (449150)Termination reason: Instruction limit
% 3.19/0.80 % (449150)Termination phase: Saturation
% 3.19/0.80 % (449150)Time elapsed: 0.107 s
% 3.19/0.80 % (449150)Peak memory usage: 14 MB
% 3.19/0.80 % (449150)Instructions burned: 195 (million)
% 3.19/0.80 % (449176)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2803380044:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.19/0.80 % (449176)Instruction limit reached!
% 3.19/0.80 % (449176)------------------------------
% 3.19/0.80 % (449176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.80 % (449176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.80 % (449176)CaDiCaL version: 2.1.3
% 3.19/0.80 % (449176)Termination reason: Instruction limit
% 3.19/0.80 % (449176)Termination phase: Property scanning
% 3.19/0.80 % (449176)Time elapsed: 0.006 s
% 3.19/0.80 % (449176)Peak memory usage: 10 MB
% 3.19/0.80 % (449176)Instructions burned: 24 (million)
% 3.19/0.80 % (449177)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.19/0.80 % (449179)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3084788030:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.19/0.80 % (449177)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=12998041:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.19/0.80 % (449179)Instruction limit reached!
% 3.19/0.80 % (449179)------------------------------
% 3.19/0.80 % (449179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.80 % (449179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.80 % (449179)CaDiCaL version: 2.1.3
% 3.19/0.80 % (449179)Termination reason: Instruction limit
% 3.19/0.80 % (449179)Termination phase: shuffling
% 3.19/0.80 % (449179)Time elapsed: 0.004 s
% 3.19/0.80 % (449179)Peak memory usage: 10 MB
% 3.19/0.80 % (449179)Instructions burned: 16 (million)
% 3.72/0.94 % (449182)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=987692166:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.72/0.94 % (449171)Refutation not found, incomplete strategy
% 3.72/0.94 % (449171)------------------------------
% 3.72/0.94 % (449171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.72/0.94 % (449171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/0.94 % (449171)CaDiCaL version: 2.1.3
% 3.72/0.94 % (449171)Termination reason: Refutation not found, incomplete strategy
% 3.72/0.94 % (449171)Time elapsed: 0.056 s
% 3.72/0.94 % (449171)Peak memory usage: 14 MB
% 3.72/0.94 % (449171)Instructions burned: 105 (million)
% 3.72/0.94 % (449171)------------------------------
% 3.72/0.94 % (449171)------------------------------
% 3.72/0.94 % (449182)Instruction limit reached!
% 3.72/0.94 % (449182)------------------------------
% 3.72/0.94 % (449182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.72/0.94 % (449182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/0.94 % (449182)CaDiCaL version: 2.1.3
% 3.72/0.94 % (449182)Termination reason: Instruction limit
% 3.72/0.94 % (449182)Termination phase: Preprocessing 1
% 3.72/0.94 % (449182)Time elapsed: 0.017 s
% 3.72/0.94 % (449182)Peak memory usage: 11 MB
% 3.72/0.94 % (449182)Instructions burned: 69 (million)
% 3.72/0.94 % (449089)Instruction limit reached!
% 3.72/0.94 % (449089)------------------------------
% 3.72/0.94 % (449089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.72/0.94 % (449089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/0.94 % (449089)CaDiCaL version: 2.1.3
% 3.72/0.94 % (449089)Termination reason: Instruction limit
% 3.72/0.94 % (449089)Termination phase: Saturation
% 3.72/0.94 % (449089)Time elapsed: 0.343 s
% 3.72/0.94 % (449089)Peak memory usage: 16 MB
% 3.72/0.94 % (449089)Instructions burned: 635 (million)
% 3.72/0.94 % (449185)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=717752572:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.72/0.94 % (449184)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1545651436:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.72/0.94 % (449185)Instruction limit reached!
% 3.72/0.94 % (449185)------------------------------
% 3.72/0.94 % (449185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.72/0.94 % (449185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/0.94 % (449185)CaDiCaL version: 2.1.3
% 3.72/0.94 % (449185)Termination reason: Instruction limit
% 3.72/0.94 % (449185)Termination phase: Property scanning
% 3.72/0.94 % (449185)Time elapsed: 0.009 s
% 3.72/0.94 % (449185)Peak memory usage: 10 MB
% 3.72/0.94 % (449185)Instructions burned: 36 (million)
% 3.72/0.94 % (449187)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=4183888190:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2996 on theBenchmark for (2996ds/137Mi)
% 3.72/0.94 % (449189)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=3095825956:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 3.72/0.94 % (449189)Instruction limit reached!
% 3.72/0.94 % (449189)------------------------------
% 3.72/0.94 % (449189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.72/0.94 % (449189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/0.94 % (449189)CaDiCaL version: 2.1.3
% 3.72/0.94 % (449189)Termination reason: Instruction limit
% 3.72/0.94 % (449189)Termination phase: Property scanning
% 3.72/0.94 % (449189)Time elapsed: 0.008 s
% 3.72/0.94 % (449189)Peak memory usage: 10 MB
% 3.72/0.94 % (449189)Instructions burned: 34 (million)
% 3.72/0.94 % (449184)Instruction limit reached!
% 3.72/0.94 % (449184)------------------------------
% 3.72/0.94 % (449184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.72/0.94 % (449184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/0.94 % (449184)CaDiCaL version: 2.1.3
% 3.72/0.94 % (449184)Termination reason: Instruction limit
% 3.72/0.94 % (449184)Termination phase: Property scanning
% 3.72/0.94 % (449184)Time elapsed: 0.025 s
% 3.72/0.94 % (449184)Peak memory usage: 11 MB
% 5.26/1.11 % (449184)Instructions burned: 52 (million)
% 5.26/1.11 % (449192)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2708807939:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.26/1.11 % (449193)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.26/1.11 % (449193)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=808065571:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.26/1.11 % (449177)Instruction limit reached!
% 5.26/1.11 % (449177)------------------------------
% 5.26/1.11 % (449177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.11 % (449177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.11 % (449177)CaDiCaL version: 2.1.3
% 5.26/1.11 % (449177)Termination reason: Instruction limit
% 5.26/1.11 % (449177)Termination phase: Saturation
% 5.26/1.11 % (449177)Time elapsed: 0.097 s
% 5.26/1.11 % (449177)Peak memory usage: 14 MB
% 5.26/1.11 % (449177)Instructions burned: 200 (million)
% 5.26/1.11 % (449192)Instruction limit reached!
% 5.26/1.11 % (449192)------------------------------
% 5.26/1.11 % (449192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.11 % (449192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.11 % (449192)CaDiCaL version: 2.1.3
% 5.26/1.11 % (449192)Termination reason: Instruction limit
% 5.26/1.11 % (449192)Termination phase: Property scanning
% 5.26/1.11 % (449192)Time elapsed: 0.017 s
% 5.26/1.11 % (449192)Peak memory usage: 11 MB
% 5.26/1.11 % (449192)Instructions burned: 69 (million)
% 5.26/1.11 % (449197)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=4204404392:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.26/1.11 % (449196)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3607117312:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.26/1.11 % (449166)Instruction limit reached!
% 5.26/1.11 % (449166)------------------------------
% 5.26/1.11 % (449166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.11 % (449166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.11 % (449166)CaDiCaL version: 2.1.3
% 5.26/1.11 % (449166)Termination reason: Instruction limit
% 5.26/1.11 % (449166)Termination phase: Saturation
% 5.26/1.11 % (449166)Time elapsed: 0.172 s
% 5.26/1.11 % (449166)Peak memory usage: 15 MB
% 5.26/1.11 % (449166)Instructions burned: 316 (million)
% 5.26/1.11 % (449187)Instruction limit reached!
% 5.26/1.11 % (449187)------------------------------
% 5.26/1.11 % (449187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.11 % (449187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.11 % (449187)CaDiCaL version: 2.1.3
% 5.26/1.11 % (449187)Termination reason: Instruction limit
% 5.26/1.11 % (449187)Termination phase: Saturation
% 5.26/1.11 % (449187)Time elapsed: 0.071 s
% 5.26/1.11 % (449187)Peak memory usage: 13 MB
% 5.26/1.11 % (449187)Instructions burned: 138 (million)
% 5.26/1.11 % (449197)Instruction limit reached!
% 5.26/1.11 % (449197)------------------------------
% 5.26/1.11 % (449197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.11 % (449197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.11 % (449197)CaDiCaL version: 2.1.3
% 5.26/1.11 % (449197)Termination reason: Instruction limit
% 5.26/1.11 % (449197)Termination phase: Saturation
% 5.26/1.11 % (449197)Time elapsed: 0.025 s
% 5.26/1.11 % (449197)Peak memory usage: 13 MB
% 5.26/1.11 % (449197)Instructions burned: 96 (million)
% 5.26/1.11 % (449202)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3333160297:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 5.26/1.11 % (449200)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2112351687:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 5.26/1.11 % (449201)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=4041024055:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.26/1.11 % (449193)Instruction limit reached!
% 5.26/1.11 % (449193)------------------------------
% 5.26/1.11 % (449193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.11 % (449193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (449193)CaDiCaL version: 2.1.3
% 5.92/1.18 % (449193)Termination reason: Instruction limit
% 5.92/1.18 % (449193)Termination phase: Saturation
% 5.92/1.18 % (449193)Time elapsed: 0.081 s
% 5.92/1.18 % (449193)Peak memory usage: 13 MB
% 5.92/1.18 % (449193)Instructions burned: 180 (million)
% 5.92/1.18 % (449200)Refutation not found, incomplete strategy
% 5.92/1.18 % (449200)------------------------------
% 5.92/1.18 % (449200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (449200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (449200)CaDiCaL version: 2.1.3
% 5.92/1.18 % (449200)Termination reason: Refutation not found, incomplete strategy
% 5.92/1.18 % (449200)Time elapsed: 0.024 s
% 5.92/1.18 % (449200)Peak memory usage: 13 MB
% 5.92/1.18 % (449200)Instructions burned: 47 (million)
% 5.92/1.18 % (449200)------------------------------
% 5.92/1.18 % (449200)------------------------------
% 5.92/1.18 % (449206)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3548891404:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.92/1.18 % (449207)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3127724378:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.92/1.18 % (449207)Instruction limit reached!
% 5.92/1.18 % (449207)------------------------------
% 5.92/1.18 % (449207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (449207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (449207)CaDiCaL version: 2.1.3
% 5.92/1.18 % (449207)Termination reason: Instruction limit
% 5.92/1.18 % (449207)Termination phase: Property scanning
% 5.92/1.18 % (449207)Time elapsed: 0.020 s
% 5.92/1.18 % (449207)Peak memory usage: 10 MB
% 5.92/1.18 % (449207)Instructions burned: 44 (million)
% 5.92/1.18 % (449210)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3295748666:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.92/1.18 % (449196)Instruction limit reached!
% 5.92/1.18 % (449196)------------------------------
% 5.92/1.18 % (449196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (449196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (449196)CaDiCaL version: 2.1.3
% 5.92/1.18 % (449196)Termination reason: Instruction limit
% 5.92/1.18 % (449196)Termination phase: Saturation
% 5.92/1.18 % (449196)Time elapsed: 0.131 s
% 5.92/1.18 % (449196)Peak memory usage: 14 MB
% 5.92/1.18 % (449196)Instructions burned: 248 (million)
% 5.92/1.18 % (449206)Instruction limit reached!
% 5.92/1.18 % (449206)------------------------------
% 5.92/1.18 % (449206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (449206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (449206)CaDiCaL version: 2.1.3
% 5.92/1.18 % (449206)Termination reason: Instruction limit
% 5.92/1.18 % (449206)Termination phase: Saturation
% 5.92/1.18 % (449206)Time elapsed: 0.060 s
% 5.92/1.18 % (449206)Peak memory usage: 13 MB
% 5.92/1.18 % (449206)Instructions burned: 131 (million)
% 5.92/1.18 % (449212)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=930688951:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 5.92/1.18 % (449213)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1689039862:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/95Mi)
% 5.92/1.18 % (449202)Instruction limit reached!
% 5.92/1.18 % (449202)------------------------------
% 5.92/1.18 % (449202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.92/1.18 % (449202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.92/1.18 % (449202)CaDiCaL version: 2.1.3
% 5.92/1.18 % (449202)Termination reason: Instruction limit
% 5.92/1.18 % (449202)Termination phase: Saturation
% 5.92/1.18 % (449202)Time elapsed: 0.139 s
% 5.92/1.18 % (449202)Peak memory usage: 16 MB
% 5.92/1.18 % (449202)Instructions burned: 516 (million)
% 5.92/1.18 % (449216)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=1544740771:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.92/1.18 % (449216)Instruction limit reached!
% 5.92/1.18 % (449216)------------------------------
% 6.29/1.29 % (449216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.29 % (449216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.29 % (449216)CaDiCaL version: 2.1.3
% 6.29/1.29 % (449216)Termination reason: Instruction limit
% 6.29/1.29 % (449216)Termination phase: Preprocessing 1
% 6.29/1.29 % (449216)Time elapsed: 0.016 s
% 6.29/1.29 % (449216)Peak memory usage: 11 MB
% 6.29/1.29 % (449216)Instructions burned: 65 (million)
% 6.29/1.29 % (449213)Instruction limit reached!
% 6.29/1.29 % (449213)------------------------------
% 6.29/1.29 % (449213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.29 % (449213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.29 % (449213)CaDiCaL version: 2.1.3
% 6.29/1.29 % (449213)Termination reason: Instruction limit
% 6.29/1.29 % (449213)Termination phase: Saturation
% 6.29/1.29 % (449213)Time elapsed: 0.047 s
% 6.29/1.29 % (449213)Peak memory usage: 13 MB
% 6.29/1.29 % (449213)Instructions burned: 96 (million)
% 6.29/1.29 % (449218)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=2306984221:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2993 on theBenchmark for (2993ds/105Mi)
% 6.29/1.29 % (449220)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=537320243:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 6.29/1.29 % (449218)Instruction limit reached!
% 6.29/1.29 % (449218)------------------------------
% 6.29/1.29 % (449218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.29 % (449218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.29 % (449218)CaDiCaL version: 2.1.3
% 6.29/1.29 % (449218)Termination reason: Instruction limit
% 6.29/1.29 % (449218)Termination phase: Property scanning
% 6.29/1.29 % (449218)Time elapsed: 0.026 s
% 6.29/1.29 % (449218)Peak memory usage: 12 MB
% 6.29/1.29 % (449218)Instructions burned: 109 (million)
% 6.29/1.29 % (449222)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=35094497:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/375Mi)
% 6.29/1.29 % (449169)Instruction limit reached!
% 6.29/1.29 % (449169)------------------------------
% 6.29/1.29 % (449169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.29 % (449169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.29 % (449169)CaDiCaL version: 2.1.3
% 6.29/1.29 % (449169)Termination reason: Instruction limit
% 6.29/1.29 % (449169)Termination phase: Saturation
% 6.29/1.29 % (449169)Time elapsed: 0.465 s
% 6.29/1.29 % (449169)Peak memory usage: 16 MB
% 6.29/1.29 % (449169)Instructions burned: 853 (million)
% 6.29/1.29 % (449224)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3794635093:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.29/1.29 % (449222)Instruction limit reached!
% 6.29/1.29 % (449222)------------------------------
% 6.29/1.29 % (449222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.29 % (449222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.29 % (449222)CaDiCaL version: 2.1.3
% 6.29/1.29 % (449222)Termination reason: Instruction limit
% 6.29/1.29 % (449222)Termination phase: Saturation
% 6.29/1.29 % (449222)Time elapsed: 0.107 s
% 6.29/1.29 % (449222)Peak memory usage: 14 MB
% 6.29/1.29 % (449222)Instructions burned: 377 (million)
% 6.29/1.29 % (449226)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=1652322198:cond=on:i=34:hud=10:nm=10:rtra=on_2991 on theBenchmark for (2991ds/34Mi)
% 6.29/1.29 % (449226)Instruction limit reached!
% 6.29/1.29 % (449226)------------------------------
% 6.29/1.29 % (449226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.29/1.29 % (449226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.29 % (449226)CaDiCaL version: 2.1.3
% 6.29/1.29 % (449226)Termination reason: Instruction limit
% 6.29/1.29 % (449226)Termination phase: Property scanning
% 6.29/1.29 % (449226)Time elapsed: 0.009 s
% 6.66/1.38 % (449226)Peak memory usage: 10 MB
% 6.66/1.38 % (449226)Instructions burned: 38 (million)
% 6.66/1.38 % (449212)Instruction limit reached!
% 6.66/1.38 % (449212)------------------------------
% 6.66/1.38 % (449212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.66/1.38 % (449212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/1.38 % (449212)CaDiCaL version: 2.1.3
% 6.66/1.38 % (449212)Termination reason: Instruction limit
% 6.66/1.38 % (449212)Termination phase: Saturation
% 6.66/1.38 % (449212)Time elapsed: 0.224 s
% 6.66/1.38 % (449212)Peak memory usage: 14 MB
% 6.66/1.38 % (449212)Instructions burned: 450 (million)
% 6.66/1.38 % (449228)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2006820294:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 6.66/1.38 % (449229)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3788441689:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 6.66/1.38 % (449228)Instruction limit reached!
% 6.66/1.38 % (449228)------------------------------
% 6.66/1.38 % (449228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.66/1.38 % (449228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/1.38 % (449228)CaDiCaL version: 2.1.3
% 6.66/1.38 % (449228)Termination reason: Instruction limit
% 6.66/1.38 % (449228)Termination phase: Saturation
% 6.66/1.38 % (449228)Time elapsed: 0.024 s
% 6.66/1.38 % (449228)Peak memory usage: 13 MB
% 6.66/1.38 % (449228)Instructions burned: 93 (million)
% 6.66/1.38 % (449147)Instruction limit reached!
% 6.66/1.38 % (449147)------------------------------
% 6.66/1.38 % (449147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.66/1.38 % (449147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/1.38 % (449147)CaDiCaL version: 2.1.3
% 6.66/1.38 % (449147)Termination reason: Instruction limit
% 6.66/1.38 % (449147)Termination phase: Saturation
% 6.66/1.38 % (449147)Time elapsed: 0.654 s
% 6.66/1.38 % (449147)Peak memory usage: 19 MB
% 6.66/1.38 % (449147)Instructions burned: 1241 (million)
% 6.66/1.38 % (449232)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1581715229:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.66/1.38 % (449232)Instruction limit reached!
% 6.66/1.38 % (449232)------------------------------
% 6.66/1.38 % (449232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.66/1.38 % (449232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/1.38 % (449232)CaDiCaL version: 2.1.3
% 6.66/1.38 % (449232)Termination reason: Instruction limit
% 6.66/1.38 % (449232)Termination phase: Property scanning
% 6.66/1.38 % (449232)Time elapsed: 0.006 s
% 6.66/1.38 % (449232)Peak memory usage: 10 MB
% 6.66/1.38 % (449232)Instructions burned: 25 (million)
% 6.66/1.38 % (449233)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=2000675183:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.66/1.38 % (449229)Instruction limit reached!
% 6.66/1.38 % (449229)------------------------------
% 6.66/1.38 % (449229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.66/1.38 % (449229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/1.38 % (449229)CaDiCaL version: 2.1.3
% 6.66/1.38 % (449229)Termination reason: Instruction limit
% 6.66/1.38 % (449229)Termination phase: Saturation
% 6.66/1.38 % (449229)Time elapsed: 0.035 s
% 6.66/1.38 % (449229)Peak memory usage: 13 MB
% 6.66/1.38 % (449229)Instructions burned: 67 (million)
% 6.66/1.38 % (449235)lrs+10_1_sil=128000:si=on:urr=on:random_seed=905446557:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 6.66/1.38 % (449235)Instruction limit reached!
% 6.66/1.38 % (449235)------------------------------
% 6.66/1.38 % (449235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.66/1.38 % (449235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.66/1.38 % (449235)CaDiCaL version: 2.1.3
% 6.66/1.38 % (449235)Termination reason: Instruction limit
% 6.66/1.38 % (449235)Termination phase: SInE selection
% 6.66/1.38 % (449235)Time elapsed: 0.007 s
% 6.66/1.38 % (449235)Peak memory usage: 11 MB
% 6.66/1.38 % (449235)Instructions burned: 28 (million)
% 6.66/1.38 % (449210)Instruction limit reached!
% 7.59/1.49 % (449210)------------------------------
% 7.59/1.49 % (449210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.59/1.49 % (449210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.49 % (449210)CaDiCaL version: 2.1.3
% 7.59/1.49 % (449210)Termination reason: Instruction limit
% 7.59/1.49 % (449210)Termination phase: Saturation
% 7.59/1.49 % (449210)Time elapsed: 0.321 s
% 7.59/1.49 % (449210)Peak memory usage: 15 MB
% 7.59/1.49 % (449210)Instructions burned: 572 (million)
% 7.59/1.49 % (449237)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.59/1.49 % (449237)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2069517420:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.59/1.49 % (449239)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=1711977272:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 7.59/1.49 % (449240)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=322419119:i=227:sd=1:bd=all:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/227Mi)
% 7.59/1.49 % (449240)Refutation not found, incomplete strategy
% 7.59/1.49 % (449240)------------------------------
% 7.59/1.49 % (449240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.59/1.49 % (449240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.49 % (449240)CaDiCaL version: 2.1.3
% 7.59/1.49 % (449240)Termination reason: Refutation not found, incomplete strategy
% 7.59/1.49 % (449240)Time elapsed: 0.024 s
% 7.59/1.49 % (449240)Peak memory usage: 13 MB
% 7.59/1.49 % (449240)Instructions burned: 46 (million)
% 7.59/1.49 % (449240)------------------------------
% 7.59/1.49 % (449240)------------------------------
% 7.59/1.49 % (449201)Instruction limit reached!
% 7.59/1.49 % (449201)------------------------------
% 7.59/1.49 % (449201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.59/1.49 % (449201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.49 % (449201)CaDiCaL version: 2.1.3
% 7.59/1.49 % (449201)Termination reason: Instruction limit
% 7.59/1.49 % (449201)Termination phase: Saturation
% 7.59/1.49 % (449201)Time elapsed: 0.458 s
% 7.59/1.49 % (449201)Peak memory usage: 16 MB
% 7.59/1.49 % (449201)Instructions burned: 874 (million)
% 7.59/1.49 % (449244)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.59/1.49 % (449244)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1142633885:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.59/1.49 % (449237)Instruction limit reached!
% 7.59/1.49 % (449237)------------------------------
% 7.59/1.49 % (449237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.59/1.49 % (449237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.49 % (449237)CaDiCaL version: 2.1.3
% 7.59/1.49 % (449237)Termination reason: Instruction limit
% 7.59/1.49 % (449237)Termination phase: Saturation
% 7.59/1.49 % (449237)Time elapsed: 0.062 s
% 7.59/1.49 % (449237)Peak memory usage: 13 MB
% 7.59/1.49 % (449237)Instructions burned: 139 (million)
% 7.59/1.49 % (449245)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2455377213:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.59/1.49 % (449247)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1816790761:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 7.59/1.49 % (449239)Instruction limit reached!
% 7.59/1.49 % (449239)------------------------------
% 7.59/1.49 % (449239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.59/1.49 % (449239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.59/1.49 % (449239)CaDiCaL version: 2.1.3
% 7.59/1.49 % (449239)Termination reason: Instruction limit
% 7.59/1.49 % (449239)Termination phase: Saturation
% 7.59/1.49 % (449239)Time elapsed: 0.088 s
% 7.59/1.49 % (449239)Peak memory usage: 14 MB
% 7.59/1.49 % (449239)Instructions burned: 343 (million)
% 7.59/1.49 % (449251)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1851612569:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.55/1.66 % (449245)Instruction limit reached!
% 8.55/1.66 % (449245)------------------------------
% 8.55/1.66 % (449245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.55/1.66 % (449245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.55/1.66 % (449245)CaDiCaL version: 2.1.3
% 8.55/1.66 % (449245)Termination reason: Instruction limit
% 8.55/1.66 % (449245)Termination phase: Saturation
% 8.55/1.66 % (449245)Time elapsed: 0.058 s
% 8.55/1.66 % (449245)Peak memory usage: 13 MB
% 8.55/1.66 % (449245)Instructions burned: 116 (million)
% 8.55/1.66 % (449247)Refutation not found, incomplete strategy
% 8.55/1.66 % (449247)------------------------------
% 8.55/1.66 % (449247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.55/1.66 % (449247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.55/1.66 % (449247)CaDiCaL version: 2.1.3
% 8.55/1.66 % (449247)Termination reason: Refutation not found, incomplete strategy
% 8.55/1.66 % (449247)Time elapsed: 0.061 s
% 8.55/1.66 % (449247)Peak memory usage: 14 MB
% 8.55/1.66 % (449247)Instructions burned: 116 (million)
% 8.55/1.66 % (449247)------------------------------
% 8.55/1.66 % (449247)------------------------------
% 8.55/1.66 % (449254)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=861220711:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/9840Mi)
% 8.55/1.66 % (449224)Instruction limit reached!
% 8.55/1.66 % (449224)------------------------------
% 8.55/1.66 % (449224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.55/1.66 % (449224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.55/1.66 % (449224)CaDiCaL version: 2.1.3
% 8.55/1.66 % (449224)Termination reason: Instruction limit
% 8.55/1.66 % (449224)Termination phase: Saturation
% 8.55/1.66 % (449224)Time elapsed: 0.262 s
% 8.55/1.66 % (449224)Peak memory usage: 16 MB
% 8.55/1.66 % (449224)Instructions burned: 495 (million)
% 8.55/1.66 % (449233)Instruction limit reached!
% 8.55/1.66 % (449233)------------------------------
% 8.55/1.66 % (449233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.55/1.66 % (449233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.55/1.66 % (449233)CaDiCaL version: 2.1.3
% 8.55/1.66 % (449233)Termination reason: Instruction limit
% 8.55/1.66 % (449233)Termination phase: Saturation
% 8.55/1.66 % (449233)Time elapsed: 0.174 s
% 8.55/1.66 % (449233)Peak memory usage: 16 MB
% 8.55/1.66 % (449233)Instructions burned: 338 (million)
% 8.55/1.66 % (449257)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 8.55/1.66 % (449256)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=4147560380:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 8.55/1.66 % (449257)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=3638090614:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.55/1.66 % (449258)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2521299503:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/31Mi)
% 8.55/1.66 % (449251)Instruction limit reached!
% 8.55/1.66 % (449251)------------------------------
% 8.55/1.66 % (449251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.55/1.66 % (449251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.55/1.66 % (449251)CaDiCaL version: 2.1.3
% 8.55/1.66 % (449251)Termination reason: Instruction limit
% 8.55/1.66 % (449251)Termination phase: Saturation
% 8.55/1.66 % (449251)Time elapsed: 0.077 s
% 8.55/1.66 % (449251)Peak memory usage: 14 MB
% 8.55/1.66 % (449251)Instructions burned: 272 (million)
% 8.55/1.66 % (449258)Instruction limit reached!
% 8.55/1.66 % (449258)------------------------------
% 8.55/1.66 % (449258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.93/1.83 % (449258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/1.83 % (449258)CaDiCaL version: 2.1.3
% 9.93/1.83 % (449258)Termination reason: Instruction limit
% 9.93/1.83 % (449258)Termination phase: Property scanning
% 9.93/1.83 % (449258)Time elapsed: 0.015 s
% 9.93/1.83 % (449258)Peak memory usage: 10 MB
% 9.93/1.83 % (449258)Instructions burned: 32 (million)
% 9.93/1.83 % (449266)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.93/1.83 % (449266)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 9.93/1.83 % (449266)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=1553935103:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2989 on theBenchmark for (2989ds/1440Mi)
% 9.93/1.83 % (449256)Refutation not found, incomplete strategy
% 9.93/1.83 % (449256)------------------------------
% 9.93/1.83 % (449256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.93/1.83 % (449256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/1.83 % (449256)CaDiCaL version: 2.1.3
% 9.93/1.83 % (449256)Termination reason: Refutation not found, incomplete strategy
% 9.93/1.83 % (449256)Time elapsed: 0.032 s
% 9.93/1.83 % (449256)Peak memory usage: 13 MB
% 9.93/1.83 % (449256)Instructions burned: 62 (million)
% 9.93/1.83 % (449256)------------------------------
% 9.93/1.83 % (449256)------------------------------
% 9.93/1.83 % (449270)dis+10_2_sil=128000:si=on:random_seed=2004258159:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2989 on theBenchmark for (2989ds/339Mi)
% 9.93/1.83 % (449276)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=813101130:i=111:add=on:fgj=on:rtra=on:fdi=1024_2988 on theBenchmark for (2988ds/111Mi)
% 9.93/1.83 % (449244)Instruction limit reached!
% 9.93/1.83 % (449244)------------------------------
% 9.93/1.83 % (449244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.93/1.83 % (449244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/1.83 % (449244)CaDiCaL version: 2.1.3
% 9.93/1.83 % (449244)Termination reason: Instruction limit
% 9.93/1.83 % (449244)Termination phase: Saturation
% 9.93/1.83 % (449244)Time elapsed: 0.182 s
% 9.93/1.83 % (449244)Peak memory usage: 13 MB
% 9.93/1.83 % (449244)Instructions burned: 373 (million)
% 9.93/1.83 % (449296)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=3672282766:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2988 on theBenchmark for (2988ds/122Mi)
% 9.93/1.83 % (449276)Instruction limit reached!
% 9.93/1.83 % (449276)------------------------------
% 9.93/1.83 % (449276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.93/1.83 % (449276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/1.83 % (449276)CaDiCaL version: 2.1.3
% 9.93/1.83 % (449276)Termination reason: Instruction limit
% 9.93/1.83 % (449276)Termination phase: Saturation
% 9.93/1.83 % (449276)Time elapsed: 0.055 s
% 9.93/1.83 % (449276)Peak memory usage: 13 MB
% 9.93/1.83 % (449276)Instructions burned: 111 (million)
% 9.93/1.83 % (449308)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=2869046468:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/136Mi)
% 9.93/1.83 % (449296)Refutation not found, incomplete strategy
% 9.93/1.83 % (449296)------------------------------
% 9.93/1.83 % (449296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.93/1.83 % (449296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/1.83 % (449296)CaDiCaL version: 2.1.3
% 9.93/1.83 % (449296)Termination reason: Refutation not found, incomplete strategy
% 9.93/1.83 % (449296)Time elapsed: 0.037 s
% 9.93/1.83 % (449296)Peak memory usage: 13 MB
% 9.93/1.83 % (449296)Instructions burned: 72 (million)
% 9.93/1.83 % (449296)------------------------------
% 9.93/1.83 % (449296)------------------------------
% 9.93/1.83 % (449257)Instruction limit reached!
% 9.93/1.83 % (449257)------------------------------
% 9.93/1.83 % (449257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.37/1.98 % (449257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/1.98 % (449257)CaDiCaL version: 2.1.3
% 10.37/1.98 % (449257)Termination reason: Instruction limit
% 10.37/1.98 % (449257)Termination phase: Saturation
% 10.37/1.98 % (449257)Time elapsed: 0.134 s
% 10.37/1.98 % (449257)Peak memory usage: 14 MB
% 10.37/1.98 % (449257)Instructions burned: 272 (million)
% 10.37/1.98 % (449318)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2289863355:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/232Mi)
% 10.37/1.98 % (449319)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=3953026653:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2987 on theBenchmark for (2987ds/1254Mi)
% 10.37/1.98 % (449308)Refutation not found, incomplete strategy
% 10.37/1.98 % (449308)------------------------------
% 10.37/1.98 % (449308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.37/1.98 % (449308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/1.98 % (449308)CaDiCaL version: 2.1.3
% 10.37/1.98 % (449308)Termination reason: Refutation not found, incomplete strategy
% 10.37/1.98 % (449308)Time elapsed: 0.058 s
% 10.37/1.98 % (449308)Peak memory usage: 14 MB
% 10.37/1.98 % (449308)Instructions burned: 109 (million)
% 10.37/1.98 % (449308)------------------------------
% 10.37/1.98 % (449308)------------------------------
% 10.37/1.98 % (449336)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 10.37/1.98 % (449336)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=1714771420:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2987 on theBenchmark for (2987ds/281Mi)
% 10.37/1.98 % (449270)Instruction limit reached!
% 10.37/1.98 % (449270)------------------------------
% 10.37/1.98 % (449270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.37/1.98 % (449270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/1.98 % (449270)CaDiCaL version: 2.1.3
% 10.37/1.98 % (449270)Termination reason: Instruction limit
% 10.37/1.98 % (449270)Termination phase: Saturation
% 10.37/1.98 % (449270)Time elapsed: 0.165 s
% 10.37/1.98 % (449270)Peak memory usage: 14 MB
% 10.37/1.98 % (449270)Instructions burned: 340 (million)
% 10.37/1.98 % (449352)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1905859914:i=619:add=on:rtra=on_2987 on theBenchmark for (2987ds/619Mi)
% 10.37/1.98 % (449319)Refutation not found, incomplete strategy
% 10.37/1.98 % (449319)------------------------------
% 10.37/1.98 % (449319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.37/1.98 % (449319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/1.98 % (449319)CaDiCaL version: 2.1.3
% 10.37/1.98 % (449319)Termination reason: Refutation not found, incomplete strategy
% 10.37/1.98 % (449319)Time elapsed: 0.089 s
% 10.37/1.98 % (449319)Peak memory usage: 15 MB
% 10.37/1.98 % (449319)Instructions burned: 188 (million)
% 10.37/1.98 % (449319)------------------------------
% 10.37/1.98 % (449319)------------------------------
% 10.37/1.98 % (449374)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=2283457287:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/865Mi)
% 10.37/1.98 % (449318)Instruction limit reached!
% 10.37/1.98 % (449318)------------------------------
% 10.37/1.98 % (449318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.37/1.98 % (449318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.37/1.98 % (449318)CaDiCaL version: 2.1.3
% 10.37/1.98 % (449318)Termination reason: Instruction limit
% 10.37/1.98 % (449318)Termination phase: Saturation
% 10.37/1.98 % (449318)Time elapsed: 0.126 s
% 10.37/1.98 % (449318)Peak memory usage: 14 MB
% 10.37/1.98 % (449318)Instructions burned: 233 (million)
% 10.37/1.98 % (449396)lrs+10_1_sil=128000:si=on:urr=on:random_seed=2253187144:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/212Mi)
% 10.37/1.98 % (449352)Refutation not found, incomplete strategy
% 10.37/1.98 % (449352)------------------------------
% 10.37/1.98 % (449352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.37/1.98 % (449352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.33 % (449352)CaDiCaL version: 2.1.3
% 13.90/2.33 % (449352)Termination reason: Refutation not found, incomplete strategy
% 13.90/2.33 % (449352)Time elapsed: 0.081 s
% 13.90/2.33 % (449352)Peak memory usage: 15 MB
% 13.90/2.33 % (449352)Instructions burned: 169 (million)
% 13.90/2.33 % (449352)------------------------------
% 13.90/2.33 % (449352)------------------------------
% 13.90/2.33 % (449398)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=3617103127:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2986 on theBenchmark for (2986ds/130Mi)
% 13.90/2.33 % (449336)Instruction limit reached!
% 13.90/2.33 % (449336)------------------------------
% 13.90/2.33 % (449336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.33 % (449336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.33 % (449336)CaDiCaL version: 2.1.3
% 13.90/2.33 % (449336)Termination reason: Instruction limit
% 13.90/2.33 % (449336)Termination phase: Saturation
% 13.90/2.33 % (449336)Time elapsed: 0.132 s
% 13.90/2.33 % (449336)Peak memory usage: 14 MB
% 13.90/2.33 % (449336)Instructions burned: 282 (million)
% 13.90/2.33 % (449400)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1655168357:st=1.5:i=346:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/346Mi)
% 13.90/2.33 % (449398)Instruction limit reached!
% 13.90/2.33 % (449398)------------------------------
% 13.90/2.33 % (449398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.33 % (449398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.33 % (449398)CaDiCaL version: 2.1.3
% 13.90/2.33 % (449398)Termination reason: Instruction limit
% 13.90/2.33 % (449398)Termination phase: Saturation
% 13.90/2.33 % (449398)Time elapsed: 0.067 s
% 13.90/2.33 % (449398)Peak memory usage: 13 MB
% 13.90/2.33 % (449398)Instructions burned: 131 (million)
% 13.90/2.33 % (449266)Instruction limit reached!
% 13.90/2.33 % (449266)------------------------------
% 13.90/2.33 % (449266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.33 % (449266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.33 % (449266)CaDiCaL version: 2.1.3
% 13.90/2.33 % (449266)Termination reason: Instruction limit
% 13.90/2.33 % (449266)Termination phase: Saturation
% 13.90/2.33 % (449266)Time elapsed: 0.375 s
% 13.90/2.33 % (449266)Peak memory usage: 16 MB
% 13.90/2.33 % (449266)Instructions burned: 1442 (million)
% 13.90/2.33 % (449396)Instruction limit reached!
% 13.90/2.33 % (449396)------------------------------
% 13.90/2.33 % (449396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.33 % (449396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.33 % (449396)CaDiCaL version: 2.1.3
% 13.90/2.33 % (449396)Termination reason: Instruction limit
% 13.90/2.33 % (449396)Termination phase: Saturation
% 13.90/2.33 % (449396)Time elapsed: 0.109 s
% 13.90/2.33 % (449396)Peak memory usage: 14 MB
% 13.90/2.33 % (449396)Instructions burned: 213 (million)
% 13.90/2.33 % (449403)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3118501852:i=75:ep=R:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/75Mi)
% 13.90/2.33 % (449402)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=3859616839:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/152Mi)
% 13.90/2.33 % (449404)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=2060739570:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/387Mi)
% 13.90/2.33 % (449403)Instruction limit reached!
% 13.90/2.33 % (449403)------------------------------
% 13.90/2.33 % (449403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.33 % (449403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.33 % (449403)CaDiCaL version: 2.1.3
% 13.90/2.33 % (449403)Termination reason: Instruction limit
% 13.90/2.33 % (449403)Termination phase: Property scanning
% 13.90/2.33 % (449403)Time elapsed: 0.018 s
% 13.90/2.33 % (449403)Peak memory usage: 11 MB
% 13.90/2.33 % (449403)Instructions burned: 75 (million)
% 13.90/2.33 % (449408)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=2636985072:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2984 on theBenchmark for (2984ds/148Mi)
% 13.90/2.33 % (449408)Instruction limit reached!
% 13.90/2.33 % (449408)------------------------------
% 13.90/2.34 % (449408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449408)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449408)Termination reason: Instruction limit
% 13.90/2.34 % (449408)Termination phase: Saturation
% 13.90/2.34 % (449408)Time elapsed: 0.036 s
% 13.90/2.34 % (449408)Peak memory usage: 13 MB
% 13.90/2.34 % (449408)Instructions burned: 151 (million)
% 13.90/2.34 % (449402)Instruction limit reached!
% 13.90/2.34 % (449402)------------------------------
% 13.90/2.34 % (449402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449402)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449402)Termination reason: Instruction limit
% 13.90/2.34 % (449402)Termination phase: Saturation
% 13.90/2.34 % (449402)Time elapsed: 0.077 s
% 13.90/2.34 % (449402)Peak memory usage: 14 MB
% 13.90/2.34 % (449402)Instructions burned: 152 (million)
% 13.90/2.34 % (449410)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=4174166510:i=161:piset=and:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/161Mi)
% 13.90/2.34 % (449411)lrs+10_1_sil=128000:si=on:random_seed=1327358251:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2984 on theBenchmark for (2984ds/888Mi)
% 13.90/2.34 % (449400)Instruction limit reached!
% 13.90/2.34 % (449400)------------------------------
% 13.90/2.34 % (449400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449400)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449400)Termination reason: Instruction limit
% 13.90/2.34 % (449400)Termination phase: Saturation
% 13.90/2.34 % (449400)Time elapsed: 0.178 s
% 13.90/2.34 % (449400)Peak memory usage: 15 MB
% 13.90/2.34 % (449400)Instructions burned: 348 (million)
% 13.90/2.34 % (449414)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=2184885960:i=136:add=on:ins=4:rtra=on:sup=off_2983 on theBenchmark for (2983ds/136Mi)
% 13.90/2.34 % (449410)Instruction limit reached!
% 13.90/2.34 % (449410)------------------------------
% 13.90/2.34 % (449410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449410)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449410)Termination reason: Instruction limit
% 13.90/2.34 % (449410)Termination phase: Saturation
% 13.90/2.34 % (449410)Time elapsed: 0.083 s
% 13.90/2.34 % (449410)Peak memory usage: 14 MB
% 13.90/2.34 % (449410)Instructions burned: 161 (million)
% 13.90/2.34 % (449416)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=157768697:i=88:s2at=3:nm=2:rtra=on:rawr=on_2983 on theBenchmark for (2983ds/88Mi)
% 13.90/2.34 % (449416)Instruction limit reached!
% 13.90/2.34 % (449416)------------------------------
% 13.90/2.34 % (449416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449416)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449416)Termination reason: Instruction limit
% 13.90/2.34 % (449416)Termination phase: Property scanning
% 13.90/2.34 % (449416)Time elapsed: 0.023 s
% 13.90/2.34 % (449416)Peak memory usage: 12 MB
% 13.90/2.34 % (449416)Instructions burned: 91 (million)
% 13.90/2.34 % (449414)Instruction limit reached!
% 13.90/2.34 % (449414)------------------------------
% 13.90/2.34 % (449414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449414)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449414)Termination reason: Instruction limit
% 13.90/2.34 % (449414)Termination phase: Saturation
% 13.90/2.34 % (449414)Time elapsed: 0.070 s
% 13.90/2.34 % (449414)Peak memory usage: 14 MB
% 13.90/2.34 % (449414)Instructions burned: 137 (million)
% 13.90/2.34 % (449418)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=1591799232:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2983 on theBenchmark for (2983ds/93Mi)
% 13.90/2.34 % (449404)Instruction limit reached!
% 13.90/2.34 % (449404)------------------------------
% 13.90/2.34 % (449404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449404)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449404)Termination reason: Instruction limit
% 13.90/2.34 % (449404)Termination phase: Saturation
% 13.90/2.34 % (449404)Time elapsed: 0.199 s
% 13.90/2.34 % (449404)Peak memory usage: 15 MB
% 13.90/2.34 % (449404)Instructions burned: 389 (million)
% 13.90/2.34 % (449419)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=183910142:i=2186:rtra=on:ixr=off_2983 on theBenchmark for (2983ds/2186Mi)
% 13.90/2.34 % (449421)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3720115545:s2a=on:i=240:rtra=on:ntd=on_2982 on theBenchmark for (2982ds/240Mi)
% 13.90/2.34 % (449418)Instruction limit reached!
% 13.90/2.34 % (449418)------------------------------
% 13.90/2.34 % (449418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449418)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449418)Termination reason: Instruction limit
% 13.90/2.34 % (449418)Termination phase: Property scanning
% 13.90/2.34 % (449418)Time elapsed: 0.023 s
% 13.90/2.34 % (449418)Peak memory usage: 11 MB
% 13.90/2.34 % (449418)Instructions burned: 96 (million)
% 13.90/2.34 % (449424)dis+10_1_to=lpo:sil=128000:tgt=ground:si=on:urr=on:cbe=off:uwa=one_side_constant:nwc=5:random_seed=1582426087:i=805:aac=none:doe=on:piset=not:bd=all:rtra=on:fe=abstraction_2982 on theBenchmark for (2982ds/805Mi)
% 13.90/2.34 % (449374)Instruction limit reached!
% 13.90/2.34 % (449374)------------------------------
% 13.90/2.34 % (449374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.34 % (449374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.34 % (449374)CaDiCaL version: 2.1.3
% 13.90/2.34 % (449374)Termination reason: Instruction limit
% 13.90/2.34 % (449374)Termination phase: Saturation
% 13.90/2.34 % (449374)Time elapsed: 0.480 s
% 13.90/2.34 % (449374)Peak memory usage: 18 MB
% 13.90/2.34 % (449374)Instructions burned: 865 (million)
% 13.90/2.34 % (449447)WARNING Broken Constraint: if avatar_split_queue_cutoffs(1) has been set then avatar_split_queue(off) is equal to on
% 13.90/2.35 % (449447)dis+1002_1_to=lpo:sil=128000:cnfonf=conj_eager:si=on:sp=unary_first:spb=intro:urr=on:cbe=off:uwa=one_side_interpreted:rp=on:avsqc=1:random_seed=2429794042:st=2:s2a=on:i=391:sd=4:bd=preordered:nm=16:rtra=on:ss=axioms:rawr=on_2981 on theBenchmark for (2981ds/391Mi)
% 13.90/2.35 % (449421)Instruction limit reached!
% 13.90/2.35 % (449421)------------------------------
% 13.90/2.35 % (449421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.35 % (449421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.35 % (449421)CaDiCaL version: 2.1.3
% 13.90/2.35 % (449421)Termination reason: Instruction limit
% 13.90/2.35 % (449421)Termination phase: Saturation
% 13.90/2.35 % (449421)Time elapsed: 0.122 s
% 13.90/2.35 % (449421)Peak memory usage: 14 MB
% 13.90/2.35 % (449421)Instructions burned: 241 (million)
% 13.90/2.35 % (449460)dis+10_1_sil=128000:si=on:urr=on:uwa=off:random_seed=1007345998:i=355:av=off:fsr=off:rtra=on:ixr=off_2981 on theBenchmark for (2981ds/355Mi)
% 13.90/2.35 % (449424)Instruction limit reached!
% 13.90/2.35 % (449424)------------------------------
% 13.90/2.35 % (449424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.35 % (449424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.35 % (449424)CaDiCaL version: 2.1.3
% 13.90/2.35 % (449424)Termination reason: Instruction limit
% 13.90/2.35 % (449424)Termination phase: Saturation
% 13.90/2.35 % (449424)Time elapsed: 0.235 s
% 13.90/2.35 % (449424)Peak memory usage: 17 MB
% 13.90/2.35 % (449424)Instructions burned: 808 (million)
% 13.90/2.35 % (449505)lrs+1010_5:1_sil=128000:si=on:uwa=interpreted_only:sac=on:slsq=on:random_seed=760246:lrd=on:i=314:sd=1:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/314Mi)
% 13.90/2.35 % (449447)Instruction limit reached!
% 13.90/2.35 % (449447)------------------------------
% 13.90/2.35 % (449447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.35 % (449447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.35 % (449447)CaDiCaL version: 2.1.3
% 13.90/2.35 % (449447)Termination reason: Instruction limit
% 13.90/2.35 % (449447)Termination phase: Saturation
% 13.90/2.35 % (449447)Time elapsed: 0.205 s
% 13.90/2.35 % (449447)Peak memory usage: 15 MB
% 13.90/2.35 % (449447)Instructions burned: 391 (million)
% 13.90/2.35 % (449411)Instruction limit reached!
% 13.90/2.35 % (449411)------------------------------
% 13.90/2.35 % (449411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.35 % (449411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.35 % (449411)CaDiCaL version: 2.1.3
% 13.90/2.35 % (449411)Termination reason: Instruction limit
% 13.90/2.35 % (449411)Termination phase: Saturation
% 13.90/2.35 % (449411)Time elapsed: 0.462 s
% 13.90/2.35 % (449411)Peak memory usage: 17 MB
% 13.90/2.35 % (449411)Instructions burned: 888 (million)
% 13.90/2.35 % (449505) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-449081-449505"...
% 13.90/2.35 % (449505)...printing done.
% 13.90/2.35 % (449505)Refutation found. Thanks to Tanya!
% 13.90/2.35 % SZS status Theorem for theBenchmark
% 13.90/2.35 % SZS output start Proof for theBenchmark
% 13.90/2.35 thf(type_def_5, type, tLList446370796tllist: ($tType * $tType) > $tType).
% 13.90/2.35 thf(type_def_6, type, coinductive_llist: $tType > $tType).
% 13.90/2.35 thf(type_def_7, type, product_unit: $tType).
% 13.90/2.35 thf(type_def_8, type, set: $tType > $tType).
% 13.90/2.35 thf(type_def_9, type, nat: $tType).
% 13.90/2.35 thf(type_def_10, type, int: $tType).
% 13.90/2.35 thf(type_def_11, type, itself: $tType > $tType).
% 13.90/2.35 thf(type_def_12, type, b: $tType).
% 13.90/2.35 thf(type_def_13, type, a: $tType).
% 13.90/2.35 thf(type_def_14, type, sTfun: ($tType * $tType) > $tType).
% 13.90/2.35 thf(func_def_0, type, type: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_1, type, one: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_2, type, zero: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_3, type, neg_numeral: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_4, type, order: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_5, type, group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_6, type, semiring_1: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_7, type, monoid_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_8, type, zero_neq_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_9, type, semiring_char_0: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_10, type, zero_less_one: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_11, type, comm_monoid_diff: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_12, type, linordered_semidom: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_13, type, cancel_semigroup_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_14, type, ordered_ab_group_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_15, type, cancel1352612707id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_16, type, cancel146912293up_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_17, type, linord1659791738miring: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_18, type, archim1804426504_field: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_19, type, canoni770627133id_add: !>[X0: $tType]:((itself @ X0 > $o))).
% 13.90/2.35 thf(func_def_20, type, coindu328551480prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 13.90/2.35 thf(func_def_21, type, coinductive_llast: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 13.90/2.35 thf(func_def_22, type, coinductive_LCons: !>[X0: $tType]:((X0 > coinductive_llist @ X0 > coinductive_llist @ X0))).
% 13.90/2.35 thf(func_def_23, type, coinductive_LNil: !>[X0: $tType]:(coinductive_llist @ X0)).
% 13.90/2.35 thf(func_def_24, type, coindu1478340336prefix: !>[X0: $tType]:((coinductive_llist @ X0 > coinductive_llist @ X0 > $o))).
% 13.90/2.35 thf(func_def_25, type, coinductive_lsublist: !>[X0: $tType]:((coinductive_llist @ X0 > set @ nat > coinductive_llist @ X0))).
% 13.90/2.35 thf(func_def_26, type, coindu780009021istsum: !>[X0: $tType]:((coinductive_llist @ X0 > X0))).
% 13.90/2.35 thf(func_def_27, type, minus_minus: !>[X0: $tType]:((X0 > X0 > X0))).
% 13.90/2.35 thf(func_def_28, type, one_one: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_29, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 13.90/2.35 thf(func_def_30, type, zero_zero: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_31, type, size_bool: ($o > nat)).
% 13.90/2.35 thf(func_def_32, type, default_default: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_33, type, if: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 13.90/2.35 thf(func_def_34, type, suc: (nat > nat)).
% 13.90/2.35 thf(func_def_35, type, case_nat: !>[X0: $tType]:((X0 > (nat > X0) > nat > X0))).
% 13.90/2.35 thf(func_def_36, type, pred: (nat > nat)).
% 13.90/2.35 thf(func_def_37, type, semiring_1_of_nat: !>[X0: $tType]:((nat > X0))).
% 13.90/2.35 thf(func_def_38, type, semiri532925092at_aux: !>[X0: $tType]:(((X0 > X0) > nat > X0 > X0))).
% 13.90/2.35 thf(func_def_39, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 13.90/2.35 thf(func_def_40, type, nat_triangle: (nat > nat)).
% 13.90/2.35 thf(func_def_41, type, neg_numeral_dbl_inc: !>[X0: $tType]:((X0 > X0))).
% 13.90/2.35 thf(func_def_42, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 13.90/2.35 thf(func_def_43, type, product_Unity: product_unit).
% 13.90/2.35 thf(func_def_44, type, product_rec_bool: !>[X0: $tType]:((X0 > X0 > $o > X0))).
% 13.90/2.35 thf(func_def_45, type, product_rec_unit: !>[X0: $tType]:((X0 > product_unit > X0))).
% 13.90/2.35 thf(func_def_46, type, product_size_unit: (product_unit > nat)).
% 13.90/2.35 thf(func_def_47, type, type2: !>[X0: $tType]:(itself @ X0)).
% 13.90/2.35 thf(func_def_48, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 13.90/2.35 thf(func_def_49, type, tLList98099029ppendt: !>[X0: $tType, X1: $tType]:((coinductive_llist @ X0 > tLList446370796tllist @ X0 @ X1 > tLList446370796tllist @ X0 @ X1))).
% 13.90/2.35 thf(func_def_50, type, tLList365522113concat: !>[X0: $tType, X1: $tType]:((X0 > tLList446370796tllist @ coinductive_llist @ X1 @ X0 > tLList446370796tllist @ X1 @ X0))).
% 13.90/2.35 thf(func_def_51, type, tLList1329345514concat: !>[X0: $tType, X1: $tType]:(((product_unit > X0) > tLList446370796tllist @ coinductive_llist @ X1 @ X0 > tLList446370796tllist @ X1 @ X0))).
% 13.90/2.35 thf(func_def_52, type, tLList1881248882tdropn: !>[X0: $tType, X1: $tType]:((nat > tLList446370796tllist @ X0 @ X1 > tLList446370796tllist @ X0 @ X1))).
% 13.90/2.35 thf(func_def_53, type, tLList1813626245filter: !>[X0: $tType, X1: $tType]:((X0 > (X1 > $o) > tLList446370796tllist @ X1 @ X0 > tLList446370796tllist @ X1 @ X0))).
% 13.90/2.35 thf(func_def_54, type, tLList1122525870filter: !>[X0: $tType, X1: $tType]:(((product_unit > X0) > (X1 > $o) > tLList446370796tllist @ X1 @ X0 > tLList446370796tllist @ X1 @ X0))).
% 13.90/2.35 thf(func_def_55, type, tLList1992840728_TCons: !>[X0: $tType, X1: $tType]:((X0 > tLList446370796tllist @ X0 @ X1 > tLList446370796tllist @ X0 @ X1))).
% 13.90/2.35 thf(func_def_56, type, tLList57907754e_TNil: !>[X0: $tType, X1: $tType]:((X0 > tLList446370796tllist @ X1 @ X0))).
% 13.90/2.35 thf(func_def_57, type, tLList200813139tllist: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1) > (X2 > tLList446370796tllist @ X2 @ X0 > X1) > tLList446370796tllist @ X2 @ X0 > X1))).
% 13.90/2.35 thf(func_def_58, type, tLList1614408749tllist: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > $o) > (X0 > X1) > (X0 > X2) > (X0 > $o) > (X0 > tLList446370796tllist @ X2 @ X1) > (X0 > X0) > X0 > tLList446370796tllist @ X2 @ X1))).
% 13.90/2.35 thf(func_def_59, type, tLList11265572tllist: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X1 > $o) > tLList446370796tllist @ X0 @ X1 > $o))).
% 13.90/2.35 thf(func_def_60, type, tLList457864275tllist: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X0 @ X1 > set @ X1))).
% 13.90/2.35 thf(func_def_61, type, tLList1719791291e_tset: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X0 @ X1 > set @ X0))).
% 13.90/2.35 thf(func_def_62, type, tLList_Mirabelle_ttl: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X0 @ X1 > tLList446370796tllist @ X0 @ X1))).
% 13.90/2.35 thf(func_def_63, type, tLList2115636725e_tnth: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X0 @ X1 > nat > X0))).
% 13.90/2.35 thf(func_def_64, type, tLList636831159tllist: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > $o) > (X0 > X1) > (X0 > X2) > (X0 > X0) > X0 > tLList446370796tllist @ X2 @ X1))).
% 13.90/2.35 thf(func_def_65, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 13.90/2.35 thf(func_def_66, type, n: nat).
% 13.90/2.35 thf(func_def_67, type, xs: tLList446370796tllist @ a @ b).
% 13.90/2.35 thf(func_def_71, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 13.90/2.35 thf(func_def_72, type, vAND: ($o > $o > $o)).
% 13.90/2.35 thf(func_def_73, type, vOR: ($o > $o > $o)).
% 13.90/2.35 thf(func_def_74, type, vNOT: ($o > $o)).
% 13.90/2.35 thf(func_def_75, type, db0: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_76, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 13.90/2.35 thf(func_def_77, type, vIMP: ($o > $o > $o)).
% 13.90/2.35 thf(func_def_78, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 13.90/2.35 thf(func_def_79, type, db1: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_80, type, db2: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_81, type, db6: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_82, type, db5: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_83, type, db4: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_84, type, db3: !>[X0: $tType]:(X0)).
% 13.90/2.35 thf(func_def_85, type, sK0: (nat > nat)).
% 13.90/2.35 thf(func_def_86, type, sK1: ((nat > $o) > nat)).
% 13.90/2.35 thf(func_def_87, type, sK2: (nat > nat)).
% 13.90/2.35 thf(func_def_88, type, sK3: ((nat > $o) > nat)).
% 13.90/2.35 thf(func_def_89, type, sK4: (nat > nat)).
% 13.90/2.35 thf(func_def_90, type, sK5: ((nat > $o) > nat)).
% 13.90/2.35 thf(func_def_91, type, sK6: (nat > nat)).
% 13.90/2.35 thf(func_def_92, type, sK7: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_93, type, sK8: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_94, type, sK9: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_95, type, sK10: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_96, type, sK11: !>[X0: $tType]:(((nat > X0 > $o) > (nat > X0 > X0 > $o) > nat > X0))).
% 13.90/2.35 thf(func_def_97, type, sK12: !>[X0: $tType]:(((nat > X0 > $o) > (nat > X0 > X0 > $o) > nat))).
% 13.90/2.35 thf(func_def_98, type, sK13: !>[X0: $tType]:(((nat > X0 > $o) > (nat > X0 > X0 > $o) > X0))).
% 13.90/2.35 thf(func_def_99, type, sK14: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X1 @ X0 > X0))).
% 13.90/2.35 thf(func_def_100, type, sK15: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X1 @ X0 > X1))).
% 13.90/2.35 thf(func_def_101, type, sK16: !>[X0: $tType, X1: $tType]:((tLList446370796tllist @ X1 @ X0 > tLList446370796tllist @ X1 @ X0))).
% 13.90/2.35 thf(func_def_102, type, sK17: (nat > nat > nat)).
% 13.90/2.35 thf(func_def_103, type, sK18: ((nat > $o) > nat)).
% 13.90/2.35 thf(func_def_104, type, sK19: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_105, type, sK20: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_106, type, sK21: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_107, type, sK22: ((nat > nat > $o) > nat)).
% 13.90/2.35 thf(func_def_108, type, sK23: ((nat > $o) > nat > nat)).
% 13.90/2.35 thf(func_def_109, type, sK24: ((nat > $o) > nat > nat)).
% 13.90/2.35 thf(func_def_110, type, sK25: (nat > nat > nat)).
% 13.90/2.35 thf(func_def_111, type, sK26: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 13.90/2.35 thf(f1,axiom,(
% 13.90/2.35 ! [X2 : $tType,X0 : $tType,X6 : X2,X5 : X2] : ((X5 = X6) = (((tLList57907754e_TNil @ X2 @ X0 @ X5)) = ((tLList57907754e_TNil @ X2 @ X0 @ X6))))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_tllist_Oinject_I1_J)).
% 13.90/2.35 thf(f2,axiom,(
% 13.90/2.35 ! [X1 : $tType,X0 : $tType,X2 : nat,X3 : X1] : (((tLList1881248882tdropn @ X0 @ X1 @ X2 @ (tLList57907754e_TNil @ X1 @ X0 @ X3))) = ((tLList57907754e_TNil @ X1 @ X0 @ X3)))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_tdropn__TNil)).
% 13.90/2.35 thf(f3,axiom,(
% 13.90/2.35 ! [X2 : $tType,X0 : $tType,X1 : $tType,X5 : X2,X3 : (X2 > X1),X4 : (X0 > tLList446370796tllist @ X0 @ X2 > X1)] : (((tLList200813139tllist @ X2 @ X1 @ X0 @ X3 @ X4 @ (tLList57907754e_TNil @ X2 @ X0 @ X5))) = ((X3 @ X5)))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_tllist_Osimps_I5_J)).
% 13.90/2.35 thf(f12,axiom,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X4 : tLList446370796tllist @ X1 @ X0,X3 : X1,X2 : nat] : (((tLList1881248882tdropn @ X1 @ X0 @ (suc @ X2) @ (tLList1992840728_TCons @ X1 @ X0 @ X3 @ X4))) = ((tLList1881248882tdropn @ X1 @ X0 @ X2 @ X4)))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_tdropn__Suc__TCons)).
% 13.90/2.35 thf(f24,axiom,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : tLList446370796tllist @ X1 @ X0] : (! [X3 : X0] : (X2 != ((tLList57907754e_TNil @ X0 @ X1 @ X3))) => ~ ! [X4 : X1,X5 : tLList446370796tllist @ X1 @ X0] : (X2 != ((tLList1992840728_TCons @ X1 @ X0 @ X4 @ X5))))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_tllist_Oexhaust)).
% 13.90/2.35 thf(f27,axiom,(
% 13.90/2.35 ! [X1 : $tType,X2 : $tType,X0 : $tType,X5 : X2,X6 : tLList446370796tllist @ X2 @ X1,X3 : (X1 > X0),X4 : (X2 > tLList446370796tllist @ X2 @ X1 > X0)] : (((tLList200813139tllist @ X1 @ X0 @ X2 @ X3 @ X4 @ (tLList1992840728_TCons @ X2 @ X1 @ X5 @ X6))) = ((X4 @ X5 @ X6)))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26_tllist_Osimps_I6_J)).
% 13.90/2.35 thf(f291,conjecture,(
% 13.90/2.35 (((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[X0 : a] : ((tLList1881248882tdropn @ a @ b @ n))) @ xs)) = ((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)))),
% 13.90/2.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 13.90/2.35 thf(f292,negated_conjecture,(
% 13.90/2.35 ~ (((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[X0 : a] : ((tLList1881248882tdropn @ a @ b @ n))) @ xs)) = ((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)))),
% 13.90/2.35 inference(negated_conjecture,[status(cth)],[f291])).
% 13.90/2.35 thf(f556,plain,(
% 13.90/2.35 ~ (((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[X0 : a] : ((tLList1881248882tdropn @ a @ b @ n))) @ xs)) = ((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)))),
% 13.90/2.35 inference(rectify,[],[f292])).
% 13.90/2.35 thf(f557,plain,(
% 13.90/2.35 ~ (((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) = ((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[Y0 : a]: (tLList1881248882tdropn @ a @ b @ n)) @ xs)))),
% 13.90/2.35 inference(fool_elimination,[],[f556])).
% 13.90/2.35 thf(f641,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X0] : ((X2 = X3) = (((tLList57907754e_TNil @ X0 @ X1 @ X3)) = ((tLList57907754e_TNil @ X0 @ X1 @ X2))))),
% 13.90/2.35 inference(rectify,[],[f1])).
% 13.90/2.35 thf(f642,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X0] : (((X2 = X3)) = (((tLList57907754e_TNil @ X0 @ X1 @ X3) = (tLList57907754e_TNil @ X0 @ X1 @ X2))))),
% 13.90/2.35 inference(fool_elimination,[],[f641])).
% 13.90/2.35 thf(f719,plain,(
% 13.90/2.35 (((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) != ((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[Y0 : a]: (tLList1881248882tdropn @ a @ b @ n)) @ xs)))),
% 13.90/2.35 inference(flattening,[],[f557])).
% 13.90/2.35 thf(f726,plain,(
% 13.90/2.35 ! [X1 : $tType,X0 : $tType,X2 : tLList446370796tllist @ X1 @ X0,X4 : nat,X3 : X1] : (((tLList1881248882tdropn @ X1 @ X0 @ (suc @ X4) @ (tLList1992840728_TCons @ X1 @ X0 @ X3 @ X2))) = ((tLList1881248882tdropn @ X1 @ X0 @ X4 @ X2)))),
% 13.90/2.35 inference(rectify,[],[f12])).
% 13.90/2.35 thf(f727,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : nat,X3 : X0] : (((tLList57907754e_TNil @ X0 @ X1 @ X3)) = ((tLList1881248882tdropn @ X1 @ X0 @ X2 @ (tLList57907754e_TNil @ X0 @ X1 @ X3))))),
% 13.90/2.35 inference(rectify,[],[f2])).
% 13.90/2.35 thf(f729,plain,(
% 13.90/2.35 ! [X0 : $tType,X2 : $tType,X1 : $tType,X4 : tLList446370796tllist @ X1 @ X0,X5 : (X0 > X2),X6 : (X1 > tLList446370796tllist @ X1 @ X0 > X2),X3 : X1] : (((X6 @ X3 @ X4)) = ((tLList200813139tllist @ X0 @ X2 @ X1 @ X5 @ X6 @ (tLList1992840728_TCons @ X1 @ X0 @ X3 @ X4))))),
% 13.90/2.35 inference(rectify,[],[f27])).
% 13.90/2.35 thf(f730,plain,(
% 13.90/2.35 ! [X1 : $tType,X0 : $tType,X2 : $tType,X5 : (X1 > tLList446370796tllist @ X1 @ X0 > X2),X4 : (X0 > X2),X3 : X0] : (((X4 @ X3)) = ((tLList200813139tllist @ X0 @ X2 @ X1 @ X4 @ X5 @ (tLList57907754e_TNil @ X0 @ X1 @ X3))))),
% 13.90/2.35 inference(rectify,[],[f3])).
% 13.90/2.35 thf(f732,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : tLList446370796tllist @ X1 @ X0] : (? [X3 : X0] : (((tLList57907754e_TNil @ X0 @ X1 @ X3)) = X2) | ? [X4 : X1,X5 : tLList446370796tllist @ X1 @ X0] : (((tLList1992840728_TCons @ X1 @ X0 @ X4 @ X5)) = X2))),
% 13.90/2.35 inference(ennf_transformation,[],[f24])).
% 13.90/2.35 thf(f774,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : (X0 > tLList446370796tllist @ X0 @ X1 > X2),X4 : (X1 > X2),X5 : X1] : (((X4 @ X5)) = ((tLList200813139tllist @ X1 @ X2 @ X0 @ X4 @ X3 @ (tLList57907754e_TNil @ X1 @ X0 @ X5))))),
% 13.90/2.35 inference(rectify,[],[f730])).
% 13.90/2.35 thf(f781,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : tLList446370796tllist @ X2 @ X0,X4 : (X0 > X1),X5 : (X2 > tLList446370796tllist @ X2 @ X0 > X1),X6 : X2] : (((tLList200813139tllist @ X0 @ X1 @ X2 @ X4 @ X5 @ (tLList1992840728_TCons @ X2 @ X0 @ X6 @ X3))) = ((X5 @ X6 @ X3)))),
% 13.90/2.35 inference(rectify,[],[f729])).
% 13.90/2.35 thf(f789,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : tLList446370796tllist @ X1 @ X0] : ((((tLList57907754e_TNil @ X0 @ X1 @ (sK14 @ X0 @ X1 @ X2))) = X2) | (((tLList1992840728_TCons @ X1 @ X0 @ (sK15 @ X0 @ X1 @ X2) @ (sK16 @ X0 @ X1 @ X2))) = X2))),
% 13.90/2.35 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP]),skolemize(X1,sK0 @ X0),skolemize(X1,sK0 @ X0),skolemize(X1,sK0 @ X0)],[f732])).
% 13.90/2.35 thf(f790,plain,(
% 13.90/2.35 ! [X0 : $tType,X1 : $tType,X2 : tLList446370796tllist @ X0 @ X1,X3 : nat,X4 : X0] : (((tLList1881248882tdropn @ X0 @ X1 @ (suc @ X3) @ (tLList1992840728_TCons @ X0 @ X1 @ X4 @ X2))) = ((tLList1881248882tdropn @ X0 @ X1 @ X3 @ X2)))),
% 13.90/2.35 inference(rectify,[],[f726])).
% 13.90/2.35 thf(f813,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : $tType,X3 : (X0 > tLList446370796tllist @ X0 @ X1 > X2),X4 : (X1 > X2),X5 : X1] : ((((X4 @ X5)) = ((tLList200813139tllist @ X1 @ X2 @ X0 @ X4 @ X3 @ (tLList57907754e_TNil @ X1 @ X0 @ X5))))) )),
% 13.90/2.35 inference(cnf_transformation,[],[f774])).
% 13.90/2.35 thf(f820,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X0] : ((((X2 = X3)) = (((tLList57907754e_TNil @ X0 @ X1 @ X3) = (tLList57907754e_TNil @ X0 @ X1 @ X2))))) )),
% 13.90/2.35 inference(cnf_transformation,[],[f642])).
% 13.90/2.35 thf(f825,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : nat,X3 : X0] : ((((tLList57907754e_TNil @ X0 @ X1 @ X3)) = ((tLList1881248882tdropn @ X1 @ X0 @ X2 @ (tLList57907754e_TNil @ X0 @ X1 @ X3))))) )),
% 13.90/2.35 inference(cnf_transformation,[],[f727])).
% 13.90/2.35 thf(f829,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : $tType,X3 : tLList446370796tllist @ X2 @ X0,X6 : X2,X4 : (X0 > X1),X5 : (X2 > tLList446370796tllist @ X2 @ X0 > X1)] : ((((tLList200813139tllist @ X0 @ X1 @ X2 @ X4 @ X5 @ (tLList1992840728_TCons @ X2 @ X0 @ X6 @ X3))) = ((X5 @ X6 @ X3)))) )),
% 13.90/2.35 inference(cnf_transformation,[],[f781])).
% 13.90/2.35 thf(f845,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : tLList446370796tllist @ X1 @ X0] : ((((tLList1992840728_TCons @ X1 @ X0 @ (sK15 @ X0 @ X1 @ X2) @ (sK16 @ X0 @ X1 @ X2))) = X2) | (((tLList57907754e_TNil @ X0 @ X1 @ (sK14 @ X0 @ X1 @ X2))) = X2)) )),
% 13.90/2.35 inference(cnf_transformation,[],[f789])).
% 13.90/2.35 thf(f846,plain,(
% 13.90/2.35 (((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) != ((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[Y0 : a]: (tLList1881248882tdropn @ a @ b @ n)) @ xs)))),
% 13.90/2.35 inference(cnf_transformation,[],[f719])).
% 13.90/2.35 thf(f847,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : tLList446370796tllist @ X0 @ X1,X3 : nat,X4 : X0] : ((((tLList1881248882tdropn @ X0 @ X1 @ (suc @ X3) @ (tLList1992840728_TCons @ X0 @ X1 @ X4 @ X2))) = ((tLList1881248882tdropn @ X0 @ X1 @ X3 @ X2)))) )),
% 13.90/2.35 inference(cnf_transformation,[],[f790])).
% 13.90/2.35 thf(f876,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X0] : ((((X2 = X3)) = $false) | ((((tLList57907754e_TNil @ X0 @ X1 @ X3) = (tLList57907754e_TNil @ X0 @ X1 @ X2))) = $true)) )),
% 13.90/2.35 inference(iff_proxy_clausification,[],[f820])).
% 13.90/2.35 thf(f877,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X0] : (((((tLList57907754e_TNil @ X0 @ X1 @ X3) = (tLList57907754e_TNil @ X0 @ X1 @ X2))) = $true) | (X2 != X3)) )),
% 13.90/2.35 inference(equality_proxy_clausification,[],[f876])).
% 13.90/2.35 thf(f878,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X0] : ((((tLList57907754e_TNil @ X0 @ X1 @ X3)) = ((tLList57907754e_TNil @ X0 @ X1 @ X2))) | (X2 != X3)) )),
% 13.90/2.35 inference(equality_proxy_clausification,[],[f877])).
% 13.90/2.35 thf(f2028,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X3 : $tType,X2 : X0,X6 : (X1 > tLList446370796tllist @ X1 @ X0 > X3),X4 : (X0 > X3),X5 : X0] : ((((X4 @ X5)) = ((tLList200813139tllist @ X0 @ X3 @ X1 @ X4 @ X6 @ (tLList57907754e_TNil @ X0 @ X1 @ X2)))) | (X2 != X5)) )),
% 13.90/2.35 inference(constrained_superposition,[],[f813,f878])).
% 13.90/2.35 thf(f2034,plain,(
% 13.90/2.35 ( ! [X0 : $tType,X3 : $tType,X2 : X0,X4 : (X0 > X3),X5 : X0] : ((((X4 @ X5)) = ((X4 @ X2))) | (X2 != X5)) )),
% 13.90/2.35 inference(forward_demodulation,[],[f2028,f813])).
% 13.90/2.35 thf(f2445,plain,(
% 13.90/2.35 ( ! [X0 : tLList446370796tllist @ a @ b] : ((((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) != ((tLList200813139tllist @ b @ tLList446370796tllist @ a @ b @ a @ tLList57907754e_TNil @ b @ a @ (^[Y0 : a]: (tLList1881248882tdropn @ a @ b @ n)) @ X0))) | (xs != X0)) )),
% 13.90/2.35 inference(constrained_superposition,[],[f846,f2034])).
% 13.90/2.35 thf(f2608,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : nat,X3 : tLList446370796tllist @ X0 @ X1,X4 : X1] : ((((tLList57907754e_TNil @ X1 @ X0 @ X4)) != X3) | (((tLList57907754e_TNil @ X1 @ X0 @ X4)) = ((tLList1881248882tdropn @ X0 @ X1 @ X2 @ X3)))) )),
% 13.90/2.35 inference(constrained_superposition,[],[f825,f2034])).
% 13.90/2.35 thf(f2609,plain,(
% 13.90/2.35 ( ! [X1 : $tType,X0 : $tType,X2 : nat,X3 : tLList446370796tllist @ X0 @ X1,X4 : X0,X5 : tLList446370796tllist @ X0 @ X1] : ((((tLList1992840728_TCons @ X0 @ X1 @ X4 @ X5)) != X3) | (((tLList1881248882tdropn @ X0 @ X1 @ X2 @ X5)) = ((tLList1881248882tdropn @ X0 @ X1 @ (suc @ X2) @ X3)))) )),
% 13.90/2.35 inference(constrained_superposition,[],[f847,f2034])).
% 13.90/2.35 thf(f2803,plain,(
% 13.90/2.35 ( ! [X0 : b] : ((((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) != ((tLList57907754e_TNil @ b @ a @ X0))) | (xs != ((tLList57907754e_TNil @ b @ a @ X0)))) )),
% 13.90/2.35 inference(constrained_superposition,[],[f2445,f813])).
% 13.90/2.35 thf(f2804,plain,(
% 13.90/2.35 ( ! [X0 : a,X1 : tLList446370796tllist @ a @ b] : ((xs != ((tLList1992840728_TCons @ a @ b @ X0 @ X1))) | (((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) != (((^[Y0 : a]: (tLList1881248882tdropn @ a @ b @ n)) @ X0 @ X1)))) )),
% 13.90/2.35 inference(constrained_superposition,[],[f2445,f829])).
% 13.90/2.35 thf(f2805,plain,(
% 13.90/2.35 ( ! [X0 : a,X1 : tLList446370796tllist @ a @ b] : ((xs != ((tLList1992840728_TCons @ a @ b @ X0 @ X1))) | (((tLList1881248882tdropn @ a @ b @ (suc @ n) @ xs)) != ((tLList1881248882tdropn @ a @ b @ n @ X1)))) )),
% 13.90/2.35 inference(beta-eta_normalization,[],[f2804])).
% 13.90/2.35 thf(f2806,plain,(
% 13.90/2.35 ( ! [X0 : b] : ((xs != ((tLList57907754e_TNil @ b @ a @ X0)))) )),
% 13.90/2.35 inference(forward_subsumption_resolution,[],[f2803,f2608])).
% 13.90/2.35 thf(f2807,plain,(
% 13.90/2.35 ( ! [X0 : a,X1 : tLList446370796tllist @ a @ b] : ((xs != ((tLList1992840728_TCons @ a @ b @ X0 @ X1)))) )),
% 13.90/2.35 inference(forward_subsumption_resolution,[],[f2805,f2609])).
% 13.90/2.35 thf(f2825,plain,(
% 13.90/2.35 ( ! [X0 : tLList446370796tllist @ a @ b] : ((xs != X0) | (((tLList57907754e_TNil @ b @ a @ (sK14 @ b @ a @ X0))) = X0)) )),
% 13.90/2.35 inference(constrained_superposition,[],[f2807,f845])).
% 13.90/2.35 thf(f2928,plain,(
% 13.90/2.35 (xs = ((tLList57907754e_TNil @ b @ a @ (sK14 @ b @ a @ xs))))),
% 13.90/2.35 inference(equality_resolution,[],[f2825])).
% 13.90/2.35 thf(f2930,plain,(
% 13.90/2.35 $false),
% 13.90/2.35 inference(forward_subsumption_resolution,[],[f2928,f2806])).
% 13.90/2.35 % SZS output end Proof for theBenchmark
% 13.90/2.35 % (449505)------------------------------
% 13.90/2.35 % (449505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.90/2.35 % (449505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.90/2.35 % (449505)CaDiCaL version: 2.1.3
% 13.90/2.35 % (449505)Termination reason: Refutation
% 13.90/2.35 % (449505)Time elapsed: 0.078 s
% 13.90/2.35 % (449505)Peak memory usage: 15 MB
% 13.90/2.35 % (449505)Instructions burned: 264 (million)
% 13.90/2.35 % (449081)Success in time 2.064 s
% 13.90/2.35 % Vampire exiting
%------------------------------------------------------------------------------