%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU788^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:31:23 AM UTC 2026
% Result : Theorem 0.89s 0.44s
% Output : Refutation 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU788^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 14:29:16 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.36 % (164920)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.22/0.36 % (164930)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2414405180:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.22/0.36 % (164927)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2088704505:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.22/0.36 % (164929)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=469320924:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.22/0.36 % (164928)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=1778149922: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.22/0.36 % (164926)lrs+10_16_si=on:nwc=1.5:random_seed=1691830164:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.22/0.36 % (164925)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=573096297:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.22/0.36 % (164927)Instruction limit reached!
% 0.22/0.36 % (164927)------------------------------
% 0.22/0.36 % (164927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (164927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (164927)CaDiCaL version: 2.1.3
% 0.22/0.36 % (164927)Termination reason: Instruction limit
% 0.22/0.36 % (164927)Termination phase: Property scanning
% 0.22/0.36 % (164927)Time elapsed: 0.002 s
% 0.22/0.36 % (164927)Peak memory usage: 11 MB
% 0.22/0.36 % (164927)Instructions burned: 4 (million)
% 0.22/0.36 % (164931)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.22/0.36 % (164931)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.22/0.36 % (164926)Instruction limit reached!
% 0.22/0.36 % (164926)------------------------------
% 0.22/0.36 % (164926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (164926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (164926)CaDiCaL version: 2.1.3
% 0.22/0.36 % (164926)Termination reason: Instruction limit
% 0.22/0.36 % (164926)Termination phase: Saturation
% 0.22/0.36 % (164926)Time elapsed: 0.010 s
% 0.22/0.36 % (164926)Peak memory usage: 12 MB
% 0.22/0.36 % (164926)Instructions burned: 18 (million)
% 0.22/0.36 % (164929)Instruction limit reached!
% 0.22/0.36 % (164929)------------------------------
% 0.22/0.36 % (164929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (164929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (164929)CaDiCaL version: 2.1.3
% 0.22/0.36 % (164929)Termination reason: Instruction limit
% 0.22/0.36 % (164929)Termination phase: Saturation
% 0.22/0.36 % (164929)Time elapsed: 0.014 s
% 0.22/0.36 % (164929)Peak memory usage: 12 MB
% 0.22/0.36 % (164929)Instructions burned: 26 (million)
% 0.22/0.36 % (164930)Instruction limit reached!
% 0.22/0.36 % (164930)------------------------------
% 0.22/0.36 % (164930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (164930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.36 % (164930)CaDiCaL version: 2.1.3
% 0.22/0.36 % (164930)Termination reason: Instruction limit
% 0.22/0.36 % (164930)Termination phase: Saturation
% 0.22/0.36 % (164930)Time elapsed: 0.022 s
% 0.22/0.36 % (164930)Peak memory usage: 13 MB
% 0.22/0.36 % (164930)Instructions burned: 77 (million)
% 0.22/0.36 % (164931)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=2992247173:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.22/0.36 % (164938)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1594898800:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.22/0.36 % (164938)Instruction limit reached!
% 0.22/0.36 % (164938)------------------------------
% 0.22/0.36 % (164938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.36 % (164938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.42 % (164938)CaDiCaL version: 2.1.3
% 0.89/0.42 % (164938)Termination reason: Instruction limit
% 0.89/0.42 % (164938)Termination phase: Property scanning
% 0.89/0.42 % (164938)Time elapsed: 0.002 s
% 0.89/0.42 % (164938)Peak memory usage: 10 MB
% 0.89/0.42 % (164938)Instructions burned: 4 (million)
% 0.89/0.42 % (164942)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=4218389887:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.89/0.42 % (164939)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3334213593:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.89/0.42 % (164940)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.89/0.42 % (164942)Instruction limit reached!
% 0.89/0.42 % (164942)------------------------------
% 0.89/0.42 % (164942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.42 % (164942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.42 % (164942)CaDiCaL version: 2.1.3
% 0.89/0.42 % (164942)Termination reason: Instruction limit
% 0.89/0.42 % (164942)Termination phase: Saturation
% 0.89/0.42 % (164942)Time elapsed: 0.004 s
% 0.89/0.42 % (164942)Peak memory usage: 12 MB
% 0.89/0.42 % (164942)Instructions burned: 15 (million)
% 0.89/0.42 % (164939)Instruction limit reached!
% 0.89/0.42 % (164939)------------------------------
% 0.89/0.42 % (164939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.42 % (164939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.42 % (164939)CaDiCaL version: 2.1.3
% 0.89/0.42 % (164939)Termination reason: Instruction limit
% 0.89/0.42 % (164939)Termination phase: Saturation
% 0.89/0.42 % (164939)Time elapsed: 0.003 s
% 0.89/0.42 % (164939)Peak memory usage: 11 MB
% 0.89/0.42 % (164939)Instructions burned: 6 (million)
% 0.89/0.42 % (164940)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1241067796:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.89/0.42 % (164940)Instruction limit reached!
% 0.89/0.42 % (164940)------------------------------
% 0.89/0.42 % (164940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.42 % (164940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.42 % (164940)CaDiCaL version: 2.1.3
% 0.89/0.42 % (164940)Termination reason: Instruction limit
% 0.89/0.42 % (164940)Termination phase: Saturation
% 0.89/0.42 % (164940)Time elapsed: 0.004 s
% 0.89/0.42 % (164940)Peak memory usage: 12 MB
% 0.89/0.42 % (164940)Instructions burned: 7 (million)
% 0.89/0.42 % (164944)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.89/0.42 % (164944)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.89/0.42 % (164925)Instruction limit reached!
% 0.89/0.42 % (164925)------------------------------
% 0.89/0.42 % (164925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.42 % (164925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.42 % (164925)CaDiCaL version: 2.1.3
% 0.89/0.42 % (164925)Termination reason: Instruction limit
% 0.89/0.42 % (164925)Termination phase: Saturation
% 0.89/0.42 % (164925)Time elapsed: 0.041 s
% 0.89/0.42 % (164925)Peak memory usage: 13 MB
% 0.89/0.42 % (164925)Instructions burned: 87 (million)
% 0.89/0.42 % (164947)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=3318401879:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.89/0.42 % (164944)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2258463286: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.89/0.42 % (164948)lrs+10_1_si=on:cs=on:random_seed=3044481445:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.89/0.42 % (164950)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.89/0.44 % (164948)Instruction limit reached!
% 0.89/0.44 % (164948)------------------------------
% 0.89/0.44 % (164948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164948)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164948)Termination reason: Instruction limit
% 0.89/0.44 % (164948)Termination phase: Saturation
% 0.89/0.44 % (164948)Time elapsed: 0.004 s
% 0.89/0.44 % (164948)Peak memory usage: 12 MB
% 0.89/0.44 % (164948)Instructions burned: 9 (million)
% 0.89/0.44 % (164944)Instruction limit reached!
% 0.89/0.44 % (164944)------------------------------
% 0.89/0.44 % (164944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164944)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164944)Termination reason: Instruction limit
% 0.89/0.44 % (164944)Termination phase: Saturation
% 0.89/0.44 % (164944)Time elapsed: 0.014 s
% 0.89/0.44 % (164944)Peak memory usage: 12 MB
% 0.89/0.44 % (164944)Instructions burned: 29 (million)
% 0.89/0.44 % (164950)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=2316863060:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.89/0.44 % (164950)Instruction limit reached!
% 0.89/0.44 % (164950)------------------------------
% 0.89/0.44 % (164950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164950)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164950)Termination reason: Instruction limit
% 0.89/0.44 % (164950)Termination phase: Property scanning
% 0.89/0.44 % (164950)Time elapsed: 0.001 s
% 0.89/0.44 % (164950)Peak memory usage: 10 MB
% 0.89/0.44 % (164950)Instructions burned: 2 (million)
% 0.89/0.44 % (164952)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1010743778:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.89/0.44 % (164947)Instruction limit reached!
% 0.89/0.44 % (164947)------------------------------
% 0.89/0.44 % (164947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164947)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164947)Termination reason: Instruction limit
% 0.89/0.44 % (164947)Termination phase: Saturation
% 0.89/0.44 % (164947)Time elapsed: 0.025 s
% 0.89/0.44 % (164947)Peak memory usage: 12 MB
% 0.89/0.44 % (164947)Instructions burned: 90 (million)
% 0.89/0.44 % (164956)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1204332737:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.89/0.44 % (164957)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3800221577:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.89/0.44 % (164960)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1610034044:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.89/0.44 % (164958)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=526682692:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.89/0.44 % (164952)Instruction limit reached!
% 0.89/0.44 % (164952)------------------------------
% 0.89/0.44 % (164952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164952)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164952)Termination reason: Instruction limit
% 0.89/0.44 % (164952)Termination phase: Saturation
% 0.89/0.44 % (164952)Time elapsed: 0.020 s
% 0.89/0.44 % (164952)Peak memory usage: 12 MB
% 0.89/0.44 % (164952)Instructions burned: 39 (million)
% 0.89/0.44 % (164958)Instruction limit reached!
% 0.89/0.44 % (164958)------------------------------
% 0.89/0.44 % (164958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164958)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164958)Termination reason: Instruction limit
% 0.89/0.44 % (164958)Termination phase: Saturation
% 0.89/0.44 % (164958)Time elapsed: 0.008 s
% 0.89/0.44 % (164958)Peak memory usage: 12 MB
% 0.89/0.44 % (164958)Instructions burned: 14 (million)
% 0.89/0.44 % (164957)Instruction limit reached!
% 0.89/0.44 % (164957)------------------------------
% 0.89/0.44 % (164957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164957)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164957)Termination reason: Instruction limit
% 0.89/0.44 % (164957)Termination phase: Saturation
% 0.89/0.44 % (164957)Time elapsed: 0.015 s
% 0.89/0.44 % (164957)Peak memory usage: 12 MB
% 0.89/0.44 % (164957)Instructions burned: 26 (million)
% 0.89/0.44 % (164965)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1527065877:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.89/0.44 % (164966)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1469359457: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)
% 0.89/0.44 % (164965)Instruction limit reached!
% 0.89/0.44 % (164965)------------------------------
% 0.89/0.44 % (164965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164965)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164965)Termination reason: Instruction limit
% 0.89/0.44 % (164965)Termination phase: Saturation
% 0.89/0.44 % (164965)Time elapsed: 0.007 s
% 0.89/0.44 % (164965)Peak memory usage: 12 MB
% 0.89/0.44 % (164965)Instructions burned: 14 (million)
% 0.89/0.44 % (164966)Instruction limit reached!
% 0.89/0.44 % (164966)------------------------------
% 0.89/0.44 % (164966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164966)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164966)Termination reason: Instruction limit
% 0.89/0.44 % (164966)Termination phase: Saturation
% 0.89/0.44 % (164966)Time elapsed: 0.003 s
% 0.89/0.44 % (164966)Peak memory usage: 12 MB
% 0.89/0.44 % (164966)Instructions burned: 7 (million)
% 0.89/0.44 % (164967)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=753041167:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.89/0.44 % (164970)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1934581901:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.89/0.44 % (164967)Instruction limit reached!
% 0.89/0.44 % (164967)------------------------------
% 0.89/0.44 % (164967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164967)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164967)Termination reason: Instruction limit
% 0.89/0.44 % (164967)Termination phase: Saturation
% 0.89/0.44 % (164967)Time elapsed: 0.014 s
% 0.89/0.44 % (164967)Peak memory usage: 12 MB
% 0.89/0.44 % (164967)Instructions burned: 27 (million)
% 0.89/0.44 % (164971)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3677353005:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.89/0.44 % (164970)Instruction limit reached!
% 0.89/0.44 % (164970)------------------------------
% 0.89/0.44 % (164970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164970)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164970)Termination reason: Instruction limit
% 0.89/0.44 % (164970)Termination phase: Saturation
% 0.89/0.44 % (164970)Time elapsed: 0.012 s
% 0.89/0.44 % (164970)Peak memory usage: 12 MB
% 0.89/0.44 % (164970)Instructions burned: 23 (million)
% 0.89/0.44 % (164974)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
% 0.89/0.44 % (164974)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.89/0.44 % (164974)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=3662594512:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.89/0.44 % (164976)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.89/0.44 % (164931)Instruction limit reached!
% 0.89/0.44 % (164931)------------------------------
% 0.89/0.44 % (164931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164931)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164931)Termination reason: Instruction limit
% 0.89/0.44 % (164931)Termination phase: Saturation
% 0.89/0.44 % (164931)Time elapsed: 0.139 s
% 0.89/0.44 % (164931)Peak memory usage: 13 MB
% 0.89/0.44 % (164931)Instructions burned: 158 (million)
% 0.89/0.44 % (164974)Instruction limit reached!
% 0.89/0.44 % (164974)------------------------------
% 0.89/0.44 % (164974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164974)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164974)Termination reason: Instruction limit
% 0.89/0.44 % (164974)Termination phase: Saturation
% 0.89/0.44 % (164974)Time elapsed: 0.008 s
% 0.89/0.44 % (164974)Peak memory usage: 12 MB
% 0.89/0.44 % (164974)Instructions burned: 16 (million)
% 0.89/0.44 % (164971) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-164920-164971"...
% 0.89/0.44 % (164976)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=2074803749:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.89/0.44 % (164960)Instruction limit reached!
% 0.89/0.44 % (164960)------------------------------
% 0.89/0.44 % (164960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164960)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164960)Termination reason: Instruction limit
% 0.89/0.44 % (164960)Termination phase: Saturation
% 0.89/0.44 % (164960)Time elapsed: 0.081 s
% 0.89/0.44 % (164960)Peak memory usage: 13 MB
% 0.89/0.44 % (164960)Instructions burned: 329 (million)
% 0.89/0.44 % (164976)Instruction limit reached!
% 0.89/0.44 % (164976)------------------------------
% 0.89/0.44 % (164976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164976)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164976)Termination reason: Instruction limit
% 0.89/0.44 % (164976)Termination phase: Saturation
% 0.89/0.44 % (164976)Time elapsed: 0.004 s
% 0.89/0.44 % (164976)Peak memory usage: 12 MB
% 0.89/0.44 % (164976)Instructions burned: 8 (million)
% 0.89/0.44 % (164971)...printing done.
% 0.89/0.44 % (164971)Refutation found. Thanks to Tanya!
% 0.89/0.44 % SZS status Theorem for theBenchmark
% 0.89/0.44 % SZS output start Proof for theBenchmark
% 0.89/0.44 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.89/0.44 thf(func_def_0, type, in: ($i > $i > $o)).
% 0.89/0.44 thf(func_def_1, type, subset: ($i > $i > $o)).
% 0.89/0.44 thf(func_def_2, type, setextsub: $o).
% 0.89/0.44 thf(func_def_4, type, binunion: ($i > $i > $i)).
% 0.89/0.44 thf(func_def_5, type, kpair: ($i > $i > $i)).
% 0.89/0.44 thf(func_def_6, type, breln1: ($i > $i > $o)).
% 0.89/0.44 thf(func_def_7, type, subbreln1: $o).
% 0.89/0.44 thf(func_def_8, type, breln1unionprop: $o).
% 0.89/0.44 thf(func_def_9, type, breln1unionIL: $o).
% 0.89/0.44 thf(func_def_10, type, breln1unionIR: $o).
% 0.89/0.44 thf(func_def_11, type, breln1unionE: $o).
% 0.89/0.44 thf(func_def_17, type, sK3: ($i > $i > $i > $i)).
% 0.89/0.44 thf(func_def_18, type, sK4: ($i > $i > $i > $i)).
% 0.89/0.44 thf(func_def_42, type, sF28: $o).
% 0.89/0.44 thf(func_def_43, type, sF29: $o).
% 0.89/0.44 thf(func_def_46, type, vNOT: ($o > $o)).
% 0.89/0.44 thf(f1,axiom,(
% 0.89/0.44 (! [X1 : $i,X0 : $i] : ((subset @ X0 @ X1) => ((subset @ X1 @ X0) => (X0 = X1))) = setextsub)),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setextsub)).
% 0.89/0.44 thf(f2,axiom,(
% 0.89/0.44 (! [X1 : $i,X0 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X1) => (in @ (kpair @ X3 @ X4) @ X2)))) => (subset @ X1 @ X2)))) = subbreln1)),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subbreln1)).
% 0.89/0.44 thf(f3,axiom,(
% 0.89/0.44 (breln1unionprop = ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (breln1 @ X0 @ (binunion @ X1 @ X2)))))),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',breln1unionprop)).
% 0.89/0.44 thf(f4,axiom,(
% 0.89/0.44 (! [X1 : $i,X0 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => ! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X1) => (in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))))))) = breln1unionIL)),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',breln1unionIL)).
% 0.89/0.44 thf(f5,axiom,(
% 0.89/0.44 (breln1unionIR = ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => ! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X2) => (in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))))))))),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',breln1unionIR)).
% 0.89/0.44 thf(f6,axiom,(
% 0.89/0.44 (breln1unionE = ! [X1 : $i,X0 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => ! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2)) => ((in @ (kpair @ X3 @ X4) @ X2) | (in @ (kpair @ X3 @ X4) @ X1))))))))),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',breln1unionE)).
% 0.89/0.44 thf(f7,conjecture,(
% 0.89/0.44 setextsub => (subbreln1 => (breln1unionprop => (breln1unionIL => (breln1unionIR => (breln1unionE => ! [X1 : $i,X0 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (((binunion @ X1 @ X2)) = ((binunion @ X2 @ X1))))))))))),
% 0.89/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',breln1unionCommutes)).
% 0.89/0.44 thf(f8,negated_conjecture,(
% 0.89/0.44 ~(setextsub => (subbreln1 => (breln1unionprop => (breln1unionIL => (breln1unionIR => (breln1unionE => ! [X1 : $i,X0 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (((binunion @ X1 @ X2)) = ((binunion @ X2 @ X1)))))))))))),
% 0.89/0.44 inference(negated_conjecture,[status(cth)],[f7])).
% 0.89/0.44 thf(f9,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((breln1 @ X1 @ X0) => ! [X2 : $i] : ((breln1 @ X1 @ X2) => (! [X3 : $i] : ((in @ X3 @ X1) => ! [X4 : $i] : ((in @ X4 @ X1) => ((in @ (kpair @ X3 @ X4) @ X0) => (in @ (kpair @ X3 @ X4) @ X2)))) => (subset @ X0 @ X2)))) = subbreln1)),
% 0.89/0.44 inference(rectify,[],[f2])).
% 0.89/0.44 thf(f10,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : (($true = ((breln1 @ X1 @ X0))) => ! [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) => (! [X3 : $i] : (($true = ((in @ X3 @ X1))) => ! [X4 : $i] : (($true = ((in @ X4 @ X1))) => (($true = ((in @ (kpair @ X3 @ X4) @ X0))) => (((in @ (kpair @ X3 @ X4) @ X2)) = $true)))) => ($true = ((subset @ X0 @ X2)))))) <=> (subbreln1 = $true)),
% 0.89/0.44 inference(fool_elimination,[],[f9])).
% 0.89/0.44 thf(f11,plain,(
% 0.89/0.44 ~(setextsub => (subbreln1 => (breln1unionprop => (breln1unionIL => (breln1unionIR => (breln1unionE => ! [X0 : $i,X1 : $i] : ((breln1 @ X1 @ X0) => ! [X2 : $i] : ((breln1 @ X1 @ X2) => (((binunion @ X0 @ X2)) = ((binunion @ X2 @ X0)))))))))))),
% 0.89/0.44 inference(rectify,[],[f8])).
% 0.89/0.44 thf(f12,plain,(
% 0.89/0.44 ~((setextsub = $true) => ((subbreln1 = $true) => ((breln1unionprop = $true) => ((breln1unionIL = $true) => ((breln1unionIR = $true) => ((breln1unionE = $true) => ! [X0 : $i,X1 : $i] : (($true = ((breln1 @ X1 @ X0))) => ! [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) => (((binunion @ X0 @ X2)) = ((binunion @ X2 @ X0)))))))))))),
% 0.89/0.44 inference(fool_elimination,[],[f11])).
% 0.89/0.44 thf(f13,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((subset @ X1 @ X0) => ((subset @ X0 @ X1) => (X0 = X1))) = setextsub)),
% 0.89/0.44 inference(rectify,[],[f1])).
% 0.89/0.44 thf(f14,plain,(
% 0.89/0.44 (setextsub = $true) <=> ! [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) = $true) => ((((subset @ X0 @ X1)) = $true) => (X0 = X1)))),
% 0.89/0.44 inference(fool_elimination,[],[f13])).
% 0.89/0.44 thf(f15,plain,(
% 0.89/0.44 (breln1unionE = ! [X0 : $i,X1 : $i] : ((breln1 @ X1 @ X0) => ! [X2 : $i] : ((breln1 @ X1 @ X2) => ! [X3 : $i] : ((in @ X3 @ X1) => ! [X4 : $i] : ((in @ X4 @ X1) => ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)) => ((in @ (kpair @ X3 @ X4) @ X2) | (in @ (kpair @ X3 @ X4) @ X0))))))))),
% 0.89/0.44 inference(rectify,[],[f6])).
% 0.89/0.44 thf(f16,plain,(
% 0.89/0.44 (breln1unionE = $true) <=> ! [X1 : $i,X0 : $i] : (($true = ((breln1 @ X1 @ X0))) => ! [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) => ! [X3 : $i] : (($true = ((in @ X3 @ X1))) => ! [X4 : $i] : (($true = ((in @ X4 @ X1))) => (($true = ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))) => (($true = ((in @ (kpair @ X3 @ X4) @ X0))) | (((in @ (kpair @ X3 @ X4) @ X2)) = $true)))))))),
% 0.89/0.44 inference(fool_elimination,[],[f15])).
% 0.89/0.44 thf(f17,plain,(
% 0.89/0.44 (breln1unionprop = ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (breln1 @ X0 @ (binunion @ X1 @ X2)))))),
% 0.89/0.44 inference(rectify,[],[f3])).
% 0.89/0.44 thf(f18,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X1)) = $true) => ! [X2 : $i] : ((((breln1 @ X0 @ X2)) = $true) => (((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true))) <=> (breln1unionprop = $true)),
% 0.89/0.44 inference(fool_elimination,[],[f17])).
% 0.89/0.44 thf(f19,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((breln1 @ X1 @ X0) => ! [X2 : $i] : ((breln1 @ X1 @ X2) => ! [X3 : $i] : ((in @ X3 @ X1) => ! [X4 : $i] : ((in @ X4 @ X1) => ((in @ (kpair @ X3 @ X4) @ X0) => (in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2))))))) = breln1unionIL)),
% 0.89/0.44 inference(rectify,[],[f4])).
% 0.89/0.44 thf(f20,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : (($true = ((breln1 @ X1 @ X0))) => ! [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) => ! [X3 : $i] : (($true = ((in @ X3 @ X1))) => ! [X4 : $i] : (($true = ((in @ X4 @ X1))) => (($true = ((in @ (kpair @ X3 @ X4) @ X0))) => ($true = ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2))))))))) <=> (breln1unionIL = $true)),
% 0.89/0.44 inference(fool_elimination,[],[f19])).
% 0.89/0.44 thf(f21,plain,(
% 0.89/0.44 (breln1unionIR = ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => ! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X2) => (in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))))))))),
% 0.89/0.44 inference(rectify,[],[f5])).
% 0.89/0.44 thf(f22,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X1)) = $true) => ! [X2 : $i] : ((((breln1 @ X0 @ X2)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => ! [X4 : $i] : ((((in @ X4 @ X0)) = $true) => ((((in @ (kpair @ X3 @ X4) @ X2)) = $true) => (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) = $true)))))) <=> (breln1unionIR = $true)),
% 0.89/0.44 inference(fool_elimination,[],[f21])).
% 0.89/0.44 thf(f23,plain,(
% 0.89/0.44 (((((? [X0 : $i,X1 : $i] : (($true = ((breln1 @ X1 @ X0))) & ? [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) & (((binunion @ X0 @ X2)) != ((binunion @ X2 @ X0))))) & (breln1unionE = $true)) & (breln1unionIR = $true)) & (breln1unionIL = $true)) & (breln1unionprop = $true)) & (subbreln1 = $true)) & (setextsub = $true)),
% 0.89/0.44 inference(ennf_transformation,[],[f12])).
% 0.89/0.44 thf(f24,plain,(
% 0.89/0.44 (breln1unionIL = $true) & (setextsub = $true) & (breln1unionIR = $true) & (subbreln1 = $true) & (breln1unionprop = $true) & ? [X0 : $i,X1 : $i] : (($true = ((breln1 @ X1 @ X0))) & ? [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) & (((binunion @ X0 @ X2)) != ((binunion @ X2 @ X0))))) & (breln1unionE = $true)),
% 0.89/0.44 inference(flattening,[],[f23])).
% 0.89/0.44 thf(f25,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (! [X4 : $i] : (((((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) = $true) | (((in @ (kpair @ X3 @ X4) @ X2)) != $true)) | (((in @ X4 @ X0)) != $true)) | (((in @ X3 @ X0)) != $true)) | (((breln1 @ X0 @ X2)) != $true)) | (((breln1 @ X0 @ X1)) != $true)) <=> (breln1unionIR = $true)),
% 0.89/0.44 inference(ennf_transformation,[],[f22])).
% 0.89/0.44 thf(f26,plain,(
% 0.89/0.44 (breln1unionIR = $true) <=> ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((breln1 @ X0 @ X2)) != $true) | ! [X3 : $i] : (! [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) != $true) | (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) = $true) | (((in @ X4 @ X0)) != $true)) | (((in @ X3 @ X0)) != $true))) | (((breln1 @ X0 @ X1)) != $true))),
% 0.89/0.44 inference(flattening,[],[f25])).
% 0.89/0.44 thf(f27,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true) | (((breln1 @ X0 @ X2)) != $true)) | (((breln1 @ X0 @ X1)) != $true)) <=> (breln1unionprop = $true)),
% 0.89/0.44 inference(ennf_transformation,[],[f18])).
% 0.89/0.44 thf(f28,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (! [X4 : $i] : ((($true = ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))) | ($true != ((in @ (kpair @ X3 @ X4) @ X0)))) | ($true != ((in @ X4 @ X1)))) | ($true != ((in @ X3 @ X1)))) | ($true != ((breln1 @ X1 @ X2)))) | ($true != ((breln1 @ X1 @ X0)))) <=> (breln1unionIL = $true)),
% 0.89/0.44 inference(ennf_transformation,[],[f20])).
% 0.89/0.44 thf(f29,plain,(
% 0.89/0.44 (breln1unionIL = $true) <=> ! [X1 : $i,X0 : $i] : (! [X2 : $i] : (($true != ((breln1 @ X1 @ X2))) | ! [X3 : $i] : (($true != ((in @ X3 @ X1))) | ! [X4 : $i] : (($true != ((in @ X4 @ X1))) | ($true = ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))) | ($true != ((in @ (kpair @ X3 @ X4) @ X0)))))) | ($true != ((breln1 @ X1 @ X0))))),
% 0.89/0.44 inference(flattening,[],[f28])).
% 0.89/0.44 thf(f30,plain,(
% 0.89/0.44 (breln1unionE = $true) <=> ! [X1 : $i,X0 : $i] : (! [X2 : $i] : (! [X3 : $i] : (! [X4 : $i] : (((($true = ((in @ (kpair @ X3 @ X4) @ X0))) | (((in @ (kpair @ X3 @ X4) @ X2)) = $true)) | ($true != ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2))))) | ($true != ((in @ X4 @ X1)))) | ($true != ((in @ X3 @ X1)))) | ($true != ((breln1 @ X1 @ X2)))) | ($true != ((breln1 @ X1 @ X0))))),
% 0.89/0.44 inference(ennf_transformation,[],[f16])).
% 0.89/0.44 thf(f31,plain,(
% 0.89/0.44 (breln1unionE = $true) <=> ! [X1 : $i,X0 : $i] : (! [X2 : $i] : (! [X3 : $i] : (($true != ((in @ X3 @ X1))) | ! [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) = $true) | ($true != ((in @ X4 @ X1))) | ($true = ((in @ (kpair @ X3 @ X4) @ X0))) | ($true != ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))))) | ($true != ((breln1 @ X1 @ X2)))) | ($true != ((breln1 @ X1 @ X0))))),
% 0.89/0.44 inference(flattening,[],[f30])).
% 0.89/0.44 thf(f32,plain,(
% 0.89/0.44 (setextsub = $true) <=> ! [X0 : $i,X1 : $i] : (((X0 = X1) | (((subset @ X0 @ X1)) != $true)) | (((subset @ X1 @ X0)) != $true))),
% 0.89/0.44 inference(ennf_transformation,[],[f14])).
% 0.89/0.44 thf(f33,plain,(
% 0.89/0.44 ! [X1 : $i,X0 : $i] : ((((subset @ X1 @ X0)) != $true) | (X0 = X1) | (((subset @ X0 @ X1)) != $true)) <=> (setextsub = $true)),
% 0.89/0.44 inference(flattening,[],[f32])).
% 0.89/0.44 thf(f34,plain,(
% 0.89/0.44 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((($true = ((subset @ X0 @ X2))) | ? [X3 : $i] : (? [X4 : $i] : (((((in @ (kpair @ X3 @ X4) @ X2)) != $true) & ($true = ((in @ (kpair @ X3 @ X4) @ X0)))) & ($true = ((in @ X4 @ X1)))) & ($true = ((in @ X3 @ X1))))) | ($true != ((breln1 @ X1 @ X2)))) | ($true != ((breln1 @ X1 @ X0)))) <=> (subbreln1 = $true)),
% 0.89/0.44 inference(ennf_transformation,[],[f10])).
% 0.89/0.44 thf(f35,plain,(
% 0.89/0.44 ! [X1 : $i,X0 : $i] : (($true != ((breln1 @ X1 @ X0))) | ! [X2 : $i] : (($true != ((breln1 @ X1 @ X2))) | ($true = ((subset @ X0 @ X2))) | ? [X3 : $i] : (? [X4 : $i] : (($true = ((in @ (kpair @ X3 @ X4) @ X0))) & ($true = ((in @ X4 @ X1))) & (((in @ (kpair @ X3 @ X4) @ X2)) != $true)) & ($true = ((in @ X3 @ X1)))))) <=> (subbreln1 = $true)),
% 0.89/0.44 inference(flattening,[],[f34])).
% 0.89/0.44 thf(f36,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true) | (((breln1 @ X0 @ X2)) != $true)) | (((breln1 @ X0 @ X1)) != $true)) | (breln1unionprop != $true)) & ((breln1unionprop = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((breln1 @ X0 @ (binunion @ X1 @ X2))) != $true) & (((breln1 @ X0 @ X2)) = $true)) & (((breln1 @ X0 @ X1)) = $true)))),
% 0.89/0.44 inference(nnf_transformation,[],[f27])).
% 0.89/0.44 thf(f37,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true) | (((breln1 @ X0 @ X2)) != $true)) | (((breln1 @ X0 @ X1)) != $true)) | (breln1unionprop != $true)) & ((breln1unionprop = $true) | ? [X3 : $i,X4 : $i] : (? [X5 : $i] : (($true != ((breln1 @ X3 @ (binunion @ X4 @ X5)))) & ($true = ((breln1 @ X3 @ X5)))) & ($true = ((breln1 @ X3 @ X4)))))),
% 0.89/0.44 inference(rectify,[],[f36])).
% 0.89/0.44 thf(f38,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true) | (((breln1 @ X0 @ X2)) != $true)) | (((breln1 @ X0 @ X1)) != $true)) | (breln1unionprop != $true)) & ((breln1unionprop = $true) | ((($true != ((breln1 @ sK0 @ (binunion @ sK1 @ sK2)))) & ($true = ((breln1 @ sK0 @ sK2)))) & ($true = ((breln1 @ sK0 @ sK1)))))),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X3,sK0),skolemize(X4,sK1),skolemize(X5,sK2)],[f37])).
% 0.89/0.44 thf(f39,plain,(
% 0.89/0.44 (! [X1 : $i,X0 : $i] : (($true != ((breln1 @ X1 @ X0))) | ! [X2 : $i] : (($true != ((breln1 @ X1 @ X2))) | ($true = ((subset @ X0 @ X2))) | ? [X3 : $i] : (? [X4 : $i] : (($true = ((in @ (kpair @ X3 @ X4) @ X0))) & ($true = ((in @ X4 @ X1))) & (((in @ (kpair @ X3 @ X4) @ X2)) != $true)) & ($true = ((in @ X3 @ X1)))))) | (subbreln1 != $true)) & ((subbreln1 = $true) | ? [X1 : $i,X0 : $i] : (($true = ((breln1 @ X1 @ X0))) & ? [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) & ($true != ((subset @ X0 @ X2))) & ! [X3 : $i] : (! [X4 : $i] : (($true != ((in @ (kpair @ X3 @ X4) @ X0))) | ($true != ((in @ X4 @ X1))) | (((in @ (kpair @ X3 @ X4) @ X2)) = $true)) | ($true != ((in @ X3 @ X1)))))))),
% 0.89/0.44 inference(nnf_transformation,[],[f35])).
% 0.89/0.44 thf(f40,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X1)) != $true) | ! [X2 : $i] : ((((breln1 @ X0 @ X2)) != $true) | (((subset @ X1 @ X2)) = $true) | ? [X3 : $i] : (? [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X1)) = $true) & (((in @ X4 @ X0)) = $true) & (((in @ (kpair @ X3 @ X4) @ X2)) != $true)) & (((in @ X3 @ X0)) = $true)))) | (subbreln1 != $true)) & ((subbreln1 = $true) | ? [X5 : $i,X6 : $i] : (($true = ((breln1 @ X5 @ X6))) & ? [X7 : $i] : (($true = ((breln1 @ X5 @ X7))) & ($true != ((subset @ X6 @ X7))) & ! [X8 : $i] : (! [X9 : $i] : (($true != ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ X7)))) | ($true != ((in @ X8 @ X5)))))))),
% 0.89/0.44 inference(rectify,[],[f39])).
% 0.89/0.44 thf(f41,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X1)) != $true) | ! [X2 : $i] : ((((breln1 @ X0 @ X2)) != $true) | (((subset @ X1 @ X2)) = $true) | ((($true = ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X1))) & ($true = ((in @ (sK4 @ X2 @ X1 @ X0) @ X0))) & ($true != ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X2)))) & ($true = ((in @ (sK3 @ X2 @ X1 @ X0) @ X0)))))) | (subbreln1 != $true)) & ((subbreln1 = $true) | (($true = ((breln1 @ sK5 @ sK6))) & (($true = ((breln1 @ sK5 @ sK7))) & ($true != ((subset @ sK6 @ sK7))) & ! [X8 : $i] : (! [X9 : $i] : (($true != ((in @ (kpair @ X8 @ X9) @ sK6))) | ($true != ((in @ X9 @ sK5))) | ($true = ((in @ (kpair @ X8 @ X9) @ sK7)))) | ($true != ((in @ X8 @ sK5)))))))),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,sK5,sK6,sK7]),skolemize(X4,sK4 @ X2 @ X1 @ X0),skolemize(X4,sK4 @ X2 @ X1 @ X0),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7)],[f40])).
% 0.89/0.44 thf(f42,plain,(
% 0.89/0.44 (breln1unionIL = $true) & (setextsub = $true) & (breln1unionIR = $true) & (subbreln1 = $true) & (breln1unionprop = $true) & (($true = ((breln1 @ sK9 @ sK8))) & (($true = ((breln1 @ sK9 @ sK10))) & (((binunion @ sK8 @ sK10)) != ((binunion @ sK10 @ sK8))))) & (breln1unionE = $true)),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10)],[f24])).
% 0.89/0.44 thf(f43,plain,(
% 0.89/0.44 ((breln1unionIL = $true) | ? [X1 : $i,X0 : $i] : (? [X2 : $i] : (($true = ((breln1 @ X1 @ X2))) & ? [X3 : $i] : (($true = ((in @ X3 @ X1))) & ? [X4 : $i] : (($true = ((in @ X4 @ X1))) & ($true != ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))) & ($true = ((in @ (kpair @ X3 @ X4) @ X0)))))) & ($true = ((breln1 @ X1 @ X0))))) & (! [X1 : $i,X0 : $i] : (! [X2 : $i] : (($true != ((breln1 @ X1 @ X2))) | ! [X3 : $i] : (($true != ((in @ X3 @ X1))) | ! [X4 : $i] : (($true != ((in @ X4 @ X1))) | ($true = ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))) | ($true != ((in @ (kpair @ X3 @ X4) @ X0)))))) | ($true != ((breln1 @ X1 @ X0)))) | (breln1unionIL != $true))),
% 0.89/0.44 inference(nnf_transformation,[],[f29])).
% 0.89/0.44 thf(f44,plain,(
% 0.89/0.44 ((breln1unionIL = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((breln1 @ X0 @ X2)) = $true) & ? [X3 : $i] : ((((in @ X3 @ X0)) = $true) & ? [X4 : $i] : ((((in @ X4 @ X0)) = $true) & (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) != $true) & (((in @ (kpair @ X3 @ X4) @ X1)) = $true)))) & (((breln1 @ X0 @ X1)) = $true))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (($true != ((breln1 @ X5 @ X7))) | ! [X8 : $i] : (($true != ((in @ X8 @ X5))) | ! [X9 : $i] : (($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ (kpair @ X8 @ X9) @ X6)))))) | ($true != ((breln1 @ X5 @ X6)))) | (breln1unionIL != $true))),
% 0.89/0.44 inference(rectify,[],[f43])).
% 0.89/0.44 thf(f45,plain,(
% 0.89/0.44 ((breln1unionIL = $true) | ((($true = ((breln1 @ sK11 @ sK13))) & (($true = ((in @ sK14 @ sK11))) & (($true = ((in @ sK15 @ sK11))) & ($true != ((in @ (kpair @ sK14 @ sK15) @ (binunion @ sK12 @ sK13)))) & ($true = ((in @ (kpair @ sK14 @ sK15) @ sK12)))))) & ($true = ((breln1 @ sK11 @ sK12))))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (($true != ((breln1 @ X5 @ X7))) | ! [X8 : $i] : (($true != ((in @ X8 @ X5))) | ! [X9 : $i] : (($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ (kpair @ X8 @ X9) @ X6)))))) | ($true != ((breln1 @ X5 @ X6)))) | (breln1unionIL != $true))),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14,sK15]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13),skolemize(X3,sK14),skolemize(X4,sK15)],[f44])).
% 0.89/0.44 thf(f46,plain,(
% 0.89/0.44 (! [X1 : $i,X0 : $i] : ((((subset @ X1 @ X0)) != $true) | (X0 = X1) | (((subset @ X0 @ X1)) != $true)) | (setextsub != $true)) & ((setextsub = $true) | ? [X1 : $i,X0 : $i] : ((((subset @ X1 @ X0)) = $true) & (X0 != X1) & (((subset @ X0 @ X1)) = $true)))),
% 0.89/0.44 inference(nnf_transformation,[],[f33])).
% 0.89/0.44 thf(f47,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((((subset @ X0 @ X1)) != $true) | (X0 = X1) | (((subset @ X1 @ X0)) != $true)) | (setextsub != $true)) & ((setextsub = $true) | ? [X2 : $i,X3 : $i] : (($true = ((subset @ X2 @ X3))) & (X2 != X3) & ($true = ((subset @ X3 @ X2)))))),
% 0.89/0.44 inference(rectify,[],[f46])).
% 0.89/0.44 thf(f48,plain,(
% 0.89/0.44 (! [X0 : $i,X1 : $i] : ((((subset @ X0 @ X1)) != $true) | (X0 = X1) | (((subset @ X1 @ X0)) != $true)) | (setextsub != $true)) & ((setextsub = $true) | (($true = ((subset @ sK16 @ sK17))) & (sK16 != sK17) & ($true = ((subset @ sK17 @ sK16)))))),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X2,sK16),skolemize(X3,sK17)],[f47])).
% 0.89/0.44 thf(f49,plain,(
% 0.89/0.44 ((breln1unionIR = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((breln1 @ X0 @ X2)) = $true) & ? [X3 : $i] : (? [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) = $true) & (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) != $true) & (((in @ X4 @ X0)) = $true)) & (((in @ X3 @ X0)) = $true))) & (((breln1 @ X0 @ X1)) = $true))) & (! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((breln1 @ X0 @ X2)) != $true) | ! [X3 : $i] : (! [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) != $true) | (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) = $true) | (((in @ X4 @ X0)) != $true)) | (((in @ X3 @ X0)) != $true))) | (((breln1 @ X0 @ X1)) != $true)) | (breln1unionIR != $true))),
% 0.89/0.44 inference(nnf_transformation,[],[f26])).
% 0.89/0.44 thf(f50,plain,(
% 0.89/0.44 ((breln1unionIR = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((breln1 @ X0 @ X2)) = $true) & ? [X3 : $i] : (? [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) = $true) & (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) != $true) & (((in @ X4 @ X0)) = $true)) & (((in @ X3 @ X0)) = $true))) & (((breln1 @ X0 @ X1)) = $true))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (($true != ((breln1 @ X5 @ X7))) | ! [X8 : $i] : (! [X9 : $i] : (($true != ((in @ (kpair @ X8 @ X9) @ X7))) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ X9 @ X5)))) | ($true != ((in @ X8 @ X5))))) | ($true != ((breln1 @ X5 @ X6)))) | (breln1unionIR != $true))),
% 0.89/0.44 inference(rectify,[],[f49])).
% 0.89/0.44 thf(f51,plain,(
% 0.89/0.44 ((breln1unionIR = $true) | ((($true = ((breln1 @ sK18 @ sK20))) & ((($true = ((in @ (kpair @ sK21 @ sK22) @ sK20))) & ($true != ((in @ (kpair @ sK21 @ sK22) @ (binunion @ sK19 @ sK20)))) & ($true = ((in @ sK22 @ sK18)))) & ($true = ((in @ sK21 @ sK18))))) & ($true = ((breln1 @ sK18 @ sK19))))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (($true != ((breln1 @ X5 @ X7))) | ! [X8 : $i] : (! [X9 : $i] : (($true != ((in @ (kpair @ X8 @ X9) @ X7))) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ X9 @ X5)))) | ($true != ((in @ X8 @ X5))))) | ($true != ((breln1 @ X5 @ X6)))) | (breln1unionIR != $true))),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20,sK21,sK22]),skolemize(X0,sK18),skolemize(X1,sK19),skolemize(X2,sK20),skolemize(X3,sK21),skolemize(X4,sK22)],[f50])).
% 0.89/0.44 thf(f52,plain,(
% 0.89/0.44 ((breln1unionE = $true) | ? [X1 : $i,X0 : $i] : (? [X2 : $i] : (? [X3 : $i] : (($true = ((in @ X3 @ X1))) & ? [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) != $true) & ($true = ((in @ X4 @ X1))) & ($true != ((in @ (kpair @ X3 @ X4) @ X0))) & ($true = ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))))) & ($true = ((breln1 @ X1 @ X2)))) & ($true = ((breln1 @ X1 @ X0))))) & (! [X1 : $i,X0 : $i] : (! [X2 : $i] : (! [X3 : $i] : (($true != ((in @ X3 @ X1))) | ! [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) = $true) | ($true != ((in @ X4 @ X1))) | ($true = ((in @ (kpair @ X3 @ X4) @ X0))) | ($true != ((in @ (kpair @ X3 @ X4) @ (binunion @ X0 @ X2)))))) | ($true != ((breln1 @ X1 @ X2)))) | ($true != ((breln1 @ X1 @ X0)))) | (breln1unionE != $true))),
% 0.89/0.44 inference(nnf_transformation,[],[f31])).
% 0.89/0.44 thf(f53,plain,(
% 0.89/0.44 ((breln1unionE = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ X0)) = $true) & ? [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) != $true) & (((in @ X4 @ X0)) = $true) & (((in @ (kpair @ X3 @ X4) @ X1)) != $true) & (((in @ (kpair @ X3 @ X4) @ (binunion @ X1 @ X2))) = $true))) & (((breln1 @ X0 @ X2)) = $true)) & (((breln1 @ X0 @ X1)) = $true))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (! [X8 : $i] : (($true != ((in @ X8 @ X5))) | ! [X9 : $i] : (($true = ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))))) | ($true != ((breln1 @ X5 @ X7)))) | ($true != ((breln1 @ X5 @ X6)))) | (breln1unionE != $true))),
% 0.89/0.44 inference(rectify,[],[f52])).
% 0.89/0.44 thf(f54,plain,(
% 0.89/0.44 ((breln1unionE = $true) | (((($true = ((in @ sK26 @ sK23))) & (($true != ((in @ (kpair @ sK26 @ sK27) @ sK25))) & ($true = ((in @ sK27 @ sK23))) & ($true != ((in @ (kpair @ sK26 @ sK27) @ sK24))) & ($true = ((in @ (kpair @ sK26 @ sK27) @ (binunion @ sK24 @ sK25)))))) & ($true = ((breln1 @ sK23 @ sK25)))) & ($true = ((breln1 @ sK23 @ sK24))))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (! [X8 : $i] : (($true != ((in @ X8 @ X5))) | ! [X9 : $i] : (($true = ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))))) | ($true != ((breln1 @ X5 @ X7)))) | ($true != ((breln1 @ X5 @ X6)))) | (breln1unionE != $true))),
% 0.89/0.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24,sK25,sK26,sK27]),skolemize(X0,sK23),skolemize(X1,sK24),skolemize(X2,sK25),skolemize(X3,sK26),skolemize(X4,sK27)],[f53])).
% 0.89/0.44 thf(f58,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((breln1unionprop != $true) | (((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true) | (((breln1 @ X0 @ X2)) != $true) | (((breln1 @ X0 @ X1)) != $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f38])).
% 0.89/0.44 thf(f63,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((subbreln1 != $true) | ($true = ((in @ (sK3 @ X2 @ X1 @ X0) @ X0))) | (((breln1 @ X0 @ X1)) != $true) | (((breln1 @ X0 @ X2)) != $true) | (((subset @ X1 @ X2)) = $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f41])).
% 0.89/0.44 thf(f64,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X2)) != $true) | (subbreln1 != $true) | (((subset @ X1 @ X2)) = $true) | ($true != ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X2))) | (((breln1 @ X0 @ X1)) != $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f41])).
% 0.89/0.44 thf(f65,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((subbreln1 != $true) | ($true = ((in @ (sK4 @ X2 @ X1 @ X0) @ X0))) | (((breln1 @ X0 @ X1)) != $true) | (((breln1 @ X0 @ X2)) != $true) | (((subset @ X1 @ X2)) = $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f41])).
% 0.89/0.44 thf(f66,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((subbreln1 != $true) | (((breln1 @ X0 @ X1)) != $true) | (((breln1 @ X0 @ X2)) != $true) | ($true = ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X1))) | (((subset @ X1 @ X2)) = $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f41])).
% 0.89/0.44 thf(f67,plain,(
% 0.89/0.44 (breln1unionE = $true)),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f68,plain,(
% 0.89/0.44 (((binunion @ sK8 @ sK10)) != ((binunion @ sK10 @ sK8)))),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f69,plain,(
% 0.89/0.44 ($true = ((breln1 @ sK9 @ sK10)))),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f70,plain,(
% 0.89/0.44 ($true = ((breln1 @ sK9 @ sK8)))),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f71,plain,(
% 0.89/0.44 (breln1unionprop = $true)),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f72,plain,(
% 0.89/0.44 (subbreln1 = $true)),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f73,plain,(
% 0.89/0.44 (breln1unionIR = $true)),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f74,plain,(
% 0.89/0.44 (setextsub = $true)),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f75,plain,(
% 0.89/0.44 (breln1unionIL = $true)),
% 0.89/0.44 inference(cnf_transformation,[],[f42])).
% 0.89/0.44 thf(f76,plain,(
% 0.89/0.44 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : (($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((breln1 @ X5 @ X7))) | ($true != ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((in @ X8 @ X5))) | ($true != ((breln1 @ X5 @ X6))) | (breln1unionIL != $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f45])).
% 0.89/0.44 thf(f86,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : ((setextsub != $true) | (X0 = X1) | (((subset @ X0 @ X1)) != $true) | (((subset @ X1 @ X0)) != $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f48])).
% 0.89/0.44 thf(f87,plain,(
% 0.89/0.44 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : ((breln1unionIR != $true) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((in @ X8 @ X5))) | ($true != ((in @ X9 @ X5))) | ($true != ((breln1 @ X5 @ X7))) | ($true != ((breln1 @ X5 @ X6)))) )),
% 0.89/0.44 inference(cnf_transformation,[],[f51])).
% 0.89/0.44 thf(f94,plain,(
% 0.89/0.44 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : (($true != ((breln1 @ X5 @ X7))) | ($true != ((in @ X8 @ X5))) | ($true != ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true = ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((breln1 @ X5 @ X6))) | ($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ X6))) | (breln1unionE != $true)) )),
% 0.89/0.44 inference(cnf_transformation,[],[f54])).
% 0.89/0.44 thf(f104,definition,(
% 0.89/0.44 (sF28 = ((breln1 @ sK9 @ sK8)))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[sF28])],[function_definition])).
% 0.89/0.44 thf(f105,plain,(
% 0.89/0.44 (((breln1 @ sK9 @ sK8)) = sF28)),
% 0.89/0.44 inference(reorient_equations,[],[f104])).
% 0.89/0.44 thf(f106,plain,(
% 0.89/0.44 ($true = sF28)),
% 0.89/0.44 inference(definition_folding,[],[f70,f105])).
% 0.89/0.44 thf(f107,definition,(
% 0.89/0.44 (sF29 = ((breln1 @ sK9 @ sK10)))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[sF29])],[function_definition])).
% 0.89/0.44 thf(f108,plain,(
% 0.89/0.44 (((breln1 @ sK9 @ sK10)) = sF29)),
% 0.89/0.44 inference(reorient_equations,[],[f107])).
% 0.89/0.44 thf(f109,plain,(
% 0.89/0.44 ($true = sF29)),
% 0.89/0.44 inference(definition_folding,[],[f69,f108])).
% 0.89/0.44 thf(f110,definition,(
% 0.89/0.44 (sF30 = ((binunion @ sK8 @ sK10)))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[sF30])],[function_definition])).
% 0.89/0.44 thf(f111,plain,(
% 0.89/0.44 (((binunion @ sK8 @ sK10)) = sF30)),
% 0.89/0.44 inference(reorient_equations,[],[f110])).
% 0.89/0.44 thf(f112,definition,(
% 0.89/0.44 (sF31 = ((binunion @ sK10 @ sK8)))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[sF31])],[function_definition])).
% 0.89/0.44 thf(f113,plain,(
% 0.89/0.44 (sF31 != sF30)),
% 0.89/0.44 inference(definition_folding,[],[f68,f112,f111])).
% 0.89/0.44 thf(f114,plain,(
% 0.89/0.44 ($false = sF29) | ($true = ((breln1 @ sK9 @ sK10)))),
% 0.89/0.44 inference(iff_proxy_clausification,[],[f108])).
% 0.89/0.44 thf(f116,plain,(
% 0.89/0.44 ($true = ((breln1 @ sK9 @ sK8))) | (sF28 = $false)),
% 0.89/0.44 inference(iff_proxy_clausification,[],[f105])).
% 0.89/0.44 thf(f119,definition,(
% 0.89/0.44 spl32_1 <=> (breln1unionIR = $true)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition])).
% 0.89/0.44 thf(f128,definition,(
% 0.89/0.44 spl32_3 <=> (subbreln1 = $true)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition])).
% 0.89/0.44 thf(f132,definition,(
% 0.89/0.44 spl32_4 <=> ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (sK3 @ X2 @ X1 @ X0) @ X0))) | (((subset @ X1 @ X2)) = $true) | (((breln1 @ X0 @ X2)) != $true) | (((breln1 @ X0 @ X1)) != $true))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition])).
% 0.89/0.44 thf(f133,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (sK3 @ X2 @ X1 @ X0) @ X0))) | (((breln1 @ X0 @ X2)) != $true) | (((subset @ X1 @ X2)) = $true) | (((breln1 @ X0 @ X1)) != $true)) ) | ~spl32_4),
% 0.89/0.44 inference(avatar_component_clause,[],[f132])).
% 0.89/0.44 thf(f134,plain,(
% 0.89/0.44 ~spl32_3 | spl32_4),
% 0.89/0.44 inference(avatar_split_clause,[],[f63,f132,f128])).
% 0.89/0.44 thf(f141,definition,(
% 0.89/0.44 spl32_6 <=> ! [X0 : $i,X1 : $i] : ((X0 = X1) | (((subset @ X1 @ X0)) != $true) | (((subset @ X0 @ X1)) != $true))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition])).
% 0.89/0.44 thf(f142,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : ((((subset @ X1 @ X0)) != $true) | (X0 = X1) | (((subset @ X0 @ X1)) != $true)) ) | ~spl32_6),
% 0.89/0.44 inference(avatar_component_clause,[],[f141])).
% 0.89/0.44 thf(f144,definition,(
% 0.89/0.44 spl32_7 <=> (setextsub = $true)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_7])],[avatar_definition])).
% 0.89/0.44 thf(f147,plain,(
% 0.89/0.44 spl32_6 | ~spl32_7),
% 0.89/0.44 inference(avatar_split_clause,[],[f86,f144,f141])).
% 0.89/0.44 thf(f149,definition,(
% 0.89/0.44 spl32_8 <=> (breln1unionE = $true)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition])).
% 0.89/0.44 thf(f162,definition,(
% 0.89/0.44 spl32_11 <=> (breln1unionIL = $true)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_11])],[avatar_definition])).
% 0.89/0.44 thf(f166,plain,(
% 0.89/0.44 spl32_1),
% 0.89/0.44 inference(avatar_split_clause,[],[f73,f119])).
% 0.89/0.44 thf(f177,plain,(
% 0.89/0.44 spl32_7),
% 0.89/0.44 inference(avatar_split_clause,[],[f74,f144])).
% 0.89/0.44 thf(f179,definition,(
% 0.89/0.44 spl32_14 <=> ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (sK4 @ X2 @ X1 @ X0) @ X0))) | (((subset @ X1 @ X2)) = $true) | (((breln1 @ X0 @ X2)) != $true) | (((breln1 @ X0 @ X1)) != $true))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition])).
% 0.89/0.44 thf(f180,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (sK4 @ X2 @ X1 @ X0) @ X0))) | (((subset @ X1 @ X2)) = $true) | (((breln1 @ X0 @ X2)) != $true) | (((breln1 @ X0 @ X1)) != $true)) ) | ~spl32_14),
% 0.89/0.44 inference(avatar_component_clause,[],[f179])).
% 0.89/0.44 thf(f181,plain,(
% 0.89/0.44 spl32_14 | ~spl32_3),
% 0.89/0.44 inference(avatar_split_clause,[],[f65,f128,f179])).
% 0.89/0.44 thf(f182,plain,(
% 0.89/0.44 spl32_3),
% 0.89/0.44 inference(avatar_split_clause,[],[f72,f128])).
% 0.89/0.44 thf(f194,definition,(
% 0.89/0.44 spl32_17 <=> ! [X5 : $i,X9 : $i,X7 : $i,X6 : $i,X8 : $i] : (($true != ((breln1 @ X5 @ X7))) | ($true = ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((in @ X9 @ X5))) | ($true != ((breln1 @ X5 @ X6))) | ($true = ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ X8 @ X5))))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_17])],[avatar_definition])).
% 0.89/0.44 thf(f195,plain,(
% 0.89/0.44 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : (($true != ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ X8 @ X5))) | ($true != ((breln1 @ X5 @ X7))) | ($true = ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((breln1 @ X5 @ X6))) | ($true != ((in @ X9 @ X5))) | ($true = ((in @ (kpair @ X8 @ X9) @ X6)))) ) | ~spl32_17),
% 0.89/0.44 inference(avatar_component_clause,[],[f194])).
% 0.89/0.44 thf(f196,plain,(
% 0.89/0.44 spl32_17 | ~spl32_8),
% 0.89/0.44 inference(avatar_split_clause,[],[f94,f149,f194])).
% 0.89/0.44 thf(f198,definition,(
% 0.89/0.44 spl32_18 <=> ! [X2 : $i,X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X1)) != $true) | (((subset @ X1 @ X2)) = $true) | ($true = ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X1))) | (((breln1 @ X0 @ X2)) != $true))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_18])],[avatar_definition])).
% 0.89/0.44 thf(f199,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X1))) | (((subset @ X1 @ X2)) = $true) | (((breln1 @ X0 @ X2)) != $true) | (((breln1 @ X0 @ X1)) != $true)) ) | ~spl32_18),
% 0.89/0.44 inference(avatar_component_clause,[],[f198])).
% 0.89/0.44 thf(f200,plain,(
% 0.89/0.44 ~spl32_3 | spl32_18),
% 0.89/0.44 inference(avatar_split_clause,[],[f66,f198,f128])).
% 0.89/0.44 thf(f221,plain,(
% 0.89/0.44 spl32_8),
% 0.89/0.44 inference(avatar_split_clause,[],[f67,f149])).
% 0.89/0.44 thf(f228,definition,(
% 0.89/0.44 spl32_24 <=> ! [X2 : $i,X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X2)) != $true) | (((breln1 @ X0 @ X1)) != $true) | ($true != ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X2))) | (((subset @ X1 @ X2)) = $true))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_24])],[avatar_definition])).
% 0.89/0.44 thf(f229,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ X2 @ X1 @ X0) @ (sK4 @ X2 @ X1 @ X0)) @ X2))) | (((breln1 @ X0 @ X1)) != $true) | (((subset @ X1 @ X2)) = $true) | (((breln1 @ X0 @ X2)) != $true)) ) | ~spl32_24),
% 0.89/0.44 inference(avatar_component_clause,[],[f228])).
% 0.89/0.44 thf(f230,plain,(
% 0.89/0.44 spl32_24 | ~spl32_3),
% 0.89/0.44 inference(avatar_split_clause,[],[f64,f128,f228])).
% 0.89/0.44 thf(f247,definition,(
% 0.89/0.44 spl32_28 <=> ! [X5 : $i,X9 : $i,X7 : $i,X6 : $i,X8 : $i] : (($true != ((in @ X9 @ X5))) | ($true != ((breln1 @ X5 @ X6))) | ($true != ((in @ X8 @ X5))) | ($true != ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((breln1 @ X5 @ X7))) | ($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition])).
% 0.89/0.44 thf(f248,plain,(
% 0.89/0.44 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ X8 @ X5))) | ($true != ((in @ (kpair @ X8 @ X9) @ X6))) | ($true != ((breln1 @ X5 @ X7))) | ($true != ((in @ X9 @ X5))) | ($true != ((breln1 @ X5 @ X6)))) ) | ~spl32_28),
% 0.89/0.44 inference(avatar_component_clause,[],[f247])).
% 0.89/0.44 thf(f249,plain,(
% 0.89/0.44 ~spl32_11 | spl32_28),
% 0.89/0.44 inference(avatar_split_clause,[],[f76,f247,f162])).
% 0.89/0.44 thf(f250,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((breln1 @ X0 @ (binunion @ X1 @ X2))) = $true) | (((breln1 @ X0 @ X1)) != $true) | (((breln1 @ X0 @ X2)) != $true)) )),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f58,f71])).
% 0.89/0.44 thf(f275,plain,(
% 0.89/0.44 spl32_11),
% 0.89/0.44 inference(avatar_split_clause,[],[f75,f162])).
% 0.89/0.44 thf(f281,definition,(
% 0.89/0.44 spl32_35 <=> ($true = sF29)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_35])],[avatar_definition])).
% 0.89/0.44 thf(f283,plain,(
% 0.89/0.44 ($true = sF29) | ~spl32_35),
% 0.89/0.44 inference(avatar_component_clause,[],[f281])).
% 0.89/0.44 thf(f286,definition,(
% 0.89/0.44 spl32_36 <=> ($true = ((breln1 @ sK9 @ sK10)))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_36])],[avatar_definition])).
% 0.89/0.44 thf(f288,plain,(
% 0.89/0.44 ($true = ((breln1 @ sK9 @ sK10))) | ~spl32_36),
% 0.89/0.44 inference(avatar_component_clause,[],[f286])).
% 0.89/0.44 thf(f290,definition,(
% 0.89/0.44 spl32_37 <=> ($false = sF29)),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_37])],[avatar_definition])).
% 0.89/0.44 thf(f292,plain,(
% 0.89/0.44 ($false = sF29) | ~spl32_37),
% 0.89/0.44 inference(avatar_component_clause,[],[f290])).
% 0.89/0.44 thf(f293,plain,(
% 0.89/0.44 spl32_36 | spl32_37),
% 0.89/0.44 inference(avatar_split_clause,[],[f114,f290,f286])).
% 0.89/0.44 thf(f304,plain,(
% 0.89/0.44 ($true = ((breln1 @ sK9 @ sK8))) | ($true = $false)),
% 0.89/0.44 inference(forward_demodulation,[],[f116,f106])).
% 0.89/0.44 thf(f305,plain,(
% 0.89/0.44 ($true = ((breln1 @ sK9 @ sK8)))),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f304])).
% 0.89/0.44 thf(f307,definition,(
% 0.89/0.44 spl32_40 <=> ! [X5 : $i,X9 : $i,X7 : $i,X6 : $i,X8 : $i] : (($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((breln1 @ X5 @ X6))) | ($true != ((breln1 @ X5 @ X7))) | ($true != ((in @ X9 @ X5))) | ($true != ((in @ X8 @ X5))) | ($true != ((in @ (kpair @ X8 @ X9) @ X7))))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_40])],[avatar_definition])).
% 0.89/0.44 thf(f308,plain,(
% 0.89/0.44 ( ! [X8 : $i,X6 : $i,X9 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (kpair @ X8 @ X9) @ (binunion @ X6 @ X7)))) | ($true != ((in @ X8 @ X5))) | ($true != ((breln1 @ X5 @ X6))) | ($true != ((breln1 @ X5 @ X7))) | ($true != ((in @ (kpair @ X8 @ X9) @ X7))) | ($true != ((in @ X9 @ X5)))) ) | ~spl32_40),
% 0.89/0.44 inference(avatar_component_clause,[],[f307])).
% 0.89/0.44 thf(f309,plain,(
% 0.89/0.44 spl32_40 | ~spl32_1),
% 0.89/0.44 inference(avatar_split_clause,[],[f87,f119,f307])).
% 0.89/0.44 thf(f310,plain,(
% 0.89/0.44 spl32_35),
% 0.89/0.44 inference(avatar_split_clause,[],[f109,f281])).
% 0.89/0.44 thf(f326,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true = ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sK10)))) )),
% 0.89/0.44 inference(superposition,[],[f250,f111])).
% 0.89/0.44 thf(f327,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true = ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sK8)))) )),
% 0.89/0.44 inference(superposition,[],[f250,f112])).
% 0.89/0.44 thf(f331,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sF30))) | ($true != ((in @ X0 @ X2))) | ($true != ((in @ X1 @ X2))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ (kpair @ X0 @ X1) @ sK8))) | ($true != ((breln1 @ X2 @ sK8)))) ) | ~spl32_28),
% 0.89/0.44 inference(superposition,[],[f248,f111])).
% 0.89/0.44 thf(f332,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sF31))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ X1 @ X2))) | ($true != ((in @ X0 @ X2))) | ($true != ((in @ (kpair @ X0 @ X1) @ sK10))) | ($true != ((breln1 @ X2 @ sK8)))) ) | ~spl32_28),
% 0.89/0.44 inference(superposition,[],[f248,f112])).
% 0.89/0.44 thf(f335,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X2))) | ($true != $true) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((breln1 @ X2 @ sK10))) | ($true = ((subset @ X0 @ sF30))) | ($true != ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sK8))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((breln1 @ X1 @ X0)))) ) | (~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(superposition,[],[f229,f331])).
% 0.89/0.44 thf(f336,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sK8))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X2))) | ($true = ((subset @ X0 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X2)))) ) | (~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f335])).
% 0.89/0.44 thf(f337,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X2 @ sK10))) | ($true != $true) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X2 @ sK8))) | ($true = ((subset @ X0 @ sF31))) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sK10))) | ($true != ((breln1 @ X1 @ sF31)))) ) | (~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(superposition,[],[f229,f332])).
% 0.89/0.44 thf(f338,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sK10))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X1 @ sF31))) | ($true = ((subset @ X0 @ sF31))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X2)))) ) | (~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f337])).
% 0.89/0.44 thf(f339,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sF30))) | ($true != ((in @ (kpair @ X0 @ X1) @ sK10))) | ($true != ((in @ X0 @ X2))) | ($true != ((in @ X1 @ X2))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((breln1 @ X2 @ sK10)))) ) | ~spl32_40),
% 0.89/0.44 inference(superposition,[],[f308,f111])).
% 0.89/0.44 thf(f340,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sF31))) | ($true != ((in @ (kpair @ X0 @ X1) @ sK8))) | ($true != ((in @ X1 @ X2))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ X0 @ X2))) | ($true != ((breln1 @ X2 @ sK8)))) ) | ~spl32_40),
% 0.89/0.44 inference(superposition,[],[f308,f112])).
% 0.89/0.44 thf(f343,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sK10))) | ($true = ((subset @ X0 @ sF30))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X2)))) ) | (~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(superposition,[],[f229,f339])).
% 0.89/0.44 thf(f344,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sK10))) | ($true != ((breln1 @ X2 @ sK8))) | ($true = ((subset @ X0 @ sF30))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X2 @ sK10)))) ) | (~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f343])).
% 0.89/0.44 thf(f345,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sK8))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((breln1 @ X1 @ sF31))) | ($true = ((subset @ X0 @ sF31))) | ($true != $true) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X2)))) ) | (~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(superposition,[],[f229,f340])).
% 0.89/0.44 thf(f346,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sK8))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X1 @ sF31))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X1 @ X0))) | ($true = ((subset @ X0 @ sF31))) | ($true != ((breln1 @ X2 @ sK10)))) ) | (~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f345])).
% 0.89/0.44 thf(f347,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sK10))) | ($true != ((in @ X0 @ X2))) | ($true != ((in @ X1 @ X2))) | ($true != ((in @ (kpair @ X0 @ X1) @ sF30))) | ($true != ((breln1 @ X2 @ sK10))) | ($true = ((in @ (kpair @ X0 @ X1) @ sK8))) | ($true != ((breln1 @ X2 @ sK8)))) ) | ~spl32_17),
% 0.89/0.44 inference(superposition,[],[f195,f111])).
% 0.89/0.44 thf(f348,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sK10))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ X0 @ X2))) | ($true != ((in @ X1 @ X2))) | ($true != ((in @ (kpair @ X0 @ X1) @ sF31))) | ($true = ((in @ (kpair @ X0 @ X1) @ sK8))) | ($true != ((breln1 @ X2 @ sK8)))) ) | ~spl32_17),
% 0.89/0.44 inference(superposition,[],[f195,f112])).
% 0.89/0.44 thf(f380,plain,(
% 0.89/0.44 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X1 @ X0))) | ($true != $true) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X3 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X3))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sF30))) | ($true = ((subset @ X0 @ sF31))) | ($true != ((breln1 @ X2 @ sK8))) | ($true = ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sK8))) | ($true != ((breln1 @ X3 @ sK10))) | ($true != ((breln1 @ X1 @ sF31))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X3)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(superposition,[],[f338,f347])).
% 0.89/0.44 thf(f382,plain,(
% 0.89/0.44 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sF30))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X3 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X3))) | ($true != ((breln1 @ X3 @ sK10))) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ X0 @ X1) @ X2))) | ($true != ((in @ (sK4 @ sF31 @ X0 @ X1) @ X3))) | ($true != ((breln1 @ X1 @ sF31))) | ($true = ((subset @ X0 @ sF31))) | ($true = ((in @ (kpair @ (sK3 @ sF31 @ X0 @ X1) @ (sK4 @ sF31 @ X0 @ X1)) @ sK8)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f380])).
% 0.89/0.44 thf(f383,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK3 @ sF31 @ X1 @ X2) @ X0))) | ($true != ((breln1 @ X2 @ sF31))) | ($true = ((in @ (kpair @ (sK3 @ sF31 @ X1 @ X2) @ (sK4 @ sF31 @ X1 @ X2)) @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ X1 @ X2) @ X0))) | ($true != ((breln1 @ X2 @ X1))) | ($true = ((subset @ X1 @ sF31))) | ($true != ((in @ (sK4 @ sF31 @ X1 @ X2) @ X0))) | ($true != ((in @ (sK4 @ sF31 @ X1 @ X2) @ X0))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (kpair @ (sK3 @ sF31 @ X1 @ X2) @ (sK4 @ sF31 @ X1 @ X2)) @ sF30))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(condensation,[],[f382])).
% 0.89/0.44 thf(f384,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X2 @ X1))) | ($true = ((in @ (kpair @ (sK3 @ sF31 @ X1 @ X2) @ (sK4 @ sF31 @ X1 @ X2)) @ sK8))) | ($true = ((subset @ X1 @ sF31))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X2 @ sF31))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (kpair @ (sK3 @ sF31 @ X1 @ X2) @ (sK4 @ sF31 @ X1 @ X2)) @ sF30))) | ($true != ((in @ (sK4 @ sF31 @ X1 @ X2) @ X0))) | ($true != ((in @ (sK3 @ sF31 @ X1 @ X2) @ X0)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_28)),
% 0.89/0.44 inference(duplicate_literal_removal,[],[f383])).
% 0.89/0.44 thf(f390,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF31 @ X1 @ X2) @ (sK4 @ sF31 @ X1 @ X2)) @ sF30))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((in @ (sK3 @ sF31 @ X1 @ X2) @ X0))) | ($true != ((breln1 @ X2 @ sF31))) | ($true != ((breln1 @ X2 @ X1))) | ($true != ((in @ (sK4 @ sF31 @ X1 @ X2) @ X0))) | ($true = ((subset @ X1 @ sF31))) | ($true != ((breln1 @ X0 @ sK8)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f384,f346])).
% 0.89/0.44 thf(f406,definition,(
% 0.89/0.44 spl32_50 <=> ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sK8))))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_50])],[avatar_definition])).
% 0.89/0.44 thf(f407,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sK8)))) ) | ~spl32_50),
% 0.89/0.44 inference(avatar_component_clause,[],[f406])).
% 0.89/0.44 thf(f420,plain,(
% 0.89/0.44 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X2 @ sK10))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sF31))) | ($true = ((subset @ X0 @ sF30))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X3))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X3))) | ($true = ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sK8))) | ($true != ((breln1 @ X1 @ X0))) | ($true != ((breln1 @ X3 @ sK8))) | ($true != $true) | ($true != ((breln1 @ X3 @ sK10)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(superposition,[],[f344,f348])).
% 0.89/0.44 thf(f428,plain,(
% 0.89/0.44 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X1 @ X0))) | ($true = ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sK8))) | ($true != ((breln1 @ X2 @ sK8))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X3))) | ($true != ((breln1 @ X2 @ sK10))) | ($true != ((breln1 @ X3 @ sK8))) | ($true = ((subset @ X0 @ sF30))) | ($true != ((in @ (kpair @ (sK3 @ sF30 @ X0 @ X1) @ (sK4 @ sF30 @ X0 @ X1)) @ sF31))) | ($true != ((in @ (sK3 @ sF30 @ X0 @ X1) @ X2))) | ($true != ((breln1 @ X3 @ sK10))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X3))) | ($true != ((in @ (sK4 @ sF30 @ X0 @ X1) @ X2)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f420])).
% 0.89/0.44 thf(f429,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X0 @ sK10))) | ($true != ((in @ (sK3 @ sF30 @ X2 @ X1) @ X0))) | ($true != ((in @ (sK4 @ sF30 @ X2 @ X1) @ X0))) | ($true = ((subset @ X2 @ sF30))) | ($true = ((in @ (kpair @ (sK3 @ sF30 @ X2 @ X1) @ (sK4 @ sF30 @ X2 @ X1)) @ sK8))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (kpair @ (sK3 @ sF30 @ X2 @ X1) @ (sK4 @ sF30 @ X2 @ X1)) @ sF31))) | ($true != ((in @ (sK4 @ sF30 @ X2 @ X1) @ X0))) | ($true != ((breln1 @ X1 @ X2))) | ($true != ((in @ (sK3 @ sF30 @ X2 @ X1) @ X0))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(condensation,[],[f428])).
% 0.89/0.44 thf(f430,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((breln1 @ X0 @ sK8))) | ($true = ((subset @ X2 @ sF30))) | ($true != ((in @ (sK4 @ sF30 @ X2 @ X1) @ X0))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X1 @ X2))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((in @ (kpair @ (sK3 @ sF30 @ X2 @ X1) @ (sK4 @ sF30 @ X2 @ X1)) @ sF31))) | ($true = ((in @ (kpair @ (sK3 @ sF30 @ X2 @ X1) @ (sK4 @ sF30 @ X2 @ X1)) @ sK8))) | ($true != ((in @ (sK3 @ sF30 @ X2 @ X1) @ X0)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_40)),
% 0.89/0.44 inference(duplicate_literal_removal,[],[f429])).
% 0.89/0.44 thf(f440,plain,(
% 0.89/0.44 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (kpair @ (sK3 @ sF30 @ X2 @ X1) @ (sK4 @ sF30 @ X2 @ X1)) @ sF31))) | ($true = ((subset @ X2 @ sF30))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (sK4 @ sF30 @ X2 @ X1) @ X0))) | ($true != ((breln1 @ X1 @ X2))) | ($true != ((in @ (sK3 @ sF30 @ X2 @ X1) @ X0))) | ($true != ((breln1 @ X1 @ sF30))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_17 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f430,f336])).
% 0.89/0.44 thf(f488,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true != ((breln1 @ X0 @ sF31))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X1))) | ($true != $true) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((in @ (sK4 @ sF31 @ sF30 @ X0) @ X1))) | ($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sF30))) | ($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X1 @ sK8)))) ) | (~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(superposition,[],[f390,f199])).
% 0.89/0.44 thf(f489,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true = ((subset @ sF30 @ sF31))) | ($true != ((in @ (sK4 @ sF31 @ sF30 @ X0) @ X1))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X1))) | ($true != $true) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X1 @ sK8))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X1 @ sK10)))) ) | (~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(duplicate_literal_removal,[],[f488])).
% 0.89/0.44 thf(f490,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X1))) | ($true != ((in @ (sK4 @ sF31 @ sF30 @ X0) @ X1))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((breln1 @ X1 @ sK8))) | ($true != ((breln1 @ X0 @ sF31)))) ) | (~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f489])).
% 0.89/0.44 thf(f498,definition,(
% 0.89/0.44 spl32_61 <=> ! [X0 : $i,X1 : $i] : (($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X1 @ sK8))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((in @ (sK4 @ sF31 @ sF30 @ X0) @ X1))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X1))))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_61])],[avatar_definition])).
% 0.89/0.44 thf(f499,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK4 @ sF31 @ sF30 @ X0) @ X1))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X1))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((breln1 @ X1 @ sK8))) | ($true != ((breln1 @ X0 @ sF30)))) ) | ~spl32_61),
% 0.89/0.44 inference(avatar_component_clause,[],[f498])).
% 0.89/0.44 thf(f501,definition,(
% 0.89/0.44 spl32_62 <=> ($true = ((subset @ sF30 @ sF31)))),
% 0.89/0.44 introduced(definition,[new_symbols(definition,[spl32_62])],[avatar_definition])).
% 0.89/0.44 thf(f503,plain,(
% 0.89/0.44 ($true = ((subset @ sF30 @ sF31))) | ~spl32_62),
% 0.89/0.44 inference(avatar_component_clause,[],[f501])).
% 0.89/0.44 thf(f504,plain,(
% 0.89/0.44 spl32_61 | spl32_62 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40),
% 0.89/0.44 inference(avatar_split_clause,[],[f490,f307,f247,f228,f198,f194,f501,f498])).
% 0.89/0.44 thf(f505,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X0))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != $true) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sK8))) | ($true = ((subset @ sF30 @ sF31)))) ) | (~spl32_14 | ~spl32_61)),
% 0.89/0.44 inference(superposition,[],[f499,f180])).
% 0.89/0.44 thf(f506,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != $true) | ($true != ((breln1 @ X0 @ sF31))) | ($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X0))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_14 | ~spl32_61)),
% 0.89/0.44 inference(duplicate_literal_removal,[],[f505])).
% 0.89/0.44 thf(f507,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (sK3 @ sF31 @ sF30 @ X0) @ X0))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_14 | ~spl32_61)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f506])).
% 0.89/0.44 thf(f508,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sK10))) | ($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sF30)))) ) | (~spl32_4 | ~spl32_14 | ~spl32_61)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f507,f133])).
% 0.89/0.44 thf(f509,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sK8)))) ) | (~spl32_4 | ~spl32_14 | ~spl32_61)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f508,f327])).
% 0.89/0.44 thf(f510,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true = ((subset @ sF30 @ sF31))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sK8)))) ) | (~spl32_4 | ~spl32_14 | ~spl32_61)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f509,f326])).
% 0.89/0.44 thf(f511,plain,(
% 0.89/0.44 spl32_50 | spl32_62 | ~spl32_4 | ~spl32_14 | ~spl32_61),
% 0.89/0.44 inference(avatar_split_clause,[],[f510,f498,f179,f132,f501,f406])).
% 0.89/0.44 thf(f512,plain,(
% 0.89/0.44 ($true != ((subset @ sF31 @ sF30))) | ($true != $true) | (sF31 = sF30) | (~spl32_6 | ~spl32_62)),
% 0.89/0.44 inference(superposition,[],[f142,f503])).
% 0.89/0.44 thf(f513,plain,(
% 0.89/0.44 ($true != ((subset @ sF31 @ sF30))) | (sF31 = sF30) | (~spl32_6 | ~spl32_62)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f512])).
% 0.89/0.44 thf(f514,plain,(
% 0.89/0.44 ($true != ((subset @ sF31 @ sF30))) | (~spl32_6 | ~spl32_62)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f513,f113])).
% 0.89/0.44 thf(f517,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X1 @ sK8))) | ($true = ((subset @ sF31 @ sF30))) | ($true != ((in @ (sK4 @ sF30 @ sF31 @ X0) @ X1))) | ($true != ((breln1 @ X1 @ sK10))) | ($true = ((subset @ sF31 @ sF30))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X1))) | ($true != $true) | ($true != ((breln1 @ X0 @ sF31)))) ) | (~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(superposition,[],[f440,f199])).
% 0.89/0.44 thf(f524,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK4 @ sF30 @ sF31 @ X0) @ X1))) | ($true = ((subset @ sF31 @ sF30))) | ($true != $true) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X1))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X1 @ sK8))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((breln1 @ X0 @ sF31)))) ) | (~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(duplicate_literal_removal,[],[f517])).
% 0.89/0.44 thf(f525,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK4 @ sF30 @ sF31 @ X0) @ X1))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X1 @ sK8))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((breln1 @ X0 @ sF30))) | ($true = ((subset @ sF31 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X1)))) ) | (~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f524])).
% 0.89/0.44 thf(f526,plain,(
% 0.89/0.44 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ (sK4 @ sF30 @ sF31 @ X0) @ X1))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X1 @ sK10))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X1))) | ($true != ((breln1 @ X1 @ sK8)))) ) | (~spl32_6 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f525,f514])).
% 0.89/0.44 thf(f527,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sF30))) | ($true = ((subset @ sF31 @ sF30))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X0))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != $true) | ($true != ((breln1 @ X0 @ sF31)))) ) | (~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(superposition,[],[f526,f180])).
% 0.89/0.44 thf(f528,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sF31))) | ($true = ((subset @ sF31 @ sF30))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X0))) | ($true != $true)) ) | (~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(duplicate_literal_removal,[],[f527])).
% 0.89/0.44 thf(f529,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sF30))) | ($true != ((in @ (sK3 @ sF30 @ sF31 @ X0) @ X0))) | ($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sK10))) | ($true = ((subset @ sF31 @ sF30)))) ) | (~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f528])).
% 0.89/0.44 thf(f530,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sF30))) | ($true = ((subset @ sF31 @ sF30))) | ($true != ((breln1 @ X0 @ sK8)))) ) | (~spl32_4 | ~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f529,f133])).
% 0.89/0.44 thf(f531,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sF31))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_4 | ~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f530,f514])).
% 0.89/0.44 thf(f532,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK10))) | ($true != ((breln1 @ X0 @ sF30))) | ($true != ((breln1 @ X0 @ sK8)))) ) | (~spl32_4 | ~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f531,f327])).
% 0.89/0.44 thf(f533,plain,(
% 0.89/0.44 ( ! [X0 : $i] : (($true != ((breln1 @ X0 @ sK8))) | ($true != ((breln1 @ X0 @ sK10)))) ) | (~spl32_4 | ~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f532,f326])).
% 0.89/0.44 thf(f534,plain,(
% 0.89/0.44 spl32_50 | ~spl32_4 | ~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | ~spl32_62),
% 0.89/0.44 inference(avatar_split_clause,[],[f533,f501,f307,f247,f228,f198,f194,f179,f141,f132,f406])).
% 0.89/0.44 thf(f547,plain,(
% 0.89/0.44 ($true != $true) | ($true != ((breln1 @ sK9 @ sK8))) | (~spl32_36 | ~spl32_50)),
% 0.89/0.44 inference(superposition,[],[f407,f288])).
% 0.89/0.44 thf(f548,plain,(
% 0.89/0.44 ($true != ((breln1 @ sK9 @ sK8))) | (~spl32_36 | ~spl32_50)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f547])).
% 0.89/0.44 thf(f549,plain,(
% 0.89/0.44 $false | (~spl32_36 | ~spl32_50)),
% 0.89/0.44 inference(forward_subsumption_resolution,[],[f548,f305])).
% 0.89/0.44 thf(f550,plain,(
% 0.89/0.44 ~spl32_36 | ~spl32_50),
% 0.89/0.44 inference(avatar_contradiction_clause,[],[f549])).
% 0.89/0.44 thf(f552,plain,(
% 0.89/0.44 ($true = $false) | (~spl32_35 | ~spl32_37)),
% 0.89/0.44 inference(superposition,[],[f283,f292])).
% 0.89/0.44 thf(f555,plain,(
% 0.89/0.44 $false | (~spl32_35 | ~spl32_37)),
% 0.89/0.44 inference(trivial_inequality_removal,[],[f552])).
% 0.89/0.44 thf(f556,plain,(
% 0.89/0.44 ~spl32_35 | ~spl32_37),
% 0.89/0.44 inference(avatar_contradiction_clause,[],[f555])).
% 0.89/0.44 cnf(s2, plain, ~spl32_3 | spl32_4, inference(sat_conversion,[],[f134])).
% 0.89/0.44 cnf(s4, plain, spl32_6 | ~spl32_7, inference(sat_conversion,[],[f147])).
% 0.89/0.44 cnf(s7, plain, spl32_1, inference(sat_conversion,[],[f166])).
% 0.89/0.44 cnf(s10, plain, spl32_7, inference(sat_conversion,[],[f177])).
% 0.89/0.44 cnf(s11, plain, ~spl32_3 | spl32_14, inference(sat_conversion,[],[f181])).
% 0.89/0.44 cnf(s12, plain, spl32_3, inference(sat_conversion,[],[f182])).
% 0.89/0.44 cnf(s15, plain, ~spl32_8 | spl32_17, inference(sat_conversion,[],[f196])).
% 0.89/0.44 cnf(s16, plain, ~spl32_3 | spl32_18, inference(sat_conversion,[],[f200])).
% 0.89/0.44 cnf(s21, plain, spl32_8, inference(sat_conversion,[],[f221])).
% 0.89/0.44 cnf(s23, plain, ~spl32_3 | spl32_24, inference(sat_conversion,[],[f230])).
% 0.89/0.44 cnf(s27, plain, ~spl32_11 | spl32_28, inference(sat_conversion,[],[f249])).
% 0.89/0.44 cnf(s33, plain, spl32_11, inference(sat_conversion,[],[f275])).
% 0.89/0.44 cnf(s35, plain, spl32_36 | spl32_37, inference(sat_conversion,[],[f293])).
% 0.89/0.44 cnf(s38, plain, ~spl32_1 | spl32_40, inference(sat_conversion,[],[f309])).
% 0.89/0.44 cnf(s39, plain, spl32_35, inference(sat_conversion,[],[f310])).
% 0.89/0.44 cnf(s54, plain, ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | spl32_61 | spl32_62, inference(sat_conversion,[],[f504])).
% 0.89/0.44 cnf(s55, plain, ~spl32_4 | ~spl32_14 | spl32_50 | ~spl32_61 | spl32_62, inference(sat_conversion,[],[f511])).
% 0.89/0.44 cnf(s56, plain, ~spl32_4 | ~spl32_6 | ~spl32_14 | ~spl32_17 | ~spl32_18 | ~spl32_24 | ~spl32_28 | ~spl32_40 | spl32_50 | ~spl32_62, inference(sat_conversion,[],[f534])).
% 0.89/0.44 cnf(s59, plain, ~spl32_36 | ~spl32_50, inference(sat_conversion,[],[f550])).
% 0.89/0.44 cnf(s61, plain, ~spl32_35 | ~spl32_37, inference(sat_conversion,[],[f556])).
% 0.89/0.44 cnf(s62, plain, ~spl32_37, inference(rat,[],[s61,s39])).
% 0.89/0.44 cnf(s63, plain, spl32_36, inference(rat,[],[s35,s62])).
% 0.89/0.44 cnf(s64, plain, ~spl32_50, inference(rat,[],[s59,s63])).
% 0.89/0.44 cnf(s65, plain, spl32_28, inference(rat,[],[s27,s33])).
% 0.89/0.44 cnf(s66, plain, spl32_17, inference(rat,[],[s15,s21])).
% 0.89/0.44 cnf(s67, plain, spl32_24, inference(rat,[],[s23,s12])).
% 0.89/0.44 cnf(s68, plain, spl32_18, inference(rat,[],[s16,s12])).
% 0.89/0.44 cnf(s69, plain, spl32_14, inference(rat,[],[s11,s12])).
% 0.89/0.44 cnf(s70, plain, spl32_40, inference(rat,[],[s38,s7])).
% 0.89/0.44 cnf(s71, plain, spl32_6, inference(rat,[],[s4,s10])).
% 0.89/0.44 cnf(s72, plain, spl32_4, inference(rat,[],[s2,s12])).
% 0.89/0.44 cnf(s73, plain, ~spl32_62, inference(rat,[],[s56,s71,s64,s70,s65,s67,s68,s66,s69,s72])).
% 0.89/0.44 cnf(s74, plain, ~spl32_61, inference(rat,[],[s55,s73,s69,s64,s72])).
% 0.89/0.44 cnf(s75, plain, $false, inference(rat,[],[s54,s70,s68,s67,s65,s66,s73,s74])).
% 0.89/0.44 thf(f557,plain,(
% 0.89/0.44 $false),
% 0.89/0.44 inference(avatar_sat_refutation,[],[s75])).
% 0.89/0.44 % SZS output end Proof for theBenchmark
% 0.89/0.44 % (164971)------------------------------
% 0.89/0.44 % (164971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.44 % (164971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.44 % (164971)CaDiCaL version: 2.1.3
% 0.89/0.44 % (164971)Termination reason: Refutation
% 0.89/0.44 % (164971)Time elapsed: 0.035 s
% 0.89/0.44 % (164971)Peak memory usage: 13 MB
% 0.89/0.44 % (164971)Instructions burned: 68 (million)
% 0.89/0.44 % (164920)Success in time 0.197 s
% 0.89/0.44 % Vampire exiting
%------------------------------------------------------------------------------