%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV119^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:37:50 AM UTC 2026
% Result : Theorem 3.35s 0.91s
% Output : Refutation 3.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV119^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.29 % Computer : n018.cluster.edu
% 0.12/0.29 % Model : x86_64 x86_64
% 0.12/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.29 % Memory : 8046.5625MB
% 0.12/0.29 % OS : Linux 6.8.0-71-generic
% 0.12/0.29 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Tue Sep 29 15:13:56 UTC 2026
% 0.12/0.29 % CPUTime :
% 0.12/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.29/0.35 Running higher-order theorem proving
% 0.29/0.37 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.99/0.56 % (205336)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.99/0.56 % (205341)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1273915742:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.99/0.56 % (205347)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.99/0.56 % (205347)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.99/0.56 % (205342)lrs+10_16_si=on:nwc=1.5:random_seed=1673993245:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.99/0.56 % (205343)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=4238311204:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.99/0.56 % (205345)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=186849061:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.99/0.56 % (205344)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=2774619576: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.99/0.56 % (205346)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=818220768:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.99/0.56 % (205347)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=2242856381:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.99/0.56 % (205343)Instruction limit reached!
% 0.99/0.56 % (205343)------------------------------
% 0.99/0.56 % (205343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.56 % (205343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.56 % (205343)CaDiCaL version: 2.1.3
% 0.99/0.56 % (205343)Termination reason: Instruction limit
% 0.99/0.56 % (205343)Termination phase: Saturation
% 0.99/0.56 % (205343)Time elapsed: 0.004 s
% 0.99/0.56 % (205343)Peak memory usage: 12 MB
% 0.99/0.56 % (205343)Instructions burned: 4 (million)
% 0.99/0.56 % (205342)Instruction limit reached!
% 0.99/0.56 % (205342)------------------------------
% 0.99/0.56 % (205342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.56 % (205342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.56 % (205342)CaDiCaL version: 2.1.3
% 0.99/0.56 % (205342)Termination reason: Instruction limit
% 0.99/0.56 % (205342)Termination phase: Saturation
% 0.99/0.56 % (205342)Time elapsed: 0.017 s
% 0.99/0.56 % (205342)Peak memory usage: 12 MB
% 0.99/0.56 % (205342)Instructions burned: 19 (million)
% 0.99/0.56 % (205345)Instruction limit reached!
% 0.99/0.56 % (205345)------------------------------
% 0.99/0.56 % (205345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.56 % (205345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.56 % (205345)CaDiCaL version: 2.1.3
% 0.99/0.56 % (205345)Termination reason: Instruction limit
% 0.99/0.56 % (205345)Termination phase: Saturation
% 0.99/0.56 % (205345)Time elapsed: 0.022 s
% 0.99/0.56 % (205345)Peak memory usage: 11 MB
% 0.99/0.56 % (205345)Instructions burned: 25 (million)
% 0.99/0.56 % (205341)Instruction limit reached!
% 0.99/0.56 % (205341)------------------------------
% 0.99/0.56 % (205341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.56 % (205341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.56 % (205341)CaDiCaL version: 2.1.3
% 0.99/0.56 % (205341)Termination reason: Instruction limit
% 0.99/0.56 % (205341)Termination phase: Saturation
% 0.99/0.56 % (205341)Time elapsed: 0.042 s
% 0.99/0.56 % (205341)Peak memory usage: 13 MB
% 0.99/0.56 % (205341)Instructions burned: 89 (million)
% 0.99/0.56 % (205355)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4098540647:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.99/0.56 % (205355)Instruction limit reached!
% 0.99/0.56 % (205355)------------------------------
% 0.99/0.56 % (205355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.56 % (205355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.63 % (205355)CaDiCaL version: 2.1.3
% 0.99/0.63 % (205355)Termination reason: Instruction limit
% 0.99/0.63 % (205355)Termination phase: Saturation
% 0.99/0.63 % (205355)Time elapsed: 0.002 s
% 0.99/0.63 % (205355)Peak memory usage: 10 MB
% 0.99/0.63 % (205355)Instructions burned: 2 (million)
% 0.99/0.63 % (205358)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=662444425:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.99/0.63 % (205357)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.99/0.63 % (205356)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=248315893:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.99/0.63 % (205358)Instruction limit reached!
% 0.99/0.63 % (205358)------------------------------
% 0.99/0.63 % (205358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.63 % (205358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.63 % (205358)CaDiCaL version: 2.1.3
% 0.99/0.63 % (205358)Termination reason: Instruction limit
% 0.99/0.63 % (205358)Termination phase: Saturation
% 0.99/0.63 % (205358)Time elapsed: 0.006 s
% 0.99/0.63 % (205358)Peak memory usage: 12 MB
% 0.99/0.63 % (205358)Instructions burned: 13 (million)
% 0.99/0.63 % (205357)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1654516288:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.99/0.63 % (205356)Instruction limit reached!
% 0.99/0.63 % (205356)------------------------------
% 0.99/0.63 % (205356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.63 % (205356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.63 % (205356)CaDiCaL version: 2.1.3
% 0.99/0.63 % (205356)Termination reason: Instruction limit
% 0.99/0.63 % (205356)Termination phase: Saturation
% 0.99/0.63 % (205356)Time elapsed: 0.006 s
% 0.99/0.63 % (205356)Peak memory usage: 12 MB
% 0.99/0.63 % (205356)Instructions burned: 5 (million)
% 0.99/0.63 % (205357)Instruction limit reached!
% 0.99/0.63 % (205357)------------------------------
% 0.99/0.63 % (205357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.63 % (205357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.63 % (205357)CaDiCaL version: 2.1.3
% 0.99/0.63 % (205357)Termination reason: Instruction limit
% 0.99/0.63 % (205357)Termination phase: Saturation
% 0.99/0.63 % (205357)Time elapsed: 0.007 s
% 0.99/0.63 % (205357)Peak memory usage: 12 MB
% 0.99/0.63 % (205357)Instructions burned: 7 (million)
% 0.99/0.63 % (205346)Instruction limit reached!
% 0.99/0.63 % (205346)------------------------------
% 0.99/0.63 % (205346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.99/0.63 % (205346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.99/0.63 % (205346)CaDiCaL version: 2.1.3
% 0.99/0.63 % (205346)Termination reason: Instruction limit
% 0.99/0.63 % (205346)Termination phase: Saturation
% 0.99/0.63 % (205346)Time elapsed: 0.065 s
% 0.99/0.63 % (205346)Peak memory usage: 13 MB
% 0.99/0.63 % (205346)Instructions burned: 75 (million)
% 0.99/0.63 % (205363)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=2790971921:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.99/0.63 % (205360)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.99/0.63 % (205360)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.99/0.63 % (205360)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2270876236: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.99/0.63 % (205366)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.99/0.63 % (205365)lrs+10_1_si=on:cs=on:random_seed=3770028892:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 2.36/0.70 % (205366)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=347647347:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.36/0.70 % (205365)Instruction limit reached!
% 2.36/0.70 % (205365)------------------------------
% 2.36/0.70 % (205365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.70 % (205365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.70 % (205365)CaDiCaL version: 2.1.3
% 2.36/0.70 % (205365)Termination reason: Instruction limit
% 2.36/0.70 % (205365)Termination phase: Saturation
% 2.36/0.70 % (205365)Time elapsed: 0.007 s
% 2.36/0.70 % (205365)Peak memory usage: 12 MB
% 2.36/0.70 % (205365)Instructions burned: 8 (million)
% 2.36/0.70 % (205367)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3514781711:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 2.36/0.70 % (205366)Instruction limit reached!
% 2.36/0.70 % (205366)------------------------------
% 2.36/0.70 % (205366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.70 % (205366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.70 % (205366)CaDiCaL version: 2.1.3
% 2.36/0.70 % (205366)Termination reason: Instruction limit
% 2.36/0.70 % (205366)Termination phase: Saturation
% 2.36/0.70 % (205366)Time elapsed: 0.003 s
% 2.36/0.70 % (205366)Peak memory usage: 11 MB
% 2.36/0.70 % (205366)Instructions burned: 3 (million)
% 2.36/0.70 % (205360)Instruction limit reached!
% 2.36/0.70 % (205360)------------------------------
% 2.36/0.70 % (205360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.70 % (205360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.70 % (205360)CaDiCaL version: 2.1.3
% 2.36/0.70 % (205360)Termination reason: Instruction limit
% 2.36/0.70 % (205360)Termination phase: Saturation
% 2.36/0.70 % (205360)Time elapsed: 0.025 s
% 2.36/0.70 % (205360)Peak memory usage: 12 MB
% 2.36/0.70 % (205360)Instructions burned: 29 (million)
% 2.36/0.70 % (205363)Instruction limit reached!
% 2.36/0.70 % (205363)------------------------------
% 2.36/0.70 % (205363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.70 % (205363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.70 % (205363)CaDiCaL version: 2.1.3
% 2.36/0.70 % (205363)Termination reason: Instruction limit
% 2.36/0.70 % (205363)Termination phase: Saturation
% 2.36/0.70 % (205363)Time elapsed: 0.041 s
% 2.36/0.70 % (205363)Peak memory usage: 13 MB
% 2.36/0.70 % (205363)Instructions burned: 86 (million)
% 2.36/0.70 % (205367)Refutation not found, incomplete strategy
% 2.36/0.70 % (205367)------------------------------
% 2.36/0.70 % (205367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.70 % (205367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.70 % (205367)CaDiCaL version: 2.1.3
% 2.36/0.70 % (205367)Termination reason: Refutation not found, incomplete strategy
% 2.36/0.70 % (205367)Time elapsed: 0.020 s
% 2.36/0.70 % (205367)Peak memory usage: 12 MB
% 2.36/0.70 % (205367)Instructions burned: 22 (million)
% 2.36/0.70 % (205367)------------------------------
% 2.36/0.70 % (205367)------------------------------
% 2.36/0.70 % (205376)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1295049898:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.36/0.70 % (205374)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3910298772:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 2.36/0.70 % (205373)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=375379197:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 2.36/0.70 % (205375)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2332583979:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.36/0.70 % (205347)Instruction limit reached!
% 2.36/0.70 % (205347)------------------------------
% 2.36/0.70 % (205347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.70 % (205347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.70 % (205347)CaDiCaL version: 2.1.3
% 2.36/0.70 % (205347)Termination reason: Instruction limit
% 2.36/0.80 % (205347)Termination phase: Saturation
% 2.36/0.80 % (205347)Time elapsed: 0.137 s
% 2.36/0.80 % (205347)Peak memory usage: 13 MB
% 2.36/0.80 % (205347)Instructions burned: 157 (million)
% 2.36/0.80 % (205375)Instruction limit reached!
% 2.36/0.80 % (205375)------------------------------
% 2.36/0.80 % (205375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.80 % (205375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.80 % (205375)CaDiCaL version: 2.1.3
% 2.36/0.80 % (205375)Termination reason: Instruction limit
% 2.36/0.80 % (205375)Termination phase: Saturation
% 2.36/0.80 % (205375)Time elapsed: 0.013 s
% 2.36/0.80 % (205375)Peak memory usage: 12 MB
% 2.36/0.80 % (205375)Instructions burned: 15 (million)
% 2.36/0.80 % (205377)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=32239770:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 2.36/0.80 % (205374)Instruction limit reached!
% 2.36/0.80 % (205374)------------------------------
% 2.36/0.80 % (205374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.80 % (205374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.80 % (205374)CaDiCaL version: 2.1.3
% 2.36/0.80 % (205374)Termination reason: Instruction limit
% 2.36/0.80 % (205374)Termination phase: Saturation
% 2.36/0.80 % (205374)Time elapsed: 0.023 s
% 2.36/0.80 % (205374)Peak memory usage: 12 MB
% 2.36/0.80 % (205374)Instructions burned: 25 (million)
% 2.36/0.80 % (205377)Instruction limit reached!
% 2.36/0.80 % (205377)------------------------------
% 2.36/0.80 % (205377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.80 % (205377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.80 % (205377)CaDiCaL version: 2.1.3
% 2.36/0.80 % (205377)Termination reason: Instruction limit
% 2.36/0.80 % (205377)Termination phase: Saturation
% 2.36/0.80 % (205377)Time elapsed: 0.013 s
% 2.36/0.80 % (205377)Peak memory usage: 12 MB
% 2.36/0.80 % (205377)Instructions burned: 14 (million)
% 2.36/0.80 % (205382)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3115722856:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 2.36/0.80 % (205382)Instruction limit reached!
% 2.36/0.80 % (205382)------------------------------
% 2.36/0.80 % (205382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.80 % (205382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.80 % (205382)CaDiCaL version: 2.1.3
% 2.36/0.80 % (205382)Termination reason: Instruction limit
% 2.36/0.80 % (205382)Termination phase: Property scanning
% 2.36/0.80 % (205382)Time elapsed: 0.002 s
% 2.36/0.80 % (205382)Peak memory usage: 10 MB
% 2.36/0.80 % (205382)Instructions burned: 2 (million)
% 2.36/0.80 % (205383)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1217200640:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 2.36/0.80 % (205385)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=265729550:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.36/0.80 % (205386)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=2332977904:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.36/0.80 % (205388)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.36/0.80 % (205388)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.36/0.80 % (205383)Instruction limit reached!
% 2.36/0.80 % (205383)------------------------------
% 2.36/0.80 % (205383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.36/0.80 % (205383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.36/0.80 % (205383)CaDiCaL version: 2.1.3
% 2.36/0.80 % (205383)Termination reason: Instruction limit
% 2.36/0.80 % (205383)Termination phase: Saturation
% 2.36/0.80 % (205383)Time elapsed: 0.024 s
% 2.36/0.80 % (205383)Peak memory usage: 12 MB
% 2.36/0.80 % (205383)Instructions burned: 26 (million)
% 2.36/0.80 % (205388)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=3926872036:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.78/0.89 % (205385)Instruction limit reached!
% 2.78/0.89 % (205385)------------------------------
% 2.78/0.89 % (205385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.78/0.89 % (205385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/0.89 % (205385)CaDiCaL version: 2.1.3
% 2.78/0.89 % (205385)Termination reason: Instruction limit
% 2.78/0.89 % (205385)Termination phase: Saturation
% 2.78/0.89 % (205385)Time elapsed: 0.021 s
% 2.78/0.89 % (205385)Peak memory usage: 11 MB
% 2.78/0.89 % (205385)Instructions burned: 24 (million)
% 2.78/0.89 % (205388)Instruction limit reached!
% 2.78/0.89 % (205388)------------------------------
% 2.78/0.89 % (205388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.78/0.89 % (205388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/0.89 % (205388)CaDiCaL version: 2.1.3
% 2.78/0.89 % (205388)Termination reason: Instruction limit
% 2.78/0.89 % (205388)Termination phase: Saturation
% 2.78/0.89 % (205388)Time elapsed: 0.013 s
% 2.78/0.89 % (205388)Peak memory usage: 12 MB
% 2.78/0.89 % (205388)Instructions burned: 14 (million)
% 2.78/0.89 % (205392)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.78/0.89 % (205392)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=2328998373:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.78/0.89 % (205394)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=1043136:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.78/0.89 % (205392)Instruction limit reached!
% 2.78/0.89 % (205392)------------------------------
% 2.78/0.89 % (205392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.78/0.89 % (205392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/0.89 % (205392)CaDiCaL version: 2.1.3
% 2.78/0.89 % (205392)Termination reason: Instruction limit
% 2.78/0.89 % (205392)Termination phase: Saturation
% 2.78/0.89 % (205392)Time elapsed: 0.008 s
% 2.78/0.89 % (205392)Peak memory usage: 12 MB
% 2.78/0.89 % (205392)Instructions burned: 9 (million)
% 2.78/0.89 % (205394)Refutation not found, incomplete strategy
% 2.78/0.89 % (205394)------------------------------
% 2.78/0.89 % (205394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.78/0.89 % (205394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/0.89 % (205394)CaDiCaL version: 2.1.3
% 2.78/0.89 % (205394)Termination reason: Refutation not found, incomplete strategy
% 2.78/0.89 % (205394)Time elapsed: 0.008 s
% 2.78/0.89 % (205386)Instruction limit reached!
% 2.78/0.89 % (205386)------------------------------
% 2.78/0.89 % (205386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.78/0.89 % (205386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/0.89 % (205394)Peak memory usage: 12 MB
% 2.78/0.89 % (205394)Instructions burned: 8 (million)
% 2.78/0.89 % (205386)CaDiCaL version: 2.1.3
% 2.78/0.89 % (205386)Termination reason: Instruction limit
% 2.78/0.89 % (205386)Termination phase: Saturation
% 2.78/0.89 % (205386)Time elapsed: 0.052 s
% 2.78/0.89 % (205386)Peak memory usage: 12 MB
% 2.78/0.89 % (205386)Instructions burned: 60 (million)
% 2.78/0.89 % (205394)------------------------------
% 2.78/0.89 % (205394)------------------------------
% 2.78/0.89 % (205395)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1955414675:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.78/0.89 % (205395)Instruction limit reached!
% 2.78/0.89 % (205395)------------------------------
% 2.78/0.89 % (205395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.78/0.89 % (205395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.78/0.89 % (205395)CaDiCaL version: 2.1.3
% 2.78/0.89 % (205395)Termination reason: Instruction limit
% 2.78/0.89 % (205395)Termination phase: Saturation
% 2.78/0.89 % (205395)Time elapsed: 0.007 s
% 2.78/0.89 % (205395)Peak memory usage: 12 MB
% 2.78/0.89 % (205395)Instructions burned: 7 (million)
% 2.78/0.89 % (205398)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=323438279:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 3.35/0.91 % (205376)Instruction limit reached!
% 3.35/0.91 % (205376)------------------------------
% 3.35/0.91 % (205376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205376)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205376)Termination reason: Instruction limit
% 3.35/0.91 % (205376)Termination phase: Saturation
% 3.35/0.91 % (205376)Time elapsed: 0.148 s
% 3.35/0.91 % (205376)Peak memory usage: 13 MB
% 3.35/0.91 % (205376)Instructions burned: 329 (million)
% 3.35/0.91 % (205399)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2746228200:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 3.35/0.91 % (205400)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=620165525:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 3.35/0.91 % (205398)Refutation not found, incomplete strategy
% 3.35/0.91 % (205398)------------------------------
% 3.35/0.91 % (205398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205398)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205398)Termination reason: Refutation not found, incomplete strategy
% 3.35/0.91 % (205398)Time elapsed: 0.007 s
% 3.35/0.91 % (205398)Peak memory usage: 12 MB
% 3.35/0.91 % (205398)Instructions burned: 7 (million)
% 3.35/0.91 % (205398)------------------------------
% 3.35/0.91 % (205398)------------------------------
% 3.35/0.91 % (205402)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1040660489:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 3.35/0.91 % (205399)Instruction limit reached!
% 3.35/0.91 % (205399)------------------------------
% 3.35/0.91 % (205399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205399)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205399)Termination reason: Instruction limit
% 3.35/0.91 % (205399)Termination phase: Saturation
% 3.35/0.91 % (205399)Time elapsed: 0.018 s
% 3.35/0.91 % (205399)Peak memory usage: 12 MB
% 3.35/0.91 % (205399)Instructions burned: 20 (million)
% 3.35/0.91 % (205404)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2061373020:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 3.35/0.91 % (205407)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1948702542:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 3.35/0.91 % (205409)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.35/0.91 % (205409)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3126846893:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 3.35/0.91 % (205409)Instruction limit reached!
% 3.35/0.91 % (205409)------------------------------
% 3.35/0.91 % (205409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205409)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205409)Termination reason: Instruction limit
% 3.35/0.91 % (205409)Termination phase: Saturation
% 3.35/0.91 % (205409)Time elapsed: 0.007 s
% 3.35/0.91 % (205409)Peak memory usage: 12 MB
% 3.35/0.91 % (205409)Instructions burned: 8 (million)
% 3.35/0.91 % (205407)Instruction limit reached!
% 3.35/0.91 % (205407)------------------------------
% 3.35/0.91 % (205407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205407)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205407)Termination reason: Instruction limit
% 3.35/0.91 % (205407)Termination phase: Saturation
% 3.35/0.91 % (205407)Time elapsed: 0.036 s
% 3.35/0.91 % (205407)Peak memory usage: 12 MB
% 3.35/0.91 % (205407)Instructions burned: 42 (million)
% 3.35/0.91 % (205413)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2574631921:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.35/0.91 % (205373)Instruction limit reached!
% 3.35/0.91 % (205373)------------------------------
% 3.35/0.91 % (205373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205373)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205373)Termination reason: Instruction limit
% 3.35/0.91 % (205373)Termination phase: Saturation
% 3.35/0.91 % (205373)Time elapsed: 0.245 s
% 3.35/0.91 % (205373)Peak memory usage: 13 MB
% 3.35/0.91 % (205373)Instructions burned: 249 (million)
% 3.35/0.91 % (205414)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=634391733:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.35/0.91 % (205416)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.35/0.91 % (205402)Instruction limit reached!
% 3.35/0.91 % (205402)------------------------------
% 3.35/0.91 % (205402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205402)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205402)Termination reason: Instruction limit
% 3.35/0.91 % (205402)Termination phase: Saturation
% 3.35/0.91 % (205402)Time elapsed: 0.117 s
% 3.35/0.91 % (205402)Peak memory usage: 13 MB
% 3.35/0.91 % (205402)Instructions burned: 144 (million)
% 3.35/0.91 % (205416)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2108623281:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 3.35/0.91 % (205416)Instruction limit reached!
% 3.35/0.91 % (205416)------------------------------
% 3.35/0.91 % (205416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205416)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205416)Termination reason: Instruction limit
% 3.35/0.91 % (205416)Termination phase: Saturation
% 3.35/0.91 % (205416)Time elapsed: 0.007 s
% 3.35/0.91 % (205416)Peak memory usage: 12 MB
% 3.35/0.91 % (205416)Instructions burned: 7 (million)
% 3.35/0.91 % (205404)Instruction limit reached!
% 3.35/0.91 % (205404)------------------------------
% 3.35/0.91 % (205404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205404)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205404)Termination reason: Instruction limit
% 3.35/0.91 % (205404)Termination phase: Saturation
% 3.35/0.91 % (205404)Time elapsed: 0.120 s
% 3.35/0.91 % (205404)Peak memory usage: 13 MB
% 3.35/0.91 % (205404)Instructions burned: 195 (million)
% 3.35/0.91 % (205419)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1524792093:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 3.35/0.91 % (205421)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=255358327:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 3.35/0.91 % (205420)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1999879312:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 3.35/0.91 % (205419)Refutation not found, incomplete strategy
% 3.35/0.91 % (205419)------------------------------
% 3.35/0.91 % (205419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205419)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205419)Termination reason: Refutation not found, incomplete strategy
% 3.35/0.91 % (205419)Time elapsed: 0.007 s
% 3.35/0.91 % (205419)Peak memory usage: 12 MB
% 3.35/0.91 % (205419)Instructions burned: 6 (million)
% 3.35/0.91 % (205419)------------------------------
% 3.35/0.91 % (205419)------------------------------
% 3.35/0.91 % (205400) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-205336-205400"...
% 3.35/0.91 % (205420)Instruction limit reached!
% 3.35/0.91 % (205420)------------------------------
% 3.35/0.91 % (205420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205420)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205420)Termination reason: Instruction limit
% 3.35/0.91 % (205420)Termination phase: Saturation
% 3.35/0.91 % (205420)Time elapsed: 0.017 s
% 3.35/0.91 % (205420)Peak memory usage: 13 MB
% 3.35/0.91 % (205420)Instructions burned: 19 (million)
% 3.35/0.91 % (205400)...printing done.
% 3.35/0.91 % (205400)Refutation found. Thanks to Tanya!
% 3.35/0.91 % SZS status Theorem for theBenchmark
% 3.35/0.91 % SZS output start Proof for theBenchmark
% 3.35/0.91 thf(type_def_5, type, a: $tType).
% 3.35/0.91 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 3.35/0.91 thf(func_def_1, type, vNOT: ($o > $o)).
% 3.35/0.91 thf(func_def_2, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.35/0.91 thf(func_def_3, type, vIMP: ($o > $o > $o)).
% 3.35/0.91 thf(func_def_4, type, vAND: ($o > $o > $o)).
% 3.35/0.91 thf(func_def_5, type, db5: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_6, type, db0: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_7, type, vOR: ($o > $o > $o)).
% 3.35/0.91 thf(func_def_8, type, db8: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_9, type, db1: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_10, type, db2: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_11, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.35/0.91 thf(func_def_12, type, db9: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_13, type, db6: !>[X0: $tType]:(X0)).
% 3.35/0.91 thf(func_def_14, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.35/0.91 thf(func_def_17, type, sK0: ((a > a > $o) > $o)).
% 3.35/0.91 thf(func_def_18, type, sK1: (a > a > $o)).
% 3.35/0.91 thf(func_def_19, type, sK2: (a > a > $o)).
% 3.35/0.91 thf(func_def_20, type, sK3: a).
% 3.35/0.91 thf(func_def_21, type, sK4: a).
% 3.35/0.91 thf(func_def_23, type, sK6: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_24, type, sK7: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_25, type, sK8: (a > a > $o)).
% 3.35/0.91 thf(func_def_26, type, sK9: (a > a > a > a > $o)).
% 3.35/0.91 thf(func_def_27, type, sK10: (a > a > a > a > $o)).
% 3.35/0.91 thf(func_def_28, type, sK11: (a > a > $o)).
% 3.35/0.91 thf(func_def_29, type, sK12: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_30, type, sK13: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_31, type, sK14: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_32, type, sK15: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_33, type, sK16: ((a > a > $o) > a)).
% 3.35/0.91 thf(func_def_34, type, sK17: ((a > a > $o) > a)).
% 3.35/0.91 thf(f1,conjecture,(
% 3.35/0.91 ! [X1 : (a > a > $o),X2 : (a > a > $o),X0 : ((a > a > $o) > $o)] : ((^[X3 : a, X4 : a] : (! [X5 : (a > a > $o)] : ((! [X7 : a,X6 : a] : ((! [X8 : (a > a > $o)] : (((X0 @ X8) & ! [X10 : a,X9 : a] : ((X2 @ X9 @ X10) => (X8 @ X9 @ X10))) => (X8 @ X6 @ X7)) | ! [X8 : (a > a > $o)] : ((! [X9 : a,X10 : a] : ((X1 @ X9 @ X10) => (X8 @ X9 @ X10)) & (X0 @ X8)) => (X8 @ X6 @ X7))) => (X5 @ X6 @ X7)) & (X0 @ X5)) => (X5 @ X3 @ X4)))) = (^[X3 : a, X4 : a] : (! [X5 : (a > a > $o)] : (((X0 @ X5) & ! [X6 : a,X7 : a] : (((X2 @ X6 @ X7) | (X1 @ X6 @ X7)) => (X5 @ X6 @ X7))) => (X5 @ X3 @ X4)))))),
% 3.35/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM252_pme)).
% 3.35/0.91 thf(f2,negated_conjecture,(
% 3.35/0.91 ~ ! [X1 : (a > a > $o),X2 : (a > a > $o),X0 : ((a > a > $o) > $o)] : ((^[X3 : a, X4 : a] : (! [X5 : (a > a > $o)] : ((! [X7 : a,X6 : a] : ((! [X8 : (a > a > $o)] : (((X0 @ X8) & ! [X10 : a,X9 : a] : ((X2 @ X9 @ X10) => (X8 @ X9 @ X10))) => (X8 @ X6 @ X7)) | ! [X8 : (a > a > $o)] : ((! [X9 : a,X10 : a] : ((X1 @ X9 @ X10) => (X8 @ X9 @ X10)) & (X0 @ X8)) => (X8 @ X6 @ X7))) => (X5 @ X6 @ X7)) & (X0 @ X5)) => (X5 @ X3 @ X4)))) = (^[X3 : a, X4 : a] : (! [X5 : (a > a > $o)] : (((X0 @ X5) & ! [X6 : a,X7 : a] : (((X2 @ X6 @ X7) | (X1 @ X6 @ X7)) => (X5 @ X6 @ X7))) => (X5 @ X3 @ X4)))))),
% 3.35/0.91 inference(negated_conjecture,[status(cth)],[f1])).
% 3.35/0.91 thf(f3,plain,(
% 3.35/0.91 ~ ! [X0 : (a > a > $o),X1 : (a > a > $o),X2 : ((a > a > $o) > $o)] : ((^[X3 : a, X4 : a] : (! [X5 : (a > a > $o)] : ((! [X6 : a,X7 : a] : ((! [X8 : (a > a > $o)] : (((X2 @ X8) & ! [X9 : a,X10 : a] : ((X1 @ X10 @ X9) => (X8 @ X10 @ X9))) => (X8 @ X7 @ X6)) | ! [X11 : (a > a > $o)] : ((! [X12 : a,X13 : a] : ((X0 @ X12 @ X13) => (X11 @ X12 @ X13)) & (X2 @ X11)) => (X11 @ X7 @ X6))) => (X5 @ X7 @ X6)) & (X2 @ X5)) => (X5 @ X3 @ X4)))) = (^[X14 : a, X15 : a] : (! [X16 : (a > a > $o)] : (((X2 @ X16) & ! [X17 : a,X18 : a] : (((X1 @ X17 @ X18) | (X0 @ X17 @ X18)) => (X16 @ X17 @ X18))) => (X16 @ X14 @ X15)))))),
% 3.35/0.91 inference(rectify,[],[f2])).
% 3.35/0.91 thf(f4,plain,(
% 3.35/0.91 ($true = ((~ (!! @ ((a > a > $o) > $o) @ (^[Y0 : (a > a > $o) > $o]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: ((^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((Y0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((Y0 @ Y8) & (!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y2 @ Y10 @ Y9) => (Y8 @ Y10 @ Y9))))))) => (Y8 @ Y6 @ Y7)))) | (!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y1 @ Y9 @ Y10) => (Y8 @ Y9 @ Y10)))))) & (Y0 @ Y8)) => (Y8 @ Y6 @ Y7))))) => (Y5 @ Y6 @ Y7))))))) => (Y5 @ Y3 @ Y4))))))) = (^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((Y2 @ Y7 @ Y6) | (Y1 @ Y7 @ Y6)) => (Y5 @ Y7 @ Y6)))))) & (Y0 @ Y5)) => (Y5 @ Y3 @ Y4)))))))))))))))))),
% 3.35/0.91 inference(fool_elimination,[],[f3])).
% 3.35/0.91 thf(f5,plain,(
% 3.35/0.91 ($true = ((~ (!! @ ((a > a > $o) > $o) @ (^[Y0 : (a > a > $o) > $o]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: ((^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((Y0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((Y0 @ Y8) & (!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y2 @ Y10 @ Y9) => (Y8 @ Y10 @ Y9))))))) => (Y8 @ Y6 @ Y7)))) | (!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y1 @ Y9 @ Y10) => (Y8 @ Y9 @ Y10)))))) & (Y0 @ Y8)) => (Y8 @ Y6 @ Y7))))) => (Y5 @ Y6 @ Y7))))))) => (Y5 @ Y3 @ Y4))))))) = (^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((Y2 @ Y7 @ Y6) | (Y1 @ Y7 @ Y6)) => (Y5 @ Y7 @ Y6)))))) & (Y0 @ Y5)) => (Y5 @ Y3 @ Y4)))))))))))))))))),
% 3.35/0.91 inference(cnf_transformation,[],[f4])).
% 3.35/0.91 thf(f7,definition,(
% 3.35/0.91 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.35/0.91 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.35/0.91 thf(f8,plain,(
% 3.35/0.91 (((!! @ ((a > a > $o) > $o) @ (^[Y0 : (a > a > $o) > $o]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: ((^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((Y0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((Y0 @ Y8) & (!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y2 @ Y10 @ Y9) => (Y8 @ Y10 @ Y9))))))) => (Y8 @ Y6 @ Y7)))) | (!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y1 @ Y9 @ Y10) => (Y8 @ Y9 @ Y10)))))) & (Y0 @ Y8)) => (Y8 @ Y6 @ Y7))))) => (Y5 @ Y6 @ Y7))))))) => (Y5 @ Y3 @ Y4))))))) = (^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((Y2 @ Y7 @ Y6) | (Y1 @ Y7 @ Y6)) => (Y5 @ Y7 @ Y6)))))) & (Y0 @ Y5)) => (Y5 @ Y3 @ Y4))))))))))))))) = $false)),
% 3.35/0.91 inference(not_proxy_clausification,[],[f5])).
% 3.35/0.91 thf(f9,plain,(
% 3.35/0.91 ((((^[Y0 : (a > a > $o) > $o]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: ((^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((Y0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((Y0 @ Y8) & (!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y2 @ Y10 @ Y9) => (Y8 @ Y10 @ Y9))))))) => (Y8 @ Y6 @ Y7)))) | (!! @ (a > a > $o) @ (^[Y8 : a > a > $o]: (((!! @ a @ (^[Y9 : a]: (!! @ a @ (^[Y10 : a]: ((Y1 @ Y9 @ Y10) => (Y8 @ Y9 @ Y10)))))) & (Y0 @ Y8)) => (Y8 @ Y6 @ Y7))))) => (Y5 @ Y6 @ Y7))))))) => (Y5 @ Y3 @ Y4))))))) = (^[Y3 : a]: ((^[Y4 : a]: (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: (((Y2 @ Y7 @ Y6) | (Y1 @ Y7 @ Y6)) => (Y5 @ Y7 @ Y6)))))) & (Y0 @ Y5)) => (Y5 @ Y3 @ Y4))))))))))))) @ sK0)) = $false)),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f8])).
% 3.35/0.91 thf(f10,plain,(
% 3.35/0.91 ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: ((^[Y2 : a]: ((^[Y3 : a]: (!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((sK0 @ Y4) & (!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: (((!! @ (a > a > $o) @ (^[Y7 : a > a > $o]: (((sK0 @ Y7) & (!! @ a @ (^[Y8 : a]: (!! @ a @ (^[Y9 : a]: ((Y1 @ Y9 @ Y8) => (Y7 @ Y9 @ Y8))))))) => (Y7 @ Y5 @ Y6)))) | (!! @ (a > a > $o) @ (^[Y7 : a > a > $o]: (((!! @ a @ (^[Y8 : a]: (!! @ a @ (^[Y9 : a]: ((Y0 @ Y8 @ Y9) => (Y7 @ Y8 @ Y9)))))) & (sK0 @ Y7)) => (Y7 @ Y5 @ Y6))))) => (Y4 @ Y5 @ Y6))))))) => (Y4 @ Y2 @ Y3))))))) = (^[Y2 : a]: ((^[Y3 : a]: (!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: (((Y1 @ Y6 @ Y5) | (Y0 @ Y6 @ Y5)) => (Y4 @ Y6 @ Y5)))))) & (sK0 @ Y4)) => (Y4 @ Y2 @ Y3))))))))))))))),
% 3.35/0.91 inference(beta-eta_normalization,[],[f9])).
% 3.35/0.91 thf(f11,plain,(
% 3.35/0.91 ((((^[Y0 : a > a > $o]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: ((^[Y2 : a]: ((^[Y3 : a]: (!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((sK0 @ Y4) & (!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: (((!! @ (a > a > $o) @ (^[Y7 : a > a > $o]: (((sK0 @ Y7) & (!! @ a @ (^[Y8 : a]: (!! @ a @ (^[Y9 : a]: ((Y1 @ Y9 @ Y8) => (Y7 @ Y9 @ Y8))))))) => (Y7 @ Y5 @ Y6)))) | (!! @ (a > a > $o) @ (^[Y7 : a > a > $o]: (((!! @ a @ (^[Y8 : a]: (!! @ a @ (^[Y9 : a]: ((Y0 @ Y8 @ Y9) => (Y7 @ Y8 @ Y9)))))) & (sK0 @ Y7)) => (Y7 @ Y5 @ Y6))))) => (Y4 @ Y5 @ Y6))))))) => (Y4 @ Y2 @ Y3))))))) = (^[Y2 : a]: ((^[Y3 : a]: (!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: (((Y1 @ Y6 @ Y5) | (Y0 @ Y6 @ Y5)) => (Y4 @ Y6 @ Y5)))))) & (sK0 @ Y4)) => (Y4 @ Y2 @ Y3))))))))))) @ sK1)) = $false)),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f10])).
% 3.35/0.91 thf(f12,plain,(
% 3.35/0.91 (((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: ((^[Y1 : a]: ((^[Y2 : a]: (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: (((!! @ (a > a > $o) @ (^[Y6 : a > a > $o]: (((sK0 @ Y6) & (!! @ a @ (^[Y7 : a]: (!! @ a @ (^[Y8 : a]: ((Y0 @ Y8 @ Y7) => (Y6 @ Y8 @ Y7))))))) => (Y6 @ Y4 @ Y5)))) | (!! @ (a > a > $o) @ (^[Y6 : a > a > $o]: (((!! @ a @ (^[Y7 : a]: (!! @ a @ (^[Y8 : a]: ((sK1 @ Y7 @ Y8) => (Y6 @ Y7 @ Y8)))))) & (sK0 @ Y6)) => (Y6 @ Y4 @ Y5))))) => (Y3 @ Y4 @ Y5))))))) => (Y3 @ Y1 @ Y2))))))) = (^[Y1 : a]: ((^[Y2 : a]: (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: (((Y0 @ Y5 @ Y4) | (sK1 @ Y5 @ Y4)) => (Y3 @ Y5 @ Y4)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))))))))) = $false)),
% 3.35/0.91 inference(beta-eta_normalization,[],[f11])).
% 3.35/0.91 thf(f24,plain,(
% 3.35/0.91 ((((^[Y0 : a > a > $o]: ((^[Y1 : a]: ((^[Y2 : a]: (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: (((!! @ (a > a > $o) @ (^[Y6 : a > a > $o]: (((sK0 @ Y6) & (!! @ a @ (^[Y7 : a]: (!! @ a @ (^[Y8 : a]: ((Y0 @ Y8 @ Y7) => (Y6 @ Y8 @ Y7))))))) => (Y6 @ Y4 @ Y5)))) | (!! @ (a > a > $o) @ (^[Y6 : a > a > $o]: (((!! @ a @ (^[Y7 : a]: (!! @ a @ (^[Y8 : a]: ((sK1 @ Y7 @ Y8) => (Y6 @ Y7 @ Y8)))))) & (sK0 @ Y6)) => (Y6 @ Y4 @ Y5))))) => (Y3 @ Y4 @ Y5))))))) => (Y3 @ Y1 @ Y2))))))) = (^[Y1 : a]: ((^[Y2 : a]: (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: (((Y0 @ Y5 @ Y4) | (sK1 @ Y5 @ Y4)) => (Y3 @ Y5 @ Y4)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))))))) @ sK2)) = $false)),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f12])).
% 3.35/0.91 thf(f27,plain,(
% 3.35/0.91 ($false = (((^[Y0 : a]: ((^[Y1 : a]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: (((!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((sK0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: ((sK2 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6))))))) => (Y5 @ Y3 @ Y4)))) | (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: ((sK1 @ Y6 @ Y7) => (Y5 @ Y6 @ Y7)))))) & (sK0 @ Y5)) => (Y5 @ Y3 @ Y4))))) => (Y2 @ Y3 @ Y4))))))) => (Y2 @ Y0 @ Y1))))))) = (^[Y0 : a]: ((^[Y1 : a]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: (((sK2 @ Y4 @ Y3) | (sK1 @ Y4 @ Y3)) => (Y2 @ Y4 @ Y3)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))))))))),
% 3.35/0.91 inference(beta-eta_normalization,[],[f24])).
% 3.35/0.91 thf(f28,plain,(
% 3.35/0.91 ((^[Y0 : a]: ((^[Y1 : a]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: (((!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((sK0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: ((sK2 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6))))))) => (Y5 @ Y3 @ Y4)))) | (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: ((sK1 @ Y6 @ Y7) => (Y5 @ Y6 @ Y7)))))) & (sK0 @ Y5)) => (Y5 @ Y3 @ Y4))))) => (Y2 @ Y3 @ Y4))))))) => (Y2 @ Y0 @ Y1))))))) != (^[Y0 : a]: ((^[Y1 : a]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: (((sK2 @ Y4 @ Y3) | (sK1 @ Y4 @ Y3)) => (Y2 @ Y4 @ Y3)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))))))),
% 3.35/0.91 inference(equality_proxy_clausification,[],[f27])).
% 3.35/0.91 thf(f29,plain,(
% 3.35/0.91 ((((^[Y0 : a]: ((^[Y1 : a]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: (((!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((sK0 @ Y5) & (!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: ((sK2 @ Y7 @ Y6) => (Y5 @ Y7 @ Y6))))))) => (Y5 @ Y3 @ Y4)))) | (!! @ (a > a > $o) @ (^[Y5 : a > a > $o]: (((!! @ a @ (^[Y6 : a]: (!! @ a @ (^[Y7 : a]: ((sK1 @ Y6 @ Y7) => (Y5 @ Y6 @ Y7)))))) & (sK0 @ Y5)) => (Y5 @ Y3 @ Y4))))) => (Y2 @ Y3 @ Y4))))))) => (Y2 @ Y0 @ Y1))))))) @ sK3)) != (((^[Y0 : a]: ((^[Y1 : a]: (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: (((sK2 @ Y4 @ Y3) | (sK1 @ Y4 @ Y3)) => (Y2 @ Y4 @ Y3)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))))) @ sK3)))),
% 3.35/0.91 inference(negative_extensionality,[],[f28])).
% 3.35/0.91 thf(f30,plain,(
% 3.35/0.91 ((^[Y0 : a]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((sK0 @ Y1) & (!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: (((!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((sK0 @ Y4) & (!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: ((sK2 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5))))))) => (Y4 @ Y2 @ Y3)))) | (!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: ((sK1 @ Y5 @ Y6) => (Y4 @ Y5 @ Y6)))))) & (sK0 @ Y4)) => (Y4 @ Y2 @ Y3))))) => (Y1 @ Y2 @ Y3))))))) => (Y1 @ sK3 @ Y0))))) != (^[Y0 : a]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: (((sK2 @ Y3 @ Y2) | (sK1 @ Y3 @ Y2)) => (Y1 @ Y3 @ Y2)))))) & (sK0 @ Y1)) => (Y1 @ sK3 @ Y0))))))),
% 3.35/0.91 inference(beta-eta_normalization,[],[f29])).
% 3.35/0.91 thf(f31,plain,(
% 3.35/0.91 ((((^[Y0 : a]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((sK0 @ Y1) & (!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: (((!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((sK0 @ Y4) & (!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: ((sK2 @ Y6 @ Y5) => (Y4 @ Y6 @ Y5))))))) => (Y4 @ Y2 @ Y3)))) | (!! @ (a > a > $o) @ (^[Y4 : a > a > $o]: (((!! @ a @ (^[Y5 : a]: (!! @ a @ (^[Y6 : a]: ((sK1 @ Y5 @ Y6) => (Y4 @ Y5 @ Y6)))))) & (sK0 @ Y4)) => (Y4 @ Y2 @ Y3))))) => (Y1 @ Y2 @ Y3))))))) => (Y1 @ sK3 @ Y0))))) @ sK4)) != (((^[Y0 : a]: (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: (((sK2 @ Y3 @ Y2) | (sK1 @ Y3 @ Y2)) => (Y1 @ Y3 @ Y2)))))) & (sK0 @ Y1)) => (Y1 @ sK3 @ Y0))))) @ sK4)))),
% 3.35/0.91 inference(negative_extensionality,[],[f30])).
% 3.35/0.91 thf(f32,plain,(
% 3.35/0.91 (((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4))))) != ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 inference(beta-eta_normalization,[],[f31])).
% 3.35/0.91 thf(f33,plain,(
% 3.35/0.91 ($true = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | ($true = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 inference(xor_proxy_clausification,[],[f32])).
% 3.35/0.91 thf(f34,plain,(
% 3.35/0.91 ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 inference(xor_proxy_clausification,[],[f32])).
% 3.35/0.91 thf(f36,definition,(
% 3.35/0.91 spl5_1 <=> ($true = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 3.35/0.91 thf(f37,plain,(
% 3.35/0.91 ($true != ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | spl5_1),
% 3.35/0.91 inference(avatar_component_clause,[],[f36])).
% 3.35/0.91 thf(f38,plain,(
% 3.35/0.91 ($true = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | ~spl5_1),
% 3.35/0.91 inference(avatar_component_clause,[],[f36])).
% 3.35/0.91 thf(f40,definition,(
% 3.35/0.91 spl5_2 <=> ($true = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 3.35/0.91 thf(f42,plain,(
% 3.35/0.91 ($true = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4)))))) | ~spl5_2),
% 3.35/0.91 inference(avatar_component_clause,[],[f40])).
% 3.35/0.91 thf(f43,plain,(
% 3.35/0.91 spl5_1 | spl5_2),
% 3.35/0.91 inference(avatar_split_clause,[],[f33,f40,f36])).
% 3.35/0.91 thf(f45,definition,(
% 3.35/0.91 spl5_3 <=> ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 3.35/0.91 thf(f47,plain,(
% 3.35/0.91 ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | ~spl5_3),
% 3.35/0.91 inference(avatar_component_clause,[],[f45])).
% 3.35/0.91 thf(f49,definition,(
% 3.35/0.91 spl5_4 <=> ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))))))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 3.35/0.91 thf(f51,plain,(
% 3.35/0.91 ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4)))))) | ~spl5_4),
% 3.35/0.91 inference(avatar_component_clause,[],[f49])).
% 3.35/0.91 thf(f52,plain,(
% 3.35/0.91 spl5_3 | spl5_4),
% 3.35/0.91 inference(avatar_split_clause,[],[f34,f49,f45])).
% 3.35/0.91 thf(f53,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = (((^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))) @ X1)))) ) | ~spl5_2),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f42])).
% 3.35/0.91 thf(f54,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (X1 @ Y1 @ Y0)))))) & (sK0 @ X1)) => (X1 @ sK3 @ sK4))))) ) | ~spl5_2),
% 3.35/0.91 inference(beta-eta_normalization,[],[f53])).
% 3.35/0.91 thf(f55,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (X1 @ Y1 @ Y0)))))) & (sK0 @ X1))) = $false)) ) | ~spl5_2),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f54])).
% 3.35/0.91 thf(f56,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (X1 @ Y1 @ Y0))))))) = $false) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_2),
% 3.35/0.91 inference(and_proxy_clausification,[],[f55])).
% 3.35/0.91 thf(f57,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : ((((sK0 @ X1)) = $false) | ((((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (X1 @ Y1 @ Y0))))) @ (sK6 @ X1))) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_2),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f56])).
% 3.35/0.91 thf(f60,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: (((sK2 @ Y0 @ (sK6 @ X1)) | (sK1 @ Y0 @ (sK6 @ X1))) => (X1 @ Y0 @ (sK6 @ X1)))))) = $false) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_2),
% 3.35/0.91 inference(beta-eta_normalization,[],[f57])).
% 3.35/0.91 thf(f61,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (((((^[Y0 : a]: (((sK2 @ Y0 @ (sK6 @ X1)) | (sK1 @ Y0 @ (sK6 @ X1))) => (X1 @ Y0 @ (sK6 @ X1)))) @ (sK7 @ X1))) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false)) ) | ~spl5_2),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f60])).
% 3.35/0.91 thf(f64,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | (((((sK2 @ (sK7 @ X1) @ (sK6 @ X1)) | (sK1 @ (sK7 @ X1) @ (sK6 @ X1))) => (X1 @ (sK7 @ X1) @ (sK6 @ X1)))) = $false)) ) | ~spl5_2),
% 3.35/0.91 inference(beta-eta_normalization,[],[f61])).
% 3.35/0.91 thf(f65,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($false = ((X1 @ (sK7 @ X1) @ (sK6 @ X1)))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_2),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f64])).
% 3.35/0.91 thf(f66,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ($true = (((sK2 @ (sK7 @ X1) @ (sK6 @ X1)) | (sK1 @ (sK7 @ X1) @ (sK6 @ X1)))))) ) | ~spl5_2),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f64])).
% 3.35/0.91 thf(f67,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((sK1 @ (sK7 @ X1) @ (sK6 @ X1)))) | (((sK0 @ X1)) = $false) | (((sK2 @ (sK7 @ X1) @ (sK6 @ X1))) = $true) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_2),
% 3.35/0.91 inference(or_proxy_clausification,[],[f66])).
% 3.35/0.91 thf(f68,plain,(
% 3.35/0.91 ((((^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4))) @ sK8)) = $false) | ~spl5_3),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f47])).
% 3.35/0.91 thf(f71,plain,(
% 3.35/0.91 (((((sK0 @ sK8) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (sK8 @ Y0 @ Y1))))))) => (sK8 @ sK3 @ sK4))) = $false) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f68])).
% 3.35/0.91 thf(f72,plain,(
% 3.35/0.91 ($false = ((sK8 @ sK3 @ sK4))) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f71])).
% 3.35/0.91 thf(f73,plain,(
% 3.35/0.91 ($true = (((sK0 @ sK8) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (sK8 @ Y0 @ Y1))))))))) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f71])).
% 3.35/0.91 thf(f74,plain,(
% 3.35/0.91 (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (sK8 @ Y0 @ Y1))))))) = $true) | ~spl5_3),
% 3.35/0.91 inference(and_proxy_clausification,[],[f73])).
% 3.35/0.91 thf(f75,plain,(
% 3.35/0.91 ($true = ((sK0 @ sK8))) | ~spl5_3),
% 3.35/0.91 inference(and_proxy_clausification,[],[f73])).
% 3.35/0.91 thf(f129,plain,(
% 3.35/0.91 ($true = $false) | (~spl5_1 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f38,f47])).
% 3.35/0.91 thf(f130,plain,(
% 3.35/0.91 $false | (~spl5_1 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f129])).
% 3.35/0.91 thf(f131,plain,(
% 3.35/0.91 ~spl5_1 | ~spl5_3),
% 3.35/0.91 inference(avatar_contradiction_clause,[],[f130])).
% 3.35/0.91 thf(f255,plain,(
% 3.35/0.91 ( ! [X1 : a] : (((((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (sK8 @ Y0 @ Y1))))) @ X1)) = $true)) ) | ~spl5_3),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f74])).
% 3.35/0.91 thf(f256,plain,(
% 3.35/0.91 ( ! [X1 : a] : (($true = ((!! @ a @ (^[Y0 : a]: (((!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((sK0 @ Y1) & (!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK2 @ Y3 @ Y2) => (Y1 @ Y3 @ Y2))))))) => (Y1 @ X1 @ Y0)))) | (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK1 @ Y2 @ Y3) => (Y1 @ Y2 @ Y3)))))) & (sK0 @ Y1)) => (Y1 @ X1 @ Y0))))) => (sK8 @ X1 @ Y0))))))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f255])).
% 3.35/0.91 thf(f257,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = (((^[Y0 : a]: (((!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((sK0 @ Y1) & (!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK2 @ Y3 @ Y2) => (Y1 @ Y3 @ Y2))))))) => (Y1 @ X1 @ Y0)))) | (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK1 @ Y2 @ Y3) => (Y1 @ Y2 @ Y3)))))) & (sK0 @ Y1)) => (Y1 @ X1 @ Y0))))) => (sK8 @ X1 @ Y0))) @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f256])).
% 3.35/0.91 thf(f258,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ X1 @ X2)))) | (!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ X1 @ X2))))) => (sK8 @ X1 @ X2))))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f257])).
% 3.35/0.91 thf(f259,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ X1 @ X2)))) | (!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ X1 @ X2)))))) = $false)) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f258])).
% 3.35/0.91 thf(f260,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ X1 @ X2))))) = $false) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(or_proxy_clausification,[],[f259])).
% 3.35/0.91 thf(f261,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ X1 @ X2)))))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(or_proxy_clausification,[],[f259])).
% 3.35/0.91 thf(f262,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | ($false = (((^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ X1 @ X2))) @ (sK9 @ X1 @ X2))))) ) | ~spl5_3),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f260])).
% 3.35/0.91 thf(f264,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | (((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (sK9 @ X1 @ X2 @ Y0 @ Y1)))))) & (sK0 @ (sK9 @ X1 @ X2))) => (sK9 @ X1 @ X2 @ X1 @ X2))) = $false)) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f262])).
% 3.35/0.91 thf(f266,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : ((((sK9 @ X1 @ X2 @ X1 @ X2)) = $false) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f264])).
% 3.35/0.91 thf(f267,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | ($true = (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (sK9 @ X1 @ X2 @ Y0 @ Y1)))))) & (sK0 @ (sK9 @ X1 @ X2)))))) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f264])).
% 3.35/0.91 thf(f269,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (sK9 @ X1 @ X2 @ Y0 @ Y1))))))) = $true) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(and_proxy_clausification,[],[f267])).
% 3.35/0.91 thf(f272,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | ((((^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ X1 @ X2))) @ (sK10 @ X1 @ X2))) = $false)) ) | ~spl5_3),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f261])).
% 3.35/0.91 thf(f274,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : ((((((sK0 @ (sK10 @ X1 @ X2)) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (sK10 @ X1 @ X2 @ Y1 @ Y0))))))) => (sK10 @ X1 @ X2 @ X1 @ X2))) = $false) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f272])).
% 3.35/0.91 thf(f276,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : ((((sK10 @ X1 @ X2 @ X1 @ X2)) = $false) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f274])).
% 3.35/0.91 thf(f277,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = (((sK0 @ (sK10 @ X1 @ X2)) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (sK10 @ X1 @ X2 @ Y1 @ Y0))))))))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f274])).
% 3.35/0.91 thf(f278,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (sK10 @ X1 @ X2 @ Y1 @ Y0)))))))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(and_proxy_clausification,[],[f277])).
% 3.35/0.91 thf(f282,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | ($true = (((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (sK9 @ X1 @ X2 @ Y0 @ Y1))))) @ X3)))) ) | ~spl5_3),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f269])).
% 3.35/0.91 thf(f283,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a] : (($true = ((!! @ a @ (^[Y0 : a]: ((sK1 @ X3 @ Y0) => (sK9 @ X1 @ X2 @ X3 @ Y0)))))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f282])).
% 3.35/0.91 thf(f284,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a,X4 : a] : (($true = ((sK8 @ X1 @ X2))) | ($true = (((^[Y0 : a]: ((sK1 @ X3 @ Y0) => (sK9 @ X1 @ X2 @ X3 @ Y0))) @ X4)))) ) | ~spl5_3),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f283])).
% 3.35/0.91 thf(f285,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a,X4 : a] : (($true = (((sK1 @ X3 @ X4) => (sK9 @ X1 @ X2 @ X3 @ X4)))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f284])).
% 3.35/0.91 thf(f286,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a,X4 : a] : ((((sK9 @ X1 @ X2 @ X3 @ X4)) = $true) | ($true = ((sK8 @ X1 @ X2))) | (((sK1 @ X3 @ X4)) = $false)) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f285])).
% 3.35/0.91 thf(f287,plain,(
% 3.35/0.91 ( ! [X0 : a,X1 : a] : ((((sK8 @ X0 @ X1)) = $true) | (((sK8 @ X0 @ X1)) = $true) | ($true = $false) | ($false = ((sK1 @ X0 @ X1)))) ) | ~spl5_3),
% 3.35/0.91 inference(superposition,[],[f286,f266])).
% 3.35/0.91 thf(f292,plain,(
% 3.35/0.91 ( ! [X0 : a,X1 : a] : (($false = ((sK1 @ X0 @ X1))) | ($true = $false) | (((sK8 @ X0 @ X1)) = $true)) ) | ~spl5_3),
% 3.35/0.91 inference(duplicate_literal_removal,[],[f287])).
% 3.35/0.91 thf(f293,plain,(
% 3.35/0.91 ( ! [X0 : a,X1 : a] : (($false = ((sK1 @ X0 @ X1))) | (((sK8 @ X0 @ X1)) = $true)) ) | ~spl5_3),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f292])).
% 3.35/0.91 thf(f297,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a] : (($true = ((sK8 @ X1 @ X2))) | ($true = (((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (sK10 @ X1 @ X2 @ Y1 @ Y0))))) @ X3)))) ) | ~spl5_3),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f278])).
% 3.35/0.91 thf(f298,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a] : (($true = ((!! @ a @ (^[Y0 : a]: ((sK2 @ Y0 @ X3) => (sK10 @ X1 @ X2 @ Y0 @ X3)))))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f297])).
% 3.35/0.91 thf(f299,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a,X4 : a] : (($true = (((^[Y0 : a]: ((sK2 @ Y0 @ X3) => (sK10 @ X1 @ X2 @ Y0 @ X3))) @ X4))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f298])).
% 3.35/0.91 thf(f300,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a,X4 : a] : (($true = ((sK8 @ X1 @ X2))) | ($true = (((sK2 @ X4 @ X3) => (sK10 @ X1 @ X2 @ X4 @ X3))))) ) | ~spl5_3),
% 3.35/0.91 inference(beta-eta_normalization,[],[f299])).
% 3.35/0.91 thf(f301,plain,(
% 3.35/0.91 ( ! [X2 : a,X3 : a,X1 : a,X4 : a] : (($true = ((sK10 @ X1 @ X2 @ X4 @ X3))) | ($false = ((sK2 @ X4 @ X3))) | ($true = ((sK8 @ X1 @ X2)))) ) | ~spl5_3),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f300])).
% 3.35/0.91 thf(f302,plain,(
% 3.35/0.91 ( ! [X0 : a,X1 : a] : ((((sK8 @ X0 @ X1)) = $true) | ($true = $false) | (((sK2 @ X0 @ X1)) = $false) | (((sK8 @ X0 @ X1)) = $true)) ) | ~spl5_3),
% 3.35/0.91 inference(superposition,[],[f301,f276])).
% 3.35/0.91 thf(f306,plain,(
% 3.35/0.91 ( ! [X0 : a,X1 : a] : ((((sK2 @ X0 @ X1)) = $false) | ($true = $false) | (((sK8 @ X0 @ X1)) = $true)) ) | ~spl5_3),
% 3.35/0.91 inference(duplicate_literal_removal,[],[f302])).
% 3.35/0.91 thf(f307,plain,(
% 3.35/0.91 ( ! [X0 : a,X1 : a] : ((((sK8 @ X0 @ X1)) = $true) | (((sK2 @ X0 @ X1)) = $false)) ) | ~spl5_3),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f306])).
% 3.35/0.91 thf(f315,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((sK8 @ (sK7 @ X0) @ (sK6 @ X0))) = $true) | ($true = ((sK2 @ (sK7 @ X0) @ (sK6 @ X0)))) | ($true = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false)) ) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(superposition,[],[f67,f293])).
% 3.35/0.91 thf(f318,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK2 @ (sK7 @ X0) @ (sK6 @ X0)))) | (((sK0 @ X0)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK8 @ (sK7 @ X0) @ (sK6 @ X0))) = $true)) ) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f315])).
% 3.35/0.91 thf(f336,plain,(
% 3.35/0.91 ((((^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((sK2 @ Y2 @ Y1) | (sK1 @ Y2 @ Y1)) => (Y0 @ Y2 @ Y1)))))) & (sK0 @ Y0)) => (Y0 @ sK3 @ sK4))) @ sK11)) = $false) | ~spl5_4),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f51])).
% 3.35/0.91 thf(f338,plain,(
% 3.35/0.91 (((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (sK11 @ Y1 @ Y0)))))) & (sK0 @ sK11)) => (sK11 @ sK3 @ sK4))) = $false) | ~spl5_4),
% 3.35/0.91 inference(beta-eta_normalization,[],[f336])).
% 3.35/0.91 thf(f340,plain,(
% 3.35/0.91 (((sK11 @ sK3 @ sK4)) = $false) | ~spl5_4),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f338])).
% 3.35/0.91 thf(f341,plain,(
% 3.35/0.91 ($true = (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (sK11 @ Y1 @ Y0)))))) & (sK0 @ sK11)))) | ~spl5_4),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f338])).
% 3.35/0.91 thf(f342,plain,(
% 3.35/0.91 ($true = ((sK0 @ sK11))) | ~spl5_4),
% 3.35/0.91 inference(and_proxy_clausification,[],[f341])).
% 3.35/0.91 thf(f343,plain,(
% 3.35/0.91 ($true = ((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (sK11 @ Y1 @ Y0)))))))) | ~spl5_4),
% 3.35/0.91 inference(and_proxy_clausification,[],[f341])).
% 3.35/0.91 thf(f345,plain,(
% 3.35/0.91 ($true != $true) | ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | spl5_1),
% 3.35/0.91 inference(superposition,[],[f37,f7])).
% 3.35/0.91 thf(f346,plain,(
% 3.35/0.91 ($false = ((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4)))))) | spl5_1),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f345])).
% 3.35/0.91 thf(f348,plain,(
% 3.35/0.91 spl5_3 | spl5_1),
% 3.35/0.91 inference(avatar_split_clause,[],[f346,f36,f45])).
% 3.35/0.91 thf(f446,plain,(
% 3.35/0.91 ( ! [X1 : a] : (((((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((sK2 @ Y1 @ Y0) | (sK1 @ Y1 @ Y0)) => (sK11 @ Y1 @ Y0))))) @ X1)) = $true)) ) | ~spl5_4),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f343])).
% 3.35/0.91 thf(f447,plain,(
% 3.35/0.91 ( ! [X1 : a] : ((((!! @ a @ (^[Y0 : a]: (((sK2 @ Y0 @ X1) | (sK1 @ Y0 @ X1)) => (sK11 @ Y0 @ X1))))) = $true)) ) | ~spl5_4),
% 3.35/0.91 inference(beta-eta_normalization,[],[f446])).
% 3.35/0.91 thf(f460,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = (((^[Y0 : a]: (((sK2 @ Y0 @ X1) | (sK1 @ Y0 @ X1)) => (sK11 @ Y0 @ X1))) @ X2)))) ) | ~spl5_4),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f447])).
% 3.35/0.91 thf(f461,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($true = ((((sK2 @ X2 @ X1) | (sK1 @ X2 @ X1)) => (sK11 @ X2 @ X1))))) ) | ~spl5_4),
% 3.35/0.91 inference(beta-eta_normalization,[],[f460])).
% 3.35/0.91 thf(f462,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (((((sK2 @ X2 @ X1) | (sK1 @ X2 @ X1))) = $false) | (((sK11 @ X2 @ X1)) = $true)) ) | ~spl5_4),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f461])).
% 3.35/0.91 thf(f463,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : (($false = ((sK1 @ X2 @ X1))) | (((sK11 @ X2 @ X1)) = $true)) ) | ~spl5_4),
% 3.35/0.91 inference(or_proxy_clausification,[],[f462])).
% 3.35/0.91 thf(f464,plain,(
% 3.35/0.91 ( ! [X2 : a,X1 : a] : ((((sK11 @ X2 @ X1)) = $true) | (((sK2 @ X2 @ X1)) = $false)) ) | ~spl5_4),
% 3.35/0.91 inference(or_proxy_clausification,[],[f462])).
% 3.35/0.91 thf(f518,plain,(
% 3.35/0.91 (((sK2 @ (sK7 @ sK8) @ (sK6 @ sK8))) = $false) | ($false = ((sK0 @ sK8))) | ($true = $false) | ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(superposition,[],[f65,f307])).
% 3.35/0.91 thf(f520,plain,(
% 3.35/0.91 (((sK2 @ (sK7 @ sK8) @ (sK6 @ sK8))) = $false) | ($false = ((sK0 @ sK8))) | ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f518])).
% 3.35/0.91 thf(f524,plain,(
% 3.35/0.91 ($true = $false) | ($true = ((sK8 @ sK3 @ sK4))) | (((sK2 @ (sK7 @ sK8) @ (sK6 @ sK8))) = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f520,f75])).
% 3.35/0.91 thf(f525,plain,(
% 3.35/0.91 ($true = ((sK8 @ sK3 @ sK4))) | (((sK2 @ (sK7 @ sK8) @ (sK6 @ sK8))) = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f524])).
% 3.35/0.91 thf(f528,plain,(
% 3.35/0.91 ($true = $false) | (((sK2 @ (sK7 @ sK8) @ (sK6 @ sK8))) = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f525,f72])).
% 3.35/0.91 thf(f529,plain,(
% 3.35/0.91 (((sK2 @ (sK7 @ sK8) @ (sK6 @ sK8))) = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f528])).
% 3.35/0.91 thf(f590,plain,(
% 3.35/0.91 ($true = $false) | ($true = ((sK8 @ sK3 @ sK4))) | ($false = ((sK0 @ sK8))) | ($true = ((sK8 @ (sK7 @ sK8) @ (sK6 @ sK8)))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(superposition,[],[f318,f529])).
% 3.35/0.91 thf(f594,plain,(
% 3.35/0.91 ($false = ((sK0 @ sK8))) | ($true = ((sK8 @ sK3 @ sK4))) | ($true = ((sK8 @ (sK7 @ sK8) @ (sK6 @ sK8)))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f590])).
% 3.35/0.91 thf(f600,plain,(
% 3.35/0.91 ($true = $false) | ($true = ((sK8 @ (sK7 @ sK8) @ (sK6 @ sK8)))) | ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f594,f75])).
% 3.35/0.91 thf(f601,plain,(
% 3.35/0.91 ($true = ((sK8 @ (sK7 @ sK8) @ (sK6 @ sK8)))) | ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f600])).
% 3.35/0.91 thf(f608,plain,(
% 3.35/0.91 ($true = ((sK8 @ (sK7 @ sK8) @ (sK6 @ sK8)))) | ($true = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f601,f72])).
% 3.35/0.91 thf(f609,plain,(
% 3.35/0.91 ($true = ((sK8 @ (sK7 @ sK8) @ (sK6 @ sK8)))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f608])).
% 3.35/0.91 thf(f622,plain,(
% 3.35/0.91 ($true = $false) | ($false = ((sK0 @ sK8))) | ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(superposition,[],[f609,f65])).
% 3.35/0.91 thf(f624,plain,(
% 3.35/0.91 ($false = ((sK0 @ sK8))) | ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f622])).
% 3.35/0.91 thf(f626,plain,(
% 3.35/0.91 ($true = ((sK8 @ sK3 @ sK4))) | ($true = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f624,f75])).
% 3.35/0.91 thf(f627,plain,(
% 3.35/0.91 ($true = ((sK8 @ sK3 @ sK4))) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f626])).
% 3.35/0.91 thf(f630,plain,(
% 3.35/0.91 ($true = $false) | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(forward_demodulation,[],[f627,f72])).
% 3.35/0.91 thf(f631,plain,(
% 3.35/0.91 $false | (~spl5_2 | ~spl5_3)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f630])).
% 3.35/0.91 thf(f632,plain,(
% 3.35/0.91 ~spl5_2 | ~spl5_3),
% 3.35/0.91 inference(avatar_contradiction_clause,[],[f631])).
% 3.35/0.91 thf(f679,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = (((^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: (((!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((sK0 @ Y3) & (!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK2 @ Y5 @ Y4) => (Y3 @ Y5 @ Y4))))))) => (Y3 @ Y1 @ Y2)))) | (!! @ (a > a > $o) @ (^[Y3 : a > a > $o]: (((!! @ a @ (^[Y4 : a]: (!! @ a @ (^[Y5 : a]: ((sK1 @ Y4 @ Y5) => (Y3 @ Y4 @ Y5)))))) & (sK0 @ Y3)) => (Y3 @ Y1 @ Y2))))) => (Y0 @ Y1 @ Y2))))))) => (Y0 @ sK3 @ sK4))) @ X1)))) ) | ~spl5_1),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f38])).
% 3.35/0.91 thf(f680,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((((sK0 @ X1) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (X1 @ Y0 @ Y1))))))) => (X1 @ sK3 @ sK4))))) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f679])).
% 3.35/0.91 thf(f681,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ((((sK0 @ X1) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (X1 @ Y0 @ Y1)))))))) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f680])).
% 3.35/0.91 thf(f682,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($false = ((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (X1 @ Y0 @ Y1)))))))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_1),
% 3.35/0.91 inference(and_proxy_clausification,[],[f681])).
% 3.35/0.91 thf(f683,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : ((((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | ($false = (((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: (((!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((sK0 @ Y2) & (!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK2 @ Y4 @ Y3) => (Y2 @ Y4 @ Y3))))))) => (Y2 @ Y0 @ Y1)))) | (!! @ (a > a > $o) @ (^[Y2 : a > a > $o]: (((!! @ a @ (^[Y3 : a]: (!! @ a @ (^[Y4 : a]: ((sK1 @ Y3 @ Y4) => (Y2 @ Y3 @ Y4)))))) & (sK0 @ Y2)) => (Y2 @ Y0 @ Y1))))) => (X1 @ Y0 @ Y1))))) @ (sK12 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f682])).
% 3.35/0.91 thf(f686,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($false = ((!! @ a @ (^[Y0 : a]: (((!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((sK0 @ Y1) & (!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK2 @ Y3 @ Y2) => (Y1 @ Y3 @ Y2))))))) => (Y1 @ (sK12 @ X1) @ Y0)))) | (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK1 @ Y2 @ Y3) => (Y1 @ Y2 @ Y3)))))) & (sK0 @ Y1)) => (Y1 @ (sK12 @ X1) @ Y0))))) => (X1 @ (sK12 @ X1) @ Y0)))))) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f683])).
% 3.35/0.91 thf(f687,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (((((^[Y0 : a]: (((!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((sK0 @ Y1) & (!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK2 @ Y3 @ Y2) => (Y1 @ Y3 @ Y2))))))) => (Y1 @ (sK12 @ X1) @ Y0)))) | (!! @ (a > a > $o) @ (^[Y1 : a > a > $o]: (((!! @ a @ (^[Y2 : a]: (!! @ a @ (^[Y3 : a]: ((sK1 @ Y2 @ Y3) => (Y1 @ Y2 @ Y3)))))) & (sK0 @ Y1)) => (Y1 @ (sK12 @ X1) @ Y0))))) => (X1 @ (sK12 @ X1) @ Y0))) @ (sK13 @ X1))) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f686])).
% 3.35/0.91 thf(f690,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | (((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1))))) | (!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) => (X1 @ (sK12 @ X1) @ (sK13 @ X1)))) = $false) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f687])).
% 3.35/0.91 thf(f691,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($false = ((X1 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f690])).
% 3.35/0.91 thf(f692,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1))))) | (!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1))))))) = $true)) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f690])).
% 3.35/0.91 thf(f693,plain,(
% 3.35/0.91 ( ! [X1 : (a > a > $o)] : ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) = $true) | (((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) = $true) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(or_proxy_clausification,[],[f692])).
% 3.35/0.91 thf(f715,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | (((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) = $true) | (((sK0 @ X1)) = $false) | ((((^[Y0 : a > a > $o]: (((sK0 @ Y0) & (!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK2 @ Y2 @ Y1) => (Y0 @ Y2 @ Y1))))))) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))) @ X2)) = $true)) ) | ~spl5_1),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f693])).
% 3.35/0.91 thf(f716,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((((sK0 @ X2) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))))) => (X2 @ (sK12 @ X1) @ (sK13 @ X1))))) | ($true = ((X1 @ sK3 @ sK4))) | (((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) = $true) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f715])).
% 3.35/0.91 thf(f717,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) = $true) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ((((sK0 @ X2) & (!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0)))))))) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f716])).
% 3.35/0.91 thf(f718,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ (a > a > $o) @ (^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))))) = $true) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))))) = $false) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((sK0 @ X2)))) ) | ~spl5_1),
% 3.35/0.91 inference(and_proxy_clausification,[],[f717])).
% 3.35/0.91 thf(f719,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))))) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ($true = (((^[Y0 : a > a > $o]: (((!! @ a @ (^[Y1 : a]: (!! @ a @ (^[Y2 : a]: ((sK1 @ Y1 @ Y2) => (Y0 @ Y1 @ Y2)))))) & (sK0 @ Y0)) => (Y0 @ (sK12 @ X1) @ (sK13 @ X1)))) @ X3))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X2)))) ) | ~spl5_1),
% 3.35/0.91 inference(pi_proxy_clausification,[],[f718])).
% 3.35/0.91 thf(f720,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ($true = ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1)))))) & (sK0 @ X3)) => (X3 @ (sK12 @ X1) @ (sK13 @ X1))))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))))) = $false) | ($false = ((sK0 @ X2))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f719])).
% 3.35/0.91 thf(f721,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))))) = $false) | ($false = ((sK0 @ X2))) | ($false = (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1)))))) & (sK0 @ X3)))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f720])).
% 3.35/0.91 thf(f722,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))))) = $false) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ($false = ((sK0 @ X3))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X2))) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | ($true = ((X1 @ sK3 @ sK4)))) ) | ~spl5_1),
% 3.35/0.91 inference(and_proxy_clausification,[],[f721])).
% 3.35/0.91 thf(f723,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | ($false = ((sK0 @ X2))) | ($false = (((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK2 @ Y1 @ Y0) => (X2 @ Y1 @ Y0))))) @ (sK14 @ X2)))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f722])).
% 3.35/0.91 thf(f726,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($false = ((!! @ a @ (^[Y0 : a]: ((sK2 @ Y0 @ (sK14 @ X2)) => (X2 @ Y0 @ (sK14 @ X2))))))) | ($false = ((sK0 @ X2))) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ($false = ((sK0 @ X3))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f723])).
% 3.35/0.91 thf(f727,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($false = ((sK0 @ X3))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X1 @ sK3 @ sK4))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ((((^[Y0 : a]: ((sK2 @ Y0 @ (sK14 @ X2)) => (X2 @ Y0 @ (sK14 @ X2)))) @ (sK15 @ X2))) = $false) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | ($false = ((sK0 @ X2)))) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f726])).
% 3.35/0.91 thf(f730,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ($false = (((sK2 @ (sK15 @ X2) @ (sK14 @ X2)) => (X2 @ (sK15 @ X2) @ (sK14 @ X2))))) | ($false = ((sK0 @ X2))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | (((sK0 @ X1)) = $false) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3)))) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f727])).
% 3.35/0.91 thf(f731,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | ($true = ((X1 @ sK3 @ sK4))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | ($false = ((sK0 @ X2))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f730])).
% 3.35/0.91 thf(f732,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))))) = $false) | (((sK0 @ X1)) = $false) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((sK0 @ X2))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f730])).
% 3.35/0.91 thf(f770,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | (((sK0 @ X1)) = $false) | ($false = ((sK0 @ X2))) | ((((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))) @ (sK16 @ X3))) = $false) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X1 @ sK3 @ sK4))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3)))) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f731])).
% 3.35/0.91 thf(f773,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: ((sK1 @ (sK16 @ X3) @ Y0) => (X3 @ (sK16 @ X3) @ Y0))))) = $false) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | ($false = ((sK0 @ X3))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((sK0 @ X2))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f770])).
% 3.35/0.91 thf(f774,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ((((^[Y0 : a]: (!! @ a @ (^[Y1 : a]: ((sK1 @ Y0 @ Y1) => (X3 @ Y0 @ Y1))))) @ (sK16 @ X3))) = $false) | ($false = ((sK0 @ X3))) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X2))) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f732])).
% 3.35/0.91 thf(f776,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : ((((!! @ a @ (^[Y0 : a]: ((sK1 @ (sK16 @ X3) @ Y0) => (X3 @ (sK16 @ X3) @ Y0))))) = $false) | ($false = ((sK0 @ X2))) | ($false = ((sK0 @ X3))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f774])).
% 3.35/0.91 thf(f778,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ((((^[Y0 : a]: ((sK1 @ (sK16 @ X3) @ Y0) => (X3 @ (sK16 @ X3) @ Y0))) @ (sK17 @ X3))) = $false) | ($false = ((sK0 @ X3))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | ($false = ((sK0 @ X2))) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f773])).
% 3.35/0.91 thf(f780,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | ((((sK1 @ (sK16 @ X3) @ (sK17 @ X3)) => (X3 @ (sK16 @ X3) @ (sK17 @ X3)))) = $false) | (((sK0 @ X1)) = $false) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X2))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2))))) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f778])).
% 3.35/0.91 thf(f782,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ($false = ((sK0 @ X2))) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | (((X3 @ (sK16 @ X3) @ (sK17 @ X3))) = $false) | ($false = ((sK0 @ X3)))) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f780])).
% 3.35/0.91 thf(f783,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK1 @ (sK16 @ X3) @ (sK17 @ X3)))) | (((sK0 @ X1)) = $false) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((sK0 @ X2))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f780])).
% 3.35/0.91 thf(f800,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ((((^[Y0 : a]: ((sK1 @ (sK16 @ X3) @ Y0) => (X3 @ (sK16 @ X3) @ Y0))) @ (sK17 @ X3))) = $false) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | ($false = ((sK0 @ X2))) | ($true = ((X1 @ sK3 @ sK4))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(sigma_proxy_clausification,[],[f776])).
% 3.35/0.91 thf(f802,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($false = ((sK0 @ X2))) | ((((sK1 @ (sK16 @ X3) @ (sK17 @ X3)) => (X3 @ (sK16 @ X3) @ (sK17 @ X3)))) = $false) | ($true = ((X1 @ sK3 @ sK4))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true)) ) | ~spl5_1),
% 3.35/0.91 inference(beta-eta_normalization,[],[f800])).
% 3.35/0.91 thf(f804,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X3))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((sK0 @ X2))) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | (((X3 @ (sK16 @ X3) @ (sK17 @ X3))) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f802])).
% 3.35/0.91 thf(f805,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X3 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK1 @ (sK16 @ X3) @ (sK17 @ X3)))) | (((sK0 @ X1)) = $false) | ($false = ((sK0 @ X2))) | ($true = ((X3 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X1 @ sK3 @ sK4))) | ($false = ((sK0 @ X3)))) ) | ~spl5_1),
% 3.35/0.91 inference(imp_proxy_clausification,[],[f802])).
% 3.35/0.91 thf(f813,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false) | ($true = $false) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((sK0 @ X0)) = $false) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | (((sK0 @ X0)) = $false) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true)) ) | ~spl5_1),
% 3.35/0.91 inference(superposition,[],[f691,f782])).
% 3.35/0.91 thf(f820,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | ($true = $false) | (((sK0 @ X0)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(duplicate_literal_removal,[],[f813])).
% 3.35/0.91 thf(f821,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f820])).
% 3.35/0.91 thf(f832,definition,(
% 3.35/0.91 spl5_18 <=> ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | (((sK0 @ X0)) = $false) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition])).
% 3.35/0.91 thf(f833,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | (((sK0 @ X0)) = $false) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true)) ) | ~spl5_18),
% 3.35/0.91 inference(avatar_component_clause,[],[f832])).
% 3.35/0.91 thf(f877,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | (((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK16 @ X0) @ (sK17 @ X0)))) | ($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ($true = $false) | ($false = ((sK0 @ X2)))) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(superposition,[],[f783,f463])).
% 3.35/0.91 thf(f879,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK11 @ (sK16 @ X0) @ (sK17 @ X0)))) | (((sK0 @ X0)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X1)) = $false) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((X2 @ (sK15 @ X2) @ (sK14 @ X2)))) | ($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X2)))) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f877])).
% 3.35/0.91 thf(f892,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X0)) = $false) | ($true = ((sK2 @ (sK15 @ X0) @ (sK14 @ X0)))) | (((sK0 @ X1)) = $false) | ($true != $true) | (((sK0 @ X0)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(equality_factoring,[],[f804])).
% 3.35/0.91 thf(f903,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X0)) = $false) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((sK0 @ X1)) = $false) | ($true != $true) | ($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((sK2 @ (sK15 @ X0) @ (sK14 @ X0))))) ) | ~spl5_1),
% 3.35/0.91 inference(duplicate_literal_removal,[],[f892])).
% 3.35/0.91 thf(f904,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK2 @ (sK15 @ X0) @ (sK14 @ X0)))) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X0)) = $false) | ($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((sK0 @ X1)) = $false)) ) | ~spl5_1),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f903])).
% 3.35/0.91 thf(f931,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK11 @ (sK16 @ X0) @ (sK17 @ X0)))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X0)) = $false) | ($true = $false) | ($false = ((sK0 @ X2))) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true) | ($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1))))) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(superposition,[],[f805,f463])).
% 3.35/0.91 thf(f933,plain,(
% 3.35/0.91 ( ! [X2 : (a > a > $o),X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK11 @ (sK16 @ X0) @ (sK17 @ X0)))) | (((sK0 @ X1)) = $false) | ($true = ((X1 @ sK3 @ sK4))) | (((sK0 @ X0)) = $false) | ($true = ((X0 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($true = ((X2 @ (sK12 @ X1) @ (sK13 @ X1)))) | ($false = ((sK0 @ X2))) | (((sK2 @ (sK15 @ X2) @ (sK14 @ X2))) = $true)) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f931])).
% 3.35/0.91 thf(f995,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ sK11)) = $false) | (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | (((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false)) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(superposition,[],[f464,f821])).
% 3.35/0.91 thf(f1003,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((sK0 @ sK11)) = $false) | (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false)) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f995])).
% 3.35/0.91 thf(f1008,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((X0 @ sK3 @ sK4)) = $true) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | ($true = $false) | (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(forward_demodulation,[],[f1003,f342])).
% 3.35/0.91 thf(f1009,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1008])).
% 3.35/0.91 thf(f1013,definition,(
% 3.35/0.91 spl5_29 <=> ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((X0 @ sK3 @ sK4)) = $true))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_29])],[avatar_definition])).
% 3.35/0.91 thf(f1014,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ X0)) = $false) | (((X0 @ (sK16 @ X0) @ (sK17 @ X0))) = $false) | (((X0 @ sK3 @ sK4)) = $true)) ) | ~spl5_29),
% 3.35/0.91 inference(avatar_component_clause,[],[f1013])).
% 3.35/0.91 thf(f1016,definition,(
% 3.35/0.91 spl5_30 <=> (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false)),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_30])],[avatar_definition])).
% 3.35/0.91 thf(f1018,plain,(
% 3.35/0.91 (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | ~spl5_30),
% 3.35/0.91 inference(avatar_component_clause,[],[f1016])).
% 3.35/0.91 thf(f1020,plain,(
% 3.35/0.91 spl5_30 | spl5_29 | ~spl5_1 | ~spl5_4),
% 3.35/0.91 inference(avatar_split_clause,[],[f1009,f49,f36,f1013,f1016])).
% 3.35/0.91 thf(f1100,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | (((sK0 @ sK11)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | ($true = $false)) ) | (~spl5_1 | ~spl5_30)),
% 3.35/0.91 inference(superposition,[],[f904,f1018])).
% 3.35/0.91 thf(f1109,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | (((sK0 @ sK11)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false)) ) | (~spl5_1 | ~spl5_30)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1100])).
% 3.35/0.91 thf(f1112,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | ($true = $false) | (((X0 @ sK3 @ sK4)) = $true)) ) | (~spl5_1 | ~spl5_4 | ~spl5_30)),
% 3.35/0.91 inference(forward_demodulation,[],[f1109,f342])).
% 3.35/0.91 thf(f1113,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_30)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1112])).
% 3.35/0.91 thf(f1115,definition,(
% 3.35/0.91 spl5_34 <=> (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false)),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_34])],[avatar_definition])).
% 3.35/0.91 thf(f1117,plain,(
% 3.35/0.91 (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | ~spl5_34),
% 3.35/0.91 inference(avatar_component_clause,[],[f1115])).
% 3.35/0.91 thf(f1119,definition,(
% 3.35/0.91 spl5_35 <=> ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true))),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_35])],[avatar_definition])).
% 3.35/0.91 thf(f1120,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false)) ) | ~spl5_35),
% 3.35/0.91 inference(avatar_component_clause,[],[f1119])).
% 3.35/0.91 thf(f1122,plain,(
% 3.35/0.91 spl5_35 | spl5_34 | ~spl5_1 | ~spl5_4 | ~spl5_30),
% 3.35/0.91 inference(avatar_split_clause,[],[f1113,f1016,f49,f36,f1115,f1119])).
% 3.35/0.91 thf(f1123,plain,(
% 3.35/0.91 (((sK0 @ sK11)) = $false) | ($true = $false) | (((sK0 @ sK11)) = $false) | (((sK11 @ sK3 @ sK4)) = $true) | (((sK11 @ sK3 @ sK4)) = $true) | (~spl5_1 | ~spl5_35)),
% 3.35/0.91 inference(superposition,[],[f1120,f691])).
% 3.35/0.91 thf(f1127,plain,(
% 3.35/0.91 (((sK11 @ sK3 @ sK4)) = $true) | ($true = $false) | (((sK0 @ sK11)) = $false) | (~spl5_1 | ~spl5_35)),
% 3.35/0.91 inference(duplicate_literal_removal,[],[f1123])).
% 3.35/0.91 thf(f1128,plain,(
% 3.35/0.91 (((sK0 @ sK11)) = $false) | (((sK11 @ sK3 @ sK4)) = $true) | (~spl5_1 | ~spl5_35)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1127])).
% 3.35/0.91 thf(f1131,plain,(
% 3.35/0.91 (((sK11 @ sK3 @ sK4)) = $true) | ($true = $false) | (~spl5_1 | ~spl5_4 | ~spl5_35)),
% 3.35/0.91 inference(forward_demodulation,[],[f1128,f342])).
% 3.35/0.91 thf(f1132,plain,(
% 3.35/0.91 (((sK11 @ sK3 @ sK4)) = $true) | (~spl5_1 | ~spl5_4 | ~spl5_35)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1131])).
% 3.35/0.91 thf(f1133,plain,(
% 3.35/0.91 ($true = $false) | (~spl5_1 | ~spl5_4 | ~spl5_35)),
% 3.35/0.91 inference(forward_demodulation,[],[f1132,f340])).
% 3.35/0.91 thf(f1134,plain,(
% 3.35/0.91 $false | (~spl5_1 | ~spl5_4 | ~spl5_35)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1133])).
% 3.35/0.91 thf(f1135,plain,(
% 3.35/0.91 ~spl5_1 | ~spl5_4 | ~spl5_35),
% 3.35/0.91 inference(avatar_contradiction_clause,[],[f1134])).
% 3.35/0.91 thf(f1143,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((X0 @ sK3 @ sK4)) = $true) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | ($true = $false) | (((sK0 @ X1)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | (((sK0 @ sK11)) = $false) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(superposition,[],[f1117,f879])).
% 3.35/0.91 thf(f1144,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((sK0 @ sK11)) = $false) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ X1)) = $false) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1143])).
% 3.35/0.91 thf(f1146,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | ($true = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(forward_demodulation,[],[f1144,f342])).
% 3.35/0.91 thf(f1147,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X1)) = $false) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X1 @ (sK15 @ X1) @ (sK14 @ X1))) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1146])).
% 3.35/0.91 thf(f1150,plain,(
% 3.35/0.91 spl5_18 | ~spl5_1 | ~spl5_4 | ~spl5_34),
% 3.35/0.91 inference(avatar_split_clause,[],[f1147,f1115,f49,f36,f832])).
% 3.35/0.91 thf(f1153,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ sK11)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | ($true != $true) | (((sK0 @ X0)) = $false) | (((sK11 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false)) ) | ~spl5_18),
% 3.35/0.91 inference(equality_factoring,[],[f833])).
% 3.35/0.91 thf(f1154,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ sK11)) = $false) | (((sK11 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false)) ) | ~spl5_18),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1153])).
% 3.35/0.91 thf(f1159,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ X0)) = $false) | ($true = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK11 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false)) ) | (~spl5_4 | ~spl5_18)),
% 3.35/0.91 inference(forward_demodulation,[],[f1154,f342])).
% 3.35/0.91 thf(f1160,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK11 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false)) ) | (~spl5_4 | ~spl5_18)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1159])).
% 3.35/0.91 thf(f1166,definition,(
% 3.35/0.91 spl5_36 <=> (((sK11 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false)),
% 3.35/0.91 introduced(definition,[new_symbols(definition,[spl5_36])],[avatar_definition])).
% 3.35/0.91 thf(f1168,plain,(
% 3.35/0.91 (((sK11 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | ~spl5_36),
% 3.35/0.91 inference(avatar_component_clause,[],[f1166])).
% 3.35/0.91 thf(f1169,plain,(
% 3.35/0.91 spl5_36 | spl5_35 | ~spl5_4 | ~spl5_18),
% 3.35/0.91 inference(avatar_split_clause,[],[f1160,f832,f49,f1119,f1166])).
% 3.35/0.91 thf(f1223,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((sK0 @ X0)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK2 @ (sK15 @ X1) @ (sK14 @ X1))) = $true) | (((sK0 @ X1)) = $false) | (((sK0 @ sK11)) = $false) | ($true = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(superposition,[],[f1117,f933])).
% 3.35/0.91 thf(f1224,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((sK2 @ (sK15 @ X1) @ (sK14 @ X1))) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ sK11)) = $false) | (((sK0 @ X0)) = $false) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1223])).
% 3.35/0.91 thf(f1226,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : ((((sK2 @ (sK15 @ X1) @ (sK14 @ X1))) = $true) | ($true = $false) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((sK0 @ X1)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(forward_demodulation,[],[f1224,f342])).
% 3.35/0.91 thf(f1227,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o),X1 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((X1 @ (sK12 @ X0) @ (sK13 @ X0))) = $true) | (((sK0 @ X0)) = $false) | (((sK2 @ (sK15 @ X1) @ (sK14 @ X1))) = $true) | (((sK0 @ X1)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1226])).
% 3.35/0.91 thf(f1234,plain,(
% 3.35/0.91 ($true = $false) | (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | (~spl5_4 | ~spl5_36)),
% 3.35/0.91 inference(superposition,[],[f464,f1168])).
% 3.35/0.91 thf(f1235,plain,(
% 3.35/0.91 (((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11))) = $false) | (~spl5_4 | ~spl5_36)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1234])).
% 3.35/0.91 thf(f1362,plain,(
% 3.35/0.91 (((sK0 @ sK11)) = $false) | ($true = $false) | (((sK11 @ sK3 @ sK4)) = $true) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | (((sK0 @ sK11)) = $false) | (((sK11 @ sK3 @ sK4)) = $true) | (~spl5_1 | ~spl5_29)),
% 3.35/0.91 inference(superposition,[],[f1014,f691])).
% 3.35/0.91 thf(f1364,plain,(
% 3.35/0.91 (((sK11 @ sK3 @ sK4)) = $true) | (((sK0 @ sK11)) = $false) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | ($true = $false) | (~spl5_1 | ~spl5_29)),
% 3.35/0.91 inference(duplicate_literal_removal,[],[f1362])).
% 3.35/0.91 thf(f1365,plain,(
% 3.35/0.91 (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | (((sK11 @ sK3 @ sK4)) = $true) | (((sK0 @ sK11)) = $false) | (~spl5_1 | ~spl5_29)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1364])).
% 3.35/0.91 thf(f1686,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((X0 @ sK3 @ sK4)) = $true) | ($true = ((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11)))) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ sK11)) = $false) | ($true != $true) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(equality_factoring,[],[f1227])).
% 3.35/0.91 thf(f1691,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK2 @ (sK15 @ sK11) @ (sK14 @ sK11)))) | (((sK0 @ X0)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ sK11)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1686])).
% 3.35/0.91 thf(f1696,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((X0 @ sK3 @ sK4)) = $true) | ($true = $false) | (((sK0 @ X0)) = $false) | (((sK0 @ sK11)) = $false) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0))))) ) | (~spl5_1 | ~spl5_4 | ~spl5_30 | ~spl5_34)),
% 3.35/0.91 inference(forward_demodulation,[],[f1691,f1018])).
% 3.35/0.91 thf(f1697,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((sK0 @ sK11)) = $false) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_30 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1696])).
% 3.35/0.91 thf(f1702,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : ((((X0 @ sK3 @ sK4)) = $true) | ($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | ($true = $false) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_30 | ~spl5_34)),
% 3.35/0.91 inference(forward_demodulation,[],[f1697,f342])).
% 3.35/0.91 thf(f1703,plain,(
% 3.35/0.91 ( ! [X0 : (a > a > $o)] : (($true = ((sK11 @ (sK12 @ X0) @ (sK13 @ X0)))) | (((X0 @ sK3 @ sK4)) = $true) | (((sK0 @ X0)) = $false)) ) | (~spl5_1 | ~spl5_4 | ~spl5_30 | ~spl5_34)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1702])).
% 3.35/0.91 thf(f1705,plain,(
% 3.35/0.91 spl5_35 | ~spl5_1 | ~spl5_4 | ~spl5_30 | ~spl5_34),
% 3.35/0.91 inference(avatar_split_clause,[],[f1703,f1115,f1016,f49,f36,f1119])).
% 3.35/0.91 thf(f1706,plain,(
% 3.35/0.91 spl5_30 | ~spl5_4 | ~spl5_36),
% 3.35/0.91 inference(avatar_split_clause,[],[f1235,f1166,f49,f1016])).
% 3.35/0.91 thf(f1709,plain,(
% 3.35/0.91 (((sK0 @ sK11)) = $false) | ($true = $false) | (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | (~spl5_1 | ~spl5_4 | ~spl5_29)),
% 3.35/0.91 inference(forward_demodulation,[],[f1365,f340])).
% 3.35/0.91 thf(f1710,plain,(
% 3.35/0.91 (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | (((sK0 @ sK11)) = $false) | (~spl5_1 | ~spl5_4 | ~spl5_29)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1709])).
% 3.35/0.91 thf(f1717,plain,(
% 3.35/0.91 (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | ($true = $false) | (~spl5_1 | ~spl5_4 | ~spl5_29)),
% 3.35/0.91 inference(forward_demodulation,[],[f1710,f342])).
% 3.35/0.91 thf(f1718,plain,(
% 3.35/0.91 (((sK11 @ (sK16 @ sK11) @ (sK17 @ sK11))) = $false) | (~spl5_1 | ~spl5_4 | ~spl5_29)),
% 3.35/0.91 inference(trivial_inequality_removal,[],[f1717])).
% 3.35/0.91 thf(f1724,plain,(
% 3.35/0.91 spl5_34 | ~spl5_1 | ~spl5_4 | ~spl5_29),
% 3.35/0.91 inference(avatar_split_clause,[],[f1718,f1013,f49,f36,f1115])).
% 3.35/0.91 cnf(s1, plain, spl5_1 | spl5_2, inference(sat_conversion,[],[f43])).
% 3.35/0.91 cnf(s2, plain, spl5_3 | spl5_4, inference(sat_conversion,[],[f52])).
% 3.35/0.91 cnf(s6, plain, ~spl5_1 | ~spl5_3, inference(sat_conversion,[],[f131])).
% 3.35/0.91 cnf(s21, plain, spl5_1 | spl5_3, inference(sat_conversion,[],[f348])).
% 3.35/0.91 cnf(s29, plain, ~spl5_2 | ~spl5_3, inference(sat_conversion,[],[f632])).
% 3.35/0.91 cnf(s44, plain, ~spl5_1 | ~spl5_4 | spl5_29 | spl5_30, inference(sat_conversion,[],[f1020])).
% 3.35/0.91 cnf(s56, plain, ~spl5_1 | ~spl5_4 | ~spl5_30 | spl5_34 | spl5_35, inference(sat_conversion,[],[f1122])).
% 3.35/0.91 cnf(s57, plain, ~spl5_1 | ~spl5_4 | ~spl5_35, inference(sat_conversion,[],[f1135])).
% 3.35/0.91 cnf(s58, plain, ~spl5_1 | ~spl5_4 | spl5_18 | ~spl5_34, inference(sat_conversion,[],[f1150])).
% 3.35/0.91 cnf(s60, plain, ~spl5_4 | ~spl5_18 | spl5_35 | spl5_36, inference(sat_conversion,[],[f1169])).
% 3.35/0.91 cnf(s98, plain, ~spl5_1 | ~spl5_4 | ~spl5_30 | ~spl5_34 | spl5_35, inference(sat_conversion,[],[f1705])).
% 3.35/0.91 cnf(s99, plain, ~spl5_4 | spl5_30 | ~spl5_36, inference(sat_conversion,[],[f1706])).
% 3.35/0.91 cnf(s102, plain, ~spl5_1 | ~spl5_4 | ~spl5_29 | spl5_34, inference(sat_conversion,[],[f1724])).
% 3.35/0.91 cnf(s105, plain, spl5_1, inference(rat,[],[s29,s1,s21])).
% 3.35/0.91 cnf(s106, plain, ~spl5_3, inference(rat,[],[s6,s105])).
% 3.35/0.91 cnf(s107, plain, spl5_4, inference(rat,[],[s2,s106])).
% 3.35/0.91 cnf(s108, plain, ~spl5_35, inference(rat,[],[s57,s105,s107])).
% 3.35/0.91 cnf(s110, plain, ~spl5_34, inference(rat,[],[s99,s60,s98,s58,s107,s108,s105])).
% 3.35/0.91 cnf(s111, plain, ~spl5_29, inference(rat,[],[s102,s107,s105,s110])).
% 3.35/0.91 cnf(s113, plain, ~spl5_30, inference(rat,[],[s56,s108,s107,s105,s110])).
% 3.35/0.91 cnf(s114, plain, $false, inference(rat,[],[s44,s107,s105,s113,s111])).
% 3.35/0.91 thf(f1725,plain,(
% 3.35/0.91 $false),
% 3.35/0.91 inference(avatar_sat_refutation,[],[s114])).
% 3.35/0.91 % SZS output end Proof for theBenchmark
% 3.35/0.91 % (205400)------------------------------
% 3.35/0.91 % (205400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.91 % (205400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.91 % (205400)CaDiCaL version: 2.1.3
% 3.35/0.91 % (205400)Termination reason: Refutation
% 3.35/0.91 % (205400)Time elapsed: 0.198 s
% 3.35/0.91 % (205400)Peak memory usage: 14 MB
% 3.35/0.91 % (205400)Instructions burned: 223 (million)
% 3.35/0.91 % (205336)Success in time 0.529 s
% 3.35/0.91 % Vampire exiting
%------------------------------------------------------------------------------