%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU517^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:29:53 AM UTC 2026
% Result : Theorem 9.74s 1.88s
% Output : Refutation 9.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU517^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n001.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 13:53:36 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.24 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.75/0.37 % (1271502)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.75/0.37 % (1271512)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=983284476:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.75/0.37 % (1271513)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.75/0.37 % (1271513)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.75/0.37 % (1271507)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1411152777:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.75/0.37 % (1271508)lrs+10_16_si=on:nwc=1.5:random_seed=3127807977:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.75/0.37 % (1271509)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3903751538:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.75/0.37 % (1271511)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2307476858:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.75/0.37 % (1271510)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=1885908300:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.75/0.37 % (1271513)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=976794417:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.75/0.37 % (1271509)Instruction limit reached!
% 0.75/0.37 % (1271509)------------------------------
% 0.75/0.37 % (1271509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (1271509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (1271509)CaDiCaL version: 2.1.3
% 0.75/0.37 % (1271509)Termination reason: Instruction limit
% 0.75/0.37 % (1271509)Termination phase: shuffling
% 0.75/0.37 % (1271509)Time elapsed: 0.002 s
% 0.75/0.37 % (1271509)Peak memory usage: 9 MB
% 0.75/0.37 % (1271509)Instructions burned: 4 (million)
% 0.75/0.37 % (1271508)Instruction limit reached!
% 0.75/0.37 % (1271508)------------------------------
% 0.75/0.37 % (1271508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (1271508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (1271508)CaDiCaL version: 2.1.3
% 0.75/0.37 % (1271508)Termination reason: Instruction limit
% 0.75/0.37 % (1271508)Termination phase: Saturation
% 0.75/0.37 % (1271508)Time elapsed: 0.008 s
% 0.75/0.37 % (1271508)Peak memory usage: 11 MB
% 0.75/0.37 % (1271508)Instructions burned: 18 (million)
% 0.75/0.37 % (1271511)Instruction limit reached!
% 0.75/0.37 % (1271511)------------------------------
% 0.75/0.37 % (1271511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (1271511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (1271511)CaDiCaL version: 2.1.3
% 0.75/0.37 % (1271511)Termination reason: Instruction limit
% 0.75/0.37 % (1271511)Termination phase: Saturation
% 0.75/0.37 % (1271511)Time elapsed: 0.011 s
% 0.75/0.37 % (1271511)Peak memory usage: 11 MB
% 0.75/0.37 % (1271511)Instructions burned: 25 (million)
% 0.75/0.37 % (1271512)Instruction limit reached!
% 0.75/0.37 % (1271512)------------------------------
% 0.75/0.37 % (1271512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.37 % (1271512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.37 % (1271512)CaDiCaL version: 2.1.3
% 0.75/0.37 % (1271512)Termination reason: Instruction limit
% 0.75/0.37 % (1271512)Termination phase: Saturation
% 0.75/0.37 % (1271512)Time elapsed: 0.022 s
% 0.75/0.37 % (1271512)Peak memory usage: 13 MB
% 0.75/0.37 % (1271512)Instructions burned: 78 (million)
% 0.75/0.37 % (1271521)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3389915845:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.37 % (1271521)Instruction limit reached!
% 0.75/0.37 % (1271521)------------------------------
% 0.75/0.37 % (1271521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (1271521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (1271521)CaDiCaL version: 2.1.3
% 0.75/0.40 % (1271521)Termination reason: Instruction limit
% 0.75/0.40 % (1271521)Termination phase: shuffling
% 0.75/0.40 % (1271521)Time elapsed: 0.002 s
% 0.75/0.40 % (1271521)Peak memory usage: 9 MB
% 0.75/0.40 % (1271521)Instructions burned: 4 (million)
% 0.75/0.40 % (1271524)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=417140173:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.75/0.40 % (1271522)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3338145534:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.75/0.40 % (1271523)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.75/0.40 % (1271524)Instruction limit reached!
% 0.75/0.40 % (1271524)------------------------------
% 0.75/0.40 % (1271524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (1271524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (1271524)CaDiCaL version: 2.1.3
% 0.75/0.40 % (1271524)Termination reason: Instruction limit
% 0.75/0.40 % (1271524)Termination phase: Property scanning
% 0.75/0.40 % (1271524)Time elapsed: 0.003 s
% 0.75/0.40 % (1271524)Peak memory usage: 10 MB
% 0.75/0.40 % (1271524)Instructions burned: 13 (million)
% 0.75/0.40 % (1271522)Instruction limit reached!
% 0.75/0.40 % (1271522)------------------------------
% 0.75/0.40 % (1271522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (1271522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (1271522)CaDiCaL version: 2.1.3
% 0.75/0.40 % (1271522)Termination reason: Instruction limit
% 0.75/0.40 % (1271522)Termination phase: Property scanning
% 0.75/0.40 % (1271522)Time elapsed: 0.003 s
% 0.75/0.40 % (1271522)Peak memory usage: 10 MB
% 0.75/0.40 % (1271522)Instructions burned: 6 (million)
% 0.75/0.40 % (1271523)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2367342821:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.75/0.40 % (1271523)Instruction limit reached!
% 0.75/0.40 % (1271523)------------------------------
% 0.75/0.40 % (1271523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (1271523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (1271523)CaDiCaL version: 2.1.3
% 0.75/0.40 % (1271523)Termination reason: Instruction limit
% 0.75/0.40 % (1271523)Termination phase: Property scanning
% 0.75/0.40 % (1271523)Time elapsed: 0.003 s
% 0.75/0.40 % (1271523)Peak memory usage: 9 MB
% 0.75/0.40 % (1271523)Instructions burned: 7 (million)
% 0.75/0.40 % (1271529)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=903734248:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.75/0.40 % (1271526)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.75/0.40 % (1271526)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.75/0.40 % (1271526)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2003615668:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.75/0.40 % (1271507)Instruction limit reached!
% 0.75/0.40 % (1271507)------------------------------
% 0.75/0.40 % (1271507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.40 % (1271507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.40 % (1271507)CaDiCaL version: 2.1.3
% 0.75/0.40 % (1271507)Termination reason: Instruction limit
% 0.75/0.40 % (1271507)Termination phase: Saturation
% 0.75/0.40 % (1271507)Time elapsed: 0.047 s
% 0.75/0.40 % (1271507)Peak memory usage: 13 MB
% 0.75/0.40 % (1271507)Instructions burned: 89 (million)
% 0.75/0.40 % (1271530)lrs+10_1_si=on:cs=on:random_seed=2488504514:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.75/0.40 % (1271532)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.75/0.44 % (1271530)Instruction limit reached!
% 0.75/0.44 % (1271530)------------------------------
% 0.75/0.44 % (1271530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (1271530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (1271530)CaDiCaL version: 2.1.3
% 0.75/0.44 % (1271530)Termination reason: Instruction limit
% 0.75/0.44 % (1271530)Termination phase: Preprocessing 3
% 0.75/0.44 % (1271530)Time elapsed: 0.004 s
% 0.75/0.44 % (1271530)Peak memory usage: 10 MB
% 0.75/0.44 % (1271530)Instructions burned: 8 (million)
% 0.75/0.44 % (1271532)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=3997240047:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.44 % (1271532)Instruction limit reached!
% 0.75/0.44 % (1271532)------------------------------
% 0.75/0.44 % (1271532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (1271532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (1271532)CaDiCaL version: 2.1.3
% 0.75/0.44 % (1271532)Termination reason: Instruction limit
% 0.75/0.44 % (1271532)Termination phase: Property scanning
% 0.75/0.44 % (1271532)Time elapsed: 0.003 s
% 0.75/0.44 % (1271532)Peak memory usage: 9 MB
% 0.75/0.44 % (1271532)Instructions burned: 6 (million)
% 0.75/0.44 % (1271526)Instruction limit reached!
% 0.75/0.44 % (1271526)------------------------------
% 0.75/0.44 % (1271526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (1271526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (1271526)CaDiCaL version: 2.1.3
% 0.75/0.44 % (1271526)Termination reason: Instruction limit
% 0.75/0.44 % (1271526)Termination phase: Saturation
% 0.75/0.44 % (1271526)Time elapsed: 0.014 s
% 0.75/0.44 % (1271526)Peak memory usage: 12 MB
% 0.75/0.44 % (1271526)Instructions burned: 29 (million)
% 0.75/0.44 % (1271529)Instruction limit reached!
% 0.75/0.44 % (1271529)------------------------------
% 0.75/0.44 % (1271529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (1271529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (1271529)CaDiCaL version: 2.1.3
% 0.75/0.44 % (1271529)Termination reason: Instruction limit
% 0.75/0.44 % (1271529)Termination phase: Saturation
% 0.75/0.44 % (1271529)Time elapsed: 0.020 s
% 0.75/0.44 % (1271529)Peak memory usage: 12 MB
% 0.75/0.44 % (1271529)Instructions burned: 88 (million)
% 0.75/0.44 % (1271535)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1561473587:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.75/0.44 % (1271513)Instruction limit reached!
% 0.75/0.44 % (1271513)------------------------------
% 0.75/0.44 % (1271513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (1271513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.44 % (1271513)CaDiCaL version: 2.1.3
% 0.75/0.44 % (1271513)Termination reason: Instruction limit
% 0.75/0.44 % (1271513)Termination phase: Saturation
% 0.75/0.44 % (1271513)Time elapsed: 0.068 s
% 0.75/0.44 % (1271513)Peak memory usage: 14 MB
% 0.75/0.44 % (1271513)Instructions burned: 158 (million)
% 0.75/0.44 % (1271541)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3537199599:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.75/0.44 % (1271537)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=3099575161:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.75/0.44 % (1271539)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=80564810:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.75/0.44 % (1271540)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3385910710:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.75/0.44 % (1271540)Instruction limit reached!
% 0.75/0.44 % (1271540)------------------------------
% 0.75/0.44 % (1271540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.44 % (1271540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271540)CaDiCaL version: 2.1.3
% 1.50/0.49 % (1271540)Termination reason: Instruction limit
% 1.50/0.49 % (1271540)Termination phase: Property scanning
% 1.50/0.49 % (1271540)Time elapsed: 0.006 s
% 1.50/0.49 % (1271540)Peak memory usage: 11 MB
% 1.50/0.49 % (1271540)Instructions burned: 14 (million)
% 1.50/0.49 % (1271535)Instruction limit reached!
% 1.50/0.49 % (1271535)------------------------------
% 1.50/0.49 % (1271535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.49 % (1271535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271535)CaDiCaL version: 2.1.3
% 1.50/0.49 % (1271535)Termination reason: Instruction limit
% 1.50/0.49 % (1271535)Termination phase: Saturation
% 1.50/0.49 % (1271535)Time elapsed: 0.019 s
% 1.50/0.49 % (1271535)Peak memory usage: 13 MB
% 1.50/0.49 % (1271535)Instructions burned: 39 (million)
% 1.50/0.49 % (1271539)Instruction limit reached!
% 1.50/0.49 % (1271539)------------------------------
% 1.50/0.49 % (1271539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.49 % (1271539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271539)CaDiCaL version: 2.1.3
% 1.50/0.49 % (1271539)Termination reason: Instruction limit
% 1.50/0.49 % (1271539)Termination phase: Saturation
% 1.50/0.49 % (1271539)Time elapsed: 0.012 s
% 1.50/0.49 % (1271539)Peak memory usage: 12 MB
% 1.50/0.49 % (1271539)Instructions burned: 25 (million)
% 1.50/0.49 % (1271544)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=4188727386:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.50/0.49 % (1271544)Instruction limit reached!
% 1.50/0.49 % (1271544)------------------------------
% 1.50/0.49 % (1271544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.49 % (1271544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271544)CaDiCaL version: 2.1.3
% 1.50/0.49 % (1271544)Termination reason: Instruction limit
% 1.50/0.49 % (1271544)Termination phase: Property scanning
% 1.50/0.49 % (1271544)Time elapsed: 0.006 s
% 1.50/0.49 % (1271544)Peak memory usage: 11 MB
% 1.50/0.49 % (1271544)Instructions burned: 14 (million)
% 1.50/0.49 % (1271548)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3951760740: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.50/0.49 % (1271549)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2182340691:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.50/0.49 % (1271548)Instruction limit reached!
% 1.50/0.49 % (1271548)------------------------------
% 1.50/0.49 % (1271548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.49 % (1271548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271548)CaDiCaL version: 2.1.3
% 1.50/0.49 % (1271548)Termination reason: Instruction limit
% 1.50/0.49 % (1271548)Termination phase: shuffling
% 1.50/0.49 % (1271548)Time elapsed: 0.002 s
% 1.50/0.49 % (1271548)Peak memory usage: 9 MB
% 1.50/0.49 % (1271548)Instructions burned: 4 (million)
% 1.50/0.49 % (1271551)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=873280973:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.50/0.49 % (1271552)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3878272715:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.50/0.49 % (1271549)Instruction limit reached!
% 1.50/0.49 % (1271549)------------------------------
% 1.50/0.49 % (1271549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.49 % (1271549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271549)CaDiCaL version: 2.1.3
% 1.50/0.49 % (1271549)Termination reason: Instruction limit
% 1.50/0.49 % (1271549)Termination phase: Saturation
% 1.50/0.49 % (1271549)Time elapsed: 0.012 s
% 1.50/0.49 % (1271549)Peak memory usage: 11 MB
% 1.50/0.49 % (1271549)Instructions burned: 27 (million)
% 1.50/0.49 % (1271551)Instruction limit reached!
% 1.50/0.49 % (1271551)------------------------------
% 1.50/0.49 % (1271551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.49 % (1271551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.49 % (1271551)CaDiCaL version: 2.1.3
% 1.50/0.54 % (1271551)Termination reason: Instruction limit
% 1.50/0.54 % (1271551)Termination phase: Saturation
% 1.50/0.54 % (1271551)Time elapsed: 0.010 s
% 1.50/0.54 % (1271551)Peak memory usage: 11 MB
% 1.50/0.54 % (1271551)Instructions burned: 24 (million)
% 1.50/0.54 % (1271555)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.50/0.54 % (1271555)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.50/0.54 % (1271555)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=3825484259:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.50/0.54 % (1271555)Instruction limit reached!
% 1.50/0.54 % (1271555)------------------------------
% 1.50/0.54 % (1271555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.54 % (1271555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.54 % (1271555)CaDiCaL version: 2.1.3
% 1.50/0.54 % (1271555)Termination reason: Instruction limit
% 1.50/0.54 % (1271555)Termination phase: Property scanning
% 1.50/0.54 % (1271555)Time elapsed: 0.006 s
% 1.50/0.54 % (1271555)Peak memory usage: 10 MB
% 1.50/0.54 % (1271555)Instructions burned: 15 (million)
% 1.50/0.54 % (1271558)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.50/0.54 % (1271558)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=4094010468:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.50/0.54 % (1271559)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=2044776344:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.50/0.54 % (1271558)Instruction limit reached!
% 1.50/0.54 % (1271558)------------------------------
% 1.50/0.54 % (1271558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.54 % (1271558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.54 % (1271558)CaDiCaL version: 2.1.3
% 1.50/0.54 % (1271558)Termination reason: Instruction limit
% 1.50/0.54 % (1271558)Termination phase: SInE selection
% 1.50/0.54 % (1271558)Time elapsed: 0.004 s
% 1.50/0.54 % (1271558)Peak memory usage: 10 MB
% 1.50/0.54 % (1271558)Instructions burned: 9 (million)
% 1.50/0.54 % (1271552)Instruction limit reached!
% 1.50/0.54 % (1271552)------------------------------
% 1.50/0.54 % (1271552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.54 % (1271552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.54 % (1271552)CaDiCaL version: 2.1.3
% 1.50/0.54 % (1271552)Termination reason: Instruction limit
% 1.50/0.54 % (1271552)Termination phase: Saturation
% 1.50/0.54 % (1271552)Time elapsed: 0.031 s
% 1.50/0.54 % (1271552)Peak memory usage: 12 MB
% 1.50/0.54 % (1271552)Instructions burned: 60 (million)
% 1.50/0.54 % (1271561)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3576728080:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.50/0.54 % (1271561)Instruction limit reached!
% 1.50/0.54 % (1271561)------------------------------
% 1.50/0.54 % (1271561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.54 % (1271561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.54 % (1271561)CaDiCaL version: 2.1.3
% 1.50/0.54 % (1271561)Termination reason: Instruction limit
% 1.50/0.54 % (1271561)Termination phase: Property scanning
% 1.50/0.54 % (1271561)Time elapsed: 0.003 s
% 1.50/0.54 % (1271561)Peak memory usage: 9 MB
% 1.50/0.54 % (1271561)Instructions burned: 7 (million)
% 1.50/0.54 % (1271559)Instruction limit reached!
% 1.50/0.54 % (1271559)------------------------------
% 1.50/0.54 % (1271559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.50/0.54 % (1271559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.50/0.54 % (1271559)CaDiCaL version: 2.1.3
% 1.50/0.54 % (1271559)Termination reason: Instruction limit
% 1.50/0.54 % (1271559)Termination phase: Saturation
% 1.50/0.54 % (1271559)Time elapsed: 0.017 s
% 2.22/0.63 % (1271559)Peak memory usage: 12 MB
% 2.22/0.63 % (1271559)Instructions burned: 33 (million)
% 2.22/0.63 % (1271541)Instruction limit reached!
% 2.22/0.63 % (1271541)------------------------------
% 2.22/0.63 % (1271541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (1271541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (1271541)CaDiCaL version: 2.1.3
% 2.22/0.63 % (1271541)Termination reason: Instruction limit
% 2.22/0.63 % (1271541)Termination phase: Saturation
% 2.22/0.63 % (1271541)Time elapsed: 0.088 s
% 2.22/0.63 % (1271541)Peak memory usage: 14 MB
% 2.22/0.63 % (1271541)Instructions burned: 328 (million)
% 2.22/0.63 % (1271564)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3639060551:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.22/0.63 % (1271565)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2076935324:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.22/0.63 % (1271569)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=3175464653:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.22/0.63 % (1271564)Instruction limit reached!
% 2.22/0.63 % (1271564)------------------------------
% 2.22/0.63 % (1271564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (1271564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (1271564)CaDiCaL version: 2.1.3
% 2.22/0.63 % (1271564)Termination reason: Instruction limit
% 2.22/0.63 % (1271564)Termination phase: Saturation
% 2.22/0.63 % (1271564)Time elapsed: 0.010 s
% 2.22/0.63 % (1271564)Peak memory usage: 11 MB
% 2.22/0.63 % (1271564)Instructions burned: 24 (million)
% 2.22/0.63 % (1271567)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3452491953:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.22/0.63 % (1271568)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3571158588:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.22/0.63 % (1271565)Instruction limit reached!
% 2.22/0.63 % (1271565)------------------------------
% 2.22/0.63 % (1271565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (1271565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (1271565)CaDiCaL version: 2.1.3
% 2.22/0.63 % (1271565)Termination reason: Instruction limit
% 2.22/0.63 % (1271565)Termination phase: Saturation
% 2.22/0.63 % (1271565)Time elapsed: 0.010 s
% 2.22/0.63 % (1271565)Peak memory usage: 12 MB
% 2.22/0.63 % (1271565)Instructions burned: 20 (million)
% 2.22/0.63 % (1271573)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1268211691:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.22/0.63 % (1271576)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.22/0.63 % (1271576)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3654799932:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.22/0.63 % (1271576)Instruction limit reached!
% 2.22/0.63 % (1271576)------------------------------
% 2.22/0.63 % (1271576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (1271576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (1271576)CaDiCaL version: 2.1.3
% 2.22/0.63 % (1271576)Termination reason: Instruction limit
% 2.22/0.63 % (1271576)Termination phase: Property scanning
% 2.22/0.63 % (1271576)Time elapsed: 0.004 s
% 2.22/0.63 % (1271576)Peak memory usage: 10 MB
% 2.22/0.63 % (1271576)Instructions burned: 9 (million)
% 2.22/0.63 % (1271537)Instruction limit reached!
% 2.22/0.63 % (1271537)------------------------------
% 2.22/0.63 % (1271537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.22/0.63 % (1271537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.22/0.63 % (1271537)CaDiCaL version: 2.1.3
% 2.22/0.63 % (1271537)Termination reason: Instruction limit
% 2.22/0.63 % (1271537)Termination phase: Saturation
% 2.22/0.63 % (1271537)Time elapsed: 0.130 s
% 2.22/0.63 % (1271537)Peak memory usage: 14 MB
% 2.22/0.63 % (1271537)Instructions burned: 251 (million)
% 2.22/0.63 % (1271573)Instruction limit reached!
% 2.71/0.69 % (1271573)------------------------------
% 2.71/0.69 % (1271573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.69 % (1271573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.69 % (1271573)CaDiCaL version: 2.1.3
% 2.71/0.69 % (1271573)Termination reason: Instruction limit
% 2.71/0.69 % (1271573)Termination phase: Saturation
% 2.71/0.69 % (1271573)Time elapsed: 0.021 s
% 2.71/0.69 % (1271573)Peak memory usage: 13 MB
% 2.71/0.69 % (1271573)Instructions burned: 43 (million)
% 2.71/0.69 % (1271579)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1624019721:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.71/0.69 % (1271580)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=4238278508: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.71/0.69 % (1271569)Instruction limit reached!
% 2.71/0.69 % (1271569)------------------------------
% 2.71/0.69 % (1271569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.69 % (1271569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.69 % (1271569)CaDiCaL version: 2.1.3
% 2.71/0.69 % (1271569)Termination reason: Instruction limit
% 2.71/0.69 % (1271569)Termination phase: Saturation
% 2.71/0.69 % (1271569)Time elapsed: 0.055 s
% 2.71/0.69 % (1271569)Peak memory usage: 14 MB
% 2.71/0.69 % (1271569)Instructions burned: 196 (million)
% 2.71/0.69 % (1271581)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.71/0.69 % (1271581)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2275287618: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.71/0.69 % (1271581)Instruction limit reached!
% 2.71/0.69 % (1271581)------------------------------
% 2.71/0.69 % (1271581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.69 % (1271581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.69 % (1271581)CaDiCaL version: 2.1.3
% 2.71/0.69 % (1271581)Termination reason: Instruction limit
% 2.71/0.69 % (1271581)Termination phase: Property scanning
% 2.71/0.69 % (1271581)Time elapsed: 0.003 s
% 2.71/0.69 % (1271581)Peak memory usage: 9 MB
% 2.71/0.69 % (1271581)Instructions burned: 7 (million)
% 2.71/0.69 % (1271584)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=624010665:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.71/0.69 % (1271568)Instruction limit reached!
% 2.71/0.69 % (1271568)------------------------------
% 2.71/0.69 % (1271568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.69 % (1271568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.69 % (1271568)CaDiCaL version: 2.1.3
% 2.71/0.69 % (1271568)Termination reason: Instruction limit
% 2.71/0.69 % (1271568)Termination phase: Saturation
% 2.71/0.69 % (1271568)Time elapsed: 0.061 s
% 2.71/0.69 % (1271568)Peak memory usage: 14 MB
% 2.71/0.69 % (1271568)Instructions burned: 143 (million)
% 2.71/0.69 % (1271584)Instruction limit reached!
% 2.71/0.69 % (1271584)------------------------------
% 2.71/0.69 % (1271584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.71/0.69 % (1271584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.71/0.69 % (1271584)CaDiCaL version: 2.1.3
% 2.71/0.69 % (1271584)Termination reason: Instruction limit
% 2.71/0.69 % (1271584)Termination phase: Saturation
% 2.71/0.69 % (1271584)Time elapsed: 0.005 s
% 2.71/0.69 % (1271584)Peak memory usage: 11 MB
% 2.71/0.69 % (1271584)Instructions burned: 23 (million)
% 2.71/0.69 % (1271589)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=1076296450: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)
% 2.71/0.69 % (1271586)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3880861535:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.71/0.69 % (1271588)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=2188302499:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 3.07/0.78 % (1271586)Instruction limit reached!
% 3.07/0.78 % (1271586)------------------------------
% 3.07/0.78 % (1271586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.78 % (1271586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.78 % (1271586)CaDiCaL version: 2.1.3
% 3.07/0.78 % (1271586)Termination reason: Instruction limit
% 3.07/0.78 % (1271586)Termination phase: Saturation
% 3.07/0.78 % (1271586)Time elapsed: 0.008 s
% 3.07/0.78 % (1271586)Peak memory usage: 11 MB
% 3.07/0.78 % (1271586)Instructions burned: 19 (million)
% 3.07/0.78 % (1271593)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=4129354878: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.07/0.78 % (1271593)Instruction limit reached!
% 3.07/0.78 % (1271593)------------------------------
% 3.07/0.78 % (1271593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.78 % (1271593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.78 % (1271593)CaDiCaL version: 2.1.3
% 3.07/0.78 % (1271593)Termination reason: Instruction limit
% 3.07/0.78 % (1271593)Termination phase: Saturation
% 3.07/0.78 % (1271593)Time elapsed: 0.024 s
% 3.07/0.78 % (1271593)Peak memory usage: 13 MB
% 3.07/0.78 % (1271593)Instructions burned: 46 (million)
% 3.07/0.78 % (1271580)Instruction limit reached!
% 3.07/0.78 % (1271580)------------------------------
% 3.07/0.78 % (1271580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.78 % (1271580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.78 % (1271580)CaDiCaL version: 2.1.3
% 3.07/0.78 % (1271580)Termination reason: Instruction limit
% 3.07/0.78 % (1271580)Termination phase: Saturation
% 3.07/0.78 % (1271580)Time elapsed: 0.085 s
% 3.07/0.78 % (1271580)Peak memory usage: 13 MB
% 3.07/0.78 % (1271580)Instructions burned: 170 (million)
% 3.07/0.78 % (1271579)Instruction limit reached!
% 3.07/0.78 % (1271579)------------------------------
% 3.07/0.78 % (1271579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.78 % (1271579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.78 % (1271579)CaDiCaL version: 2.1.3
% 3.07/0.78 % (1271579)Termination reason: Instruction limit
% 3.07/0.78 % (1271579)Termination phase: Saturation
% 3.07/0.78 % (1271579)Time elapsed: 0.093 s
% 3.07/0.78 % (1271579)Peak memory usage: 13 MB
% 3.07/0.78 % (1271579)Instructions burned: 181 (million)
% 3.07/0.78 % (1271595)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2046283743:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.07/0.78 % (1271596)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=4212501485: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.07/0.78 % (1271597)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.07/0.78 % (1271597)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1692458323:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.07/0.78 % (1271596)Instruction limit reached!
% 3.07/0.78 % (1271596)------------------------------
% 3.07/0.78 % (1271596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.78 % (1271596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.78 % (1271596)CaDiCaL version: 2.1.3
% 3.07/0.78 % (1271596)Termination reason: Instruction limit
% 3.07/0.78 % (1271596)Termination phase: Saturation
% 3.07/0.78 % (1271596)Time elapsed: 0.009 s
% 3.07/0.78 % (1271596)Peak memory usage: 11 MB
% 3.07/0.78 % (1271596)Instructions burned: 21 (million)
% 3.07/0.78 % (1271595)Refutation not found, incomplete strategy
% 3.07/0.78 % (1271595)------------------------------
% 3.07/0.78 % (1271595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.07/0.78 % (1271595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.07/0.78 % (1271595)CaDiCaL version: 2.1.3
% 3.07/0.78 % (1271595)Termination reason: Refutation not found, incomplete strategy
% 4.09/0.93 % (1271595)Time elapsed: 0.019 s
% 4.09/0.93 % (1271595)Peak memory usage: 12 MB
% 4.09/0.93 % (1271595)Instructions burned: 37 (million)
% 4.09/0.93 % (1271510)Instruction limit reached!
% 4.09/0.93 % (1271510)------------------------------
% 4.09/0.93 % (1271510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.09/0.93 % (1271510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/0.93 % (1271510)CaDiCaL version: 2.1.3
% 4.09/0.93 % (1271510)Termination reason: Instruction limit
% 4.09/0.93 % (1271510)Termination phase: Saturation
% 4.09/0.93 % (1271510)Time elapsed: 0.342 s
% 4.09/0.93 % (1271510)Peak memory usage: 17 MB
% 4.09/0.93 % (1271510)Instructions burned: 634 (million)
% 4.09/0.93 % (1271595)------------------------------
% 4.09/0.93 % (1271595)------------------------------
% 4.09/0.93 % (1271601)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2032257011:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 4.09/0.93 % (1271601)Instruction limit reached!
% 4.09/0.93 % (1271601)------------------------------
% 4.09/0.93 % (1271601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.09/0.93 % (1271601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/0.93 % (1271601)CaDiCaL version: 2.1.3
% 4.09/0.93 % (1271601)Termination reason: Instruction limit
% 4.09/0.93 % (1271601)Termination phase: Saturation
% 4.09/0.93 % (1271601)Time elapsed: 0.006 s
% 4.09/0.93 % (1271601)Peak memory usage: 11 MB
% 4.09/0.93 % (1271601)Instructions burned: 14 (million)
% 4.09/0.93 % (1271602)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=1876678638:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 4.09/0.93 % (1271603)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1992605029:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 4.09/0.93 % (1271605)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2799149349:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 4.09/0.93 % (1271603)Instruction limit reached!
% 4.09/0.93 % (1271603)------------------------------
% 4.09/0.93 % (1271603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.09/0.93 % (1271603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/0.93 % (1271603)CaDiCaL version: 2.1.3
% 4.09/0.93 % (1271603)Termination reason: Instruction limit
% 4.09/0.93 % (1271603)Termination phase: Saturation
% 4.09/0.93 % (1271603)Time elapsed: 0.025 s
% 4.09/0.93 % (1271603)Peak memory usage: 13 MB
% 4.09/0.93 % (1271603)Instructions burned: 51 (million)
% 4.09/0.93 % (1271602)Instruction limit reached!
% 4.09/0.93 % (1271602)------------------------------
% 4.09/0.93 % (1271602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.09/0.93 % (1271602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/0.93 % (1271602)CaDiCaL version: 2.1.3
% 4.09/0.93 % (1271602)Termination reason: Instruction limit
% 4.09/0.93 % (1271602)Termination phase: Saturation
% 4.09/0.93 % (1271602)Time elapsed: 0.030 s
% 4.09/0.93 % (1271602)Peak memory usage: 12 MB
% 4.09/0.93 % (1271602)Instructions burned: 66 (million)
% 4.09/0.93 % (1271605)Instruction limit reached!
% 4.09/0.93 % (1271605)------------------------------
% 4.09/0.93 % (1271605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.09/0.93 % (1271605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/0.93 % (1271605)CaDiCaL version: 2.1.3
% 4.09/0.93 % (1271605)Termination reason: Instruction limit
% 4.09/0.93 % (1271605)Termination phase: Saturation
% 4.09/0.93 % (1271605)Time elapsed: 0.015 s
% 4.09/0.93 % (1271605)Peak memory usage: 12 MB
% 4.09/0.93 % (1271605)Instructions burned: 31 (million)
% 4.09/0.93 % (1271588)Instruction limit reached!
% 4.09/0.93 % (1271588)------------------------------
% 4.09/0.93 % (1271588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.09/0.93 % (1271588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.09/0.93 % (1271588)CaDiCaL version: 2.1.3
% 4.09/0.93 % (1271588)Termination reason: Instruction limit
% 4.09/0.93 % (1271588)Termination phase: Saturation
% 4.09/0.93 % (1271588)Time elapsed: 0.142 s
% 4.09/0.93 % (1271588)Peak memory usage: 14 MB
% 4.09/0.93 % (1271588)Instructions burned: 318 (million)
% 4.09/0.93 % (1271609)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2717886359:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 5.55/1.06 % (1271610)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=3874980830:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 5.55/1.06 % (1271612)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.55/1.06 % (1271611)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=594564318:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.55/1.06 % (1271612)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1493043810:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.55/1.06 % (1271610)Instruction limit reached!
% 5.55/1.06 % (1271610)------------------------------
% 5.55/1.06 % (1271610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.06 % (1271610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.06 % (1271610)CaDiCaL version: 2.1.3
% 5.55/1.06 % (1271610)Termination reason: Instruction limit
% 5.55/1.06 % (1271610)Termination phase: Saturation
% 5.55/1.06 % (1271610)Time elapsed: 0.015 s
% 5.55/1.06 % (1271610)Peak memory usage: 12 MB
% 5.55/1.06 % (1271610)Instructions burned: 36 (million)
% 5.55/1.06 % (1271597)Instruction limit reached!
% 5.55/1.06 % (1271597)------------------------------
% 5.55/1.06 % (1271597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.06 % (1271597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.06 % (1271597)CaDiCaL version: 2.1.3
% 5.55/1.06 % (1271597)Termination reason: Instruction limit
% 5.55/1.06 % (1271597)Termination phase: Saturation
% 5.55/1.06 % (1271597)Time elapsed: 0.096 s
% 5.55/1.06 % (1271597)Peak memory usage: 13 MB
% 5.55/1.06 % (1271597)Instructions burned: 200 (million)
% 5.55/1.06 % (1271617)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=3564476866:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.55/1.06 % (1271611)Instruction limit reached!
% 5.55/1.06 % (1271611)------------------------------
% 5.55/1.06 % (1271611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.06 % (1271611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.06 % (1271611)CaDiCaL version: 2.1.3
% 5.55/1.06 % (1271611)Termination reason: Instruction limit
% 5.55/1.06 % (1271611)Termination phase: Saturation
% 5.55/1.06 % (1271611)Time elapsed: 0.034 s
% 5.55/1.06 % (1271611)Peak memory usage: 12 MB
% 5.55/1.06 % (1271611)Instructions burned: 68 (million)
% 5.55/1.06 % (1271618)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=4061152394:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.55/1.06 % (1271621)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3210226806:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 5.55/1.06 % (1271609)Instruction limit reached!
% 5.55/1.06 % (1271609)------------------------------
% 5.55/1.06 % (1271609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.06 % (1271609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.06 % (1271609)CaDiCaL version: 2.1.3
% 5.55/1.06 % (1271609)Termination reason: Instruction limit
% 5.55/1.06 % (1271609)Termination phase: Saturation
% 5.55/1.06 % (1271609)Time elapsed: 0.059 s
% 5.55/1.06 % (1271609)Peak memory usage: 13 MB
% 5.55/1.06 % (1271609)Instructions burned: 137 (million)
% 5.55/1.06 % (1271623)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2949808728:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 5.55/1.06 % (1271618)Instruction limit reached!
% 5.55/1.06 % (1271618)------------------------------
% 5.55/1.06 % (1271618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.55/1.06 % (1271618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.55/1.06 % (1271618)CaDiCaL version: 2.1.3
% 5.55/1.06 % (1271618)Termination reason: Instruction limit
% 5.55/1.06 % (1271618)Termination phase: Saturation
% 5.55/1.06 % (1271618)Time elapsed: 0.041 s
% 5.55/1.06 % (1271618)Peak memory usage: 12 MB
% 5.55/1.06 % (1271618)Instructions burned: 97 (million)
% 6.16/1.15 % (1271612)Instruction limit reached!
% 6.16/1.15 % (1271612)------------------------------
% 6.16/1.15 % (1271612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.15 % (1271612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.15 % (1271612)CaDiCaL version: 2.1.3
% 6.16/1.15 % (1271612)Termination reason: Instruction limit
% 6.16/1.15 % (1271612)Termination phase: Saturation
% 6.16/1.15 % (1271612)Time elapsed: 0.073 s
% 6.16/1.15 % (1271612)Peak memory usage: 12 MB
% 6.16/1.15 % (1271612)Instructions burned: 180 (million)
% 6.16/1.15 % (1271589)Instruction limit reached!
% 6.16/1.15 % (1271589)------------------------------
% 6.16/1.15 % (1271589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.15 % (1271589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.15 % (1271589)CaDiCaL version: 2.1.3
% 6.16/1.15 % (1271589)Termination reason: Instruction limit
% 6.16/1.15 % (1271589)Termination phase: Saturation
% 6.16/1.15 % (1271589)Time elapsed: 0.247 s
% 6.16/1.15 % (1271589)Peak memory usage: 18 MB
% 6.16/1.15 % (1271589)Instructions burned: 856 (million)
% 6.16/1.15 % (1271627)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4278254446:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 6.16/1.15 % (1271625)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1709701165:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 6.16/1.15 % (1271626)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1346508363:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 6.16/1.15 % (1271627)Instruction limit reached!
% 6.16/1.15 % (1271627)------------------------------
% 6.16/1.15 % (1271627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.15 % (1271627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.15 % (1271627)CaDiCaL version: 2.1.3
% 6.16/1.15 % (1271627)Termination reason: Instruction limit
% 6.16/1.15 % (1271627)Termination phase: Saturation
% 6.16/1.15 % (1271627)Time elapsed: 0.011 s
% 6.16/1.15 % (1271627)Peak memory usage: 12 MB
% 6.16/1.15 % (1271627)Instructions burned: 44 (million)
% 6.16/1.15 % (1271631)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3752032111:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 6.16/1.15 % (1271617)Instruction limit reached!
% 6.16/1.15 % (1271617)------------------------------
% 6.16/1.15 % (1271617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.15 % (1271617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.15 % (1271617)CaDiCaL version: 2.1.3
% 6.16/1.15 % (1271617)Termination reason: Instruction limit
% 6.16/1.15 % (1271617)Termination phase: Saturation
% 6.16/1.15 % (1271617)Time elapsed: 0.130 s
% 6.16/1.15 % (1271617)Peak memory usage: 14 MB
% 6.16/1.15 % (1271617)Instructions burned: 247 (million)
% 6.16/1.15 % (1271626)Instruction limit reached!
% 6.16/1.15 % (1271626)------------------------------
% 6.16/1.15 % (1271626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.15 % (1271626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.15 % (1271626)CaDiCaL version: 2.1.3
% 6.16/1.16 % (1271626)Termination reason: Instruction limit
% 6.16/1.16 % (1271626)Termination phase: Saturation
% 6.16/1.16 % (1271626)Time elapsed: 0.070 s
% 6.16/1.16 % (1271626)Peak memory usage: 13 MB
% 6.16/1.16 % (1271626)Instructions burned: 131 (million)
% 6.16/1.16 % (1271633)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2394433890:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 6.16/1.16 % (1271634)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=582248642:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 6.16/1.16 % (1271634)Instruction limit reached!
% 6.16/1.16 % (1271634)------------------------------
% 6.16/1.16 % (1271634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.16 % (1271634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.16 % (1271634)CaDiCaL version: 2.1.3
% 6.16/1.16 % (1271634)Termination reason: Instruction limit
% 6.16/1.16 % (1271634)Termination phase: Saturation
% 6.16/1.16 % (1271634)Time elapsed: 0.048 s
% 6.67/1.31 % (1271634)Peak memory usage: 12 MB
% 6.67/1.31 % (1271634)Instructions burned: 95 (million)
% 6.67/1.31 % (1271637)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=786483106:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 6.67/1.31 % (1271621)Instruction limit reached!
% 6.67/1.31 % (1271621)------------------------------
% 6.67/1.31 % (1271621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.31 % (1271621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.31 % (1271621)CaDiCaL version: 2.1.3
% 6.67/1.31 % (1271621)Termination reason: Instruction limit
% 6.67/1.31 % (1271621)Termination phase: Saturation
% 6.67/1.31 % (1271621)Time elapsed: 0.214 s
% 6.67/1.31 % (1271621)Peak memory usage: 14 MB
% 6.67/1.31 % (1271621)Instructions burned: 427 (million)
% 6.67/1.31 % (1271631)Instruction limit reached!
% 6.67/1.31 % (1271631)------------------------------
% 6.67/1.31 % (1271631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.31 % (1271631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.31 % (1271631)CaDiCaL version: 2.1.3
% 6.67/1.31 % (1271631)Termination reason: Instruction limit
% 6.67/1.31 % (1271631)Termination phase: Saturation
% 6.67/1.31 % (1271631)Time elapsed: 0.156 s
% 6.67/1.31 % (1271631)Peak memory usage: 14 MB
% 6.67/1.31 % (1271631)Instructions burned: 574 (million)
% 6.67/1.31 % (1271640)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=3556046086:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.67/1.31 % (1271639)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=691584644:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2992 on theBenchmark for (2992ds/105Mi)
% 6.67/1.31 % (1271637)Instruction limit reached!
% 6.67/1.31 % (1271637)------------------------------
% 6.67/1.31 % (1271637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.31 % (1271637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.31 % (1271637)CaDiCaL version: 2.1.3
% 6.67/1.31 % (1271637)Termination reason: Instruction limit
% 6.67/1.31 % (1271637)Termination phase: Saturation
% 6.67/1.31 % (1271637)Time elapsed: 0.032 s
% 6.67/1.31 % (1271637)Peak memory usage: 12 MB
% 6.67/1.31 % (1271637)Instructions burned: 65 (million)
% 6.67/1.31 % (1271643)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1208722376:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.67/1.31 % (1271625)Instruction limit reached!
% 6.67/1.31 % (1271625)------------------------------
% 6.67/1.31 % (1271625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.31 % (1271625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.31 % (1271625)CaDiCaL version: 2.1.3
% 6.67/1.31 % (1271625)Termination reason: Instruction limit
% 6.67/1.31 % (1271625)Termination phase: Saturation
% 6.67/1.31 % (1271625)Time elapsed: 0.245 s
% 6.67/1.31 % (1271625)Peak memory usage: 15 MB
% 6.67/1.31 % (1271625)Instructions burned: 515 (million)
% 6.67/1.31 % (1271639)Instruction limit reached!
% 6.67/1.31 % (1271639)------------------------------
% 6.67/1.31 % (1271639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.31 % (1271639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.31 % (1271639)CaDiCaL version: 2.1.3
% 6.67/1.31 % (1271639)Termination reason: Instruction limit
% 6.67/1.31 % (1271639)Termination phase: Saturation
% 6.67/1.31 % (1271639)Time elapsed: 0.054 s
% 6.67/1.31 % (1271639)Peak memory usage: 13 MB
% 6.67/1.31 % (1271639)Instructions burned: 107 (million)
% 6.67/1.31 % (1271645)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=676078020:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.67/1.31 % (1271646)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=872332925:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.67/1.38 % (1271567)Instruction limit reached!
% 6.67/1.38 % (1271567)------------------------------
% 6.67/1.38 % (1271567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.38 % (1271567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.38 % (1271567)CaDiCaL version: 2.1.3
% 6.67/1.38 % (1271567)Termination reason: Instruction limit
% 6.67/1.38 % (1271567)Termination phase: Saturation
% 6.67/1.38 % (1271567)Time elapsed: 0.615 s
% 6.67/1.38 % (1271567)Peak memory usage: 18 MB
% 6.67/1.38 % (1271567)Instructions burned: 1240 (million)
% 6.67/1.38 % (1271646)Instruction limit reached!
% 6.67/1.38 % (1271646)------------------------------
% 6.67/1.38 % (1271646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.38 % (1271646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.38 % (1271646)CaDiCaL version: 2.1.3
% 6.67/1.38 % (1271646)Termination reason: Instruction limit
% 6.67/1.38 % (1271646)Termination phase: Saturation
% 6.67/1.38 % (1271646)Time elapsed: 0.016 s
% 6.67/1.38 % (1271646)Peak memory usage: 12 MB
% 6.67/1.38 % (1271646)Instructions burned: 36 (million)
% 6.67/1.38 % (1271649)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2275899272:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/91Mi)
% 6.67/1.38 % (1271633)Instruction limit reached!
% 6.67/1.38 % (1271633)------------------------------
% 6.67/1.38 % (1271633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.38 % (1271633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.38 % (1271633)CaDiCaL version: 2.1.3
% 6.67/1.38 % (1271633)Termination reason: Instruction limit
% 6.67/1.38 % (1271633)Termination phase: Saturation
% 6.67/1.38 % (1271633)Time elapsed: 0.211 s
% 6.67/1.38 % (1271633)Peak memory usage: 17 MB
% 6.67/1.38 % (1271633)Instructions burned: 451 (million)
% 6.67/1.38 % (1271650)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3935963341: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.67/1.38 % (1271653)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=319566053:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.67/1.38 % (1271653)Instruction limit reached!
% 6.67/1.38 % (1271653)------------------------------
% 6.67/1.38 % (1271653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.38 % (1271653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.38 % (1271653)CaDiCaL version: 2.1.3
% 6.67/1.38 % (1271653)Termination reason: Instruction limit
% 6.67/1.38 % (1271653)Termination phase: Saturation
% 6.67/1.38 % (1271653)Time elapsed: 0.010 s
% 6.67/1.38 % (1271653)Peak memory usage: 11 MB
% 6.67/1.38 % (1271653)Instructions burned: 23 (million)
% 6.67/1.38 % (1271650)Instruction limit reached!
% 6.67/1.38 % (1271650)------------------------------
% 6.67/1.38 % (1271650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.38 % (1271650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.38 % (1271650)CaDiCaL version: 2.1.3
% 6.67/1.38 % (1271650)Termination reason: Instruction limit
% 6.67/1.38 % (1271650)Termination phase: Saturation
% 6.67/1.38 % (1271650)Time elapsed: 0.034 s
% 6.67/1.38 % (1271650)Peak memory usage: 13 MB
% 6.67/1.38 % (1271650)Instructions burned: 66 (million)
% 6.67/1.38 % (1271649)Instruction limit reached!
% 6.67/1.38 % (1271649)------------------------------
% 6.67/1.38 % (1271649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.67/1.38 % (1271649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.67/1.38 % (1271649)CaDiCaL version: 2.1.3
% 6.67/1.38 % (1271649)Termination reason: Instruction limit
% 6.67/1.38 % (1271649)Termination phase: Saturation
% 6.67/1.38 % (1271649)Time elapsed: 0.046 s
% 6.67/1.38 % (1271649)Peak memory usage: 13 MB
% 6.67/1.38 % (1271649)Instructions burned: 93 (million)
% 6.67/1.38 % (1271655)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=2597085275:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.67/1.38 % (1271656)lrs+10_1_sil=128000:si=on:urr=on:random_seed=430779457:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 6.67/1.38 % (1271657)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 8.15/1.59 % (1271657)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=4004668711: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)
% 8.15/1.59 % (1271656)Instruction limit reached!
% 8.15/1.59 % (1271656)------------------------------
% 8.15/1.59 % (1271656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.15/1.59 % (1271656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.15/1.59 % (1271656)CaDiCaL version: 2.1.3
% 8.15/1.59 % (1271656)Termination reason: Instruction limit
% 8.15/1.59 % (1271656)Termination phase: Saturation
% 8.15/1.59 % (1271656)Time elapsed: 0.013 s
% 8.15/1.59 % (1271656)Peak memory usage: 12 MB
% 8.15/1.59 % (1271656)Instructions burned: 29 (million)
% 8.15/1.59 % (1271661)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=772391216:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2990 on theBenchmark for (2990ds/340Mi)
% 8.15/1.59 % (1271623)Instruction limit reached!
% 8.15/1.59 % (1271623)------------------------------
% 8.15/1.59 % (1271623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.15/1.59 % (1271623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.15/1.59 % (1271623)CaDiCaL version: 2.1.3
% 8.15/1.59 % (1271623)Termination reason: Instruction limit
% 8.15/1.59 % (1271623)Termination phase: Saturation
% 8.15/1.59 % (1271623)Time elapsed: 0.422 s
% 8.15/1.59 % (1271623)Peak memory usage: 15 MB
% 8.15/1.59 % (1271623)Instructions burned: 874 (million)
% 8.15/1.59 % (1271643)Instruction limit reached!
% 8.15/1.59 % (1271643)------------------------------
% 8.15/1.59 % (1271643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.15/1.59 % (1271643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.15/1.59 % (1271643)CaDiCaL version: 2.1.3
% 8.15/1.59 % (1271643)Termination reason: Instruction limit
% 8.15/1.59 % (1271643)Termination phase: Saturation
% 8.15/1.59 % (1271643)Time elapsed: 0.198 s
% 8.15/1.59 % (1271643)Peak memory usage: 14 MB
% 8.15/1.59 % (1271643)Instructions burned: 375 (million)
% 8.15/1.59 % (1271663)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1102967144:i=227:sd=1:bd=all:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/227Mi)
% 8.15/1.59 % (1271664)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 8.15/1.59 % (1271657)Instruction limit reached!
% 8.15/1.59 % (1271657)------------------------------
% 8.15/1.59 % (1271657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.15/1.59 % (1271657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.15/1.59 % (1271657)CaDiCaL version: 2.1.3
% 8.15/1.59 % (1271657)Termination reason: Instruction limit
% 8.15/1.59 % (1271657)Termination phase: Saturation
% 8.15/1.59 % (1271657)Time elapsed: 0.062 s
% 8.15/1.59 % (1271657)Peak memory usage: 13 MB
% 8.15/1.59 % (1271657)Instructions burned: 138 (million)
% 8.15/1.59 % (1271664)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2503363330:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 8.15/1.59 % (1271666)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=10882335:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 8.15/1.59 % (1271666)Instruction limit reached!
% 8.15/1.59 % (1271666)------------------------------
% 8.15/1.59 % (1271666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.15/1.59 % (1271666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.15/1.59 % (1271666)CaDiCaL version: 2.1.3
% 8.15/1.59 % (1271666)Termination reason: Instruction limit
% 8.15/1.59 % (1271666)Termination phase: Saturation
% 8.15/1.59 % (1271666)Time elapsed: 0.062 s
% 8.15/1.59 % (1271666)Peak memory usage: 13 MB
% 8.15/1.59 % (1271666)Instructions burned: 117 (million)
% 8.15/1.59 % (1271655)Instruction limit reached!
% 8.15/1.59 % (1271655)------------------------------
% 8.15/1.59 % (1271655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.15/1.59 % (1271655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/1.79 % (1271655)CaDiCaL version: 2.1.3
% 9.33/1.79 % (1271655)Termination reason: Instruction limit
% 9.33/1.79 % (1271655)Termination phase: Saturation
% 9.33/1.79 % (1271655)Time elapsed: 0.168 s
% 9.33/1.79 % (1271655)Peak memory usage: 15 MB
% 9.33/1.79 % (1271655)Instructions burned: 339 (million)
% 9.33/1.79 % (1271645)Instruction limit reached!
% 9.33/1.79 % (1271645)------------------------------
% 9.33/1.79 % (1271645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.33/1.79 % (1271645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/1.79 % (1271645)CaDiCaL version: 2.1.3
% 9.33/1.79 % (1271645)Termination reason: Instruction limit
% 9.33/1.79 % (1271645)Termination phase: Saturation
% 9.33/1.79 % (1271645)Time elapsed: 0.256 s
% 9.33/1.79 % (1271645)Peak memory usage: 16 MB
% 9.33/1.79 % (1271645)Instructions burned: 496 (million)
% 9.33/1.79 % (1271669)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1071130414:i=575:rtra=on_2989 on theBenchmark for (2989ds/575Mi)
% 9.33/1.79 % (1271670)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3597358665: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)
% 9.33/1.79 % (1271663)Instruction limit reached!
% 9.33/1.79 % (1271663)------------------------------
% 9.33/1.79 % (1271663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.33/1.79 % (1271663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/1.79 % (1271663)CaDiCaL version: 2.1.3
% 9.33/1.79 % (1271663)Termination reason: Instruction limit
% 9.33/1.79 % (1271663)Termination phase: Saturation
% 9.33/1.79 % (1271663)Time elapsed: 0.117 s
% 9.33/1.79 % (1271663)Peak memory usage: 13 MB
% 9.33/1.79 % (1271663)Instructions burned: 228 (million)
% 9.33/1.79 % (1271671)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=279983516: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)
% 9.33/1.79 % (1271661)Instruction limit reached!
% 9.33/1.79 % (1271661)------------------------------
% 9.33/1.79 % (1271661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.33/1.79 % (1271661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/1.79 % (1271661)CaDiCaL version: 2.1.3
% 9.33/1.79 % (1271661)Termination reason: Instruction limit
% 9.33/1.79 % (1271661)Termination phase: Saturation
% 9.33/1.79 % (1271661)Time elapsed: 0.157 s
% 9.33/1.79 % (1271661)Peak memory usage: 13 MB
% 9.33/1.79 % (1271661)Instructions burned: 341 (million)
% 9.33/1.79 % (1271674)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1607306996:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 9.33/1.79 % (1271676)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
% 9.33/1.79 % (1271676)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=3055983613:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 9.33/1.79 % (1271676)Refutation not found, incomplete strategy
% 9.33/1.79 % (1271676)------------------------------
% 9.33/1.79 % (1271676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.33/1.79 % (1271676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/1.79 % (1271676)CaDiCaL version: 2.1.3
% 9.33/1.79 % (1271676)Termination reason: Refutation not found, incomplete strategy
% 9.33/1.79 % (1271676)Time elapsed: 0.015 s
% 9.33/1.79 % (1271676)Peak memory usage: 12 MB
% 9.33/1.79 % (1271676)Instructions burned: 31 (million)
% 9.33/1.79 % (1271676)------------------------------
% 9.33/1.79 % (1271676)------------------------------
% 9.33/1.79 % (1271664)Instruction limit reached!
% 9.33/1.79 % (1271664)------------------------------
% 9.33/1.79 % (1271664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.33/1.79 % (1271664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.33/1.79 % (1271664)CaDiCaL version: 2.1.3
% 9.33/1.79 % (1271664)Termination reason: Instruction limit
% 9.74/1.88 % (1271664)Termination phase: Saturation
% 9.74/1.88 % (1271664)Time elapsed: 0.159 s
% 9.74/1.88 % (1271664)Peak memory usage: 12 MB
% 9.74/1.88 % (1271664)Instructions burned: 374 (million)
% 9.74/1.88 % (1271679)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2174435469:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/31Mi)
% 9.74/1.88 % (1271680)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.74/1.88 % (1271680)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.74/1.88 % (1271680)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=1873784991:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2988 on theBenchmark for (2988ds/1440Mi)
% 9.74/1.88 % (1271679)Instruction limit reached!
% 9.74/1.88 % (1271679)------------------------------
% 9.74/1.88 % (1271679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271679)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271679)Termination reason: Instruction limit
% 9.74/1.88 % (1271679)Termination phase: Saturation
% 9.74/1.88 % (1271679)Time elapsed: 0.015 s
% 9.74/1.88 % (1271679)Peak memory usage: 12 MB
% 9.74/1.88 % (1271679)Instructions burned: 32 (million)
% 9.74/1.88 % (1271683)dis+10_2_sil=128000:si=on:random_seed=1315404786:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 9.74/1.88 % (1271670)Instruction limit reached!
% 9.74/1.88 % (1271670)------------------------------
% 9.74/1.88 % (1271670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271670)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271670)Termination reason: Instruction limit
% 9.74/1.88 % (1271670)Termination phase: Saturation
% 9.74/1.88 % (1271670)Time elapsed: 0.139 s
% 9.74/1.88 % (1271670)Peak memory usage: 14 MB
% 9.74/1.88 % (1271670)Instructions burned: 272 (million)
% 9.74/1.88 % (1271685)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2515440187:i=111:add=on:fgj=on:rtra=on:fdi=1024_2987 on theBenchmark for (2987ds/111Mi)
% 9.74/1.88 % (1271685)Instruction limit reached!
% 9.74/1.88 % (1271685)------------------------------
% 9.74/1.88 % (1271685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271685)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271685)Termination reason: Instruction limit
% 9.74/1.88 % (1271685)Termination phase: Saturation
% 9.74/1.88 % (1271685)Time elapsed: 0.057 s
% 9.74/1.88 % (1271685)Peak memory usage: 13 MB
% 9.74/1.88 % (1271685)Instructions burned: 112 (million)
% 9.74/1.88 % (1271674)Instruction limit reached!
% 9.74/1.88 % (1271674)------------------------------
% 9.74/1.88 % (1271674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271674)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271674)Termination reason: Instruction limit
% 9.74/1.88 % (1271674)Termination phase: Saturation
% 9.74/1.88 % (1271674)Time elapsed: 0.210 s
% 9.74/1.88 % (1271674)Peak memory usage: 14 MB
% 9.74/1.88 % (1271674)Instructions burned: 423 (million)
% 9.74/1.88 % (1271687)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=902859533:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/122Mi)
% 9.74/1.88 % (1271688)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=2964013625:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/136Mi)
% 9.74/1.88 % (1271683)Instruction limit reached!
% 9.74/1.88 % (1271683)------------------------------
% 9.74/1.88 % (1271683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271683)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271683)Termination reason: Instruction limit
% 9.74/1.88 % (1271683)Termination phase: Saturation
% 9.74/1.88 % (1271683)Time elapsed: 0.160 s
% 9.74/1.88 % (1271683)Peak memory usage: 13 MB
% 9.74/1.88 % (1271683)Instructions burned: 339 (million)
% 9.74/1.88 % (1271669)Instruction limit reached!
% 9.74/1.88 % (1271669)------------------------------
% 9.74/1.88 % (1271669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271669)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271669)Termination reason: Instruction limit
% 9.74/1.88 % (1271669)Termination phase: Saturation
% 9.74/1.88 % (1271669)Time elapsed: 0.283 s
% 9.74/1.88 % (1271669)Peak memory usage: 14 MB
% 9.74/1.88 % (1271669)Instructions burned: 575 (million)
% 9.74/1.88 % (1271691)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1024435322:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2986 on theBenchmark for (2986ds/232Mi)
% 9.74/1.88 % (1271693)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=2944358870:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2986 on theBenchmark for (2986ds/1254Mi)
% 9.74/1.88 % (1271687)Instruction limit reached!
% 9.74/1.88 % (1271687)------------------------------
% 9.74/1.88 % (1271687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271687)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271687)Termination reason: Instruction limit
% 9.74/1.88 % (1271687)Termination phase: Saturation
% 9.74/1.88 % (1271687)Time elapsed: 0.063 s
% 9.74/1.88 % (1271687)Peak memory usage: 13 MB
% 9.74/1.88 % (1271687)Instructions burned: 123 (million)
% 9.74/1.88 % (1271695)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 9.74/1.88 % (1271688)Instruction limit reached!
% 9.74/1.88 % (1271688)------------------------------
% 9.74/1.88 % (1271688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271688)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271688)Termination reason: Instruction limit
% 9.74/1.88 % (1271688)Termination phase: Saturation
% 9.74/1.88 % (1271688)Time elapsed: 0.069 s
% 9.74/1.88 % (1271688)Peak memory usage: 13 MB
% 9.74/1.88 % (1271688)Instructions burned: 137 (million)
% 9.74/1.88 % (1271695)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=2878194209:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2986 on theBenchmark for (2986ds/281Mi)
% 9.74/1.88 % (1271697)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1233203369:i=619:add=on:rtra=on_2985 on theBenchmark for (2985ds/619Mi)
% 9.74/1.88 % (1271691)Instruction limit reached!
% 9.74/1.88 % (1271691)------------------------------
% 9.74/1.88 % (1271691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271691)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271691)Termination reason: Instruction limit
% 9.74/1.88 % (1271691)Termination phase: Saturation
% 9.74/1.88 % (1271691)Time elapsed: 0.126 s
% 9.74/1.88 % (1271691)Peak memory usage: 14 MB
% 9.74/1.88 % (1271691)Instructions burned: 232 (million)
% 9.74/1.88 % (1271699)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=138610144:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2985 on theBenchmark for (2985ds/865Mi)
% 9.74/1.88 % (1271695)Instruction limit reached!
% 9.74/1.88 % (1271695)------------------------------
% 9.74/1.88 % (1271695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271695)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271695)Termination reason: Instruction limit
% 9.74/1.88 % (1271695)Termination phase: Saturation
% 9.74/1.88 % (1271695)Time elapsed: 0.117 s
% 9.74/1.88 % (1271695)Peak memory usage: 13 MB
% 9.74/1.88 % (1271695)Instructions burned: 283 (million)
% 9.74/1.88 % (1271701)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3663623133:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/212Mi)
% 9.74/1.88 % (1271693) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1271502-1271693"...
% 9.74/1.88 % (1271693)...printing done.
% 9.74/1.88 % (1271693)Refutation found. Thanks to Tanya!
% 9.74/1.88 % SZS status Theorem for theBenchmark
% 9.74/1.88 % SZS output start Proof for theBenchmark
% 9.74/1.88 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 9.74/1.88 thf(func_def_0, type, in: ($i > $i > $o)).
% 9.74/1.88 thf(func_def_1, type, exu: (($i > $o) > $o)).
% 9.74/1.88 thf(func_def_3, type, setextAx: $o).
% 9.74/1.88 thf(func_def_5, type, emptysetAx: $o).
% 9.74/1.88 thf(func_def_6, type, setadjoin: ($i > $i > $i)).
% 9.74/1.88 thf(func_def_7, type, setadjoinAx: $o).
% 9.74/1.88 thf(func_def_8, type, powerset: ($i > $i)).
% 9.74/1.88 thf(func_def_9, type, powersetAx: $o).
% 9.74/1.88 thf(func_def_10, type, setunion: ($i > $i)).
% 9.74/1.88 thf(func_def_11, type, setunionAx: $o).
% 9.74/1.88 thf(func_def_13, type, omega0Ax: $o).
% 9.74/1.88 thf(func_def_14, type, omegaSAx: $o).
% 9.74/1.88 thf(func_def_15, type, omegaIndAx: $o).
% 9.74/1.88 thf(func_def_16, type, replAx: $o).
% 9.74/1.88 thf(func_def_17, type, foundationAx: $o).
% 9.74/1.88 thf(func_def_18, type, wellorderingAx: $o).
% 9.74/1.88 thf(func_def_19, type, descr: (($i > $o) > $i)).
% 9.74/1.88 thf(func_def_20, type, descrp: $o).
% 9.74/1.88 thf(func_def_21, type, dsetconstr: ($i > ($i > $o) > $i)).
% 9.74/1.88 thf(func_def_22, type, dsetconstrI: $o).
% 9.74/1.88 thf(func_def_23, type, dsetconstrEL: $o).
% 9.74/1.88 thf(func_def_24, type, dsetconstrER: $o).
% 9.74/1.88 thf(func_def_25, type, exuE1: $o).
% 9.74/1.88 thf(func_def_26, type, prop2set: ($o > $i)).
% 9.74/1.88 thf(func_def_27, type, prop2setE: $o).
% 9.74/1.88 thf(func_def_28, type, emptysetE: $o).
% 9.74/1.88 thf(func_def_29, type, emptysetimpfalse: $o).
% 9.74/1.88 thf(func_def_30, type, notinemptyset: $o).
% 9.74/1.88 thf(func_def_31, type, exuE3e: $o).
% 9.74/1.88 thf(func_def_32, type, setext: $o).
% 9.74/1.88 thf(func_def_33, type, emptyI: $o).
% 9.74/1.88 thf(func_def_34, type, noeltsimpempty: $o).
% 9.74/1.88 thf(func_def_35, type, setbeta: $o).
% 9.74/1.88 thf(func_def_36, type, nonempty: ($i > $o)).
% 9.74/1.88 thf(func_def_37, type, nonemptyE1: $o).
% 9.74/1.88 thf(func_def_38, type, nonemptyI: $o).
% 9.74/1.88 thf(func_def_39, type, nonemptyI1: $o).
% 9.74/1.88 thf(func_def_40, type, setadjoinIL: $o).
% 9.74/1.88 thf(func_def_41, type, emptyinunitempty: $o).
% 9.74/1.88 thf(func_def_42, type, setadjoinIR: $o).
% 9.74/1.88 thf(func_def_43, type, setadjoinE: $o).
% 9.74/1.88 thf(func_def_44, type, setadjoinOr: $o).
% 9.74/1.88 thf(func_def_45, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 9.74/1.88 thf(func_def_46, type, vIMP: ($o > $o > $o)).
% 9.74/1.88 thf(func_def_47, type, vNOT: ($o > $o)).
% 9.74/1.88 thf(func_def_48, type, db0: !>[X0: $tType]:(X0)).
% 9.74/1.88 thf(func_def_49, type, db1: !>[X0: $tType]:(X0)).
% 9.74/1.88 thf(func_def_50, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 9.74/1.88 thf(func_def_51, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 9.74/1.88 thf(func_def_52, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 9.74/1.88 thf(func_def_53, type, vAND: ($o > $o > $o)).
% 9.74/1.88 thf(func_def_54, type, db3: !>[X0: $tType]:(X0)).
% 9.74/1.88 thf(func_def_55, type, db2: !>[X0: $tType]:(X0)).
% 9.74/1.88 thf(func_def_56, type, vIFF: ($o > $o > $o)).
% 9.74/1.88 thf(func_def_57, type, db4: !>[X0: $tType]:(X0)).
% 9.74/1.88 thf(func_def_58, type, vOR: ($o > $o > $o)).
% 9.74/1.88 thf(func_def_61, type, sF0: $o).
% 9.74/1.88 thf(func_def_62, type, sF1: $o).
% 9.74/1.88 thf(func_def_63, type, sF2: $o).
% 9.74/1.88 thf(func_def_64, type, sF3: $o).
% 9.74/1.88 thf(func_def_65, type, sF4: $o).
% 9.74/1.88 thf(func_def_66, type, sF5: $o).
% 9.74/1.88 thf(func_def_67, type, sF6: $o).
% 9.74/1.88 thf(func_def_68, type, sF7: $o).
% 9.74/1.88 thf(func_def_69, type, sF8: $o).
% 9.74/1.88 thf(func_def_70, type, sF9: $o).
% 9.74/1.88 thf(func_def_71, type, sF10: $o).
% 9.74/1.88 thf(func_def_72, type, sF11: $o).
% 9.74/1.88 thf(func_def_73, type, sF12: $o).
% 9.74/1.88 thf(func_def_74, type, sF13: $o).
% 9.74/1.88 thf(func_def_75, type, sF14: $o).
% 9.74/1.88 thf(func_def_76, type, sF15: $o).
% 9.74/1.88 thf(func_def_77, type, sF16: $o).
% 9.74/1.88 thf(func_def_78, type, sF17: $o).
% 9.74/1.88 thf(func_def_79, type, sF18: $o).
% 9.74/1.88 thf(func_def_80, type, sF19: $o).
% 9.74/1.88 thf(func_def_81, type, sF20: $o).
% 9.74/1.88 thf(func_def_82, type, sF21: $o).
% 9.74/1.88 thf(func_def_83, type, sF22: $o).
% 9.74/1.88 thf(func_def_84, type, sF23: $o).
% 9.74/1.88 thf(func_def_85, type, sF24: $o).
% 9.74/1.88 thf(func_def_86, type, sF25: $o).
% 9.74/1.88 thf(func_def_87, type, sF26: $o).
% 9.74/1.88 thf(func_def_88, type, sF27: $o).
% 9.74/1.88 thf(func_def_89, type, sF28: $o).
% 9.74/1.88 thf(func_def_90, type, sF29: $o).
% 9.74/1.88 thf(func_def_91, type, sF30: $o).
% 9.74/1.88 thf(func_def_92, type, sF31: $o).
% 9.74/1.88 thf(func_def_93, type, sF32: $o).
% 9.74/1.88 thf(func_def_94, type, sF33: $o).
% 9.74/1.88 thf(func_def_95, type, sF34: $o).
% 9.74/1.88 thf(func_def_97, type, sK36: ($i > $i)).
% 9.74/1.88 thf(f2,axiom,(
% 9.74/1.88 (setextAx = ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X1) <=> (in @ X2 @ X0)) => (X0 = X1)))),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setextAx)).
% 9.74/1.88 thf(f3,axiom,(
% 9.74/1.88 (! [X0 : $i] : ~(in @ X0 @ emptyset) = emptysetAx)),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',emptysetAx)).
% 9.74/1.88 thf(f15,axiom,(
% 9.74/1.88 (dsetconstrEL = ! [X2 : $i,X1 : ($i > $o),X0 : $i] : ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) => (in @ X2 @ X0)))),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dsetconstrEL)).
% 9.74/1.88 thf(f21,axiom,(
% 9.74/1.88 (! [X0 : $i] : ((in @ X0 @ emptyset) => $false) = emptysetimpfalse)),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',emptysetimpfalse)).
% 9.74/1.88 thf(f22,axiom,(
% 9.74/1.88 (notinemptyset = ! [X0 : $i] : ~(in @ X0 @ emptyset))),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',notinemptyset)).
% 9.74/1.88 thf(f25,axiom,(
% 9.74/1.88 (! [X0 : $i] : (! [X1 : $i] : ~(in @ X1 @ X0) => (X0 = emptyset)) = emptyI)),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',emptyI)).
% 9.74/1.88 thf(f26,axiom,(
% 9.74/1.88 (! [X0 : $i] : (! [X1 : $i] : ~(in @ X1 @ X0) => (X0 = emptyset)) = noeltsimpempty)),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',noeltsimpempty)).
% 9.74/1.88 thf(f27,axiom,(
% 9.74/1.88 (setbeta = ! [X1 : ($i > $o),X2 : $i,X0 : $i] : ((in @ X2 @ X0) => ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) <=> (X1 @ X2))))),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setbeta)).
% 9.74/1.88 thf(f37,conjecture,(
% 9.74/1.88 setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => ! [X0 : $i] : (X0 = ((dsetconstr @ X0 @ (^[X1 : $i] : ($true)))))))))))))))))))))))))))))))))))))),
% 9.74/1.88 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setoftrueEq)).
% 9.74/1.88 thf(f38,negated_conjecture,(
% 9.74/1.88 ~(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => ! [X0 : $i] : (X0 = ((dsetconstr @ X0 @ (^[X1 : $i] : ($true))))))))))))))))))))))))))))))))))))))),
% 9.74/1.88 inference(negated_conjecture,[status(cth)],[f37])).
% 9.74/1.88 thf(f39,plain,(
% 9.74/1.88 (! [X0 : $i] : (! [X1 : $i] : ~(in @ X1 @ X0) => (X0 = emptyset)) = noeltsimpempty)),
% 9.74/1.88 inference(rectify,[],[f26])).
% 9.74/1.88 thf(f40,plain,(
% 9.74/1.88 (noeltsimpempty = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (~ (in @ Y1 @ Y0)))) => (emptyset = Y0))))))),
% 9.74/1.88 inference(fool_elimination,[],[f39])).
% 9.74/1.88 thf(f54,plain,(
% 9.74/1.88 (notinemptyset = ! [X0 : $i] : ~(in @ X0 @ emptyset))),
% 9.74/1.88 inference(rectify,[],[f22])).
% 9.74/1.88 thf(f55,plain,(
% 9.74/1.88 (notinemptyset = ((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset))))))),
% 9.74/1.88 inference(fool_elimination,[],[f54])).
% 9.74/1.88 thf(f60,plain,(
% 9.74/1.88 (setbeta = ! [X0 : ($i > $o),X1 : $i,X2 : $i] : ((in @ X1 @ X2) => ((in @ X1 @ (dsetconstr @ X2 @ (^[X3 : $i] : ((X0 @ X3))))) <=> (X0 @ X1))))),
% 9.74/1.88 inference(rectify,[],[f27])).
% 9.74/1.88 thf(f61,plain,(
% 9.74/1.88 (setbeta = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((in @ Y1 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y2 @ Y3)))) = (Y2 @ Y1)))))))))))),
% 9.74/1.88 inference(fool_elimination,[],[f60])).
% 9.74/1.88 thf(f64,plain,(
% 9.74/1.88 (! [X0 : $i] : (! [X1 : $i] : ~(in @ X1 @ X0) => (X0 = emptyset)) = emptyI)),
% 9.74/1.88 inference(rectify,[],[f25])).
% 9.74/1.88 thf(f65,plain,(
% 9.74/1.88 (emptyI = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (~ (in @ Y1 @ Y0)))) => (emptyset = Y0))))))),
% 9.74/1.88 inference(fool_elimination,[],[f64])).
% 9.74/1.88 thf(f72,plain,(
% 9.74/1.88 (dsetconstrEL = ! [X0 : $i,X1 : ($i > $o),X2 : $i] : ((in @ X0 @ (dsetconstr @ X2 @ (^[X3 : $i] : ((X1 @ X3))))) => (in @ X0 @ X2)))),
% 9.74/1.88 inference(rectify,[],[f15])).
% 9.74/1.88 thf(f73,plain,(
% 9.74/1.88 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))))),
% 9.74/1.88 inference(fool_elimination,[],[f72])).
% 9.74/1.88 thf(f89,plain,(
% 9.74/1.88 (! [X0 : $i] : ~(in @ X0 @ emptyset) = emptysetAx)),
% 9.74/1.88 inference(rectify,[],[f3])).
% 9.74/1.88 thf(f90,plain,(
% 9.74/1.88 (emptysetAx = ((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset))))))),
% 9.74/1.88 inference(fool_elimination,[],[f89])).
% 9.74/1.88 thf(f91,plain,(
% 9.74/1.88 (! [X0 : $i] : ((in @ X0 @ emptyset) => $false) = emptysetimpfalse)),
% 9.74/1.88 inference(rectify,[],[f21])).
% 9.74/1.88 thf(f92,plain,(
% 9.74/1.88 (emptysetimpfalse = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ emptyset) => $false)))))),
% 9.74/1.88 inference(fool_elimination,[],[f91])).
% 9.74/1.88 thf(f93,plain,(
% 9.74/1.88 (setextAx = ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X1) <=> (in @ X2 @ X0)) => (X0 = X1)))),
% 9.74/1.88 inference(rectify,[],[f2])).
% 9.74/1.88 thf(f94,plain,(
% 9.74/1.88 (setextAx = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) = (in @ Y2 @ Y1)))) => (Y1 = Y0))))))))),
% 9.74/1.88 inference(fool_elimination,[],[f93])).
% 9.74/1.88 thf(f102,plain,(
% 9.74/1.88 ~(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => ! [X0 : $i] : (X0 = ((dsetconstr @ X0 @ (^[X1 : $i] : ($true))))))))))))))))))))))))))))))))))))))),
% 9.74/1.88 inference(rectify,[],[f38])).
% 9.74/1.88 thf(f103,plain,(
% 9.74/1.88 ($true = ((~ (setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => (!! @ $i @ (^[Y0 : $i]: (Y0 = (dsetconstr @ Y0 @ (^[Y1 : $i]: ($true))))))))))))))))))))))))))))))))))))))))))),
% 9.74/1.88 inference(fool_elimination,[],[f102])).
% 9.74/1.88 thf(f114,plain,(
% 9.74/1.88 ($true = ((~ (setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (setadjoinE => (setadjoinOr => (!! @ $i @ (^[Y0 : $i]: (Y0 = (dsetconstr @ Y0 @ (^[Y1 : $i]: ($true))))))))))))))))))))))))))))))))))))))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f103])).
% 9.74/1.88 thf(f128,plain,(
% 9.74/1.88 (noeltsimpempty = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (~ (in @ Y1 @ Y0)))) => (emptyset = Y0))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f40])).
% 9.74/1.88 thf(f131,plain,(
% 9.74/1.88 (emptysetimpfalse = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ emptyset) => $false)))))),
% 9.74/1.88 inference(cnf_transformation,[],[f92])).
% 9.74/1.88 thf(f132,plain,(
% 9.74/1.88 (notinemptyset = ((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f55])).
% 9.74/1.88 thf(f134,plain,(
% 9.74/1.88 (setextAx = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) = (in @ Y2 @ Y1)))) => (Y1 = Y0))))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f94])).
% 9.74/1.88 thf(f137,plain,(
% 9.74/1.88 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f73])).
% 9.74/1.88 thf(f140,plain,(
% 9.74/1.88 (emptyI = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (~ (in @ Y1 @ Y0)))) => (emptyset = Y0))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f65])).
% 9.74/1.88 thf(f142,plain,(
% 9.74/1.88 (setbeta = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((in @ Y1 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y2 @ Y3)))) = (Y2 @ Y1)))))))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f61])).
% 9.74/1.88 thf(f143,plain,(
% 9.74/1.88 (emptysetAx = ((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset))))))),
% 9.74/1.88 inference(cnf_transformation,[],[f90])).
% 9.74/1.88 thf(f148,definition,(
% 9.74/1.88 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 9.74/1.88 introduced(theory,[fool_exhaustiveness_axiom])).
% 9.74/1.88 thf(f157,definition,(
% 9.74/1.88 (sF0 = ((!! @ $i @ (^[Y0 : $i]: (Y0 = (dsetconstr @ Y0 @ (^[Y1 : $i]: ($true))))))))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 9.74/1.88 thf(f158,definition,(
% 9.74/1.88 (sF1 = ((setadjoinOr => sF0)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 9.74/1.88 thf(f159,definition,(
% 9.74/1.88 (sF2 = ((setadjoinE => sF1)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 9.74/1.88 thf(f160,definition,(
% 9.74/1.88 (sF3 = ((setadjoinIR => sF2)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 9.74/1.88 thf(f161,definition,(
% 9.74/1.88 (sF4 = ((emptyinunitempty => sF3)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 9.74/1.88 thf(f162,plain,(
% 9.74/1.88 (((emptyinunitempty => sF3)) = sF4)),
% 9.74/1.88 inference(reorient_equations,[],[f161])).
% 9.74/1.88 thf(f163,definition,(
% 9.74/1.88 (sF5 = ((setadjoinIL => sF4)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 9.74/1.88 thf(f164,plain,(
% 9.74/1.88 (((setadjoinIL => sF4)) = sF5)),
% 9.74/1.88 inference(reorient_equations,[],[f163])).
% 9.74/1.88 thf(f165,definition,(
% 9.74/1.88 (sF6 = ((nonemptyI1 => sF5)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 9.74/1.88 thf(f166,plain,(
% 9.74/1.88 (((nonemptyI1 => sF5)) = sF6)),
% 9.74/1.88 inference(reorient_equations,[],[f165])).
% 9.74/1.88 thf(f167,definition,(
% 9.74/1.88 (sF7 = ((nonemptyI => sF6)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 9.74/1.88 thf(f168,definition,(
% 9.74/1.88 (sF8 = ((nonemptyE1 => sF7)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 9.74/1.88 thf(f169,plain,(
% 9.74/1.88 (((nonemptyE1 => sF7)) = sF8)),
% 9.74/1.88 inference(reorient_equations,[],[f168])).
% 9.74/1.88 thf(f170,definition,(
% 9.74/1.88 (sF9 = ((setbeta => sF8)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 9.74/1.88 thf(f171,definition,(
% 9.74/1.88 (sF10 = ((noeltsimpempty => sF9)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 9.74/1.88 thf(f172,plain,(
% 9.74/1.88 (((noeltsimpempty => sF9)) = sF10)),
% 9.74/1.88 inference(reorient_equations,[],[f171])).
% 9.74/1.88 thf(f173,definition,(
% 9.74/1.88 (sF11 = ((emptyI => sF10)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 9.74/1.88 thf(f174,definition,(
% 9.74/1.88 (sF12 = ((setext => sF11)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 9.74/1.88 thf(f175,plain,(
% 9.74/1.88 (((setext => sF11)) = sF12)),
% 9.74/1.88 inference(reorient_equations,[],[f174])).
% 9.74/1.88 thf(f176,definition,(
% 9.74/1.88 (sF13 = ((exuE3e => sF12)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 9.74/1.88 thf(f177,plain,(
% 9.74/1.88 (((exuE3e => sF12)) = sF13)),
% 9.74/1.88 inference(reorient_equations,[],[f176])).
% 9.74/1.88 thf(f178,definition,(
% 9.74/1.88 (sF14 = ((notinemptyset => sF13)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 9.74/1.88 thf(f179,plain,(
% 9.74/1.88 (((notinemptyset => sF13)) = sF14)),
% 9.74/1.88 inference(reorient_equations,[],[f178])).
% 9.74/1.88 thf(f180,definition,(
% 9.74/1.88 (sF15 = ((emptysetimpfalse => sF14)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 9.74/1.88 thf(f181,plain,(
% 9.74/1.88 (((emptysetimpfalse => sF14)) = sF15)),
% 9.74/1.88 inference(reorient_equations,[],[f180])).
% 9.74/1.88 thf(f182,definition,(
% 9.74/1.88 (sF16 = ((emptysetE => sF15)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 9.74/1.88 thf(f183,plain,(
% 9.74/1.88 (((emptysetE => sF15)) = sF16)),
% 9.74/1.88 inference(reorient_equations,[],[f182])).
% 9.74/1.88 thf(f184,definition,(
% 9.74/1.88 (sF17 = ((prop2setE => sF16)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 9.74/1.88 thf(f185,definition,(
% 9.74/1.88 (sF18 = ((exuE1 => sF17)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 9.74/1.88 thf(f186,definition,(
% 9.74/1.88 (sF19 = ((dsetconstrER => sF18)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF19])],[function_definition])).
% 9.74/1.88 thf(f187,plain,(
% 9.74/1.88 (((dsetconstrER => sF18)) = sF19)),
% 9.74/1.88 inference(reorient_equations,[],[f186])).
% 9.74/1.88 thf(f188,definition,(
% 9.74/1.88 (sF20 = ((dsetconstrEL => sF19)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF20])],[function_definition])).
% 9.74/1.88 thf(f189,plain,(
% 9.74/1.88 (((dsetconstrEL => sF19)) = sF20)),
% 9.74/1.88 inference(reorient_equations,[],[f188])).
% 9.74/1.88 thf(f190,definition,(
% 9.74/1.88 (sF21 = ((dsetconstrI => sF20)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF21])],[function_definition])).
% 9.74/1.88 thf(f191,plain,(
% 9.74/1.88 (((dsetconstrI => sF20)) = sF21)),
% 9.74/1.88 inference(reorient_equations,[],[f190])).
% 9.74/1.88 thf(f192,definition,(
% 9.74/1.88 (sF22 = ((descrp => sF21)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF22])],[function_definition])).
% 9.74/1.88 thf(f193,definition,(
% 9.74/1.88 (sF23 = ((wellorderingAx => sF22)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF23])],[function_definition])).
% 9.74/1.88 thf(f194,plain,(
% 9.74/1.88 (((wellorderingAx => sF22)) = sF23)),
% 9.74/1.88 inference(reorient_equations,[],[f193])).
% 9.74/1.88 thf(f195,definition,(
% 9.74/1.88 (sF24 = ((foundationAx => sF23)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF24])],[function_definition])).
% 9.74/1.88 thf(f196,plain,(
% 9.74/1.88 (((foundationAx => sF23)) = sF24)),
% 9.74/1.88 inference(reorient_equations,[],[f195])).
% 9.74/1.88 thf(f197,definition,(
% 9.74/1.88 (sF25 = ((replAx => sF24)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF25])],[function_definition])).
% 9.74/1.88 thf(f198,plain,(
% 9.74/1.88 (((replAx => sF24)) = sF25)),
% 9.74/1.88 inference(reorient_equations,[],[f197])).
% 9.74/1.88 thf(f199,definition,(
% 9.74/1.88 (sF26 = ((omegaIndAx => sF25)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF26])],[function_definition])).
% 9.74/1.88 thf(f200,definition,(
% 9.74/1.88 (sF27 = ((omegaSAx => sF26)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF27])],[function_definition])).
% 9.74/1.88 thf(f201,definition,(
% 9.74/1.88 (sF28 = ((omega0Ax => sF27)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF28])],[function_definition])).
% 9.74/1.88 thf(f202,plain,(
% 9.74/1.88 (((omega0Ax => sF27)) = sF28)),
% 9.74/1.88 inference(reorient_equations,[],[f201])).
% 9.74/1.88 thf(f203,definition,(
% 9.74/1.88 (sF29 = ((setunionAx => sF28)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF29])],[function_definition])).
% 9.74/1.88 thf(f204,definition,(
% 9.74/1.88 (sF30 = ((powersetAx => sF29)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF30])],[function_definition])).
% 9.74/1.88 thf(f205,plain,(
% 9.74/1.88 (((powersetAx => sF29)) = sF30)),
% 9.74/1.88 inference(reorient_equations,[],[f204])).
% 9.74/1.88 thf(f206,definition,(
% 9.74/1.88 (sF31 = ((setadjoinAx => sF30)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF31])],[function_definition])).
% 9.74/1.88 thf(f207,plain,(
% 9.74/1.88 (((setadjoinAx => sF30)) = sF31)),
% 9.74/1.88 inference(reorient_equations,[],[f206])).
% 9.74/1.88 thf(f208,definition,(
% 9.74/1.88 (sF32 = ((emptysetAx => sF31)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF32])],[function_definition])).
% 9.74/1.88 thf(f209,plain,(
% 9.74/1.88 (((emptysetAx => sF31)) = sF32)),
% 9.74/1.88 inference(reorient_equations,[],[f208])).
% 9.74/1.88 thf(f210,definition,(
% 9.74/1.88 (sF33 = ((setextAx => sF32)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF33])],[function_definition])).
% 9.74/1.88 thf(f211,definition,(
% 9.74/1.88 (sF34 = ((~ sF33)))),
% 9.74/1.88 introduced(definition,[new_symbols(definition,[sF34])],[function_definition])).
% 9.74/1.88 thf(f212,plain,(
% 9.74/1.88 (((~ sF33)) = sF34)),
% 9.74/1.88 inference(reorient_equations,[],[f211])).
% 9.74/1.88 thf(f213,plain,(
% 9.74/1.88 ($true = sF34)),
% 9.74/1.88 inference(definition_folding,[],[f114,f212,f210,f209,f207,f205,f203,f202,f200,f199,f198,f196,f194,f192,f191,f189,f187,f185,f184,f183,f181,f179,f177,f175,f173,f172,f170,f169,f167,f166,f164,f162,f160,f159,f158,f157])).
% 9.74/1.88 thf(f216,plain,(
% 9.74/1.88 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ Y1)) => (in @ Y2 @ Y0))))))))))),
% 9.74/1.88 inference(beta-eta_normalization,[],[f137])).
% 9.74/1.88 thf(f219,plain,(
% 9.74/1.88 (setbeta = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) = (Y2 @ Y1)))))))))))),
% 9.74/1.88 inference(beta-eta_normalization,[],[f142])).
% 9.74/1.88 thf(f221,plain,(
% 9.74/1.88 (emptysetimpfalse = ((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset))))))),
% 9.74/1.88 inference(boolean_simplification,[],[f131])).
% 9.74/1.88 thf(f227,plain,(
% 9.74/1.88 ($true = ((~ sF33)))),
% 9.74/1.88 inference(backward_demodulation,[],[f212,f213])).
% 9.74/1.88 thf(f228,plain,(
% 9.74/1.88 ($false = sF33)),
% 9.74/1.88 inference(not_proxy_clausification,[],[f227])).
% 9.74/1.88 thf(f233,plain,(
% 9.74/1.88 ($false = ((setextAx => sF32)))),
% 9.74/1.88 inference(backward_demodulation,[],[f210,f228])).
% 9.74/1.88 thf(f237,plain,(
% 9.74/1.88 (sF32 = $false)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f233])).
% 9.74/1.88 thf(f238,plain,(
% 9.74/1.88 (setextAx = $true)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f233])).
% 9.74/1.88 thf(f247,plain,(
% 9.74/1.88 (((emptysetAx => sF31)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f209,f237])).
% 9.74/1.88 thf(f251,plain,(
% 9.74/1.88 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) = (in @ Y2 @ Y1)))) => (Y1 = Y0))))))))),
% 9.74/1.88 inference(backward_demodulation,[],[f134,f238])).
% 9.74/1.88 thf(f254,plain,(
% 9.74/1.88 ($false = (((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset)))) => sF31)))),
% 9.74/1.88 inference(forward_demodulation,[],[f247,f143])).
% 9.74/1.88 thf(f257,plain,(
% 9.74/1.88 (((emptysetimpfalse => sF31)) = $false)),
% 9.74/1.88 inference(forward_demodulation,[],[f254,f221])).
% 9.74/1.88 thf(f259,plain,(
% 9.74/1.88 (emptysetimpfalse = $true)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f257])).
% 9.74/1.88 thf(f260,plain,(
% 9.74/1.88 ($false = ((emptysetimpfalse => $true))) | ($false = sF31)),
% 9.74/1.88 inference(superposition,[],[f257,f148])).
% 9.74/1.88 thf(f263,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF31)),
% 9.74/1.88 inference(boolean_simplification,[],[f260])).
% 9.74/1.88 thf(f264,plain,(
% 9.74/1.88 ($false = sF31)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f263])).
% 9.74/1.88 thf(f268,plain,(
% 9.74/1.88 ($false = ((setadjoinAx => sF30)))),
% 9.74/1.88 inference(backward_demodulation,[],[f207,f264])).
% 9.74/1.88 thf(f272,plain,(
% 9.74/1.88 ($true = ((!! @ $i @ (^[Y0 : $i]: (~ (in @ Y0 @ emptyset))))))),
% 9.74/1.88 inference(backward_demodulation,[],[f221,f259])).
% 9.74/1.88 thf(f273,plain,(
% 9.74/1.88 (sF15 = (($true => sF14)))),
% 9.74/1.88 inference(backward_demodulation,[],[f181,f259])).
% 9.74/1.88 thf(f274,plain,(
% 9.74/1.88 (sF15 = sF14)),
% 9.74/1.88 inference(boolean_simplification,[],[f273])).
% 9.74/1.88 thf(f279,plain,(
% 9.74/1.88 (((notinemptyset => sF13)) = sF15)),
% 9.74/1.88 inference(backward_demodulation,[],[f179,f274])).
% 9.74/1.88 thf(f280,plain,(
% 9.74/1.88 (notinemptyset = $true)),
% 9.74/1.88 inference(backward_demodulation,[],[f132,f272])).
% 9.74/1.88 thf(f282,plain,(
% 9.74/1.88 (sF15 = (($true => sF13)))),
% 9.74/1.88 inference(backward_demodulation,[],[f279,f280])).
% 9.74/1.88 thf(f283,plain,(
% 9.74/1.88 (sF15 = sF13)),
% 9.74/1.88 inference(boolean_simplification,[],[f282])).
% 9.74/1.88 thf(f285,plain,(
% 9.74/1.88 (((emptysetE => sF13)) = sF16)),
% 9.74/1.88 inference(backward_demodulation,[],[f183,f283])).
% 9.74/1.88 thf(f300,plain,(
% 9.74/1.88 ($false = ((setadjoinAx => $true))) | ($false = sF30)),
% 9.74/1.88 inference(superposition,[],[f268,f148])).
% 9.74/1.88 thf(f304,plain,(
% 9.74/1.88 ($false = sF30) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f300])).
% 9.74/1.88 thf(f305,plain,(
% 9.74/1.88 ($false = sF30)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f304])).
% 9.74/1.88 thf(f308,plain,(
% 9.74/1.88 (((powersetAx => sF29)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f205,f305])).
% 9.74/1.88 thf(f319,plain,(
% 9.74/1.88 (((emptysetE => $true)) = sF16) | ($false = sF13)),
% 9.74/1.88 inference(superposition,[],[f285,f148])).
% 9.74/1.88 thf(f323,plain,(
% 9.74/1.88 ($false = sF13) | ($true = sF16)),
% 9.74/1.88 inference(boolean_simplification,[],[f319])).
% 9.74/1.88 thf(f329,plain,(
% 9.74/1.88 ($false = ((powersetAx => $true))) | ($false = sF29)),
% 9.74/1.88 inference(superposition,[],[f308,f148])).
% 9.74/1.88 thf(f332,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF29)),
% 9.74/1.88 inference(boolean_simplification,[],[f329])).
% 9.74/1.88 thf(f333,plain,(
% 9.74/1.88 ($false = sF29)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f332])).
% 9.74/1.88 thf(f337,plain,(
% 9.74/1.88 ($false = ((setunionAx => sF28)))),
% 9.74/1.88 inference(backward_demodulation,[],[f203,f333])).
% 9.74/1.88 thf(f346,plain,(
% 9.74/1.88 (((setunionAx => $true)) = $false) | ($false = sF28)),
% 9.74/1.88 inference(superposition,[],[f337,f148])).
% 9.74/1.88 thf(f349,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF28)),
% 9.74/1.88 inference(boolean_simplification,[],[f346])).
% 9.74/1.88 thf(f350,plain,(
% 9.74/1.88 ($false = sF28)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f349])).
% 9.74/1.88 thf(f354,plain,(
% 9.74/1.88 ($false = ((omega0Ax => sF27)))),
% 9.74/1.88 inference(backward_demodulation,[],[f202,f350])).
% 9.74/1.88 thf(f361,plain,(
% 9.74/1.88 (sF27 = $false)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f354])).
% 9.74/1.88 thf(f371,plain,(
% 9.74/1.88 ($false = ((omegaSAx => sF26)))),
% 9.74/1.88 inference(backward_demodulation,[],[f200,f361])).
% 9.74/1.88 thf(f378,plain,(
% 9.74/1.88 (sF26 = $false)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f371])).
% 9.74/1.88 thf(f388,plain,(
% 9.74/1.88 (((omegaIndAx => sF25)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f199,f378])).
% 9.74/1.88 thf(f395,plain,(
% 9.74/1.88 ($false = sF25)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f388])).
% 9.74/1.88 thf(f411,plain,(
% 9.74/1.88 (((replAx => sF24)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f198,f395])).
% 9.74/1.88 thf(f414,plain,(
% 9.74/1.88 ($false = sF24) | ($false = ((replAx => $true)))),
% 9.74/1.88 inference(superposition,[],[f411,f148])).
% 9.74/1.88 thf(f418,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF24)),
% 9.74/1.88 inference(boolean_simplification,[],[f414])).
% 9.74/1.88 thf(f419,plain,(
% 9.74/1.88 ($false = sF24)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f418])).
% 9.74/1.88 thf(f422,plain,(
% 9.74/1.88 ($false = ((foundationAx => sF23)))),
% 9.74/1.88 inference(backward_demodulation,[],[f196,f419])).
% 9.74/1.88 thf(f431,plain,(
% 9.74/1.88 ($false = ((foundationAx => $true))) | ($false = sF23)),
% 9.74/1.88 inference(superposition,[],[f422,f148])).
% 9.74/1.88 thf(f435,plain,(
% 9.74/1.88 ($false = sF23) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f431])).
% 9.74/1.88 thf(f436,plain,(
% 9.74/1.88 ($false = sF23)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f435])).
% 9.74/1.88 thf(f439,plain,(
% 9.74/1.88 ($false = ((wellorderingAx => sF22)))),
% 9.74/1.88 inference(backward_demodulation,[],[f194,f436])).
% 9.74/1.88 thf(f444,plain,(
% 9.74/1.88 ($false = sF22)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f439])).
% 9.74/1.88 thf(f460,plain,(
% 9.74/1.88 ($false = ((descrp => sF21)))),
% 9.74/1.88 inference(backward_demodulation,[],[f192,f444])).
% 9.74/1.88 thf(f461,plain,(
% 9.74/1.88 ($false = sF21)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f460])).
% 9.74/1.88 thf(f471,plain,(
% 9.74/1.88 ($false = ((dsetconstrI => sF20)))),
% 9.74/1.88 inference(backward_demodulation,[],[f191,f461])).
% 9.74/1.88 thf(f480,plain,(
% 9.74/1.88 ($false = sF20)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f471])).
% 9.74/1.88 thf(f490,plain,(
% 9.74/1.88 (((dsetconstrEL => sF19)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f189,f480])).
% 9.74/1.88 thf(f496,plain,(
% 9.74/1.88 (dsetconstrEL = $true)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f490])).
% 9.74/1.88 thf(f497,plain,(
% 9.74/1.88 ($false = sF19) | ($false = ((dsetconstrEL => $true)))),
% 9.74/1.88 inference(superposition,[],[f490,f148])).
% 9.74/1.88 thf(f500,plain,(
% 9.74/1.88 ($false = sF19) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f497])).
% 9.74/1.88 thf(f501,plain,(
% 9.74/1.88 ($false = sF19)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f500])).
% 9.74/1.88 thf(f505,plain,(
% 9.74/1.88 ($false = ((dsetconstrER => sF18)))),
% 9.74/1.88 inference(backward_demodulation,[],[f187,f501])).
% 9.74/1.88 thf(f509,plain,(
% 9.74/1.88 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ Y1)) => (in @ Y2 @ Y0))))))))))),
% 9.74/1.88 inference(backward_demodulation,[],[f216,f496])).
% 9.74/1.88 thf(f516,plain,(
% 9.74/1.88 ($false = ((dsetconstrER => $true))) | (sF18 = $false)),
% 9.74/1.88 inference(superposition,[],[f505,f148])).
% 9.74/1.88 thf(f519,plain,(
% 9.74/1.88 ($true = $false) | (sF18 = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f516])).
% 9.74/1.88 thf(f520,plain,(
% 9.74/1.88 (sF18 = $false)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f519])).
% 9.74/1.88 thf(f524,plain,(
% 9.74/1.88 ($false = ((exuE1 => sF17)))),
% 9.74/1.88 inference(backward_demodulation,[],[f185,f520])).
% 9.74/1.88 thf(f533,plain,(
% 9.74/1.88 ($false = ((exuE1 => $true))) | ($false = sF17)),
% 9.74/1.88 inference(superposition,[],[f524,f148])).
% 9.74/1.88 thf(f536,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF17)),
% 9.74/1.88 inference(boolean_simplification,[],[f533])).
% 9.74/1.88 thf(f537,plain,(
% 9.74/1.88 ($false = sF17)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f536])).
% 9.74/1.88 thf(f541,plain,(
% 9.74/1.88 ($false = ((prop2setE => sF16)))),
% 9.74/1.88 inference(backward_demodulation,[],[f184,f537])).
% 9.74/1.88 thf(f552,plain,(
% 9.74/1.88 ($false = sF16) | ($false = ((prop2setE => $true)))),
% 9.74/1.88 inference(superposition,[],[f541,f148])).
% 9.74/1.88 thf(f555,plain,(
% 9.74/1.88 ($false = sF16) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f552])).
% 9.74/1.88 thf(f556,plain,(
% 9.74/1.88 ($false = sF16)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f555])).
% 9.74/1.88 thf(f560,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF13)),
% 9.74/1.88 inference(backward_demodulation,[],[f323,f556])).
% 9.74/1.88 thf(f563,plain,(
% 9.74/1.88 ($false = sF13)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f560])).
% 9.74/1.88 thf(f570,plain,(
% 9.74/1.88 (((exuE3e => sF12)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f177,f563])).
% 9.74/1.88 thf(f593,plain,(
% 9.74/1.88 ($false = sF12) | ($false = ((exuE3e => $true)))),
% 9.74/1.88 inference(superposition,[],[f570,f148])).
% 9.74/1.88 thf(f596,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF12)),
% 9.74/1.88 inference(boolean_simplification,[],[f593])).
% 9.74/1.88 thf(f597,plain,(
% 9.74/1.88 ($false = sF12)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f596])).
% 9.74/1.88 thf(f601,plain,(
% 9.74/1.88 (((setext => sF11)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f175,f597])).
% 9.74/1.88 thf(f610,plain,(
% 9.74/1.88 ($false = sF11)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f601])).
% 9.74/1.88 thf(f620,plain,(
% 9.74/1.88 ($false = ((emptyI => sF10)))),
% 9.74/1.88 inference(backward_demodulation,[],[f173,f610])).
% 9.74/1.88 thf(f627,plain,(
% 9.74/1.88 ($false = sF10)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f620])).
% 9.74/1.88 thf(f628,plain,(
% 9.74/1.88 (emptyI = $true)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f620])).
% 9.74/1.88 thf(f637,plain,(
% 9.74/1.88 ($false = ((noeltsimpempty => sF9)))),
% 9.74/1.88 inference(backward_demodulation,[],[f172,f627])).
% 9.74/1.88 thf(f641,plain,(
% 9.74/1.88 ($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: (~ (in @ Y1 @ Y0)))) => (emptyset = Y0))))))),
% 9.74/1.88 inference(backward_demodulation,[],[f140,f628])).
% 9.74/1.88 thf(f646,plain,(
% 9.74/1.88 (noeltsimpempty = $true)),
% 9.74/1.88 inference(backward_demodulation,[],[f128,f641])).
% 9.74/1.88 thf(f647,plain,(
% 9.74/1.88 ($false = (($true => sF9)))),
% 9.74/1.88 inference(backward_demodulation,[],[f637,f646])).
% 9.74/1.88 thf(f648,plain,(
% 9.74/1.88 (sF9 = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f647])).
% 9.74/1.88 thf(f649,plain,(
% 9.74/1.88 ($false = ((setbeta => sF8)))),
% 9.74/1.88 inference(backward_demodulation,[],[f170,f648])).
% 9.74/1.88 thf(f653,plain,(
% 9.74/1.88 (setbeta = $true)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f649])).
% 9.74/1.88 thf(f654,plain,(
% 9.74/1.88 ($false = sF8) | ($false = ((setbeta => $true)))),
% 9.74/1.88 inference(superposition,[],[f649,f148])).
% 9.74/1.88 thf(f657,plain,(
% 9.74/1.88 ($false = sF8) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f654])).
% 9.74/1.88 thf(f658,plain,(
% 9.74/1.88 ($false = sF8)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f657])).
% 9.74/1.88 thf(f662,plain,(
% 9.74/1.88 ($false = ((nonemptyE1 => sF7)))),
% 9.74/1.88 inference(backward_demodulation,[],[f169,f658])).
% 9.74/1.88 thf(f664,plain,(
% 9.74/1.88 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) = (Y2 @ Y1)))))))))))),
% 9.74/1.88 inference(backward_demodulation,[],[f219,f653])).
% 9.74/1.88 thf(f669,plain,(
% 9.74/1.88 ($false = sF7)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f662])).
% 9.74/1.88 thf(f679,plain,(
% 9.74/1.88 ($false = ((nonemptyI => sF6)))),
% 9.74/1.88 inference(backward_demodulation,[],[f167,f669])).
% 9.74/1.88 thf(f690,plain,(
% 9.74/1.88 (sF6 = $false) | ($false = ((nonemptyI => $true)))),
% 9.74/1.88 inference(superposition,[],[f679,f148])).
% 9.74/1.88 thf(f693,plain,(
% 9.74/1.88 ($true = $false) | (sF6 = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f690])).
% 9.74/1.88 thf(f694,plain,(
% 9.74/1.88 (sF6 = $false)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f693])).
% 9.74/1.88 thf(f700,plain,(
% 9.74/1.88 (((nonemptyI1 => sF5)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f166,f694])).
% 9.74/1.88 thf(f705,plain,(
% 9.74/1.88 ($false = sF5) | ($false = ((nonemptyI1 => $true)))),
% 9.74/1.88 inference(superposition,[],[f700,f148])).
% 9.74/1.88 thf(f709,plain,(
% 9.74/1.88 ($false = sF5) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f705])).
% 9.74/1.88 thf(f710,plain,(
% 9.74/1.88 ($false = sF5)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f709])).
% 9.74/1.88 thf(f713,plain,(
% 9.74/1.88 (((setadjoinIL => sF4)) = $false)),
% 9.74/1.88 inference(backward_demodulation,[],[f164,f710])).
% 9.74/1.88 thf(f718,plain,(
% 9.74/1.88 ($false = sF4)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f713])).
% 9.74/1.88 thf(f728,plain,(
% 9.74/1.88 ($false = ((emptyinunitempty => sF3)))),
% 9.74/1.88 inference(backward_demodulation,[],[f162,f718])).
% 9.74/1.88 thf(f733,plain,(
% 9.74/1.88 ($false = sF3)),
% 9.74/1.88 inference(imp_proxy_clausification,[],[f728])).
% 9.74/1.88 thf(f743,plain,(
% 9.74/1.88 ($false = ((setadjoinIR => sF2)))),
% 9.74/1.88 inference(backward_demodulation,[],[f160,f733])).
% 9.74/1.88 thf(f752,plain,(
% 9.74/1.88 ($false = ((setadjoinIR => $true))) | ($false = sF2)),
% 9.74/1.88 inference(superposition,[],[f743,f148])).
% 9.74/1.88 thf(f756,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF2)),
% 9.74/1.88 inference(boolean_simplification,[],[f752])).
% 9.74/1.88 thf(f757,plain,(
% 9.74/1.88 ($false = sF2)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f756])).
% 9.74/1.88 thf(f764,plain,(
% 9.74/1.88 ($false = ((setadjoinE => sF1)))),
% 9.74/1.88 inference(backward_demodulation,[],[f159,f757])).
% 9.74/1.88 thf(f769,plain,(
% 9.74/1.88 (sF1 = $false) | ($false = ((setadjoinE => $true)))),
% 9.74/1.88 inference(superposition,[],[f764,f148])).
% 9.74/1.88 thf(f774,plain,(
% 9.74/1.88 (sF1 = $false) | ($true = $false)),
% 9.74/1.88 inference(boolean_simplification,[],[f769])).
% 9.74/1.88 thf(f775,plain,(
% 9.74/1.88 (sF1 = $false)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f774])).
% 9.74/1.88 thf(f777,plain,(
% 9.74/1.88 ($false = ((setadjoinOr => sF0)))),
% 9.74/1.88 inference(backward_demodulation,[],[f158,f775])).
% 9.74/1.88 thf(f786,plain,(
% 9.74/1.88 ($false = ((setadjoinOr => $true))) | ($false = sF0)),
% 9.74/1.88 inference(superposition,[],[f777,f148])).
% 9.74/1.88 thf(f789,plain,(
% 9.74/1.88 ($true = $false) | ($false = sF0)),
% 9.74/1.88 inference(boolean_simplification,[],[f786])).
% 9.74/1.88 thf(f790,plain,(
% 9.74/1.88 ($false = sF0)),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f789])).
% 9.74/1.88 thf(f794,plain,(
% 9.74/1.88 ($false = ((!! @ $i @ (^[Y0 : $i]: (Y0 = (dsetconstr @ Y0 @ (^[Y1 : $i]: ($true))))))))),
% 9.74/1.88 inference(backward_demodulation,[],[f157,f790])).
% 9.74/1.88 thf(f809,plain,(
% 9.74/1.88 ($false = (((^[Y0 : $i]: (Y0 = (dsetconstr @ Y0 @ (^[Y1 : $i]: ($true))))) @ sK35)))),
% 9.74/1.88 inference(sigma_proxy_clausification,[],[f794])).
% 9.74/1.88 thf(f812,plain,(
% 9.74/1.88 (((sK35 = (dsetconstr @ sK35 @ (^[Y0 : $i]: ($true))))) = $false)),
% 9.74/1.88 inference(beta-eta_normalization,[],[f809])).
% 9.74/1.88 thf(f903,plain,(
% 9.74/1.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) = (in @ Y2 @ Y1)))) => (Y1 = Y0))))) @ X1)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f251])).
% 9.74/1.88 thf(f904,plain,(
% 9.74/1.88 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) = (in @ Y1 @ Y0)))) => (Y0 = X1))))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f903])).
% 9.74/1.88 thf(f905,plain,(
% 9.74/1.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) = (in @ Y1 @ Y0)))) => (Y0 = X1))) @ X2)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f904])).
% 9.74/1.88 thf(f906,plain,(
% 9.74/1.88 ( ! [X2 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) = (in @ Y0 @ X2)))) => (X2 = X1))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f905])).
% 9.74/1.88 thf(f910,plain,(
% 9.74/1.88 ($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK35 @ (^[Y1 : $i]: ($true)))) = (in @ Y0 @ sK35)))) => $false)))),
% 9.74/1.88 inference(superposition,[],[f906,f812])).
% 9.74/1.88 thf(f913,plain,(
% 9.74/1.88 ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK35 @ (^[Y1 : $i]: ($true)))) = (in @ Y0 @ sK35)))))))),
% 9.74/1.88 inference(boolean_simplification,[],[f910])).
% 9.74/1.88 thf(f916,plain,(
% 9.74/1.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ Y1)) => (in @ Y2 @ Y0))))))) @ X1)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f509])).
% 9.74/1.88 thf(f917,plain,(
% 9.74/1.88 ( ! [X1 : $i] : (($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X1 @ Y0)) => (in @ Y1 @ X1))))))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f916])).
% 9.74/1.88 thf(f918,plain,(
% 9.74/1.88 ( ! [X2 : ($i > $o),X1 : $i] : (($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X1 @ Y0)) => (in @ Y1 @ X1))))) @ X2)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f917])).
% 9.74/1.88 thf(f919,plain,(
% 9.74/1.88 ( ! [X2 : ($i > $o),X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X1 @ X2)) => (in @ Y0 @ X1))))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f918])).
% 9.74/1.88 thf(f920,plain,(
% 9.74/1.88 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X1 @ X2)) => (in @ Y0 @ X1))) @ X3)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f919])).
% 9.74/1.88 thf(f921,plain,(
% 9.74/1.88 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : (($true = (((in @ X3 @ (dsetconstr @ X1 @ X2)) => (in @ X3 @ X1))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f920])).
% 9.74/1.88 thf(f926,plain,(
% 9.74/1.88 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($true = (($true => (in @ X0 @ X1)))) | ($false = ((in @ X0 @ (dsetconstr @ X1 @ X2))))) )),
% 9.74/1.88 inference(superposition,[],[f921,f148])).
% 9.74/1.88 thf(f927,plain,(
% 9.74/1.88 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($false = ((in @ X0 @ (dsetconstr @ X1 @ X2)))) | ($true = ((in @ X0 @ X1)))) )),
% 9.74/1.88 inference(boolean_simplification,[],[f926])).
% 9.74/1.88 thf(f1034,plain,(
% 9.74/1.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) = (Y2 @ Y1)))))))) @ X1)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f664])).
% 9.74/1.88 thf(f1035,plain,(
% 9.74/1.88 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ Y0 @ X1) => ((in @ Y0 @ (dsetconstr @ X1 @ Y1)) = (Y1 @ Y0)))))))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f1034])).
% 9.74/1.88 thf(f1036,plain,(
% 9.74/1.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ Y0 @ X1) => ((in @ Y0 @ (dsetconstr @ X1 @ Y1)) = (Y1 @ Y0)))))) @ X2)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f1035])).
% 9.74/1.88 thf(f1037,plain,(
% 9.74/1.88 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((in @ X2 @ X1) => ((in @ X2 @ (dsetconstr @ X1 @ Y0)) = (Y0 @ X2)))))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f1036])).
% 9.74/1.88 thf(f1038,plain,(
% 9.74/1.88 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (($true = (((^[Y0 : $i > $o]: ((in @ X2 @ X1) => ((in @ X2 @ (dsetconstr @ X1 @ Y0)) = (Y0 @ X2)))) @ X3)))) )),
% 9.74/1.88 inference(pi_proxy_clausification,[],[f1037])).
% 9.74/1.88 thf(f1039,plain,(
% 9.74/1.88 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (($true = (((in @ X2 @ X1) => ((in @ X2 @ (dsetconstr @ X1 @ X3)) = (X3 @ X2)))))) )),
% 9.74/1.88 inference(beta-eta_normalization,[],[f1038])).
% 9.74/1.88 thf(f1637,plain,(
% 9.74/1.88 ($true = ((~ $true))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK35 @ (^[Y1 : $i]: ($true)))) = (in @ Y0 @ sK35))))))),
% 9.74/1.88 inference(superposition,[],[f913,f148])).
% 9.74/1.88 thf(f1638,plain,(
% 9.74/1.88 ($true = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK35 @ (^[Y1 : $i]: ($true)))) = (in @ Y0 @ sK35))))))),
% 9.74/1.88 inference(boolean_simplification,[],[f1637])).
% 9.74/1.88 thf(f1639,plain,(
% 9.74/1.88 ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK35 @ (^[Y1 : $i]: ($true)))) = (in @ Y0 @ sK35))))))),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f1638])).
% 9.74/1.88 thf(f3954,plain,(
% 9.74/1.88 ($false = (((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ sK35 @ (^[Y1 : $i]: ($true)))) = (in @ Y0 @ sK35))) @ sK37)))),
% 9.74/1.88 inference(sigma_proxy_clausification,[],[f1639])).
% 9.74/1.88 thf(f3957,plain,(
% 9.74/1.88 ($false = (((in @ sK37 @ (dsetconstr @ sK35 @ (^[Y0 : $i]: ($true)))) = (in @ sK37 @ sK35))))),
% 9.74/1.88 inference(beta-eta_normalization,[],[f3954])).
% 9.74/1.88 thf(f3958,plain,(
% 9.74/1.88 (((in @ sK37 @ (dsetconstr @ sK35 @ (^[Y0 : $i]: ($true))))) != ((in @ sK37 @ sK35)))),
% 9.74/1.88 inference(iff_proxy_clausification,[],[f3957])).
% 9.74/1.88 thf(f3959,plain,(
% 9.74/1.88 ($true = ((in @ sK37 @ (dsetconstr @ sK35 @ (^[Y0 : $i]: ($true)))))) | ($true = ((in @ sK37 @ sK35)))),
% 9.74/1.88 inference(xor_proxy_clausification,[],[f3958])).
% 9.74/1.88 thf(f3962,plain,(
% 9.74/1.88 ($false = ((in @ sK37 @ (dsetconstr @ sK35 @ (^[Y0 : $i]: ($true)))))) | ($true != ((in @ sK37 @ sK35)))),
% 9.74/1.88 inference(superposition,[],[f3958,f148])).
% 9.74/1.88 thf(f3964,plain,(
% 9.74/1.88 ($false = ((in @ sK37 @ (dsetconstr @ sK35 @ (^[Y0 : $i]: ($true))))))),
% 9.74/1.88 inference(forward_subsumption_resolution,[],[f3962,f927])).
% 9.74/1.88 thf(f3965,plain,(
% 9.74/1.88 ($true = $false) | ($true = ((in @ sK37 @ sK35)))),
% 9.74/1.88 inference(backward_demodulation,[],[f3959,f3964])).
% 9.74/1.88 thf(f3967,plain,(
% 9.74/1.88 ($true = ((in @ sK37 @ sK35)))),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f3965])).
% 9.74/1.88 thf(f3995,plain,(
% 9.74/1.88 ( ! [X0 : ($i > $o)] : (($true = (($true => ((in @ sK37 @ (dsetconstr @ sK35 @ X0)) = (X0 @ sK37)))))) )),
% 9.74/1.88 inference(superposition,[],[f1039,f3967])).
% 9.74/1.88 thf(f4026,plain,(
% 9.74/1.88 ( ! [X0 : ($i > $o)] : (($true = (((in @ sK37 @ (dsetconstr @ sK35 @ X0)) = (X0 @ sK37))))) )),
% 9.74/1.88 inference(boolean_simplification,[],[f3995])).
% 9.74/1.88 thf(f4027,plain,(
% 9.74/1.88 ( ! [X0 : ($i > $o)] : ((((X0 @ sK37)) = ((in @ sK37 @ (dsetconstr @ sK35 @ X0))))) )),
% 9.74/1.88 inference(iff_proxy_clausification,[],[f4026])).
% 9.74/1.88 thf(f4033,plain,(
% 9.74/1.88 ($false = (((^[Y0 : $i]: ($true)) @ sK37)))),
% 9.74/1.88 inference(backward_demodulation,[],[f3964,f4027])).
% 9.74/1.88 thf(f4036,plain,(
% 9.74/1.88 ($true = $false)),
% 9.74/1.88 inference(beta-eta_normalization,[],[f4033])).
% 9.74/1.88 thf(f4037,plain,(
% 9.74/1.88 $false),
% 9.74/1.88 inference(trivial_inequality_removal,[],[f4036])).
% 9.74/1.88 % SZS output end Proof for theBenchmark
% 9.74/1.88 % (1271693)------------------------------
% 9.74/1.88 % (1271693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.74/1.88 % (1271693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.74/1.88 % (1271693)CaDiCaL version: 2.1.3
% 9.74/1.88 % (1271693)Termination reason: Refutation
% 9.74/1.88 % (1271693)Time elapsed: 0.243 s
% 9.74/1.88 % (1271693)Peak memory usage: 16 MB
% 9.74/1.88 % (1271693)Instructions burned: 454 (million)
% 9.74/1.88 % (1271502)Success in time 1.628 s
% 9.74/1.88 % Vampire exiting
%------------------------------------------------------------------------------