%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO332^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:47:27 AM UTC 2026
% Result : Theorem 9.20s 1.73s
% Output : Refutation 9.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO332^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 16:49:48 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.75/0.39 % (3782927)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.75/0.39 % (3782935)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=2463185349: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.39 % (3782933)lrs+10_16_si=on:nwc=1.5:random_seed=336971304:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.75/0.39 % (3782932)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3826495445:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.75/0.39 % (3782937)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1848542521:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.75/0.39 % (3782933)Instruction limit reached!
% 0.75/0.39 % (3782933)------------------------------
% 0.75/0.39 % (3782933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (3782933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (3782933)CaDiCaL version: 2.1.3
% 0.75/0.39 % (3782933)Termination reason: Instruction limit
% 0.75/0.39 % (3782933)Termination phase: Saturation
% 0.75/0.39 % (3782933)Time elapsed: 0.011 s
% 0.75/0.39 % (3782933)Peak memory usage: 12 MB
% 0.75/0.39 % (3782933)Instructions burned: 19 (million)
% 0.75/0.39 % (3782936)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2943559033:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.75/0.39 % (3782938)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.39 % (3782938)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.39 % (3782934)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1904800767:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.75/0.39 % (3782938)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=3567209617:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.75/0.39 % (3782934)Instruction limit reached!
% 0.75/0.39 % (3782934)------------------------------
% 0.75/0.39 % (3782934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (3782934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (3782934)CaDiCaL version: 2.1.3
% 0.75/0.39 % (3782934)Termination reason: Instruction limit
% 0.75/0.39 % (3782934)Termination phase: Saturation
% 0.75/0.39 % (3782934)Time elapsed: 0.006 s
% 0.75/0.39 % (3782934)Peak memory usage: 12 MB
% 0.75/0.39 % (3782934)Instructions burned: 4 (million)
% 0.75/0.39 % (3782938)Refutation not found, incomplete strategy
% 0.75/0.39 % (3782938)------------------------------
% 0.75/0.39 % (3782938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (3782938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (3782938)CaDiCaL version: 2.1.3
% 0.75/0.39 % (3782938)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.39 % (3782938)Time elapsed: 0.007 s
% 0.75/0.39 % (3782938)Peak memory usage: 12 MB
% 0.75/0.39 % (3782938)Instructions burned: 6 (million)
% 0.75/0.39 % (3782938)------------------------------
% 0.75/0.39 % (3782938)------------------------------
% 0.75/0.39 % (3782943)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1348827688:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.39 % (3782943)Instruction limit reached!
% 0.75/0.39 % (3782943)------------------------------
% 0.75/0.39 % (3782943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.39 % (3782943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.39 % (3782943)CaDiCaL version: 2.1.3
% 0.75/0.39 % (3782943)Termination reason: Instruction limit
% 0.75/0.39 % (3782943)Termination phase: Saturation
% 0.75/0.39 % (3782943)Time elapsed: 0.002 s
% 0.75/0.39 % (3782943)Peak memory usage: 12 MB
% 0.75/0.39 % (3782943)Instructions burned: 3 (million)
% 0.75/0.39 % (3782936)Instruction limit reached!
% 0.75/0.39 % (3782936)------------------------------
% 0.75/0.42 % (3782936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (3782936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (3782936)CaDiCaL version: 2.1.3
% 0.75/0.42 % (3782936)Termination reason: Instruction limit
% 0.75/0.42 % (3782936)Termination phase: Saturation
% 0.75/0.42 % (3782936)Time elapsed: 0.024 s
% 0.75/0.42 % (3782936)Peak memory usage: 12 MB
% 0.75/0.42 % (3782936)Instructions burned: 24 (million)
% 0.75/0.42 % (3782949)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.42 % (3782947)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3920439903:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.75/0.42 % (3782937)Instruction limit reached!
% 0.75/0.42 % (3782937)------------------------------
% 0.75/0.42 % (3782937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (3782937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (3782937)CaDiCaL version: 2.1.3
% 0.75/0.42 % (3782937)Termination reason: Instruction limit
% 0.75/0.42 % (3782937)Termination phase: Saturation
% 0.75/0.42 % (3782937)Time elapsed: 0.040 s
% 0.75/0.42 % (3782937)Peak memory usage: 13 MB
% 0.75/0.42 % (3782937)Instructions burned: 76 (million)
% 0.75/0.42 % (3782949)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2936693432: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.42 % (3782950)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2090392528:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.75/0.42 % (3782951)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.42 % (3782951)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.42 % (3782947)Instruction limit reached!
% 0.75/0.42 % (3782947)------------------------------
% 0.75/0.42 % (3782947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (3782947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (3782947)CaDiCaL version: 2.1.3
% 0.75/0.42 % (3782947)Termination reason: Instruction limit
% 0.75/0.42 % (3782947)Termination phase: Saturation
% 0.75/0.42 % (3782947)Time elapsed: 0.009 s
% 0.75/0.42 % (3782947)Peak memory usage: 12 MB
% 0.75/0.42 % (3782947)Instructions burned: 8 (million)
% 0.75/0.42 % (3782949)Instruction limit reached!
% 0.75/0.42 % (3782949)------------------------------
% 0.75/0.42 % (3782949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (3782949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (3782949)CaDiCaL version: 2.1.3
% 0.75/0.42 % (3782949)Termination reason: Instruction limit
% 0.75/0.42 % (3782949)Termination phase: Saturation
% 0.75/0.42 % (3782949)Time elapsed: 0.007 s
% 0.75/0.42 % (3782949)Peak memory usage: 12 MB
% 0.75/0.42 % (3782949)Instructions burned: 13 (million)
% 0.75/0.42 % (3782932)Instruction limit reached!
% 0.75/0.42 % (3782932)------------------------------
% 0.75/0.42 % (3782932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (3782932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (3782932)CaDiCaL version: 2.1.3
% 0.75/0.42 % (3782932)Termination reason: Instruction limit
% 0.75/0.42 % (3782932)Termination phase: Saturation
% 0.75/0.42 % (3782932)Time elapsed: 0.057 s
% 0.75/0.42 % (3782932)Peak memory usage: 12 MB
% 0.75/0.42 % (3782932)Instructions burned: 90 (million)
% 0.75/0.42 % (3782950)Instruction limit reached!
% 0.75/0.42 % (3782950)------------------------------
% 0.75/0.42 % (3782950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.42 % (3782950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.42 % (3782950)CaDiCaL version: 2.1.3
% 0.75/0.42 % (3782950)Termination reason: Instruction limit
% 0.75/0.42 % (3782950)Termination phase: Saturation
% 0.75/0.42 % (3782950)Time elapsed: 0.009 s
% 0.75/0.42 % (3782950)Peak memory usage: 12 MB
% 0.75/0.42 % (3782950)Instructions burned: 13 (million)
% 0.75/0.45 % (3782951)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3447580252: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.45 % (3782953)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=1192858832:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.75/0.45 % (3782957)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.45 % (3782957)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=1668269621:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.75/0.45 % (3782956)lrs+10_1_si=on:cs=on:random_seed=3018913245:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.75/0.45 % (3782957)Instruction limit reached!
% 0.75/0.45 % (3782957)------------------------------
% 0.75/0.45 % (3782957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (3782957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (3782957)CaDiCaL version: 2.1.3
% 0.75/0.45 % (3782957)Termination reason: Instruction limit
% 0.75/0.45 % (3782957)Termination phase: Saturation
% 0.75/0.45 % (3782957)Time elapsed: 0.002 s
% 0.75/0.45 % (3782957)Peak memory usage: 11 MB
% 0.75/0.45 % (3782957)Instructions burned: 3 (million)
% 0.75/0.45 % (3782959)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1028465236:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.75/0.45 % (3782958)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3136921761:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.75/0.45 % (3782956)Instruction limit reached!
% 0.75/0.45 % (3782956)------------------------------
% 0.75/0.45 % (3782956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (3782956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (3782956)CaDiCaL version: 2.1.3
% 0.75/0.45 % (3782956)Termination reason: Instruction limit
% 0.75/0.45 % (3782956)Termination phase: Saturation
% 0.75/0.45 % (3782956)Time elapsed: 0.007 s
% 0.75/0.45 % (3782956)Peak memory usage: 12 MB
% 0.75/0.45 % (3782956)Instructions burned: 8 (million)
% 0.75/0.45 % (3782959)Refutation not found, incomplete strategy
% 0.75/0.45 % (3782959)------------------------------
% 0.75/0.45 % (3782959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (3782959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (3782959)CaDiCaL version: 2.1.3
% 0.75/0.45 % (3782959)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.45 % (3782959)Time elapsed: 0.004 s
% 0.75/0.45 % (3782959)Peak memory usage: 12 MB
% 0.75/0.45 % (3782959)Instructions burned: 6 (million)
% 0.75/0.45 % (3782959)------------------------------
% 0.75/0.45 % (3782959)------------------------------
% 0.75/0.45 % (3782958)Refutation not found, incomplete strategy
% 0.75/0.45 % (3782958)------------------------------
% 0.75/0.45 % (3782958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (3782958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (3782958)CaDiCaL version: 2.1.3
% 0.75/0.45 % (3782958)Termination reason: Refutation not found, incomplete strategy
% 0.75/0.45 % (3782958)Time elapsed: 0.007 s
% 0.75/0.45 % (3782958)Peak memory usage: 12 MB
% 0.75/0.45 % (3782958)Instructions burned: 12 (million)
% 0.75/0.45 % (3782951)Instruction limit reached!
% 0.75/0.45 % (3782951)------------------------------
% 0.75/0.45 % (3782951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.75/0.45 % (3782951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.75/0.45 % (3782951)CaDiCaL version: 2.1.3
% 0.75/0.45 % (3782951)Termination reason: Instruction limit
% 0.75/0.45 % (3782951)Termination phase: Saturation
% 0.75/0.45 % (3782951)Time elapsed: 0.027 s
% 0.75/0.45 % (3782951)Peak memory usage: 12 MB
% 0.75/0.45 % (3782951)Instructions burned: 28 (million)
% 0.75/0.45 % (3782958)------------------------------
% 0.75/0.45 % (3782958)------------------------------
% 0.75/0.45 % (3782969)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3580927242:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.44/0.50 % (3782964)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3870845315:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.44/0.50 % (3782967)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2357766667:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.44/0.50 % (3782953)Instruction limit reached!
% 1.44/0.50 % (3782953)------------------------------
% 1.44/0.50 % (3782953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.50 % (3782953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.50 % (3782953)CaDiCaL version: 2.1.3
% 1.44/0.50 % (3782953)Termination reason: Instruction limit
% 1.44/0.50 % (3782953)Termination phase: Saturation
% 1.44/0.50 % (3782953)Time elapsed: 0.047 s
% 1.44/0.50 % (3782953)Peak memory usage: 12 MB
% 1.44/0.50 % (3782953)Instructions burned: 87 (million)
% 1.44/0.50 % (3782964)Refutation not found, incomplete strategy
% 1.44/0.50 % (3782964)------------------------------
% 1.44/0.50 % (3782964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.50 % (3782964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.50 % (3782964)CaDiCaL version: 2.1.3
% 1.44/0.50 % (3782964)Termination reason: Refutation not found, incomplete strategy
% 1.44/0.50 % (3782964)Time elapsed: 0.007 s
% 1.44/0.50 % (3782964)Peak memory usage: 12 MB
% 1.44/0.50 % (3782964)Instructions burned: 3 (million)
% 1.44/0.50 % (3782964)------------------------------
% 1.44/0.50 % (3782964)------------------------------
% 1.44/0.50 % (3782969)Instruction limit reached!
% 1.44/0.50 % (3782969)------------------------------
% 1.44/0.50 % (3782969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.50 % (3782969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.50 % (3782970)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=980374841: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.44/0.50 % (3782969)CaDiCaL version: 2.1.3
% 1.44/0.50 % (3782969)Termination reason: Instruction limit
% 1.44/0.50 % (3782969)Termination phase: Saturation
% 1.44/0.50 % (3782969)Time elapsed: 0.009 s
% 1.44/0.50 % (3782969)Peak memory usage: 12 MB
% 1.44/0.50 % (3782969)Instructions burned: 15 (million)
% 1.44/0.50 % (3782967)Instruction limit reached!
% 1.44/0.50 % (3782967)------------------------------
% 1.44/0.50 % (3782967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.50 % (3782967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.50 % (3782967)CaDiCaL version: 2.1.3
% 1.44/0.50 % (3782967)Termination reason: Instruction limit
% 1.44/0.50 % (3782967)Termination phase: Saturation
% 1.44/0.50 % (3782967)Time elapsed: 0.009 s
% 1.44/0.50 % (3782967)Peak memory usage: 12 MB
% 1.44/0.50 % (3782967)Instructions burned: 14 (million)
% 1.44/0.50 % (3782968)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1892215486:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.44/0.50 % (3782970)Instruction limit reached!
% 1.44/0.50 % (3782970)------------------------------
% 1.44/0.50 % (3782970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.44/0.50 % (3782970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.44/0.50 % (3782970)CaDiCaL version: 2.1.3
% 1.44/0.50 % (3782970)Termination reason: Instruction limit
% 1.44/0.50 % (3782970)Termination phase: Saturation
% 1.44/0.50 % (3782970)Time elapsed: 0.003 s
% 1.44/0.50 % (3782970)Peak memory usage: 11 MB
% 1.44/0.50 % (3782970)Instructions burned: 2 (million)
% 1.44/0.50 % (3782974)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=704562037:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.44/0.50 % (3782978)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.44/0.50 % (3782978)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.10/0.59 % (3782977)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3846563469:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.10/0.59 % (3782978)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=3098929224:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.10/0.59 % (3782975)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2162636567:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.10/0.59 % (3782974)Refutation not found, incomplete strategy
% 2.10/0.59 % (3782974)------------------------------
% 2.10/0.59 % (3782974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.10/0.59 % (3782974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.10/0.59 % (3782974)CaDiCaL version: 2.1.3
% 2.10/0.59 % (3782974)Termination reason: Refutation not found, incomplete strategy
% 2.10/0.59 % (3782974)Time elapsed: 0.012 s
% 2.10/0.59 % (3782974)Peak memory usage: 12 MB
% 2.10/0.59 % (3782974)Instructions burned: 19 (million)
% 2.10/0.59 % (3782974)------------------------------
% 2.10/0.59 % (3782974)------------------------------
% 2.10/0.59 % (3782978)Instruction limit reached!
% 2.10/0.59 % (3782978)------------------------------
% 2.10/0.59 % (3782978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.10/0.59 % (3782978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.10/0.59 % (3782978)CaDiCaL version: 2.1.3
% 2.10/0.59 % (3782978)Termination reason: Instruction limit
% 2.10/0.59 % (3782978)Termination phase: Saturation
% 2.10/0.59 % (3782978)Time elapsed: 0.010 s
% 2.10/0.59 % (3782978)Peak memory usage: 12 MB
% 2.10/0.59 % (3782978)Instructions burned: 15 (million)
% 2.10/0.59 % (3782980)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.10/0.59 % (3782980)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=3341658977:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.10/0.59 % (3782985)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=2520460468:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.10/0.59 % (3782975)Instruction limit reached!
% 2.10/0.59 % (3782975)------------------------------
% 2.10/0.59 % (3782975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.10/0.59 % (3782975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.10/0.59 % (3782975)CaDiCaL version: 2.1.3
% 2.10/0.59 % (3782975)Termination reason: Instruction limit
% 2.10/0.59 % (3782975)Termination phase: Saturation
% 2.10/0.59 % (3782975)Time elapsed: 0.023 s
% 2.10/0.59 % (3782975)Peak memory usage: 12 MB
% 2.10/0.59 % (3782975)Instructions burned: 25 (million)
% 2.10/0.59 % (3782980)Instruction limit reached!
% 2.10/0.59 % (3782980)------------------------------
% 2.10/0.59 % (3782980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.10/0.59 % (3782986)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2112864464:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.10/0.59 % (3782980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.10/0.59 % (3782980)CaDiCaL version: 2.1.3
% 2.10/0.59 % (3782980)Termination reason: Instruction limit
% 2.10/0.59 % (3782980)Termination phase: Saturation
% 2.10/0.59 % (3782980)Time elapsed: 0.011 s
% 2.10/0.59 % (3782980)Peak memory usage: 12 MB
% 2.10/0.59 % (3782980)Instructions burned: 8 (million)
% 2.10/0.59 % (3782935)Instruction limit reached!
% 2.10/0.59 % (3782935)------------------------------
% 2.10/0.59 % (3782935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.10/0.59 % (3782935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.10/0.59 % (3782935)CaDiCaL version: 2.1.3
% 2.10/0.59 % (3782935)Termination reason: Instruction limit
% 2.10/0.59 % (3782935)Termination phase: Saturation
% 2.10/0.59 % (3782935)Time elapsed: 0.181 s
% 2.10/0.59 % (3782935)Peak memory usage: 14 MB
% 2.10/0.59 % (3782935)Instructions burned: 636 (million)
% 2.10/0.59 % (3782986)Instruction limit reached!
% 2.10/0.59 % (3782986)------------------------------
% 2.45/0.65 % (3782986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.45/0.65 % (3782986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.45/0.65 % (3782986)CaDiCaL version: 2.1.3
% 2.45/0.65 % (3782986)Termination reason: Instruction limit
% 2.45/0.65 % (3782986)Termination phase: Saturation
% 2.45/0.65 % (3782986)Time elapsed: 0.005 s
% 2.45/0.65 % (3782986)Peak memory usage: 12 MB
% 2.45/0.65 % (3782986)Instructions burned: 8 (million)
% 2.45/0.65 % (3782977)Instruction limit reached!
% 2.45/0.65 % (3782977)------------------------------
% 2.45/0.65 % (3782977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.45/0.65 % (3782977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.45/0.65 % (3782977)CaDiCaL version: 2.1.3
% 2.45/0.65 % (3782977)Termination reason: Instruction limit
% 2.45/0.65 % (3782977)Termination phase: Saturation
% 2.45/0.65 % (3782977)Time elapsed: 0.034 s
% 2.45/0.65 % (3782977)Peak memory usage: 12 MB
% 2.45/0.65 % (3782977)Instructions burned: 60 (million)
% 2.45/0.65 % (3782992)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1473137626:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.45/0.65 % (3782990)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3441283408:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.45/0.65 % (3782985)Instruction limit reached!
% 2.45/0.65 % (3782985)------------------------------
% 2.45/0.65 % (3782985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.45/0.65 % (3782985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.45/0.65 % (3782985)CaDiCaL version: 2.1.3
% 2.45/0.65 % (3782985)Termination reason: Instruction limit
% 2.45/0.65 % (3782985)Termination phase: Saturation
% 2.45/0.65 % (3782985)Time elapsed: 0.023 s
% 2.45/0.65 % (3782985)Peak memory usage: 12 MB
% 2.45/0.65 % (3782985)Instructions burned: 32 (million)
% 2.45/0.65 % (3782994)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=733197607:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.45/0.65 % (3782991)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3476133554:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.45/0.65 % (3782990)Instruction limit reached!
% 2.45/0.65 % (3782990)------------------------------
% 2.45/0.65 % (3782990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.45/0.65 % (3782990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.45/0.65 % (3782990)CaDiCaL version: 2.1.3
% 2.45/0.65 % (3782990)Termination reason: Instruction limit
% 2.45/0.65 % (3782990)Termination phase: Saturation
% 2.45/0.65 % (3782990)Time elapsed: 0.010 s
% 2.45/0.65 % (3782990)Peak memory usage: 11 MB
% 2.45/0.65 % (3782990)Instructions burned: 23 (million)
% 2.45/0.65 % (3782993)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2658185500:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.45/0.65 % (3782991)Instruction limit reached!
% 2.45/0.65 % (3782991)------------------------------
% 2.45/0.65 % (3782991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.45/0.65 % (3782991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.45/0.65 % (3782991)CaDiCaL version: 2.1.3
% 2.45/0.65 % (3782991)Termination reason: Instruction limit
% 2.45/0.65 % (3782991)Termination phase: Saturation
% 2.45/0.65 % (3782991)Time elapsed: 0.013 s
% 2.45/0.65 % (3782991)Peak memory usage: 12 MB
% 2.45/0.65 % (3782991)Instructions burned: 22 (million)
% 2.45/0.65 % (3783001)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.45/0.65 % (3783001)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=787204075:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.45/0.65 % (3782997)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2834761868:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.45/0.65 % (3783001)Instruction limit reached!
% 2.45/0.65 % (3783001)------------------------------
% 2.45/0.65 % (3783001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.45/0.65 % (3783001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.74 % (3783001)CaDiCaL version: 2.1.3
% 2.70/0.74 % (3783001)Termination reason: Instruction limit
% 2.70/0.74 % (3783001)Termination phase: Saturation
% 2.70/0.74 % (3783001)Time elapsed: 0.004 s
% 2.70/0.74 % (3783001)Peak memory usage: 12 MB
% 2.70/0.74 % (3783001)Instructions burned: 8 (million)
% 2.70/0.74 % (3783002)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=4164204417:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.70/0.74 % (3783005)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=2164351678: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.70/0.74 % (3782997)Instruction limit reached!
% 2.70/0.74 % (3782997)------------------------------
% 2.70/0.74 % (3782997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.74 % (3782997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.74 % (3782997)CaDiCaL version: 2.1.3
% 2.70/0.74 % (3782997)Termination reason: Instruction limit
% 2.70/0.74 % (3782997)Termination phase: Saturation
% 2.70/0.74 % (3782997)Time elapsed: 0.023 s
% 2.70/0.74 % (3782997)Peak memory usage: 12 MB
% 2.70/0.74 % (3782997)Instructions burned: 42 (million)
% 2.70/0.74 % (3783008)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.70/0.74 % (3783008)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=4155497523: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.70/0.74 % (3783008)Instruction limit reached!
% 2.70/0.74 % (3783008)------------------------------
% 2.70/0.74 % (3783008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.74 % (3783008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.74 % (3783008)CaDiCaL version: 2.1.3
% 2.70/0.74 % (3783008)Termination reason: Instruction limit
% 2.70/0.74 % (3783008)Termination phase: Saturation
% 2.70/0.74 % (3783008)Time elapsed: 0.004 s
% 2.70/0.74 % (3783008)Peak memory usage: 12 MB
% 2.70/0.74 % (3783008)Instructions burned: 6 (million)
% 2.70/0.74 % (3782993)Instruction limit reached!
% 2.70/0.74 % (3782993)------------------------------
% 2.70/0.74 % (3782993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.74 % (3782993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.74 % (3782993)CaDiCaL version: 2.1.3
% 2.70/0.74 % (3782993)Termination reason: Instruction limit
% 2.70/0.74 % (3782993)Termination phase: Saturation
% 2.70/0.74 % (3782993)Time elapsed: 0.080 s
% 2.70/0.74 % (3782993)Peak memory usage: 13 MB
% 2.70/0.74 % (3782993)Instructions burned: 143 (million)
% 2.70/0.74 % (3782968)Instruction limit reached!
% 2.70/0.74 % (3782968)------------------------------
% 2.70/0.74 % (3782968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.74 % (3782968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.74 % (3782968)CaDiCaL version: 2.1.3
% 2.70/0.74 % (3782968)Termination reason: Instruction limit
% 2.70/0.74 % (3782968)Termination phase: Saturation
% 2.70/0.74 % (3782968)Time elapsed: 0.163 s
% 2.70/0.74 % (3782968)Peak memory usage: 13 MB
% 2.70/0.74 % (3782968)Instructions burned: 327 (million)
% 2.70/0.74 % (3783010)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3964642017:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.70/0.74 % (3783012)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=2893839503:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.70/0.74 % (3782994)Instruction limit reached!
% 2.70/0.74 % (3782994)------------------------------
% 2.70/0.74 % (3782994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.70/0.74 % (3782994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.70/0.74 % (3782994)CaDiCaL version: 2.1.3
% 2.70/0.74 % (3782994)Termination reason: Instruction limit
% 2.70/0.74 % (3782994)Termination phase: Saturation
% 2.70/0.74 % (3782994)Time elapsed: 0.115 s
% 2.70/0.74 % (3782994)Peak memory usage: 13 MB
% 2.70/0.74 % (3782994)Instructions burned: 195 (million)
% 3.34/0.80 % (3783011)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2864036431:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 3.34/0.80 % (3783010)Instruction limit reached!
% 3.34/0.80 % (3783010)------------------------------
% 3.34/0.80 % (3783010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.80 % (3783010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.80 % (3783010)CaDiCaL version: 2.1.3
% 3.34/0.80 % (3783010)Termination reason: Instruction limit
% 3.34/0.80 % (3783010)Termination phase: Saturation
% 3.34/0.80 % (3783010)Time elapsed: 0.023 s
% 3.34/0.80 % (3783010)Peak memory usage: 12 MB
% 3.34/0.80 % (3783010)Instructions burned: 23 (million)
% 3.34/0.80 % (3783015)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=629429475:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.34/0.80 % (3783011)Instruction limit reached!
% 3.34/0.81 % (3783011)------------------------------
% 3.34/0.81 % (3783011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.81 % (3783011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.81 % (3783011)CaDiCaL version: 2.1.3
% 3.34/0.81 % (3783011)Termination reason: Instruction limit
% 3.34/0.81 % (3783011)Termination phase: Saturation
% 3.34/0.81 % (3783011)Time elapsed: 0.012 s
% 3.34/0.81 % (3783011)Peak memory usage: 13 MB
% 3.34/0.81 % (3783011)Instructions burned: 20 (million)
% 3.34/0.81 % (3783017)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=1345054379:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.34/0.81 % (3783005)Instruction limit reached!
% 3.34/0.81 % (3783005)------------------------------
% 3.34/0.81 % (3783005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.81 % (3783005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.81 % (3783005)CaDiCaL version: 2.1.3
% 3.34/0.81 % (3783005)Termination reason: Instruction limit
% 3.34/0.81 % (3783005)Termination phase: Saturation
% 3.34/0.81 % (3783005)Time elapsed: 0.101 s
% 3.34/0.81 % (3783005)Peak memory usage: 13 MB
% 3.34/0.81 % (3783005)Instructions burned: 170 (million)
% 3.34/0.81 % (3783019)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2582686918:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.34/0.81 % (3783019)Refutation not found, incomplete strategy
% 3.34/0.81 % (3783019)------------------------------
% 3.34/0.81 % (3783019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.81 % (3783019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.81 % (3783019)CaDiCaL version: 2.1.3
% 3.34/0.81 % (3783019)Termination reason: Refutation not found, incomplete strategy
% 3.34/0.81 % (3783019)Time elapsed: 0.002 s
% 3.34/0.81 % (3783019)Peak memory usage: 12 MB
% 3.34/0.81 % (3783019)Instructions burned: 2 (million)
% 3.34/0.81 % (3783019)------------------------------
% 3.34/0.81 % (3783019)------------------------------
% 3.34/0.81 % (3783021)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2361323804: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.34/0.81 % (3783023)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.34/0.81 % (3783023)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1735220756:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.34/0.81 % (3783021)Instruction limit reached!
% 3.34/0.81 % (3783021)------------------------------
% 3.34/0.81 % (3783021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.34/0.81 % (3783021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.34/0.81 % (3783021)CaDiCaL version: 2.1.3
% 3.34/0.81 % (3783021)Termination reason: Instruction limit
% 3.34/0.81 % (3783021)Termination phase: Saturation
% 3.34/0.81 % (3783021)Time elapsed: 0.012 s
% 3.34/0.81 % (3783021)Peak memory usage: 12 MB
% 3.76/0.91 % (3783021)Instructions burned: 21 (million)
% 3.76/0.91 % (3783017)Instruction limit reached!
% 3.76/0.91 % (3783017)------------------------------
% 3.76/0.91 % (3783017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.91 % (3783017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.91 % (3783017)CaDiCaL version: 2.1.3
% 3.76/0.91 % (3783017)Termination reason: Instruction limit
% 3.76/0.91 % (3783017)Termination phase: Saturation
% 3.76/0.91 % (3783017)Time elapsed: 0.042 s
% 3.76/0.91 % (3783017)Peak memory usage: 12 MB
% 3.76/0.91 % (3783017)Instructions burned: 46 (million)
% 3.76/0.91 % (3783002)Instruction limit reached!
% 3.76/0.91 % (3783002)------------------------------
% 3.76/0.91 % (3783002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.91 % (3783002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.91 % (3783002)CaDiCaL version: 2.1.3
% 3.76/0.91 % (3783002)Termination reason: Instruction limit
% 3.76/0.91 % (3783002)Termination phase: Saturation
% 3.76/0.91 % (3783002)Time elapsed: 0.155 s
% 3.76/0.91 % (3783002)Peak memory usage: 14 MB
% 3.76/0.91 % (3783002)Instructions burned: 181 (million)
% 3.76/0.91 % (3783026)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2829189354:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.76/0.91 % (3783027)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=548184344:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 3.76/0.91 % (3783026)Instruction limit reached!
% 3.76/0.91 % (3783026)------------------------------
% 3.76/0.91 % (3783026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.91 % (3783026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.91 % (3783026)CaDiCaL version: 2.1.3
% 3.76/0.91 % (3783026)Termination reason: Instruction limit
% 3.76/0.91 % (3783026)Termination phase: Saturation
% 3.76/0.91 % (3783026)Time elapsed: 0.009 s
% 3.76/0.91 % (3783026)Peak memory usage: 12 MB
% 3.76/0.91 % (3783026)Instructions burned: 14 (million)
% 3.76/0.91 % (3783028)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=1939060062:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 3.76/0.91 % (3783031)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3084020405:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.76/0.91 % (3783031)Refutation not found, incomplete strategy
% 3.76/0.91 % (3783031)------------------------------
% 3.76/0.91 % (3783031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.91 % (3783031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.91 % (3783031)CaDiCaL version: 2.1.3
% 3.76/0.91 % (3783031)Termination reason: Refutation not found, incomplete strategy
% 3.76/0.91 % (3783031)Time elapsed: 0.008 s
% 3.76/0.91 % (3783031)Peak memory usage: 12 MB
% 3.76/0.91 % (3783031)Instructions burned: 16 (million)
% 3.76/0.91 % (3783031)------------------------------
% 3.76/0.91 % (3783031)------------------------------
% 3.76/0.91 % (3783027)Instruction limit reached!
% 3.76/0.91 % (3783027)------------------------------
% 3.76/0.91 % (3783027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.91 % (3783027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/0.91 % (3783027)CaDiCaL version: 2.1.3
% 3.76/0.91 % (3783027)Termination reason: Instruction limit
% 3.76/0.91 % (3783027)Termination phase: Saturation
% 3.76/0.91 % (3783027)Time elapsed: 0.038 s
% 3.76/0.91 % (3783027)Peak memory usage: 13 MB
% 3.76/0.91 % (3783027)Instructions burned: 66 (million)
% 3.76/0.91 % (3783034)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2054936967:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.76/0.91 % (3783035)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=2626989144:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.76/0.91 % (3783028)Instruction limit reached!
% 3.76/0.91 % (3783028)------------------------------
% 3.76/0.91 % (3783028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/0.91 % (3783028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.00 % (3783028)CaDiCaL version: 2.1.3
% 3.76/1.00 % (3783028)Termination reason: Instruction limit
% 3.76/1.00 % (3783028)Termination phase: Saturation
% 3.76/1.00 % (3783028)Time elapsed: 0.046 s
% 3.76/1.00 % (3783028)Peak memory usage: 12 MB
% 3.76/1.00 % (3783028)Instructions burned: 52 (million)
% 3.76/1.00 % (3783034)Refutation not found, incomplete strategy
% 3.76/1.00 % (3783034)------------------------------
% 3.76/1.00 % (3783034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/1.00 % (3783034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.00 % (3783034)CaDiCaL version: 2.1.3
% 3.76/1.00 % (3783034)Termination reason: Refutation not found, incomplete strategy
% 3.76/1.00 % (3783034)Time elapsed: 0.010 s
% 3.76/1.00 % (3783034)Peak memory usage: 12 MB
% 3.76/1.00 % (3783034)Instructions burned: 15 (million)
% 3.76/1.00 % (3783034)------------------------------
% 3.76/1.00 % (3783034)------------------------------
% 3.76/1.00 % (3783012)Instruction limit reached!
% 3.76/1.00 % (3783012)------------------------------
% 3.76/1.00 % (3783012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/1.00 % (3783012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.00 % (3783012)CaDiCaL version: 2.1.3
% 3.76/1.00 % (3783012)Termination reason: Instruction limit
% 3.76/1.00 % (3783012)Termination phase: Saturation
% 3.76/1.00 % (3783012)Time elapsed: 0.162 s
% 3.76/1.00 % (3783012)Peak memory usage: 13 MB
% 3.76/1.00 % (3783012)Instructions burned: 316 (million)
% 3.76/1.00 % (3783023)Instruction limit reached!
% 3.76/1.00 % (3783023)------------------------------
% 3.76/1.00 % (3783023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/1.00 % (3783023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.00 % (3783023)CaDiCaL version: 2.1.3
% 3.76/1.00 % (3783023)Termination reason: Instruction limit
% 3.76/1.00 % (3783023)Termination phase: Saturation
% 3.76/1.00 % (3783023)Time elapsed: 0.098 s
% 3.76/1.00 % (3783023)Peak memory usage: 13 MB
% 3.76/1.00 % (3783023)Instructions burned: 202 (million)
% 3.76/1.00 % (3783035)Instruction limit reached!
% 3.76/1.00 % (3783035)------------------------------
% 3.76/1.00 % (3783035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/1.00 % (3783035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.00 % (3783035)CaDiCaL version: 2.1.3
% 3.76/1.00 % (3783035)Termination reason: Instruction limit
% 3.76/1.00 % (3783035)Termination phase: Saturation
% 3.76/1.00 % (3783035)Time elapsed: 0.017 s
% 3.76/1.00 % (3783035)Peak memory usage: 12 MB
% 3.76/1.00 % (3783035)Instructions burned: 35 (million)
% 3.76/1.00 % (3783039)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.76/1.00 % (3783038)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1796209730:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2994 on theBenchmark for (2994ds/67Mi)
% 3.76/1.00 % (3783039)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=768139435:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 3.76/1.00 % (3783040)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2518547710:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 3.76/1.00 % (3783041)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2467509946:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 3.76/1.00 % (3783042)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=33082331:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 3.76/1.00 % (3782992)Instruction limit reached!
% 3.76/1.00 % (3782992)------------------------------
% 3.76/1.00 % (3782992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.76/1.00 % (3782992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.00 % (3782992)CaDiCaL version: 2.1.3
% 3.76/1.00 % (3782992)Termination reason: Instruction limit
% 3.76/1.00 % (3782992)Termination phase: Saturation
% 3.76/1.00 % (3782992)Time elapsed: 0.315 s
% 3.76/1.00 % (3782992)Peak memory usage: 15 MB
% 3.76/1.00 % (3782992)Instructions burned: 1242 (million)
% 3.76/1.00 % (3783048)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3099894276:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 3.76/1.00 % (3783038)Instruction limit reached!
% 5.43/1.07 % (3783038)------------------------------
% 5.43/1.07 % (3783038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.07 % (3783038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.07 % (3783038)CaDiCaL version: 2.1.3
% 5.43/1.07 % (3783038)Termination reason: Instruction limit
% 5.43/1.07 % (3783038)Termination phase: Saturation
% 5.43/1.07 % (3783038)Time elapsed: 0.044 s
% 5.43/1.07 % (3783038)Peak memory usage: 13 MB
% 5.43/1.07 % (3783038)Instructions burned: 68 (million)
% 5.43/1.07 % (3783041)Instruction limit reached!
% 5.43/1.07 % (3783041)------------------------------
% 5.43/1.07 % (3783041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.07 % (3783041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.07 % (3783041)CaDiCaL version: 2.1.3
% 5.43/1.07 % (3783041)Termination reason: Instruction limit
% 5.43/1.07 % (3783041)Termination phase: Saturation
% 5.43/1.07 % (3783041)Time elapsed: 0.053 s
% 5.43/1.07 % (3783041)Peak memory usage: 12 MB
% 5.43/1.07 % (3783041)Instructions burned: 97 (million)
% 5.43/1.07 % (3783050)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=2757199169:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.43/1.07 % (3783039)Instruction limit reached!
% 5.43/1.07 % (3783039)------------------------------
% 5.43/1.07 % (3783039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.07 % (3783039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.07 % (3783039)CaDiCaL version: 2.1.3
% 5.43/1.07 % (3783039)Termination reason: Instruction limit
% 5.43/1.07 % (3783039)Termination phase: Saturation
% 5.43/1.07 % (3783039)Time elapsed: 0.081 s
% 5.43/1.07 % (3783039)Peak memory usage: 14 MB
% 5.43/1.07 % (3783039)Instructions burned: 181 (million)
% 5.43/1.07 % (3783051)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2702929252:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.43/1.07 % (3783053)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3472479437:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 5.43/1.07 % (3783053)Refutation not found, incomplete strategy
% 5.43/1.07 % (3783053)------------------------------
% 5.43/1.07 % (3783053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.07 % (3783053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.07 % (3783053)CaDiCaL version: 2.1.3
% 5.43/1.07 % (3783053)Termination reason: Refutation not found, incomplete strategy
% 5.43/1.07 % (3783053)Time elapsed: 0.006 s
% 5.43/1.07 % (3783053)Peak memory usage: 12 MB
% 5.43/1.07 % (3783053)Instructions burned: 9 (million)
% 5.43/1.07 % (3783053)------------------------------
% 5.43/1.07 % (3783053)------------------------------
% 5.43/1.07 % (3783056)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1396757180:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 5.43/1.07 % (3783040)Instruction limit reached!
% 5.43/1.07 % (3783040)------------------------------
% 5.43/1.07 % (3783040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.07 % (3783040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.07 % (3783040)CaDiCaL version: 2.1.3
% 5.43/1.07 % (3783040)Termination reason: Instruction limit
% 5.43/1.07 % (3783040)Termination phase: Saturation
% 5.43/1.07 % (3783040)Time elapsed: 0.127 s
% 5.43/1.07 % (3783040)Peak memory usage: 13 MB
% 5.43/1.07 % (3783040)Instructions burned: 247 (million)
% 5.43/1.07 % (3783056)Refutation not found, incomplete strategy
% 5.43/1.07 % (3783056)------------------------------
% 5.43/1.07 % (3783056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.43/1.07 % (3783056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.43/1.07 % (3783056)CaDiCaL version: 2.1.3
% 5.43/1.07 % (3783056)Termination reason: Refutation not found, incomplete strategy
% 5.43/1.07 % (3783056)Time elapsed: 0.018 s
% 5.43/1.07 % (3783056)Peak memory usage: 12 MB
% 5.43/1.07 % (3783056)Instructions burned: 29 (million)
% 5.43/1.07 % (3783056)------------------------------
% 5.43/1.07 % (3783056)------------------------------
% 5.43/1.07 % (3783058)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=624189187:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 6.44/1.20 % (3783051)Instruction limit reached!
% 6.44/1.20 % (3783051)------------------------------
% 6.44/1.20 % (3783051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.44/1.20 % (3783051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.20 % (3783051)CaDiCaL version: 2.1.3
% 6.44/1.20 % (3783051)Termination reason: Instruction limit
% 6.44/1.20 % (3783051)Termination phase: Saturation
% 6.44/1.20 % (3783051)Time elapsed: 0.070 s
% 6.44/1.20 % (3783051)Peak memory usage: 12 MB
% 6.44/1.20 % (3783051)Instructions burned: 130 (million)
% 6.44/1.20 % (3783058)Refutation not found, incomplete strategy
% 6.44/1.20 % (3783058)------------------------------
% 6.44/1.20 % (3783058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.44/1.20 % (3783058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.20 % (3783058)CaDiCaL version: 2.1.3
% 6.44/1.20 % (3783058)Termination reason: Refutation not found, incomplete strategy
% 6.44/1.20 % (3783058)Time elapsed: 0.002 s
% 6.44/1.20 % (3783058)Peak memory usage: 12 MB
% 6.44/1.20 % (3783058)Instructions burned: 2 (million)
% 6.44/1.20 % (3783058)------------------------------
% 6.44/1.20 % (3783058)------------------------------
% 6.44/1.20 % (3783059)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2568987271:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 6.44/1.20 % (3783061)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=3364154803:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 6.44/1.20 % (3783062)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=3064223948:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2993 on theBenchmark for (2993ds/105Mi)
% 6.44/1.20 % (3783061)Instruction limit reached!
% 6.44/1.20 % (3783061)------------------------------
% 6.44/1.20 % (3783061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.44/1.20 % (3783061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.20 % (3783061)CaDiCaL version: 2.1.3
% 6.44/1.20 % (3783061)Termination reason: Instruction limit
% 6.44/1.20 % (3783061)Termination phase: Saturation
% 6.44/1.20 % (3783061)Time elapsed: 0.038 s
% 6.44/1.20 % (3783061)Peak memory usage: 12 MB
% 6.44/1.20 % (3783061)Instructions burned: 65 (million)
% 6.44/1.20 % (3783059)Instruction limit reached!
% 6.44/1.20 % (3783059)------------------------------
% 6.44/1.20 % (3783059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.44/1.20 % (3783059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.20 % (3783059)CaDiCaL version: 2.1.3
% 6.44/1.20 % (3783059)Termination reason: Instruction limit
% 6.44/1.20 % (3783059)Termination phase: Saturation
% 6.44/1.20 % (3783059)Time elapsed: 0.053 s
% 6.44/1.20 % (3783059)Peak memory usage: 13 MB
% 6.44/1.20 % (3783059)Instructions burned: 96 (million)
% 6.44/1.20 % (3783062)Instruction limit reached!
% 6.44/1.20 % (3783062)------------------------------
% 6.44/1.20 % (3783062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.44/1.20 % (3783062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.44/1.20 % (3783062)CaDiCaL version: 2.1.3
% 6.44/1.20 % (3783062)Termination reason: Instruction limit
% 6.44/1.20 % (3783062)Termination phase: Saturation
% 6.44/1.20 % (3783062)Time elapsed: 0.052 s
% 6.44/1.20 % (3783062)Peak memory usage: 13 MB
% 6.44/1.20 % (3783062)Instructions burned: 105 (million)
% 6.44/1.20 % (3783066)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=825584157: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.44/1.20 % (3783067)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1846664305:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.44/1.20 % (3783048)Instruction limit reached!
% 6.44/1.20 % (3783048)------------------------------
% 6.44/1.20 % (3783048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.39 % (3783048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.39 % (3783048)CaDiCaL version: 2.1.3
% 6.85/1.39 % (3783048)Termination reason: Instruction limit
% 6.85/1.39 % (3783048)Termination phase: Saturation
% 6.85/1.39 % (3783048)Time elapsed: 0.216 s
% 6.85/1.39 % (3783048)Peak memory usage: 14 MB
% 6.85/1.39 % (3783048)Instructions burned: 874 (million)
% 6.85/1.39 % (3783068)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2209771984:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.85/1.39 % (3783071)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=2042819802:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.85/1.39 % (3783015)Instruction limit reached!
% 6.85/1.39 % (3783015)------------------------------
% 6.85/1.39 % (3783015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.39 % (3783015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.39 % (3783015)CaDiCaL version: 2.1.3
% 6.85/1.39 % (3783015)Termination reason: Instruction limit
% 6.85/1.39 % (3783015)Termination phase: Saturation
% 6.85/1.39 % (3783015)Time elapsed: 0.411 s
% 6.85/1.39 % (3783015)Peak memory usage: 15 MB
% 6.85/1.39 % (3783015)Instructions burned: 854 (million)
% 6.85/1.39 % (3783071)Instruction limit reached!
% 6.85/1.39 % (3783071)------------------------------
% 6.85/1.39 % (3783071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.39 % (3783071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.39 % (3783071)CaDiCaL version: 2.1.3
% 6.85/1.39 % (3783071)Termination reason: Instruction limit
% 6.85/1.39 % (3783071)Termination phase: Saturation
% 6.85/1.39 % (3783071)Time elapsed: 0.010 s
% 6.85/1.39 % (3783071)Peak memory usage: 13 MB
% 6.85/1.39 % (3783071)Instructions burned: 38 (million)
% 6.85/1.39 % (3783076)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1109768028:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 6.85/1.39 % (3783042)Instruction limit reached!
% 6.85/1.39 % (3783042)------------------------------
% 6.85/1.39 % (3783042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.39 % (3783042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.39 % (3783042)CaDiCaL version: 2.1.3
% 6.85/1.39 % (3783042)Termination reason: Instruction limit
% 6.85/1.39 % (3783042)Termination phase: Saturation
% 6.85/1.39 % (3783042)Time elapsed: 0.264 s
% 6.85/1.39 % (3783042)Peak memory usage: 15 MB
% 6.85/1.39 % (3783042)Instructions burned: 429 (million)
% 6.85/1.39 % (3783075)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=341429931:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.85/1.39 % (3783078)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=207755120:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.85/1.39 % (3783076)Instruction limit reached!
% 6.85/1.39 % (3783076)------------------------------
% 6.85/1.39 % (3783076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.39 % (3783076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.39 % (3783076)CaDiCaL version: 2.1.3
% 6.85/1.39 % (3783076)Termination reason: Instruction limit
% 6.85/1.39 % (3783076)Termination phase: Saturation
% 6.85/1.39 % (3783076)Time elapsed: 0.022 s
% 6.85/1.39 % (3783076)Peak memory usage: 13 MB
% 6.85/1.39 % (3783076)Instructions burned: 69 (million)
% 6.85/1.39 % (3783078)Instruction limit reached!
% 6.85/1.39 % (3783078)------------------------------
% 6.85/1.39 % (3783078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.85/1.39 % (3783078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/1.39 % (3783078)CaDiCaL version: 2.1.3
% 6.85/1.39 % (3783078)Termination reason: Instruction limit
% 6.85/1.39 % (3783078)Termination phase: Saturation
% 6.85/1.39 % (3783078)Time elapsed: 0.011 s
% 6.85/1.39 % (3783078)Peak memory usage: 12 MB
% 6.85/1.39 % (3783078)Instructions burned: 23 (million)
% 6.85/1.39 % (3783081)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=4240145046:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 7.76/1.53 % (3783083)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1892576134:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 7.76/1.53 % (3783075)Instruction limit reached!
% 7.76/1.53 % (3783075)------------------------------
% 7.76/1.53 % (3783075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.53 % (3783075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.53 % (3783075)CaDiCaL version: 2.1.3
% 7.76/1.53 % (3783075)Termination reason: Instruction limit
% 7.76/1.53 % (3783075)Termination phase: Saturation
% 7.76/1.53 % (3783075)Time elapsed: 0.047 s
% 7.76/1.53 % (3783075)Peak memory usage: 13 MB
% 7.76/1.53 % (3783075)Instructions burned: 92 (million)
% 7.76/1.53 % (3783083)Instruction limit reached!
% 7.76/1.53 % (3783083)------------------------------
% 7.76/1.53 % (3783083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.53 % (3783083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.53 % (3783083)CaDiCaL version: 2.1.3
% 7.76/1.53 % (3783083)Termination reason: Instruction limit
% 7.76/1.53 % (3783083)Termination phase: Saturation
% 7.76/1.53 % (3783083)Time elapsed: 0.016 s
% 7.76/1.53 % (3783083)Peak memory usage: 12 MB
% 7.76/1.53 % (3783083)Instructions burned: 28 (million)
% 7.76/1.53 % (3783085)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.76/1.53 % (3783085)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=1055618853:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.76/1.53 % (3783086)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=215143897:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.76/1.53 % (3783050)Instruction limit reached!
% 7.76/1.53 % (3783050)------------------------------
% 7.76/1.53 % (3783050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.53 % (3783050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.53 % (3783050)CaDiCaL version: 2.1.3
% 7.76/1.53 % (3783050)Termination reason: Instruction limit
% 7.76/1.53 % (3783050)Termination phase: Saturation
% 7.76/1.53 % (3783050)Time elapsed: 0.330 s
% 7.76/1.53 % (3783050)Peak memory usage: 15 MB
% 7.76/1.53 % (3783050)Instructions burned: 517 (million)
% 7.76/1.53 % (3783081)Instruction limit reached!
% 7.76/1.53 % (3783081)------------------------------
% 7.76/1.53 % (3783081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.53 % (3783081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.53 % (3783081)CaDiCaL version: 2.1.3
% 7.76/1.53 % (3783081)Termination reason: Instruction limit
% 7.76/1.53 % (3783081)Termination phase: Saturation
% 7.76/1.53 % (3783081)Time elapsed: 0.095 s
% 7.76/1.53 % (3783081)Peak memory usage: 14 MB
% 7.76/1.53 % (3783081)Instructions burned: 340 (million)
% 7.76/1.53 % (3783090)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.76/1.53 % (3783090)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=1615322810:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.76/1.53 % (3783085)Instruction limit reached!
% 7.76/1.53 % (3783085)------------------------------
% 7.76/1.53 % (3783085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.53 % (3783085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.53 % (3783085)CaDiCaL version: 2.1.3
% 7.76/1.53 % (3783085)Termination reason: Instruction limit
% 7.76/1.53 % (3783085)Termination phase: Saturation
% 7.76/1.53 % (3783085)Time elapsed: 0.069 s
% 7.76/1.53 % (3783085)Peak memory usage: 12 MB
% 7.76/1.53 % (3783085)Instructions burned: 139 (million)
% 7.76/1.53 % (3783089)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=4051715406:i=227:sd=1:bd=all:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/227Mi)
% 7.76/1.53 % (3783092)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=1859115528:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.76/1.53 % (3783092)Refutation not found, incomplete strategy
% 7.76/1.58 % (3783092)------------------------------
% 7.76/1.58 % (3783092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.58 % (3783092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.58 % (3783092)CaDiCaL version: 2.1.3
% 7.76/1.58 % (3783092)Termination reason: Refutation not found, incomplete strategy
% 7.76/1.58 % (3783092)Time elapsed: 0.003 s
% 7.76/1.58 % (3783092)Peak memory usage: 12 MB
% 7.76/1.58 % (3783092)Instructions burned: 4 (million)
% 7.76/1.58 % (3783092)------------------------------
% 7.76/1.58 % (3783092)------------------------------
% 7.76/1.58 % (3783095)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1326113800:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 7.76/1.58 % (3783068)Instruction limit reached!
% 7.76/1.58 % (3783068)------------------------------
% 7.76/1.58 % (3783068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.58 % (3783068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.58 % (3783068)CaDiCaL version: 2.1.3
% 7.76/1.58 % (3783068)Termination reason: Instruction limit
% 7.76/1.58 % (3783068)Termination phase: Saturation
% 7.76/1.58 % (3783068)Time elapsed: 0.245 s
% 7.76/1.58 % (3783068)Peak memory usage: 15 MB
% 7.76/1.58 % (3783068)Instructions burned: 497 (million)
% 7.76/1.58 % (3783097)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=3588170180:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 7.76/1.58 % (3783090)Instruction limit reached!
% 7.76/1.58 % (3783090)------------------------------
% 7.76/1.58 % (3783090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.58 % (3783090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.58 % (3783090)CaDiCaL version: 2.1.3
% 7.76/1.58 % (3783090)Termination reason: Instruction limit
% 7.76/1.58 % (3783090)Termination phase: Saturation
% 7.76/1.58 % (3783090)Time elapsed: 0.100 s
% 7.76/1.58 % (3783090)Peak memory usage: 16 MB
% 7.76/1.58 % (3783090)Instructions burned: 376 (million)
% 7.76/1.58 % (3783099)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=901228821:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/9840Mi)
% 7.76/1.58 % (3783089)Instruction limit reached!
% 7.76/1.58 % (3783089)------------------------------
% 7.76/1.58 % (3783089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.58 % (3783089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.58 % (3783089)CaDiCaL version: 2.1.3
% 7.76/1.58 % (3783089)Termination reason: Instruction limit
% 7.76/1.58 % (3783089)Termination phase: Saturation
% 7.76/1.58 % (3783089)Time elapsed: 0.119 s
% 7.76/1.58 % (3783089)Peak memory usage: 13 MB
% 7.76/1.58 % (3783089)Instructions burned: 228 (million)
% 7.76/1.58 % (3783101)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3139489411:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 7.76/1.58 % (3783086)Instruction limit reached!
% 7.76/1.58 % (3783086)------------------------------
% 7.76/1.58 % (3783086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.76/1.58 % (3783086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.76/1.58 % (3783086)CaDiCaL version: 2.1.3
% 7.76/1.58 % (3783086)Termination reason: Instruction limit
% 7.76/1.58 % (3783086)Termination phase: Saturation
% 7.76/1.58 % (3783086)Time elapsed: 0.209 s
% 7.76/1.58 % (3783086)Peak memory usage: 12 MB
% 7.76/1.58 % (3783086)Instructions burned: 342 (million)
% 7.76/1.58 % (3783103)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 7.76/1.58 % (3783103)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=141877559:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 7.76/1.58 % (3783067)Instruction limit reached!
% 7.76/1.58 % (3783067)------------------------------
% 7.76/1.58 % (3783067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783067)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783067)Termination reason: Instruction limit
% 9.20/1.73 % (3783067)Termination phase: Saturation
% 9.20/1.73 % (3783067)Time elapsed: 0.386 s
% 9.20/1.73 % (3783067)Peak memory usage: 14 MB
% 9.20/1.73 % (3783067)Instructions burned: 375 (million)
% 9.20/1.73 % (3783097)Instruction limit reached!
% 9.20/1.73 % (3783097)------------------------------
% 9.20/1.73 % (3783097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783097)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783097)Termination reason: Instruction limit
% 9.20/1.73 % (3783097)Termination phase: Saturation
% 9.20/1.73 % (3783097)Time elapsed: 0.125 s
% 9.20/1.73 % (3783097)Peak memory usage: 14 MB
% 9.20/1.73 % (3783097)Instructions burned: 270 (million)
% 9.20/1.73 % (3783105)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=280927221:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/31Mi)
% 9.20/1.73 % (3783106)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 9.20/1.73 % (3783106)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.20/1.73 % (3783106)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=3598903229:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2988 on theBenchmark for (2988ds/1440Mi)
% 9.20/1.73 % (3783105)Refutation not found, incomplete strategy
% 9.20/1.73 % (3783105)------------------------------
% 9.20/1.73 % (3783105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783105)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783105)Termination reason: Refutation not found, incomplete strategy
% 9.20/1.73 % (3783105)Time elapsed: 0.009 s
% 9.20/1.73 % (3783105)Peak memory usage: 12 MB
% 9.20/1.73 % (3783105)Instructions burned: 17 (million)
% 9.20/1.73 % (3783105)------------------------------
% 9.20/1.73 % (3783105)------------------------------
% 9.20/1.73 % (3783106)Refutation not found, incomplete strategy
% 9.20/1.73 % (3783106)------------------------------
% 9.20/1.73 % (3783106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783106)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783106)Termination reason: Refutation not found, incomplete strategy
% 9.20/1.73 % (3783106)Time elapsed: 0.006 s
% 9.20/1.73 % (3783106)Peak memory usage: 12 MB
% 9.20/1.73 % (3783106)Instructions burned: 9 (million)
% 9.20/1.73 % (3783106)------------------------------
% 9.20/1.73 % (3783106)------------------------------
% 9.20/1.73 % (3783109)dis+10_2_sil=128000:si=on:random_seed=3034587331:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 9.20/1.73 % (3783110)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2920918298:i=111:add=on:fgj=on:rtra=on:fdi=1024_2988 on theBenchmark for (2988ds/111Mi)
% 9.20/1.73 % (3783110)Refutation not found, incomplete strategy
% 9.20/1.73 % (3783110)------------------------------
% 9.20/1.73 % (3783110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783110)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783110)Termination reason: Refutation not found, incomplete strategy
% 9.20/1.73 % (3783110)Time elapsed: 0.010 s
% 9.20/1.73 % (3783110)Peak memory usage: 12 MB
% 9.20/1.73 % (3783110)Instructions burned: 17 (million)
% 9.20/1.73 % (3783110)------------------------------
% 9.20/1.73 % (3783110)------------------------------
% 9.20/1.73 % (3783113)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=1809675986:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/122Mi)
% 9.20/1.73 % (3783103)Instruction limit reached!
% 9.20/1.73 % (3783103)------------------------------
% 9.20/1.73 % (3783103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783103)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783103)Termination reason: Instruction limit
% 9.20/1.73 % (3783103)Termination phase: Saturation
% 9.20/1.73 % (3783103)Time elapsed: 0.170 s
% 9.20/1.73 % (3783103)Peak memory usage: 13 MB
% 9.20/1.73 % (3783103)Instructions burned: 271 (million)
% 9.20/1.73 % (3783095)Instruction limit reached!
% 9.20/1.73 % (3783095)------------------------------
% 9.20/1.73 % (3783095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783095)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783095)Termination reason: Instruction limit
% 9.20/1.73 % (3783095)Termination phase: Saturation
% 9.20/1.73 % (3783095)Time elapsed: 0.306 s
% 9.20/1.73 % (3783095)Peak memory usage: 14 MB
% 9.20/1.73 % (3783095)Instructions burned: 576 (million)
% 9.20/1.73 % (3783115)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=2247910828:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/136Mi)
% 9.20/1.73 % (3783113)Instruction limit reached!
% 9.20/1.73 % (3783113)------------------------------
% 9.20/1.73 % (3783113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783113)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783113)Termination reason: Instruction limit
% 9.20/1.73 % (3783113)Termination phase: Saturation
% 9.20/1.73 % (3783113)Time elapsed: 0.077 s
% 9.20/1.73 % (3783113)Peak memory usage: 13 MB
% 9.20/1.73 % (3783113)Instructions burned: 124 (million)
% 9.20/1.73 % (3783116)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2626928559:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/232Mi)
% 9.20/1.73 % (3783116)Refutation not found, incomplete strategy
% 9.20/1.73 % (3783116)------------------------------
% 9.20/1.73 % (3783116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783116)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783116)Termination reason: Refutation not found, incomplete strategy
% 9.20/1.73 % (3783116)Time elapsed: 0.003 s
% 9.20/1.73 % (3783116)Peak memory usage: 12 MB
% 9.20/1.73 % (3783116)Instructions burned: 3 (million)
% 9.20/1.73 % (3783116)------------------------------
% 9.20/1.73 % (3783116)------------------------------
% 9.20/1.73 % (3783118)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=1677619970:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2986 on theBenchmark for (2986ds/1254Mi)
% 9.20/1.73 % (3783118)Refutation not found, incomplete strategy
% 9.20/1.73 % (3783118)------------------------------
% 9.20/1.73 % (3783118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783118)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783118)Termination reason: Refutation not found, incomplete strategy
% 9.20/1.73 % (3783118)Time elapsed: 0.003 s
% 9.20/1.73 % (3783118)Peak memory usage: 12 MB
% 9.20/1.73 % (3783118)Instructions burned: 5 (million)
% 9.20/1.73 % (3783118)------------------------------
% 9.20/1.73 % (3783118)------------------------------
% 9.20/1.73 % (3783120)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 9.20/1.73 % (3783101)Instruction limit reached!
% 9.20/1.73 % (3783101)------------------------------
% 9.20/1.73 % (3783101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783101)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783101)Termination reason: Instruction limit
% 9.20/1.73 % (3783101)Termination phase: Saturation
% 9.20/1.73 % (3783101)Time elapsed: 0.251 s
% 9.20/1.73 % (3783101)Peak memory usage: 14 MB
% 9.20/1.73 % (3783101)Instructions burned: 421 (million)
% 9.20/1.73 % (3783120)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=95358337:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2986 on theBenchmark for (2986ds/281Mi)
% 9.20/1.73 % (3783122)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=4055689324:i=619:add=on:rtra=on_2986 on theBenchmark for (2986ds/619Mi)
% 9.20/1.73 % (3783123)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=2180533753:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/865Mi)
% 9.20/1.73 % (3783109)Instruction limit reached!
% 9.20/1.73 % (3783109)------------------------------
% 9.20/1.73 % (3783109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783109)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783109)Termination reason: Instruction limit
% 9.20/1.73 % (3783109)Termination phase: Saturation
% 9.20/1.73 % (3783109)Time elapsed: 0.163 s
% 9.20/1.73 % (3783109)Peak memory usage: 13 MB
% 9.20/1.73 % (3783109)Instructions burned: 341 (million)
% 9.20/1.73 % (3783127)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3563581195:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/212Mi)
% 9.20/1.73 % (3783115)Instruction limit reached!
% 9.20/1.73 % (3783115)------------------------------
% 9.20/1.73 % (3783115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783115)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783115)Termination reason: Instruction limit
% 9.20/1.73 % (3783115)Termination phase: Saturation
% 9.20/1.73 % (3783115)Time elapsed: 0.098 s
% 9.20/1.73 % (3783115)Peak memory usage: 14 MB
% 9.20/1.73 % (3783115)Instructions burned: 137 (million)
% 9.20/1.73 % (3783129)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=332040176:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2985 on theBenchmark for (2985ds/130Mi)
% 9.20/1.73 % (3783120) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3782927-3783120"...
% 9.20/1.73 % (3783127)Instruction limit reached!
% 9.20/1.73 % (3783127)------------------------------
% 9.20/1.73 % (3783127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.73 % (3783127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.73 % (3783127)CaDiCaL version: 2.1.3
% 9.20/1.73 % (3783127)Termination reason: Instruction limit
% 9.20/1.73 % (3783127)Termination phase: Saturation
% 9.20/1.73 % (3783127)Time elapsed: 0.103 s
% 9.20/1.73 % (3783127)Peak memory usage: 13 MB
% 9.20/1.73 % (3783127)Instructions burned: 213 (million)
% 9.20/1.73 % (3783120)...printing done.
% 9.20/1.73 % (3783120)Refutation found. Thanks to Tanya!
% 9.20/1.73 % SZS status Theorem for theBenchmark
% 9.20/1.73 % SZS output start Proof for theBenchmark
% 9.20/1.73 thf(type_def_5, type, b: $tType).
% 9.20/1.73 thf(type_def_6, type, a: $tType).
% 9.20/1.73 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 9.20/1.73 thf(func_def_1, type, vNOT: ($o > $o)).
% 9.20/1.73 thf(func_def_2, type, vAND: ($o > $o > $o)).
% 9.20/1.73 thf(func_def_3, type, vIMP: ($o > $o > $o)).
% 9.20/1.73 thf(func_def_4, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 9.20/1.73 thf(func_def_5, type, db1: !>[X0: $tType]:(X0)).
% 9.20/1.73 thf(func_def_6, type, db0: !>[X0: $tType]:(X0)).
% 9.20/1.73 thf(func_def_7, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 9.20/1.73 thf(func_def_8, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 9.20/1.73 thf(func_def_9, type, db2: !>[X0: $tType]:(X0)).
% 9.20/1.73 thf(func_def_10, type, db3: !>[X0: $tType]:(X0)).
% 9.20/1.73 thf(func_def_13, type, diff: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 9.20/1.73 thf(func_def_14, type, sK0: ((a > $o) > $o)).
% 9.20/1.73 thf(func_def_15, type, sK1: (((a > $o) > a > $o) > (a > $o) > a)).
% 9.20/1.73 thf(func_def_16, type, sK2: (a > b > $o)).
% 9.20/1.73 thf(func_def_17, type, sK3: ((a > b) > a)).
% 9.20/1.73 thf(func_def_18, type, sK4: ((a > $o) > a)).
% 9.20/1.73 thf(func_def_19, type, sK5: (((a > $o) > a) > a > $o)).
% 9.20/1.73 thf(func_def_20, type, sK6: (((b > $o) > $o) > (b > $o) > b)).
% 9.20/1.73 thf(func_def_21, type, sK7: ((a > b) > b)).
% 9.20/1.73 thf(func_def_22, type, sK8: (((b > $o) > $o) > b > $o)).
% 9.20/1.73 thf(func_def_24, type, sF10: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > (X1 > X0) > X1 > X2))).
% 9.20/1.73 thf(func_def_25, type, sF11: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > ((X0 > X2) > X1) > X1))).
% 9.20/1.73 thf(func_def_26, type, sF12: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > X0 > X1 > X2))).
% 9.20/1.73 thf(func_def_27, type, sF13: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X1 > X0) > ((X1 > X0) > X2 > X3) > X2 > X3))).
% 9.20/1.73 thf(func_def_28, type, sF14: !>[X0: $tType, X1: $tType]:(((X0 > X1) > ((X0 > X1) > X0) > X0))).
% 9.20/1.73 thf(func_def_29, type, sF15: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > (X0 > X2 > X1) > X2 > X1))).
% 9.20/1.73 thf(func_def_30, type, sF16: !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 9.20/1.73 thf(func_def_31, type, sF17: !>[X0: $tType, X1: $tType]:((((X0 > b) > X1) > (X0 > b) > X1))).
% 9.20/1.73 thf(func_def_32, type, sF18: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((((X2 > X0) > X1) > (X1 > X3) > (X2 > X0) > X3))).
% 9.20/1.73 thf(func_def_33, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 9.20/1.73 thf(func_def_34, type, sF19: !>[X0: $tType]:((b > (b > X0) > X0))).
% 9.20/1.73 thf(f1,conjecture,(
% 9.20/1.73 (! [X4 : ((a > $o) > a > $o)] : ? [X5 : ((a > $o) > a)] : ! [X6 : (a > $o)] : (? [X2 : a] : (X4 @ X6 @ X2) => (X4 @ X6 @ (X5 @ X6))) => ! [X0 : ((a > $o) > $o)] : (! [X1 : (a > $o)] : ((X0 @ X1) => ? [X7 : a] : (X1 @ X7)) => ? [X3 : ((a > $o) > a)] : ! [X1 : (a > $o)] : ((X0 @ X1) => (X1 @ (X3 @ X1))))) & (! [X0 : ((b > $o) > $o)] : (! [X1 : (b > $o)] : ((X0 @ X1) => ? [X2 : b] : (X1 @ X2)) => ? [X3 : ((b > $o) > b)] : ! [X1 : (b > $o)] : ((X0 @ X1) => (X1 @ (X3 @ X1)))) => ! [X4 : (a > b > $o)] : ? [X5 : (a > b)] : ! [X6 : a] : (? [X2 : b] : (X4 @ X6 @ X2) => (X4 @ X6 @ (X5 @ X6))))),
% 9.20/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM561)).
% 9.20/1.73 thf(f2,negated_conjecture,(
% 9.20/1.73 ~((! [X4 : ((a > $o) > a > $o)] : ? [X5 : ((a > $o) > a)] : ! [X6 : (a > $o)] : (? [X2 : a] : (X4 @ X6 @ X2) => (X4 @ X6 @ (X5 @ X6))) => ! [X0 : ((a > $o) > $o)] : (! [X1 : (a > $o)] : ((X0 @ X1) => ? [X7 : a] : (X1 @ X7)) => ? [X3 : ((a > $o) > a)] : ! [X1 : (a > $o)] : ((X0 @ X1) => (X1 @ (X3 @ X1))))) & (! [X0 : ((b > $o) > $o)] : (! [X1 : (b > $o)] : ((X0 @ X1) => ? [X2 : b] : (X1 @ X2)) => ? [X3 : ((b > $o) > b)] : ! [X1 : (b > $o)] : ((X0 @ X1) => (X1 @ (X3 @ X1)))) => ! [X4 : (a > b > $o)] : ? [X5 : (a > b)] : ! [X6 : a] : (? [X2 : b] : (X4 @ X6 @ X2) => (X4 @ X6 @ (X5 @ X6)))))),
% 9.20/1.73 inference(negated_conjecture,[status(cth)],[f1])).
% 9.20/1.73 thf(f3,plain,(
% 9.20/1.73 ~((! [X0 : ((a > $o) > a > $o)] : ? [X1 : ((a > $o) > a)] : ! [X2 : (a > $o)] : (? [X3 : a] : (X0 @ X2 @ X3) => (X0 @ X2 @ (X1 @ X2))) => ! [X4 : ((a > $o) > $o)] : (! [X5 : (a > $o)] : ((X4 @ X5) => ? [X6 : a] : (X5 @ X6)) => ? [X7 : ((a > $o) > a)] : ! [X8 : (a > $o)] : ((X4 @ X8) => (X8 @ (X7 @ X8))))) & (! [X9 : ((b > $o) > $o)] : (! [X10 : (b > $o)] : ((X9 @ X10) => ? [X11 : b] : (X10 @ X11)) => ? [X12 : ((b > $o) > b)] : ! [X13 : (b > $o)] : ((X9 @ X13) => (X13 @ (X12 @ X13)))) => ! [X14 : (a > b > $o)] : ? [X15 : (a > b)] : ! [X16 : a] : (? [X17 : b] : (X14 @ X16 @ X17) => (X14 @ X16 @ (X15 @ X16)))))),
% 9.20/1.73 inference(rectify,[],[f2])).
% 9.20/1.73 thf(f4,plain,(
% 9.20/1.73 (((~ (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ (^[Y2 : b]: (Y1 @ Y2)))))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (^[Y3 : b]: (Y0 @ Y2 @ Y3))) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))) & ((!! @ ((a > $o) > a > $o) @ (^[Y0 : (a > $o) > a > $o]: (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((?? @ a @ (^[Y3 : a]: (Y0 @ Y2 @ Y3))) => (Y0 @ Y2 @ (Y1 @ Y2))))))))) => (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ (^[Y2 : a]: (Y1 @ Y2)))))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))))))) = $true)),
% 9.20/1.73 inference(fool_elimination,[],[f3])).
% 9.20/1.73 thf(f5,definition,(
% 9.20/1.73 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1),X3 : (X0 > X1)] : ((X2 = X3) | (((X3 @ (diff @ X0 @ X1 @ X2 @ X3))) != ((X2 @ (diff @ X0 @ X1 @ X2 @ X3))))) )),
% 9.20/1.73 introduced(theory,[functional_extensionality_axiom])).
% 9.20/1.73 thf(f6,plain,(
% 9.20/1.73 (((~ (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ (^[Y2 : b]: (Y1 @ Y2)))))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (^[Y3 : b]: (Y0 @ Y2 @ Y3))) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))) & ((!! @ ((a > $o) > a > $o) @ (^[Y0 : (a > $o) > a > $o]: (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((?? @ a @ (^[Y3 : a]: (Y0 @ Y2 @ Y3))) => (Y0 @ Y2 @ (Y1 @ Y2))))))))) => (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ (^[Y2 : a]: (Y1 @ Y2)))))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))))))) = $true)),
% 9.20/1.73 inference(cnf_transformation,[],[f4])).
% 9.20/1.73 thf(f9,plain,(
% 9.20/1.73 (((~ (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))) & ((!! @ ((a > $o) > a > $o) @ (^[Y0 : (a > $o) > a > $o]: (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((?? @ a @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))) => (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ Y1)))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))))))) = $true)),
% 9.20/1.73 inference(beta-eta_normalization,[],[f6])).
% 9.20/1.73 thf(f10,plain,(
% 9.20/1.73 ($false = ((((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))) & ((!! @ ((a > $o) > a > $o) @ (^[Y0 : (a > $o) > a > $o]: (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((?? @ a @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))) => (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ Y1)))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))))))))),
% 9.20/1.73 inference(not_proxy_clausification,[],[f9])).
% 9.20/1.73 thf(f11,plain,(
% 9.20/1.73 ($false = (((!! @ ((a > $o) > a > $o) @ (^[Y0 : (a > $o) > a > $o]: (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((?? @ a @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))) => (!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ Y1)))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))))))) | ($false = (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))))))),
% 9.20/1.73 inference(and_proxy_clausification,[],[f10])).
% 9.20/1.73 thf(f12,plain,(
% 9.20/1.73 ($false = ((!! @ ((a > $o) > $o) @ (^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ Y1)))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))))) | ($false = (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f11])).
% 9.20/1.73 thf(f16,plain,(
% 9.20/1.73 ($false = (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))))) | ($false = (((^[Y0 : (a > $o) > $o]: ((!! @ (a > $o) @ (^[Y1 : a > $o]: ((Y0 @ Y1) => (?? @ a @ Y1)))) => (?? @ ((a > $o) > a) @ (^[Y1 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y2 : a > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))) @ sK0)))),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f12])).
% 9.20/1.73 thf(f17,plain,(
% 9.20/1.73 ($false = (((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0)))) => (?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1)))))))))) | ($false = (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))))))),
% 9.20/1.73 inference(beta-eta_normalization,[],[f16])).
% 9.20/1.73 thf(f20,plain,(
% 9.20/1.73 ($false = (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))))) | ($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1)))))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f17])).
% 9.20/1.73 thf(f21,plain,(
% 9.20/1.73 ($false = (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2)))))))))) => (!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))))) | ($true = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f17])).
% 9.20/1.73 thf(f26,plain,(
% 9.20/1.73 ($true = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0)))))) | ($false = ((!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f21])).
% 9.20/1.73 thf(f27,plain,(
% 9.20/1.73 (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))))) = $true) | ($true = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f21])).
% 9.20/1.73 thf(f28,plain,(
% 9.20/1.73 ($false = ((!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))))) | ($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1)))))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f20])).
% 9.20/1.73 thf(f29,plain,(
% 9.20/1.73 (((!! @ ((b > $o) > $o) @ (^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))))) = $true) | ($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1)))))))))),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f20])).
% 9.20/1.73 thf(f34,plain,(
% 9.20/1.73 ( ! [X1 : ((b > $o) > $o)] : (($true = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0)))))) | ((((^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))) @ X1)) = $true)) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f27])).
% 9.20/1.73 thf(f35,plain,(
% 9.20/1.73 ( ! [X1 : ((b > $o) > $o)] : (($true = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0)))))) | ((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true)) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f34])).
% 9.20/1.73 thf(f36,plain,(
% 9.20/1.73 ( ! [X1 : (a > $o)] : (((((^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0))) @ X1)) = $true) | ($false = ((!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))))) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f26])).
% 9.20/1.73 thf(f37,plain,(
% 9.20/1.73 ( ! [X1 : (a > $o)] : (((((sK0 @ X1) => (?? @ a @ X1))) = $true) | ($false = ((!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f36])).
% 9.20/1.73 thf(f38,plain,(
% 9.20/1.73 ( ! [X1 : ((b > $o) > $o)] : (($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) | ((((^[Y0 : (b > $o) > $o]: ((!! @ (b > $o) @ (^[Y1 : b > $o]: ((Y0 @ Y1) => (?? @ b @ Y1)))) => (?? @ ((b > $o) > b) @ (^[Y1 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y2 : b > $o]: ((Y0 @ Y2) => (Y2 @ (Y1 @ Y2))))))))) @ X1)) = $true)) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f29])).
% 9.20/1.73 thf(f39,plain,(
% 9.20/1.73 ( ! [X1 : ((b > $o) > $o)] : (($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) | ((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true)) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f38])).
% 9.20/1.73 thf(f40,plain,(
% 9.20/1.73 ($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) | ($false = (((^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))) @ sK2)))),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f28])).
% 9.20/1.73 thf(f41,plain,(
% 9.20/1.73 ($false = ((?? @ ((a > $o) > a) @ (^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) | ($false = ((?? @ (a > b) @ (^[Y0 : a > b]: (!! @ a @ (^[Y1 : a]: ((?? @ b @ (sK2 @ Y1)) => (sK2 @ Y1 @ (Y0 @ Y1)))))))))),
% 9.20/1.73 inference(beta-eta_normalization,[],[f40])).
% 9.20/1.73 thf(f46,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : (((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true) | ((((^[Y0 : a > $o]: ((sK0 @ Y0) => (?? @ a @ Y0))) @ X2)) = $true)) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f35])).
% 9.20/1.73 thf(f47,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : (((((sK0 @ X2) => (?? @ a @ X2))) = $true) | ((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true)) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f46])).
% 9.20/1.73 thf(f48,plain,(
% 9.20/1.73 ( ! [X1 : (a > $o)] : ((((?? @ a @ X1)) = $true) | ($false = ((!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))))) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f37])).
% 9.20/1.73 thf(f49,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($false = (((^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1)))))) @ X2))) | ((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true)) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f39])).
% 9.20/1.73 thf(f50,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (Y0 @ (X2 @ Y0))))))) | ((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true)) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f49])).
% 9.20/1.73 thf(f51,plain,(
% 9.20/1.73 ( ! [X1 : ((a > $o) > a)] : (($false = ((?? @ (a > b) @ (^[Y0 : a > b]: (!! @ a @ (^[Y1 : a]: ((?? @ b @ (sK2 @ Y1)) => (sK2 @ Y1 @ (Y0 @ Y1))))))))) | ($false = (((^[Y0 : (a > $o) > a]: (!! @ (a > $o) @ (^[Y1 : a > $o]: ((sK0 @ Y1) => (Y1 @ (Y0 @ Y1)))))) @ X1)))) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f41])).
% 9.20/1.73 thf(f52,plain,(
% 9.20/1.73 ( ! [X1 : ((a > $o) > a)] : (($false = ((?? @ (a > b) @ (^[Y0 : a > b]: (!! @ a @ (^[Y1 : a]: ((?? @ b @ (sK2 @ Y1)) => (sK2 @ Y1 @ (Y0 @ Y1))))))))) | ($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (Y0 @ (X1 @ Y0)))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f51])).
% 9.20/1.73 thf(f56,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : ((((?? @ a @ X2)) = $true) | ((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true) | ($false = ((sK0 @ X2)))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f47])).
% 9.20/1.73 thf(f57,plain,(
% 9.20/1.73 ( ! [X1 : (a > $o)] : (($false = ((!! @ (a > b > $o) @ (^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2))))))))))) | ($false = ((sK0 @ X1))) | (((X1 @ (sK4 @ X1))) = $true)) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f48])).
% 9.20/1.73 thf(f58,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true) | ($false = (((^[Y0 : a > $o]: ((sK0 @ Y0) => (Y0 @ (X2 @ Y0)))) @ (sK5 @ X2))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f50])).
% 9.20/1.73 thf(f59,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true) | ($false = (((sK0 @ (sK5 @ X2)) => (sK5 @ X2 @ (X2 @ (sK5 @ X2))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f58])).
% 9.20/1.73 thf(f60,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = (((^[Y0 : a > b]: (!! @ a @ (^[Y1 : a]: ((?? @ b @ (sK2 @ Y1)) => (sK2 @ Y1 @ (Y0 @ Y1)))))) @ X2))) | ($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (Y0 @ (X1 @ Y0)))))))) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f52])).
% 9.20/1.73 thf(f61,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = ((!! @ (a > $o) @ (^[Y0 : a > $o]: ((sK0 @ Y0) => (Y0 @ (X1 @ Y0))))))) | ($false = ((!! @ a @ (^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f60])).
% 9.20/1.73 thf(f65,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : (((((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))) => (?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) = $true) | (((X2 @ (sK4 @ X2))) = $true) | ($false = ((sK0 @ X2)))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f56])).
% 9.20/1.73 thf(f66,plain,(
% 9.20/1.73 ( ! [X1 : (a > $o)] : (($false = ((sK0 @ X1))) | ($false = (((^[Y0 : a > b > $o]: (?? @ (a > b) @ (^[Y1 : a > b]: (!! @ a @ (^[Y2 : a]: ((?? @ b @ (Y0 @ Y2)) => (Y0 @ Y2 @ (Y1 @ Y2)))))))) @ sK2))) | (((X1 @ (sK4 @ X1))) = $true)) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f57])).
% 9.20/1.73 thf(f67,plain,(
% 9.20/1.73 ( ! [X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($false = ((?? @ (a > b) @ (^[Y0 : a > b]: (!! @ a @ (^[Y1 : a]: ((?? @ b @ (sK2 @ Y1)) => (sK2 @ Y1 @ (Y0 @ Y1))))))))) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f66])).
% 9.20/1.73 thf(f68,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($true = ((?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) | ($false = (((sK0 @ (sK5 @ X2)) => (sK5 @ X2 @ (X2 @ (sK5 @ X2)))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f59])).
% 9.20/1.73 thf(f69,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (((((^[Y0 : a > $o]: ((sK0 @ Y0) => (Y0 @ (X1 @ Y0)))) @ (sK5 @ X1))) = $false) | ($false = ((!! @ a @ (^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f61])).
% 9.20/1.73 thf(f70,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = (((sK0 @ (sK5 @ X1)) => (sK5 @ X1 @ (X1 @ (sK5 @ X1)))))) | ($false = ((!! @ a @ (^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f69])).
% 9.20/1.73 thf(f74,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : (($true = ((?? @ ((b > $o) > b) @ (^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1))))))))) | ($false = ((sK0 @ X2))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))))) | (((X2 @ (sK4 @ X2))) = $true)) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f65])).
% 9.20/1.73 thf(f75,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : (a > $o)] : (($false = (((^[Y0 : a > b]: (!! @ a @ (^[Y1 : a]: ((?? @ b @ (sK2 @ Y1)) => (sK2 @ Y1 @ (Y0 @ Y1)))))) @ X2))) | (((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f67])).
% 9.20/1.73 thf(f76,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK0 @ X1))) | ($false = ((!! @ a @ (^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f75])).
% 9.20/1.73 thf(f77,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (((((^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1)))))) @ (sK6 @ X1))) = $true) | ($false = (((sK0 @ (sK5 @ X2)) => (sK5 @ X2 @ (X2 @ (sK5 @ X2)))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f68])).
% 9.20/1.73 thf(f78,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($false = (((sK0 @ (sK5 @ X2)) => (sK5 @ X2 @ (X2 @ (sK5 @ X2)))))) | ($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0))))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f77])).
% 9.20/1.73 thf(f79,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = ((!! @ a @ (^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0))))))) | ($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1)))))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f70])).
% 9.20/1.73 thf(f80,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : ((((sK0 @ (sK5 @ X1))) = $true) | ($false = ((!! @ a @ (^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))))))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f70])).
% 9.20/1.73 thf(f85,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : (((((^[Y0 : (b > $o) > b]: (!! @ (b > $o) @ (^[Y1 : b > $o]: ((X1 @ Y1) => (Y1 @ (Y0 @ Y1)))))) @ (sK6 @ X1))) = $true) | (((X2 @ (sK4 @ X2))) = $true) | ($false = ((sK0 @ X2))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f74])).
% 9.20/1.73 thf(f86,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X1 : ((b > $o) > $o)] : ((((X2 @ (sK4 @ X2))) = $true) | ($false = ((sK0 @ X2))) | ($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0))))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f85])).
% 9.20/1.73 thf(f87,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($false = (((^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))) @ (sK3 @ X2)))) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f76])).
% 9.20/1.73 thf(f88,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : (a > $o)] : (($false = (((?? @ b @ (sK2 @ (sK3 @ X2))) => (sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2)))))) | (((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f87])).
% 9.20/1.73 thf(f89,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0))))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))))) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2)))))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f78])).
% 9.20/1.73 thf(f90,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : ((((sK0 @ (sK5 @ X2))) = $true) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))))) | ($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0)))))))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f78])).
% 9.20/1.73 thf(f91,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1))))) | ($false = (((^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))) @ (sK3 @ X2))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f79])).
% 9.20/1.73 thf(f92,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1))))) | ($false = (((?? @ b @ (sK2 @ (sK3 @ X2))) => (sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2))))))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f91])).
% 9.20/1.73 thf(f93,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : ((((sK0 @ (sK5 @ X1))) = $true) | ($false = (((^[Y0 : a]: ((?? @ b @ (sK2 @ Y0)) => (sK2 @ Y0 @ (X2 @ Y0)))) @ (sK3 @ X2))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f80])).
% 9.20/1.73 thf(f94,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = (((?? @ b @ (sK2 @ (sK3 @ X2))) => (sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2)))))) | (((sK0 @ (sK5 @ X1))) = $true)) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f93])).
% 9.20/1.73 thf(f99,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o)] : ((((X2 @ (sK4 @ X2))) = $true) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))))) | ($false = ((sK0 @ X2))) | ((((^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0)))) @ X3)) = $true)) )),
% 9.20/1.73 inference(pi_proxy_clausification,[],[f86])).
% 9.20/1.73 thf(f100,plain,(
% 9.20/1.73 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o)] : (((((X1 @ X3) => (X3 @ (sK6 @ X1 @ X3)))) = $true) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))))) | (((X2 @ (sK4 @ X2))) = $true) | ($false = ((sK0 @ X2)))) )),
% 9.20/1.73 inference(beta-eta_normalization,[],[f99])).
% 9.20/1.73 thf(f101,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2))))) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f88])).
% 9.20/1.73 thf(f102,plain,(
% 9.20/1.73 ( ! [X2 : (a > b),X1 : (a > $o)] : ((((?? @ b @ (sK2 @ (sK3 @ X2)))) = $true) | (((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.73 inference(imp_proxy_clausification,[],[f88])).
% 9.20/1.73 thf(f103,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : ((((sK0 @ (sK5 @ X2))) = $true) | ($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0))))))) | ($false = (((^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))) @ (sK8 @ X1))))) )),
% 9.20/1.73 inference(sigma_proxy_clausification,[],[f90])).
% 9.20/1.73 thf(f104,plain,(
% 9.20/1.73 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($false = (((X1 @ (sK8 @ X1)) => (?? @ b @ (sK8 @ X1))))) | (((sK0 @ (sK5 @ X2))) = $true) | ($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0)))))))) )),
% 9.20/1.74 inference(beta-eta_normalization,[],[f103])).
% 9.20/1.74 thf(f105,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : (((((^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0)))) @ X3)) = $true) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.74 inference(pi_proxy_clausification,[],[f89])).
% 9.20/1.74 thf(f106,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : (((((X1 @ X3) => (X3 @ (sK6 @ X1 @ X3)))) = $true) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.74 inference(beta-eta_normalization,[],[f105])).
% 9.20/1.74 thf(f107,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1))))) | ($false = ((sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2)))))) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f92])).
% 9.20/1.74 thf(f108,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : ((((?? @ b @ (sK2 @ (sK3 @ X2)))) = $true) | ($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1)))))) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f92])).
% 9.20/1.74 thf(f109,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : ((((sK0 @ (sK5 @ X1))) = $true) | ($false = ((sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2)))))) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f94])).
% 9.20/1.74 thf(f110,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : ((((sK0 @ (sK5 @ X1))) = $true) | (((?? @ b @ (sK2 @ (sK3 @ X2)))) = $true)) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f94])).
% 9.20/1.74 thf(f115,definition,(
% 9.20/1.74 spl9_2 <=> ! [X2 : (a > b)] : ($false = ((sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2)))))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition])).
% 9.20/1.74 thf(f116,plain,(
% 9.20/1.74 ( ! [X2 : (a > b)] : (($false = ((sK2 @ (sK3 @ X2) @ (X2 @ (sK3 @ X2)))))) ) | ~spl9_2),
% 9.20/1.74 inference(avatar_component_clause,[],[f115])).
% 9.20/1.74 thf(f121,plain,(
% 9.20/1.74 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o)] : ((((X3 @ (sK6 @ X1 @ X3))) = $true) | (((X2 @ (sK4 @ X2))) = $true) | ($false = ((X1 @ X3))) | ($false = ((sK0 @ X2))) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))))))) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f100])).
% 9.20/1.74 thf(f122,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($true = ((sK2 @ (sK3 @ X2) @ (sK7 @ X2)))) | ($false = ((sK0 @ X1)))) )),
% 9.20/1.74 inference(sigma_proxy_clausification,[],[f102])).
% 9.20/1.74 thf(f124,definition,(
% 9.20/1.74 spl9_3 <=> ! [X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK0 @ X1))))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition])).
% 9.20/1.74 thf(f125,plain,(
% 9.20/1.74 ( ! [X1 : (a > $o)] : ((((X1 @ (sK4 @ X1))) = $true) | ($false = ((sK0 @ X1)))) ) | ~spl9_3),
% 9.20/1.74 inference(avatar_component_clause,[],[f124])).
% 9.20/1.74 thf(f126,plain,(
% 9.20/1.74 spl9_3 | spl9_2),
% 9.20/1.74 inference(avatar_split_clause,[],[f101,f115,f124])).
% 9.20/1.74 thf(f127,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X1 : ((b > $o) > $o)] : (($true = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0))))))) | (((sK0 @ (sK5 @ X2))) = $true) | ($false = ((?? @ b @ (sK8 @ X1))))) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f104])).
% 9.20/1.74 thf(f129,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : ((((X3 @ (sK6 @ X1 @ X3))) = $true) | ($false = ((!! @ (b > $o) @ (^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0)))))) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | ($false = ((X1 @ X3)))) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f106])).
% 9.20/1.74 thf(f131,definition,(
% 9.20/1.74 spl9_4 <=> ! [X1 : ((a > $o) > a)] : ($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1)))))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition])).
% 9.20/1.74 thf(f132,plain,(
% 9.20/1.74 ( ! [X1 : ((a > $o) > a)] : (($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1)))))) ) | ~spl9_4),
% 9.20/1.74 inference(avatar_component_clause,[],[f131])).
% 9.20/1.74 thf(f133,plain,(
% 9.20/1.74 spl9_2 | spl9_4),
% 9.20/1.74 inference(avatar_split_clause,[],[f107,f131,f115])).
% 9.20/1.74 thf(f134,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($true = ((sK2 @ (sK3 @ X2) @ (sK7 @ X2)))) | ($false = ((sK5 @ X1 @ (X1 @ (sK5 @ X1)))))) )),
% 9.20/1.74 inference(sigma_proxy_clausification,[],[f108])).
% 9.20/1.74 thf(f136,definition,(
% 9.20/1.74 spl9_5 <=> ! [X1 : ((a > $o) > a)] : (((sK0 @ (sK5 @ X1))) = $true)),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition])).
% 9.20/1.74 thf(f137,plain,(
% 9.20/1.74 ( ! [X1 : ((a > $o) > a)] : ((((sK0 @ (sK5 @ X1))) = $true)) ) | ~spl9_5),
% 9.20/1.74 inference(avatar_component_clause,[],[f136])).
% 9.20/1.74 thf(f138,plain,(
% 9.20/1.74 spl9_5 | spl9_2),
% 9.20/1.74 inference(avatar_split_clause,[],[f109,f115,f136])).
% 9.20/1.74 thf(f139,plain,(
% 9.20/1.74 ( ! [X2 : (a > b),X1 : ((a > $o) > a)] : (($true = ((sK2 @ (sK3 @ X2) @ (sK7 @ X2)))) | (((sK0 @ (sK5 @ X1))) = $true)) )),
% 9.20/1.74 inference(sigma_proxy_clausification,[],[f110])).
% 9.20/1.74 thf(f141,definition,(
% 9.20/1.74 spl9_6 <=> ! [X2 : (a > b)] : ($true = ((sK2 @ (sK3 @ X2) @ (sK7 @ X2))))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition])).
% 9.20/1.74 thf(f142,plain,(
% 9.20/1.74 ( ! [X2 : (a > b)] : (($true = ((sK2 @ (sK3 @ X2) @ (sK7 @ X2))))) ) | ~spl9_6),
% 9.20/1.74 inference(avatar_component_clause,[],[f141])).
% 9.20/1.74 thf(f145,plain,(
% 9.20/1.74 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o)] : (($false = (((^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))) @ (sK8 @ X1)))) | ($false = ((X1 @ X3))) | ($false = ((sK0 @ X2))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | (((X2 @ (sK4 @ X2))) = $true)) )),
% 9.20/1.74 inference(sigma_proxy_clausification,[],[f121])).
% 9.20/1.74 thf(f146,plain,(
% 9.20/1.74 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o)] : ((((X2 @ (sK4 @ X2))) = $true) | ($false = (((X1 @ (sK8 @ X1)) => (?? @ b @ (sK8 @ X1))))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | ($false = ((X1 @ X3))) | ($false = ((sK0 @ X2)))) )),
% 9.20/1.74 inference(beta-eta_normalization,[],[f145])).
% 9.20/1.74 thf(f147,plain,(
% 9.20/1.74 spl9_3 | spl9_6),
% 9.20/1.74 inference(avatar_split_clause,[],[f122,f141,f124])).
% 9.20/1.74 thf(f148,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : ((((sK0 @ (sK5 @ X2))) = $true) | ($false = ((?? @ b @ (sK8 @ X1)))) | ((((^[Y0 : b > $o]: ((X1 @ Y0) => (Y0 @ (sK6 @ X1 @ Y0)))) @ X3)) = $true)) )),
% 9.20/1.74 inference(pi_proxy_clausification,[],[f127])).
% 9.20/1.74 thf(f149,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : (((((X1 @ X3) => (X3 @ (sK6 @ X1 @ X3)))) = $true) | ($false = ((?? @ b @ (sK8 @ X1)))) | (((sK0 @ (sK5 @ X2))) = $true)) )),
% 9.20/1.74 inference(beta-eta_normalization,[],[f148])).
% 9.20/1.74 thf(f152,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : (($false = ((X1 @ X3))) | ($false = (((^[Y0 : b > $o]: ((X1 @ Y0) => (?? @ b @ Y0))) @ (sK8 @ X1)))) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | (((X3 @ (sK6 @ X1 @ X3))) = $true)) )),
% 9.20/1.74 inference(sigma_proxy_clausification,[],[f129])).
% 9.20/1.74 thf(f153,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : ((((X3 @ (sK6 @ X1 @ X3))) = $true) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | ($false = ((X1 @ X3))) | ($false = (((X1 @ (sK8 @ X1)) => (?? @ b @ (sK8 @ X1)))))) )),
% 9.20/1.74 inference(beta-eta_normalization,[],[f152])).
% 9.20/1.74 thf(f154,plain,(
% 9.20/1.74 spl9_4 | spl9_6),
% 9.20/1.74 inference(avatar_split_clause,[],[f134,f141,f131])).
% 9.20/1.74 thf(f155,plain,(
% 9.20/1.74 spl9_5 | spl9_6),
% 9.20/1.74 inference(avatar_split_clause,[],[f139,f141,f136])).
% 9.20/1.74 thf(f158,plain,(
% 9.20/1.74 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o)] : (($false = ((?? @ b @ (sK8 @ X1)))) | ($false = ((sK0 @ X2))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | ($false = ((X1 @ X3))) | (((X2 @ (sK4 @ X2))) = $true)) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f146])).
% 9.20/1.74 thf(f160,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : (($false = ((?? @ b @ (sK8 @ X1)))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | ($false = ((X1 @ X3))) | (((sK0 @ (sK5 @ X2))) = $true)) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f149])).
% 9.20/1.74 thf(f162,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o)] : (($false = ((?? @ b @ (sK8 @ X1)))) | ($false = ((X1 @ X3))) | ($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | (((X3 @ (sK6 @ X1 @ X3))) = $true)) )),
% 9.20/1.74 inference(imp_proxy_clausification,[],[f153])).
% 9.20/1.74 thf(f169,plain,(
% 9.20/1.74 ( ! [X2 : (a > $o),X3 : (b > $o),X1 : ((b > $o) > $o),X4 : b] : (($false = ((X1 @ X3))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | (((X2 @ (sK4 @ X2))) = $true) | ($false = ((sK0 @ X2))) | ($false = ((sK8 @ X1 @ X4)))) )),
% 9.20/1.74 inference(pi_proxy_clausification,[],[f158])).
% 9.20/1.74 thf(f171,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o),X4 : b] : (($false = ((sK8 @ X1 @ X4))) | ($false = ((X1 @ X3))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | (((sK0 @ (sK5 @ X2))) = $true)) )),
% 9.20/1.74 inference(pi_proxy_clausification,[],[f160])).
% 9.20/1.74 thf(f174,plain,(
% 9.20/1.74 ( ! [X2 : ((a > $o) > a),X3 : (b > $o),X1 : ((b > $o) > $o),X4 : b] : (($false = ((sK5 @ X2 @ (X2 @ (sK5 @ X2))))) | (((X3 @ (sK6 @ X1 @ X3))) = $true) | ($false = ((sK8 @ X1 @ X4))) | ($false = ((X1 @ X3)))) )),
% 9.20/1.74 inference(pi_proxy_clausification,[],[f162])).
% 9.20/1.74 thf(f176,definition,(
% 9.20/1.74 spl9_8 <=> ! [X6 : b,X2 : ((b > $o) > $o),X5 : (b > $o)] : (($false = ((X2 @ X5))) | ($false = ((sK8 @ X2 @ X6))) | ($true = ((X5 @ (sK6 @ X2 @ X5)))))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition])).
% 9.20/1.74 thf(f177,plain,(
% 9.20/1.74 ( ! [X2 : ((b > $o) > $o),X6 : b,X5 : (b > $o)] : (($true = ((X5 @ (sK6 @ X2 @ X5)))) | ($false = ((X2 @ X5))) | ($false = ((sK8 @ X2 @ X6)))) ) | ~spl9_8),
% 9.20/1.74 inference(avatar_component_clause,[],[f176])).
% 9.20/1.74 thf(f179,plain,(
% 9.20/1.74 spl9_8 | spl9_3),
% 9.20/1.74 inference(avatar_split_clause,[],[f169,f124,f176])).
% 9.20/1.74 thf(f180,plain,(
% 9.20/1.74 spl9_8 | spl9_5),
% 9.20/1.74 inference(avatar_split_clause,[],[f171,f136,f176])).
% 9.20/1.74 thf(f181,plain,(
% 9.20/1.74 spl9_8 | spl9_4),
% 9.20/1.74 inference(avatar_split_clause,[],[f174,f131,f176])).
% 9.20/1.74 thf(f182,plain,(
% 9.20/1.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1),X3 : (X0 > X1),X4 : X0] : ((((X2 @ X4)) = ((X3 @ X4))) | (((X3 @ (diff @ X0 @ X1 @ X2 @ X3))) != ((X2 @ (diff @ X0 @ X1 @ X2 @ X3))))) )),
% 9.20/1.74 inference(argument_congruence,[],[f5])).
% 9.20/1.74 thf(f220,definition,(
% 9.20/1.74 ( ! [X1 : $tType,X0 : $tType,X3 : $tType,X2 : (X0 > X1),X4 : (X3 > X0),X5 : X3] : ((((sF10 @ X0 @ X3 @ X1 @ X2 @ X4 @ X5)) = ((X2 @ (X4 @ X5))))) )),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 9.20/1.74 thf(f221,plain,(
% 9.20/1.74 ( ! [X1 : $tType,X0 : $tType,X3 : $tType,X2 : (X0 > X1),X4 : (X3 > X0),X5 : X3] : ((((X2 @ (X4 @ X5))) = ((sF10 @ X0 @ X3 @ X1 @ X2 @ X4 @ X5)))) )),
% 9.20/1.74 inference(reorient_equations,[],[f220])).
% 9.20/1.74 thf(f226,plain,(
% 9.20/1.74 ( ! [X2 : ((b > $o) > $o),X6 : b] : (($false = ((X2 @ (^[Y0 : b]: ($false))))) | ($true = (((^[Y0 : b]: ($false)) @ (sK6 @ X2 @ (^[Y0 : b]: ($false)))))) | ($false = ((sK8 @ X2 @ X6)))) ) | ~spl9_8),
% 9.20/1.74 inference(primitive_instantiation,[],[f177])).
% 9.20/1.74 thf(f236,plain,(
% 9.20/1.74 ( ! [X2 : ((b > $o) > $o),X6 : b] : (($false = $true) | ($false = ((sK8 @ X2 @ X6))) | ($false = ((X2 @ (^[Y0 : b]: ($false)))))) ) | ~spl9_8),
% 9.20/1.74 inference(beta-eta_normalization,[],[f226])).
% 9.20/1.74 thf(f237,plain,(
% 9.20/1.74 ( ! [X2 : ((b > $o) > $o),X6 : b] : (($false = ((sK8 @ X2 @ X6))) | ($false = ((X2 @ (^[Y0 : b]: ($false)))))) ) | ~spl9_8),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f236])).
% 9.20/1.74 thf(f281,plain,(
% 9.20/1.74 ( ! [X0 : $tType,X2 : (a > X0),X1 : (X0 > b)] : (($false = ((sK2 @ (sK3 @ (sF10 @ X0 @ a @ b @ X1 @ X2)) @ (X1 @ (X2 @ (sK3 @ (sF10 @ X0 @ a @ b @ X1 @ X2)))))))) ) | ~spl9_2),
% 9.20/1.74 inference(constrained_superposition,[],[f116,f221])).
% 9.20/1.74 thf(f373,plain,(
% 9.20/1.74 ( ! [X2 : b,X0 : ((b > $o) > $o),X1 : ((b > $o) > $o)] : (($false = $true) | (((X1 @ (sK8 @ X0))) = $false) | ($false = ((sK8 @ X1 @ X2))) | ($false = ((X0 @ (^[Y0 : b]: ($false)))))) ) | ~spl9_8),
% 9.20/1.74 inference(constrained_superposition,[],[f237,f177])).
% 9.20/1.74 thf(f377,plain,(
% 9.20/1.74 ( ! [X2 : b,X0 : ((b > $o) > $o),X1 : ((b > $o) > $o)] : ((((X1 @ (sK8 @ X0))) = $false) | ($false = ((sK8 @ X1 @ X2))) | ($false = ((X0 @ (^[Y0 : b]: ($false)))))) ) | ~spl9_8),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f373])).
% 9.20/1.74 thf(f559,plain,(
% 9.20/1.74 ( ! [X2 : b,X0 : ((b > $o) > $o)] : (($false = ((sK8 @ (^[Y0 : b > $o]: ($true)) @ X2))) | ($false = ((X0 @ (^[Y0 : b]: ($false))))) | ($false = (((^[Y0 : b > $o]: ($true)) @ (sK8 @ X0))))) ) | ~spl9_8),
% 9.20/1.74 inference(primitive_instantiation,[],[f377])).
% 9.20/1.74 thf(f584,plain,(
% 9.20/1.74 ( ! [X2 : b,X0 : ((b > $o) > $o)] : (($false = $true) | ($false = ((sK8 @ (^[Y0 : b > $o]: ($true)) @ X2))) | ($false = ((X0 @ (^[Y0 : b]: ($false)))))) ) | ~spl9_8),
% 9.20/1.74 inference(beta-eta_normalization,[],[f559])).
% 9.20/1.74 thf(f585,plain,(
% 9.20/1.74 ( ! [X2 : b,X0 : ((b > $o) > $o)] : (($false = ((X0 @ (^[Y0 : b]: ($false))))) | ($false = ((sK8 @ (^[Y0 : b > $o]: ($true)) @ X2)))) ) | ~spl9_8),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f584])).
% 9.20/1.74 thf(f595,definition,(
% 9.20/1.74 spl9_9 <=> ! [X0 : ((b > $o) > $o)] : ($false = ((X0 @ (^[Y0 : b]: ($false)))))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition])).
% 9.20/1.74 thf(f596,plain,(
% 9.20/1.74 ( ! [X0 : ((b > $o) > $o)] : (($false = ((X0 @ (^[Y0 : b]: ($false)))))) ) | ~spl9_9),
% 9.20/1.74 inference(avatar_component_clause,[],[f595])).
% 9.20/1.74 thf(f598,definition,(
% 9.20/1.74 spl9_10 <=> ! [X2 : b] : ($false = ((sK8 @ (^[Y0 : b > $o]: ($true)) @ X2)))),
% 9.20/1.74 introduced(definition,[new_symbols(definition,[spl9_10])],[avatar_definition])).
% 9.20/1.74 thf(f599,plain,(
% 9.20/1.74 ( ! [X2 : b] : (($false = ((sK8 @ (^[Y0 : b > $o]: ($true)) @ X2)))) ) | ~spl9_10),
% 9.20/1.74 inference(avatar_component_clause,[],[f598])).
% 9.20/1.74 thf(f600,plain,(
% 9.20/1.74 spl9_9 | spl9_10 | ~spl9_8),
% 9.20/1.74 inference(avatar_split_clause,[],[f585,f176,f598,f595])).
% 9.20/1.74 thf(f624,plain,(
% 9.20/1.74 ( ! [X1 : ((b > $o) > $o)] : (($false = (((^[Y0 : b > $o]: (~ (X1 @ Y0))) @ (^[Y0 : b]: ($false)))))) ) | ~spl9_9),
% 9.20/1.74 inference(primitive_instantiation,[],[f596])).
% 9.20/1.74 thf(f648,plain,(
% 9.20/1.74 ( ! [X1 : ((b > $o) > $o)] : (($false = ((~ (X1 @ (^[Y0 : b]: ($false))))))) ) | ~spl9_9),
% 9.20/1.74 inference(beta-eta_normalization,[],[f624])).
% 9.20/1.74 thf(f652,plain,(
% 9.20/1.74 ($false = ((~ $false))) | ~spl9_9),
% 9.20/1.74 inference(forward_demodulation,[],[f648,f596])).
% 9.20/1.74 thf(f653,plain,(
% 9.20/1.74 ($false = $true) | ~spl9_9),
% 9.20/1.74 inference(boolean_simplification,[],[f652])).
% 9.20/1.74 thf(f654,plain,(
% 9.20/1.74 $false | ~spl9_9),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f653])).
% 9.20/1.74 thf(f655,plain,(
% 9.20/1.74 ~spl9_9),
% 9.20/1.74 inference(avatar_contradiction_clause,[],[f654])).
% 9.20/1.74 thf(f716,plain,(
% 9.20/1.74 ( ! [X0 : b,X1 : (b > $o)] : (($false = ((X1 @ X0))) | (((X1 @ (diff @ b @ $o @ (sK8 @ (^[Y0 : b > $o]: ($true))) @ X1))) != ((sK8 @ (^[Y0 : b > $o]: ($true)) @ (diff @ b @ $o @ (sK8 @ (^[Y0 : b > $o]: ($true))) @ X1))))) ) | ~spl9_10),
% 9.20/1.74 inference(constrained_superposition,[],[f182,f599])).
% 9.20/1.74 thf(f719,plain,(
% 9.20/1.74 ( ! [X0 : b,X1 : (b > $o)] : (($false != ((X1 @ (diff @ b @ $o @ (sK8 @ (^[Y0 : b > $o]: ($true))) @ X1)))) | ($false = ((X1 @ X0)))) ) | ~spl9_10),
% 9.20/1.74 inference(forward_demodulation,[],[f716,f599])).
% 9.20/1.74 thf(f773,plain,(
% 9.20/1.74 ( ! [X0 : b] : (($false != $false) | ($false = ((sK2 @ (sK3 @ (sF10 @ (b > $o) @ a @ b @ (diff @ b @ $o @ (sK8 @ (^[Y0 : b > $o]: ($true)))) @ sK2)) @ X0)))) ) | (~spl9_2 | ~spl9_10)),
% 9.20/1.74 inference(constrained_superposition,[],[f719,f281])).
% 9.20/1.74 thf(f790,plain,(
% 9.20/1.74 ( ! [X0 : b] : (($false = ((sK2 @ (sK3 @ (sF10 @ (b > $o) @ a @ b @ (diff @ b @ $o @ (sK8 @ (^[Y0 : b > $o]: ($true)))) @ sK2)) @ X0)))) ) | (~spl9_2 | ~spl9_10)),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f773])).
% 9.20/1.74 thf(f1426,plain,(
% 9.20/1.74 ($false = $true) | (~spl9_2 | ~spl9_6 | ~spl9_10)),
% 9.20/1.74 inference(constrained_superposition,[],[f142,f790])).
% 9.20/1.74 thf(f1437,plain,(
% 9.20/1.74 $false | (~spl9_2 | ~spl9_6 | ~spl9_10)),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f1426])).
% 9.20/1.74 thf(f1438,plain,(
% 9.20/1.74 ~spl9_2 | ~spl9_6 | ~spl9_10),
% 9.20/1.74 inference(avatar_contradiction_clause,[],[f1437])).
% 9.20/1.74 thf(f1630,plain,(
% 9.20/1.74 ($false = $true) | ($false = ((sK0 @ (sK5 @ sK4)))) | (~spl9_3 | ~spl9_4)),
% 9.20/1.74 inference(constrained_superposition,[],[f132,f125])).
% 9.20/1.74 thf(f1653,plain,(
% 9.20/1.74 ($false = ((sK0 @ (sK5 @ sK4)))) | (~spl9_3 | ~spl9_4)),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f1630])).
% 9.20/1.74 thf(f1692,plain,(
% 9.20/1.74 ($false = $true) | (~spl9_3 | ~spl9_4 | ~spl9_5)),
% 9.20/1.74 inference(forward_demodulation,[],[f1653,f137])).
% 9.20/1.74 thf(f1693,plain,(
% 9.20/1.74 $false | (~spl9_3 | ~spl9_4 | ~spl9_5)),
% 9.20/1.74 inference(trivial_inequality_removal,[],[f1692])).
% 9.20/1.74 thf(f1694,plain,(
% 9.20/1.74 ~spl9_3 | ~spl9_4 | ~spl9_5),
% 9.20/1.74 inference(avatar_contradiction_clause,[],[f1693])).
% 9.20/1.74 cnf(s2, plain, spl9_2 | spl9_3, inference(sat_conversion,[],[f126])).
% 9.20/1.74 cnf(s3, plain, spl9_2 | spl9_4, inference(sat_conversion,[],[f133])).
% 9.20/1.74 cnf(s4, plain, spl9_2 | spl9_5, inference(sat_conversion,[],[f138])).
% 9.20/1.74 cnf(s6, plain, spl9_3 | spl9_6, inference(sat_conversion,[],[f147])).
% 9.20/1.74 cnf(s7, plain, spl9_4 | spl9_6, inference(sat_conversion,[],[f154])).
% 9.20/1.74 cnf(s8, plain, spl9_5 | spl9_6, inference(sat_conversion,[],[f155])).
% 9.20/1.74 cnf(s14, plain, spl9_3 | spl9_8, inference(sat_conversion,[],[f179])).
% 9.20/1.74 cnf(s15, plain, spl9_5 | spl9_8, inference(sat_conversion,[],[f180])).
% 9.20/1.74 cnf(s16, plain, spl9_4 | spl9_8, inference(sat_conversion,[],[f181])).
% 9.20/1.74 cnf(s17, plain, ~spl9_8 | spl9_9 | spl9_10, inference(sat_conversion,[],[f600])).
% 9.20/1.74 cnf(s19, plain, ~spl9_9, inference(sat_conversion,[],[f655])).
% 9.20/1.74 cnf(s21, plain, ~spl9_2 | ~spl9_6 | ~spl9_10, inference(sat_conversion,[],[f1438])).
% 9.20/1.74 cnf(s23, plain, ~spl9_3 | ~spl9_4 | ~spl9_5, inference(sat_conversion,[],[f1694])).
% 9.20/1.74 cnf(s24, plain, ~spl9_8 | spl9_10, inference(rat,[],[s17,s19])).
% 9.20/1.74 cnf(s26, plain, spl9_2, inference(rat,[],[s23,s2,s3,s4])).
% 9.20/1.74 cnf(s27, plain, spl9_5, inference(rat,[],[s21,s24,s8,s15,s26])).
% 9.20/1.74 cnf(s28, plain, spl9_4, inference(rat,[],[s21,s24,s7,s16,s26])).
% 9.20/1.74 cnf(s29, plain, ~spl9_3, inference(rat,[],[s23,s27,s28])).
% 9.20/1.74 cnf(s30, plain, spl9_8, inference(rat,[],[s14,s29])).
% 9.20/1.74 cnf(s32, plain, spl9_6, inference(rat,[],[s6,s29])).
% 9.20/1.74 cnf(s33, plain, spl9_10, inference(rat,[],[s24,s30])).
% 9.20/1.74 cnf(s34, plain, $false, inference(rat,[],[s21,s26,s33,s32])).
% 9.20/1.74 thf(f1728,plain,(
% 9.20/1.74 $false),
% 9.20/1.74 inference(avatar_sat_refutation,[],[s34])).
% 9.20/1.74 % SZS output end Proof for theBenchmark
% 9.20/1.74 % (3783120)------------------------------
% 9.20/1.74 % (3783120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.20/1.74 % (3783120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/1.74 % (3783120)CaDiCaL version: 2.1.3
% 9.20/1.74 % (3783120)Termination reason: Refutation
% 9.20/1.74 % (3783120)Time elapsed: 0.144 s
% 9.20/1.74 % (3783120)Peak memory usage: 14 MB
% 9.20/1.74 % (3783120)Instructions burned: 272 (million)
% 9.20/1.74 % (3782927)Success in time 1.495 s
% 9.20/1.74 % Vampire exiting
%------------------------------------------------------------------------------