%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU757^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 : n010.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:10 AM UTC 2026
% Result : Theorem 1.35s 0.57s
% Output : Refutation 1.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU757^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 % Computer : n010.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Tue Sep 29 14:22:48 UTC 2026
% 0.09/0.24 % CPUTime :
% 0.09/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.29 Running higher-order theorem proving
% 0.23/0.30 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.49/0.51 % (2934565)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.49/0.51 % (2934571)lrs+10_16_si=on:nwc=1.5:random_seed=2356626798:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.49/0.51 % (2934573)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=2626984809: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.49/0.51 % (2934571)Instruction limit reached!
% 0.49/0.51 % (2934571)------------------------------
% 0.49/0.51 % (2934571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.51 % (2934571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.51 % (2934571)CaDiCaL version: 2.1.3
% 0.49/0.51 % (2934571)Termination reason: Instruction limit
% 0.49/0.51 % (2934571)Termination phase: Saturation
% 0.49/0.51 % (2934571)Time elapsed: 0.010 s
% 0.49/0.51 % (2934571)Peak memory usage: 12 MB
% 0.49/0.51 % (2934571)Instructions burned: 20 (million)
% 0.49/0.51 % (2934570)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3129774399:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.49/0.51 % (2934572)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3570260192:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.49/0.51 % (2934576)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.49/0.51 % (2934576)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.49/0.51 % (2934572)Instruction limit reached!
% 0.49/0.51 % (2934572)------------------------------
% 0.49/0.51 % (2934572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.51 % (2934572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.51 % (2934572)CaDiCaL version: 2.1.3
% 0.49/0.51 % (2934572)Termination reason: Instruction limit
% 0.49/0.51 % (2934572)Termination phase: Saturation
% 0.49/0.51 % (2934572)Time elapsed: 0.005 s
% 0.49/0.51 % (2934572)Peak memory usage: 11 MB
% 0.49/0.51 % (2934572)Instructions burned: 5 (million)
% 0.49/0.51 % (2934574)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1407313068:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.49/0.51 % (2934575)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1992238711:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.49/0.51 % (2934576)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=2596018918:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.49/0.51 % (2934581)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3123427728:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.49/0.51 % (2934581)Instruction limit reached!
% 0.49/0.51 % (2934581)------------------------------
% 0.49/0.51 % (2934581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.51 % (2934581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.51 % (2934581)CaDiCaL version: 2.1.3
% 0.49/0.51 % (2934581)Termination reason: Instruction limit
% 0.49/0.51 % (2934581)Termination phase: Property scanning
% 0.49/0.51 % (2934581)Time elapsed: 0.002 s
% 0.49/0.51 % (2934581)Peak memory usage: 10 MB
% 0.49/0.51 % (2934581)Instructions burned: 4 (million)
% 0.49/0.51 % (2934574)Instruction limit reached!
% 0.49/0.51 % (2934574)------------------------------
% 0.49/0.51 % (2934574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.51 % (2934574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.51 % (2934574)CaDiCaL version: 2.1.3
% 0.49/0.51 % (2934574)Termination reason: Instruction limit
% 0.49/0.51 % (2934574)Termination phase: Saturation
% 0.49/0.51 % (2934574)Time elapsed: 0.023 s
% 0.49/0.51 % (2934574)Peak memory usage: 12 MB
% 0.49/0.51 % (2934574)Instructions burned: 24 (million)
% 0.49/0.51 % (2934585)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1075634491:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.35/0.57 % (2934587)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.35/0.57 % (2934585)Instruction limit reached!
% 1.35/0.57 % (2934585)------------------------------
% 1.35/0.57 % (2934585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934585)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934585)Termination reason: Instruction limit
% 1.35/0.57 % (2934585)Termination phase: Saturation
% 1.35/0.57 % (2934585)Time elapsed: 0.005 s
% 1.35/0.57 % (2934585)Peak memory usage: 11 MB
% 1.35/0.57 % (2934585)Instructions burned: 5 (million)
% 1.35/0.57 % (2934587)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2471974648:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.35/0.57 % (2934587)Instruction limit reached!
% 1.35/0.57 % (2934587)------------------------------
% 1.35/0.57 % (2934587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934587)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934587)Termination reason: Instruction limit
% 1.35/0.57 % (2934587)Termination phase: Saturation
% 1.35/0.57 % (2934587)Time elapsed: 0.008 s
% 1.35/0.57 % (2934587)Peak memory usage: 12 MB
% 1.35/0.57 % (2934587)Instructions burned: 8 (million)
% 1.35/0.57 % (2934590)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
% 1.35/0.57 % (2934590)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.35/0.57 % (2934588)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3162467828:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.35/0.57 % (2934590)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1284044173:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.35/0.57 % (2934570)Instruction limit reached!
% 1.35/0.57 % (2934570)------------------------------
% 1.35/0.57 % (2934570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934570)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934570)Termination reason: Instruction limit
% 1.35/0.57 % (2934570)Termination phase: Saturation
% 1.35/0.57 % (2934570)Time elapsed: 0.076 s
% 1.35/0.57 % (2934570)Peak memory usage: 12 MB
% 1.35/0.57 % (2934570)Instructions burned: 87 (million)
% 1.35/0.57 % (2934588)Instruction limit reached!
% 1.35/0.57 % (2934588)------------------------------
% 1.35/0.57 % (2934588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934588)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934588)Termination reason: Instruction limit
% 1.35/0.57 % (2934588)Termination phase: Saturation
% 1.35/0.57 % (2934588)Time elapsed: 0.008 s
% 1.35/0.57 % (2934588)Peak memory usage: 12 MB
% 1.35/0.57 % (2934588)Instructions burned: 13 (million)
% 1.35/0.57 % (2934575)Instruction limit reached!
% 1.35/0.57 % (2934575)------------------------------
% 1.35/0.57 % (2934575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934575)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934575)Termination reason: Instruction limit
% 1.35/0.57 % (2934575)Termination phase: Saturation
% 1.35/0.57 % (2934575)Time elapsed: 0.069 s
% 1.35/0.57 % (2934575)Peak memory usage: 12 MB
% 1.35/0.57 % (2934575)Instructions burned: 76 (million)
% 1.35/0.57 % (2934594)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=1910300707:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.35/0.57 % (2934590)Instruction limit reached!
% 1.35/0.57 % (2934590)------------------------------
% 1.35/0.57 % (2934590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934590)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934590)Termination reason: Instruction limit
% 1.35/0.57 % (2934590)Termination phase: Saturation
% 1.35/0.57 % (2934590)Time elapsed: 0.018 s
% 1.35/0.57 % (2934590)Peak memory usage: 11 MB
% 1.35/0.57 % (2934590)Instructions burned: 30 (million)
% 1.35/0.57 % (2934596)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.35/0.57 % (2934596)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=4189270878:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.35/0.57 % (2934599)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1287425021:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.35/0.57 % (2934595)lrs+10_1_si=on:cs=on:random_seed=2423239693:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.35/0.57 % (2934597)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=226735764:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.35/0.57 % (2934596)Instruction limit reached!
% 1.35/0.57 % (2934596)------------------------------
% 1.35/0.57 % (2934596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934596)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934596)Termination reason: Instruction limit
% 1.35/0.57 % (2934596)Termination phase: Saturation
% 1.35/0.57 % (2934596)Time elapsed: 0.007 s
% 1.35/0.57 % (2934596)Peak memory usage: 11 MB
% 1.35/0.57 % (2934596)Instructions burned: 4 (million)
% 1.35/0.57 % (2934595)Instruction limit reached!
% 1.35/0.57 % (2934595)------------------------------
% 1.35/0.57 % (2934595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934595)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934595)Termination reason: Instruction limit
% 1.35/0.57 % (2934595)Termination phase: Saturation
% 1.35/0.57 % (2934595)Time elapsed: 0.007 s
% 1.35/0.57 % (2934595)Peak memory usage: 12 MB
% 1.35/0.57 % (2934595)Instructions burned: 8 (million)
% 1.35/0.57 % (2934594)Instruction limit reached!
% 1.35/0.57 % (2934594)------------------------------
% 1.35/0.57 % (2934594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934594)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934594)Termination reason: Instruction limit
% 1.35/0.57 % (2934594)Termination phase: Saturation
% 1.35/0.57 % (2934594)Time elapsed: 0.040 s
% 1.35/0.57 % (2934594)Peak memory usage: 13 MB
% 1.35/0.57 % (2934594)Instructions burned: 88 (million)
% 1.35/0.57 % (2934597)Instruction limit reached!
% 1.35/0.57 % (2934597)------------------------------
% 1.35/0.57 % (2934597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934597)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934597)Termination reason: Instruction limit
% 1.35/0.57 % (2934597)Termination phase: Saturation
% 1.35/0.57 % (2934597)Time elapsed: 0.034 s
% 1.35/0.57 % (2934597)Peak memory usage: 12 MB
% 1.35/0.57 % (2934597)Instructions burned: 39 (million)
% 1.35/0.57 % (2934576)Instruction limit reached!
% 1.35/0.57 % (2934576)------------------------------
% 1.35/0.57 % (2934576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934576)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934576)Termination reason: Instruction limit
% 1.35/0.57 % (2934576)Termination phase: Saturation
% 1.35/0.57 % (2934576)Time elapsed: 0.136 s
% 1.35/0.57 % (2934576)Peak memory usage: 12 MB
% 1.35/0.57 % (2934576)Instructions burned: 157 (million)
% 1.35/0.57 % (2934606)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=953077593:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.35/0.57 % (2934607)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=30331987:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.35/0.57 % (2934604)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1573496855:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.35/0.57 % (2934608)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2606404068:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.35/0.57 % (2934607)Instruction limit reached!
% 1.35/0.57 % (2934607)------------------------------
% 1.35/0.57 % (2934607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934607)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934607)Termination reason: Instruction limit
% 1.35/0.57 % (2934607)Termination phase: Saturation
% 1.35/0.57 % (2934607)Time elapsed: 0.008 s
% 1.35/0.57 % (2934607)Peak memory usage: 12 MB
% 1.35/0.57 % (2934607)Instructions burned: 15 (million)
% 1.35/0.57 % (2934605)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=1497111691:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.35/0.57 % (2934608)Instruction limit reached!
% 1.35/0.57 % (2934608)------------------------------
% 1.35/0.57 % (2934608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934608)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934608)Termination reason: Instruction limit
% 1.35/0.57 % (2934608)Termination phase: Saturation
% 1.35/0.57 % (2934608)Time elapsed: 0.007 s
% 1.35/0.57 % (2934608)Peak memory usage: 11 MB
% 1.35/0.57 % (2934608)Instructions burned: 15 (million)
% 1.35/0.57 % (2934573) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2934565-2934573"...
% 1.35/0.57 % (2934615)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1305587592:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 1.35/0.57 % (2934605)Instruction limit reached!
% 1.35/0.57 % (2934605)------------------------------
% 1.35/0.57 % (2934605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934605)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934605)Termination reason: Instruction limit
% 1.35/0.57 % (2934605)Termination phase: Saturation
% 1.35/0.57 % (2934605)Time elapsed: 0.029 s
% 1.35/0.57 % (2934605)Peak memory usage: 12 MB
% 1.35/0.57 % (2934605)Instructions burned: 15 (million)
% 1.35/0.57 % (2934613)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3163297367:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 1.35/0.57 % (2934615)Instruction limit reached!
% 1.35/0.57 % (2934615)------------------------------
% 1.35/0.57 % (2934615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934615)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934615)Termination reason: Instruction limit
% 1.35/0.57 % (2934615)Termination phase: Saturation
% 1.35/0.57 % (2934615)Time elapsed: 0.012 s
% 1.35/0.57 % (2934615)Peak memory usage: 11 MB
% 1.35/0.57 % (2934615)Instructions burned: 23 (million)
% 1.35/0.57 % (2934604)Instruction limit reached!
% 1.35/0.57 % (2934604)------------------------------
% 1.35/0.57 % (2934604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.57 % (2934604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.57 % (2934604)CaDiCaL version: 2.1.3
% 1.35/0.57 % (2934604)Termination reason: Instruction limit
% 1.35/0.57 % (2934604)Termination phase: Saturation
% 1.35/0.57 % (2934604)Time elapsed: 0.049 s
% 1.35/0.57 % (2934604)Peak memory usage: 12 MB
% 1.35/0.57 % (2934604)Instructions burned: 26 (million)
% 1.35/0.57 % (2934573)...printing done.
% 1.35/0.57 % (2934573)Refutation found. Thanks to Tanya!
% 1.35/0.57 % SZS status Theorem for theBenchmark
% 1.35/0.57 % SZS output start Proof for theBenchmark
% 1.35/0.57 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.35/0.57 thf(func_def_0, type, in: ($i > $i > $o)).
% 1.35/0.57 thf(func_def_1, type, powerset: ($i > $i)).
% 1.35/0.57 thf(func_def_2, type, binunion: ($i > $i > $i)).
% 1.35/0.57 thf(func_def_3, type, binintersect: ($i > $i > $i)).
% 1.35/0.57 thf(func_def_4, type, setminus: ($i > $i > $i)).
% 1.35/0.57 thf(func_def_5, type, binintersectT_lem: $o).
% 1.35/0.57 thf(func_def_7, type, binunionT_lem: $o).
% 1.35/0.57 thf(func_def_8, type, complementT_lem: $o).
% 1.35/0.57 thf(func_def_9, type, setextT: $o).
% 1.35/0.57 thf(func_def_10, type, demorgan2a: $o).
% 1.35/0.57 thf(func_def_11, type, demorgan2b: $o).
% 1.35/0.57 thf(func_def_21, type, sK7: ($i > $i > $i > $i)).
% 1.35/0.57 thf(func_def_22, type, sK8: ($i > $i > $i > $i)).
% 1.35/0.57 thf(f1,axiom,(
% 1.35/0.57 (binintersectT_lem = ! [X1 : $i,X0 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (in @ (binintersect @ X1 @ X2) @ (powerset @ X0)))))),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',binintersectT_lem)).
% 1.35/0.57 thf(f2,axiom,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (in @ (binunion @ X1 @ X2) @ (powerset @ X0)))) = binunionT_lem)),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',binunionT_lem)).
% 1.35/0.57 thf(f3,axiom,(
% 1.35/0.57 (! [X1 : $i,X0 : $i] : ((in @ X1 @ (powerset @ X0)) => (in @ (setminus @ X0 @ X1) @ (powerset @ X0))) = complementT_lem)),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complementT_lem)).
% 1.35/0.57 thf(f4,axiom,(
% 1.35/0.57 (! [X1 : $i,X0 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ X1) => (in @ X3 @ X2))) => (! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ X2) => (in @ X3 @ X1))) => (X1 = X2))))) = setextT)),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setextT)).
% 1.35/0.57 thf(f5,axiom,(
% 1.35/0.57 (! [X1 : $i,X0 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2))) => (in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))) = demorgan2a)),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan2a)).
% 1.35/0.57 thf(f6,axiom,(
% 1.35/0.57 (demorgan2b = ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) => (in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2))))))))),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan2b)).
% 1.35/0.57 thf(f7,conjecture,(
% 1.35/0.57 binintersectT_lem => (binunionT_lem => (complementT_lem => (setextT => (demorgan2a => (demorgan2b => ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))))))))))),
% 1.35/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan2)).
% 1.35/0.57 thf(f8,negated_conjecture,(
% 1.35/0.57 ~(binintersectT_lem => (binunionT_lem => (complementT_lem => (setextT => (demorgan2a => (demorgan2b => ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))))))),
% 1.35/0.57 inference(negated_conjecture,[status(cth)],[f7])).
% 1.35/0.57 thf(f9,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : ((in @ X0 @ (powerset @ X1)) => (in @ (setminus @ X1 @ X0) @ (powerset @ X1))) = complementT_lem)),
% 1.35/0.57 inference(rectify,[],[f3])).
% 1.35/0.57 thf(f10,plain,(
% 1.35/0.57 (complementT_lem = $true) <=> ! [X0 : $i,X1 : $i] : (($true = ((in @ X0 @ (powerset @ X1)))) => ($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))))),
% 1.35/0.57 inference(fool_elimination,[],[f9])).
% 1.35/0.57 thf(f11,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : ((in @ X0 @ (powerset @ X1)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X1)) => (! [X3 : $i] : ((in @ X3 @ X1) => ((in @ X3 @ X0) => (in @ X3 @ X2))) => (! [X4 : $i] : ((in @ X4 @ X1) => ((in @ X4 @ X2) => (in @ X4 @ X0))) => (X0 = X2))))) = setextT)),
% 1.35/0.57 inference(rectify,[],[f4])).
% 1.35/0.57 thf(f12,plain,(
% 1.35/0.57 (setextT = $true) <=> ! [X0 : $i,X1 : $i] : (($true = ((in @ X0 @ (powerset @ X1)))) => ! [X2 : $i] : (($true = ((in @ X2 @ (powerset @ X1)))) => (! [X3 : $i] : ((((in @ X3 @ X1)) = $true) => ((((in @ X3 @ X0)) = $true) => (((in @ X3 @ X2)) = $true))) => (! [X4 : $i] : (($true = ((in @ X4 @ X1))) => (($true = ((in @ X4 @ X2))) => ($true = ((in @ X4 @ X0))))) => (X0 = X2)))))),
% 1.35/0.57 inference(fool_elimination,[],[f11])).
% 1.35/0.57 thf(f13,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (in @ (binunion @ X1 @ X2) @ (powerset @ X0)))) = binunionT_lem)),
% 1.35/0.57 inference(rectify,[],[f2])).
% 1.35/0.57 thf(f14,plain,(
% 1.35/0.57 ! [X1 : $i,X0 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => (((in @ (binunion @ X1 @ X2) @ (powerset @ X0))) = $true))) <=> (binunionT_lem = $true)),
% 1.35/0.57 inference(fool_elimination,[],[f13])).
% 1.35/0.57 thf(f15,plain,(
% 1.35/0.57 (demorgan2b = ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) => (in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2))))))))),
% 1.35/0.57 inference(rectify,[],[f6])).
% 1.35/0.57 thf(f16,plain,(
% 1.35/0.57 ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => ((((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) => (((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2)))) = $true))))) <=> (demorgan2b = $true)),
% 1.35/0.57 inference(fool_elimination,[],[f15])).
% 1.35/0.57 thf(f17,plain,(
% 1.35/0.57 ~(binintersectT_lem => (binunionT_lem => (complementT_lem => (setextT => (demorgan2a => (demorgan2b => ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))))))),
% 1.35/0.57 inference(rectify,[],[f8])).
% 1.35/0.57 thf(f18,plain,(
% 1.35/0.57 ~((binintersectT_lem = $true) => ((binunionT_lem = $true) => ((complementT_lem = $true) => ((setextT = $true) => ((demorgan2a = $true) => ((demorgan2b = $true) => ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))))))),
% 1.35/0.57 inference(fool_elimination,[],[f17])).
% 1.35/0.57 thf(f19,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : ((in @ X0 @ (powerset @ X1)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X1)) => ! [X3 : $i] : ((in @ X3 @ X1) => ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2))) => (in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))))))) = demorgan2a)),
% 1.35/0.57 inference(rectify,[],[f5])).
% 1.35/0.57 thf(f20,plain,(
% 1.35/0.57 (demorgan2a = $true) <=> ! [X0 : $i,X1 : $i] : (($true = ((in @ X0 @ (powerset @ X1)))) => ! [X2 : $i] : (($true = ((in @ X2 @ (powerset @ X1)))) => ! [X3 : $i] : ((((in @ X3 @ X1)) = $true) => (($true = ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2))))) => ($true = ((in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2)))))))))),
% 1.35/0.57 inference(fool_elimination,[],[f19])).
% 1.35/0.57 thf(f21,plain,(
% 1.35/0.57 (binintersectT_lem = ! [X0 : $i,X1 : $i] : ((in @ X0 @ (powerset @ X1)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X1)) => (in @ (binintersect @ X0 @ X2) @ (powerset @ X1)))))),
% 1.35/0.57 inference(rectify,[],[f1])).
% 1.35/0.57 thf(f22,plain,(
% 1.35/0.57 (binintersectT_lem = $true) <=> ! [X1 : $i,X0 : $i] : (($true = ((in @ X0 @ (powerset @ X1)))) => ! [X2 : $i] : (($true = ((in @ X2 @ (powerset @ X1)))) => ($true = ((in @ (binintersect @ X0 @ X2) @ (powerset @ X1))))))),
% 1.35/0.57 inference(fool_elimination,[],[f21])).
% 1.35/0.57 thf(f23,plain,(
% 1.35/0.57 ! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1))))) <=> (complementT_lem = $true)),
% 1.35/0.57 inference(ennf_transformation,[],[f10])).
% 1.35/0.57 thf(f24,plain,(
% 1.35/0.57 (binintersectT_lem = $true) <=> ! [X1 : $i,X0 : $i] : (! [X2 : $i] : (($true = ((in @ (binintersect @ X0 @ X2) @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1))))) | ($true != ((in @ X0 @ (powerset @ X1)))))),
% 1.35/0.57 inference(ennf_transformation,[],[f22])).
% 1.35/0.57 thf(f25,plain,(
% 1.35/0.57 ! [X1 : $i,X0 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : ((((in @ (binunion @ X1 @ X2) @ (powerset @ X0))) = $true) | (((in @ X2 @ (powerset @ X0))) != $true))) <=> (binunionT_lem = $true)),
% 1.35/0.57 inference(ennf_transformation,[],[f14])).
% 1.35/0.57 thf(f26,plain,(
% 1.35/0.57 (demorgan2a = $true) <=> ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : ((($true = ((in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))))) | ($true != ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2)))))) | (((in @ X3 @ X1)) != $true)) | ($true != ((in @ X2 @ (powerset @ X1))))) | ($true != ((in @ X0 @ (powerset @ X1)))))),
% 1.35/0.57 inference(ennf_transformation,[],[f20])).
% 1.35/0.57 thf(f27,plain,(
% 1.35/0.57 (demorgan2a = $true) <=> ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (($true = ((in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))))) | (((in @ X3 @ X1)) != $true) | ($true != ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2)))))) | ($true != ((in @ X2 @ (powerset @ X1))))) | ($true != ((in @ X0 @ (powerset @ X1)))))),
% 1.35/0.57 inference(flattening,[],[f26])).
% 1.35/0.57 thf(f28,plain,(
% 1.35/0.57 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (((((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2)))) = $true) | (((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true)) | (((in @ X3 @ X0)) != $true)) | (((in @ X2 @ (powerset @ X0))) != $true)) | (((in @ X1 @ (powerset @ X0))) != $true)) <=> (demorgan2b = $true)),
% 1.35/0.57 inference(ennf_transformation,[],[f16])).
% 1.35/0.57 thf(f29,plain,(
% 1.35/0.57 (demorgan2b = $true) <=> ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2)))) = $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true)) | (((in @ X2 @ (powerset @ X0))) != $true)))),
% 1.35/0.57 inference(flattening,[],[f28])).
% 1.35/0.57 thf(f30,plain,(
% 1.35/0.57 (((((? [X1 : $i,X0 : $i] : (? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & (((setminus @ X0 @ (binunion @ X1 @ X2))) != ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) & (((in @ X1 @ (powerset @ X0))) = $true)) & (demorgan2b = $true)) & (demorgan2a = $true)) & (setextT = $true)) & (complementT_lem = $true)) & (binunionT_lem = $true)) & (binintersectT_lem = $true)),
% 1.35/0.57 inference(ennf_transformation,[],[f18])).
% 1.35/0.57 thf(f31,plain,(
% 1.35/0.57 ? [X1 : $i,X0 : $i] : (? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & (((setminus @ X0 @ (binunion @ X1 @ X2))) != ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) & (((in @ X1 @ (powerset @ X0))) = $true)) & (binunionT_lem = $true) & (complementT_lem = $true) & (demorgan2a = $true) & (binintersectT_lem = $true) & (demorgan2b = $true) & (setextT = $true)),
% 1.35/0.57 inference(flattening,[],[f30])).
% 1.35/0.57 thf(f32,plain,(
% 1.35/0.57 (setextT = $true) <=> ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((X0 = X2) | ? [X4 : $i] : ((($true != ((in @ X4 @ X0))) & ($true = ((in @ X4 @ X2)))) & ($true = ((in @ X4 @ X1))))) | ? [X3 : $i] : (((((in @ X3 @ X2)) != $true) & (((in @ X3 @ X0)) = $true)) & (((in @ X3 @ X1)) = $true))) | ($true != ((in @ X2 @ (powerset @ X1))))) | ($true != ((in @ X0 @ (powerset @ X1)))))),
% 1.35/0.57 inference(ennf_transformation,[],[f12])).
% 1.35/0.57 thf(f33,plain,(
% 1.35/0.57 (setextT = $true) <=> ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (? [X4 : $i] : (($true = ((in @ X4 @ X2))) & ($true = ((in @ X4 @ X1))) & ($true != ((in @ X4 @ X0)))) | (X0 = X2) | ($true != ((in @ X2 @ (powerset @ X1)))) | ? [X3 : $i] : ((((in @ X3 @ X1)) = $true) & (((in @ X3 @ X2)) != $true) & (((in @ X3 @ X0)) = $true))) | ($true != ((in @ X0 @ (powerset @ X1)))))),
% 1.35/0.57 inference(flattening,[],[f32])).
% 1.35/0.57 thf(f34,plain,(
% 1.35/0.57 ((demorgan2a = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : (? [X3 : $i] : (($true != ((in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))))) & (((in @ X3 @ X1)) = $true) & ($true = ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2)))))) & ($true = ((in @ X2 @ (powerset @ X1))))) & ($true = ((in @ X0 @ (powerset @ X1)))))) & (! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (($true = ((in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))))) | (((in @ X3 @ X1)) != $true) | ($true != ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2)))))) | ($true != ((in @ X2 @ (powerset @ X1))))) | ($true != ((in @ X0 @ (powerset @ X1))))) | (demorgan2a != $true))),
% 1.35/0.57 inference(nnf_transformation,[],[f27])).
% 1.35/0.57 thf(f35,plain,(
% 1.35/0.57 ((demorgan2a = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : (? [X3 : $i] : (($true != ((in @ X3 @ (binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))))) & (((in @ X3 @ X1)) = $true) & ($true = ((in @ X3 @ (setminus @ X1 @ (binunion @ X0 @ X2)))))) & ($true = ((in @ X2 @ (powerset @ X1))))) & ($true = ((in @ X0 @ (powerset @ X1)))))) & (! [X4 : $i,X5 : $i] : (! [X6 : $i] : (! [X7 : $i] : (($true = ((in @ X7 @ (binintersect @ (setminus @ X5 @ X4) @ (setminus @ X5 @ X6))))) | ($true != ((in @ X7 @ X5))) | ($true != ((in @ X7 @ (setminus @ X5 @ (binunion @ X4 @ X6)))))) | ($true != ((in @ X6 @ (powerset @ X5))))) | ($true != ((in @ X4 @ (powerset @ X5))))) | (demorgan2a != $true))),
% 1.35/0.57 inference(rectify,[],[f34])).
% 1.35/0.57 thf(f36,plain,(
% 1.35/0.57 ((demorgan2a = $true) | (((($true != ((in @ sK3 @ (binintersect @ (setminus @ sK1 @ sK0) @ (setminus @ sK1 @ sK2))))) & ($true = ((in @ sK3 @ sK1))) & (((in @ sK3 @ (setminus @ sK1 @ (binunion @ sK0 @ sK2)))) = $true)) & ($true = ((in @ sK2 @ (powerset @ sK1))))) & ($true = ((in @ sK0 @ (powerset @ sK1)))))) & (! [X4 : $i,X5 : $i] : (! [X6 : $i] : (! [X7 : $i] : (($true = ((in @ X7 @ (binintersect @ (setminus @ X5 @ X4) @ (setminus @ X5 @ X6))))) | ($true != ((in @ X7 @ X5))) | ($true != ((in @ X7 @ (setminus @ X5 @ (binunion @ X4 @ X6)))))) | ($true != ((in @ X6 @ (powerset @ X5))))) | ($true != ((in @ X4 @ (powerset @ X5))))) | (demorgan2a != $true))),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f35])).
% 1.35/0.57 thf(f37,plain,(
% 1.35/0.57 ((setextT = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : (! [X4 : $i] : (($true != ((in @ X4 @ X2))) | ($true != ((in @ X4 @ X1))) | ($true = ((in @ X4 @ X0)))) & (X0 != X2) & ($true = ((in @ X2 @ (powerset @ X1)))) & ! [X3 : $i] : ((((in @ X3 @ X1)) != $true) | (((in @ X3 @ X2)) = $true) | (((in @ X3 @ X0)) != $true))) & ($true = ((in @ X0 @ (powerset @ X1)))))) & (! [X0 : $i,X1 : $i] : (! [X2 : $i] : (? [X4 : $i] : (($true = ((in @ X4 @ X2))) & ($true = ((in @ X4 @ X1))) & ($true != ((in @ X4 @ X0)))) | (X0 = X2) | ($true != ((in @ X2 @ (powerset @ X1)))) | ? [X3 : $i] : ((((in @ X3 @ X1)) = $true) & (((in @ X3 @ X2)) != $true) & (((in @ X3 @ X0)) = $true))) | ($true != ((in @ X0 @ (powerset @ X1))))) | (setextT != $true))),
% 1.35/0.57 inference(nnf_transformation,[],[f33])).
% 1.35/0.57 thf(f38,plain,(
% 1.35/0.57 ((setextT = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X2)) != $true) | (((in @ X3 @ X1)) != $true) | (((in @ X3 @ X0)) = $true)) & (X0 != X2) & ($true = ((in @ X2 @ (powerset @ X1)))) & ! [X4 : $i] : (($true != ((in @ X4 @ X1))) | ($true = ((in @ X4 @ X2))) | ($true != ((in @ X4 @ X0))))) & ($true = ((in @ X0 @ (powerset @ X1)))))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : (? [X8 : $i] : (($true = ((in @ X8 @ X7))) & ($true = ((in @ X8 @ X6))) & ($true != ((in @ X8 @ X5)))) | (X5 = X7) | ($true != ((in @ X7 @ (powerset @ X6)))) | ? [X9 : $i] : (($true = ((in @ X9 @ X6))) & ($true != ((in @ X9 @ X7))) & ($true = ((in @ X9 @ X5))))) | ($true != ((in @ X5 @ (powerset @ X6))))) | (setextT != $true))),
% 1.35/0.57 inference(rectify,[],[f37])).
% 1.35/0.57 thf(f39,plain,(
% 1.35/0.57 ((setextT = $true) | ((! [X3 : $i] : (($true != ((in @ X3 @ sK6))) | ($true != ((in @ X3 @ sK5))) | ($true = ((in @ X3 @ sK4)))) & (sK6 != sK4) & ($true = ((in @ sK6 @ (powerset @ sK5)))) & ! [X4 : $i] : (($true != ((in @ X4 @ sK5))) | ($true = ((in @ X4 @ sK6))) | ($true != ((in @ X4 @ sK4))))) & ($true = ((in @ sK4 @ (powerset @ sK5)))))) & (! [X5 : $i,X6 : $i] : (! [X7 : $i] : ((($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) & ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) & ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5)))) | (X5 = X7) | ($true != ((in @ X7 @ (powerset @ X6)))) | (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) & ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) & ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))))) | ($true != ((in @ X5 @ (powerset @ X6))))) | (setextT != $true))),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,vAPP,vAPP]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X9,sK8 @ X7 @ X6 @ X5),skolemize(X9,sK8 @ X7 @ X6 @ X5)],[f38])).
% 1.35/0.57 thf(f40,plain,(
% 1.35/0.57 ((demorgan2b = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2)))) != $true) & (((in @ X3 @ X0)) = $true) & (((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true)) & (((in @ X2 @ (powerset @ X0))) = $true)))) & (! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2)))) = $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true)) | (((in @ X2 @ (powerset @ X0))) != $true))) | (demorgan2b != $true))),
% 1.35/0.57 inference(nnf_transformation,[],[f29])).
% 1.35/0.57 thf(f41,plain,(
% 1.35/0.57 ((demorgan2b = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ (setminus @ X0 @ (binunion @ X1 @ X2)))) != $true) & (((in @ X3 @ X0)) = $true) & (((in @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true)) & (((in @ X2 @ (powerset @ X0))) = $true)))) & (! [X4 : $i,X5 : $i] : (($true != ((in @ X5 @ (powerset @ X4)))) | ! [X6 : $i] : (! [X7 : $i] : (($true = ((in @ X7 @ (setminus @ X4 @ (binunion @ X5 @ X6))))) | ($true != ((in @ X7 @ X4))) | ($true != ((in @ X7 @ (binintersect @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))))) | ($true != ((in @ X6 @ (powerset @ X4)))))) | (demorgan2b != $true))),
% 1.35/0.57 inference(rectify,[],[f40])).
% 1.35/0.57 thf(f42,plain,(
% 1.35/0.57 ((demorgan2b = $true) | (($true = ((in @ sK10 @ (powerset @ sK9)))) & ((($true != ((in @ sK12 @ (setminus @ sK9 @ (binunion @ sK10 @ sK11))))) & ($true = ((in @ sK12 @ sK9))) & ($true = ((in @ sK12 @ (binintersect @ (setminus @ sK9 @ sK10) @ (setminus @ sK9 @ sK11)))))) & ($true = ((in @ sK11 @ (powerset @ sK9))))))) & (! [X4 : $i,X5 : $i] : (($true != ((in @ X5 @ (powerset @ X4)))) | ! [X6 : $i] : (! [X7 : $i] : (($true = ((in @ X7 @ (setminus @ X4 @ (binunion @ X5 @ X6))))) | ($true != ((in @ X7 @ X4))) | ($true != ((in @ X7 @ (binintersect @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))))) | ($true != ((in @ X6 @ (powerset @ X4)))))) | (demorgan2b != $true))),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11,sK12]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X2,sK11),skolemize(X3,sK12)],[f41])).
% 1.35/0.57 thf(f43,plain,(
% 1.35/0.57 ? [X0 : $i,X1 : $i] : (? [X2 : $i] : (($true = ((in @ X2 @ (powerset @ X1)))) & (((binintersect @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))) != ((setminus @ X1 @ (binunion @ X0 @ X2))))) & ($true = ((in @ X0 @ (powerset @ X1))))) & (binunionT_lem = $true) & (complementT_lem = $true) & (demorgan2a = $true) & (binintersectT_lem = $true) & (demorgan2b = $true) & (setextT = $true)),
% 1.35/0.57 inference(rectify,[],[f31])).
% 1.35/0.57 thf(f44,plain,(
% 1.35/0.57 ((($true = ((in @ sK15 @ (powerset @ sK14)))) & (((binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15))) != ((setminus @ sK14 @ (binunion @ sK13 @ sK15))))) & ($true = ((in @ sK13 @ (powerset @ sK14))))) & (binunionT_lem = $true) & (complementT_lem = $true) & (demorgan2a = $true) & (binintersectT_lem = $true) & (demorgan2b = $true) & (setextT = $true)),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X0,sK13),skolemize(X1,sK14),skolemize(X2,sK15)],[f43])).
% 1.35/0.57 thf(f45,plain,(
% 1.35/0.57 (! [X1 : $i,X0 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : ((((in @ (binunion @ X1 @ X2) @ (powerset @ X0))) = $true) | (((in @ X2 @ (powerset @ X0))) != $true))) | (binunionT_lem != $true)) & ((binunionT_lem = $true) | ? [X1 : $i,X0 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : ((((in @ (binunion @ X1 @ X2) @ (powerset @ X0))) != $true) & (((in @ X2 @ (powerset @ X0))) = $true))))),
% 1.35/0.57 inference(nnf_transformation,[],[f25])).
% 1.35/0.57 thf(f46,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : (($true != ((in @ X0 @ (powerset @ X1)))) | ! [X2 : $i] : (($true = ((in @ (binunion @ X0 @ X2) @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1)))))) | (binunionT_lem != $true)) & ((binunionT_lem = $true) | ? [X3 : $i,X4 : $i] : (($true = ((in @ X3 @ (powerset @ X4)))) & ? [X5 : $i] : (($true != ((in @ (binunion @ X3 @ X5) @ (powerset @ X4)))) & ($true = ((in @ X5 @ (powerset @ X4)))))))),
% 1.35/0.57 inference(rectify,[],[f45])).
% 1.35/0.57 thf(f47,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : (($true != ((in @ X0 @ (powerset @ X1)))) | ! [X2 : $i] : (($true = ((in @ (binunion @ X0 @ X2) @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1)))))) | (binunionT_lem != $true)) & ((binunionT_lem = $true) | (($true = ((in @ sK16 @ (powerset @ sK17)))) & (($true != ((in @ (binunion @ sK16 @ sK18) @ (powerset @ sK17)))) & ($true = ((in @ sK18 @ (powerset @ sK17)))))))),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X3,sK16),skolemize(X4,sK17),skolemize(X5,sK18)],[f46])).
% 1.35/0.57 thf(f48,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1))))) | (complementT_lem != $true)) & ((complementT_lem = $true) | ? [X0 : $i,X1 : $i] : (($true != ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) & ($true = ((in @ X0 @ (powerset @ X1))))))),
% 1.35/0.57 inference(nnf_transformation,[],[f23])).
% 1.35/0.57 thf(f49,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1))))) | (complementT_lem != $true)) & ((complementT_lem = $true) | ? [X2 : $i,X3 : $i] : (($true != ((in @ (setminus @ X3 @ X2) @ (powerset @ X3)))) & ($true = ((in @ X2 @ (powerset @ X3))))))),
% 1.35/0.57 inference(rectify,[],[f48])).
% 1.35/0.57 thf(f50,plain,(
% 1.35/0.57 (! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1))))) | (complementT_lem != $true)) & ((complementT_lem = $true) | (($true != ((in @ (setminus @ sK20 @ sK19) @ (powerset @ sK20)))) & ($true = ((in @ sK19 @ (powerset @ sK20))))))),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X2,sK19),skolemize(X3,sK20)],[f49])).
% 1.35/0.57 thf(f51,plain,(
% 1.35/0.57 ((binintersectT_lem = $true) | ? [X1 : $i,X0 : $i] : (? [X2 : $i] : (($true != ((in @ (binintersect @ X0 @ X2) @ (powerset @ X1)))) & ($true = ((in @ X2 @ (powerset @ X1))))) & ($true = ((in @ X0 @ (powerset @ X1)))))) & (! [X1 : $i,X0 : $i] : (! [X2 : $i] : (($true = ((in @ (binintersect @ X0 @ X2) @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1))))) | ($true != ((in @ X0 @ (powerset @ X1))))) | (binintersectT_lem != $true))),
% 1.35/0.57 inference(nnf_transformation,[],[f24])).
% 1.35/0.57 thf(f52,plain,(
% 1.35/0.57 ((binintersectT_lem = $true) | ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((in @ (binintersect @ X1 @ X2) @ (powerset @ X0))) != $true) & (((in @ X2 @ (powerset @ X0))) = $true)) & (((in @ X1 @ (powerset @ X0))) = $true))) & (! [X3 : $i,X4 : $i] : (! [X5 : $i] : (($true = ((in @ (binintersect @ X4 @ X5) @ (powerset @ X3)))) | ($true != ((in @ X5 @ (powerset @ X3))))) | ($true != ((in @ X4 @ (powerset @ X3))))) | (binintersectT_lem != $true))),
% 1.35/0.57 inference(rectify,[],[f51])).
% 1.35/0.57 thf(f53,plain,(
% 1.35/0.57 ((binintersectT_lem = $true) | ((($true != ((in @ (binintersect @ sK22 @ sK23) @ (powerset @ sK21)))) & ($true = ((in @ sK23 @ (powerset @ sK21))))) & ($true = ((in @ sK22 @ (powerset @ sK21)))))) & (! [X3 : $i,X4 : $i] : (! [X5 : $i] : (($true = ((in @ (binintersect @ X4 @ X5) @ (powerset @ X3)))) | ($true != ((in @ X5 @ (powerset @ X3))))) | ($true != ((in @ X4 @ (powerset @ X3))))) | (binintersectT_lem != $true))),
% 1.35/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23]),skolemize(X0,sK21),skolemize(X1,sK22),skolemize(X2,sK23)],[f52])).
% 1.35/0.57 thf(f54,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((in @ X7 @ (binintersect @ (setminus @ X5 @ X4) @ (setminus @ X5 @ X6))))) | (demorgan2a != $true) | ($true != ((in @ X7 @ (setminus @ X5 @ (binunion @ X4 @ X6))))) | ($true != ((in @ X6 @ (powerset @ X5)))) | ($true != ((in @ X7 @ X5))) | ($true != ((in @ X4 @ (powerset @ X5))))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f36])).
% 1.35/0.57 thf(f60,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | (setextT != $true) | (X5 = X7)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f61,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true != ((in @ X5 @ (powerset @ X6)))) | (X5 = X7) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X7 @ (powerset @ X6)))) | (setextT != $true) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7)))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f62,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ X7 @ (powerset @ X6)))) | (X5 = X7) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | (setextT != $true)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f63,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X5 @ (powerset @ X6)))) | (X5 = X7) | (setextT != $true) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X7 @ (powerset @ X6))))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f64,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | (X5 = X7) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | (setextT != $true)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f65,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((X5 = X7) | (setextT != $true) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6)))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f66,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ X7 @ (powerset @ X6)))) | (X5 = X7) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | (setextT != $true)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f67,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X5 @ (powerset @ X6)))) | (setextT != $true) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | (X5 = X7)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f68,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X5 @ (powerset @ X6)))) | (setextT != $true) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | (X5 = X7)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f39])).
% 1.35/0.57 thf(f74,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true != ((in @ X7 @ X4))) | ($true != ((in @ X5 @ (powerset @ X4)))) | (demorgan2b != $true) | ($true != ((in @ X7 @ (binintersect @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6))))) | ($true = ((in @ X7 @ (setminus @ X4 @ (binunion @ X5 @ X6))))) | ($true != ((in @ X6 @ (powerset @ X4))))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f42])).
% 1.35/0.57 thf(f80,plain,(
% 1.35/0.57 (setextT = $true)),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f81,plain,(
% 1.35/0.57 (demorgan2b = $true)),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f82,plain,(
% 1.35/0.57 (binintersectT_lem = $true)),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f83,plain,(
% 1.35/0.57 (demorgan2a = $true)),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f84,plain,(
% 1.35/0.57 (complementT_lem = $true)),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f85,plain,(
% 1.35/0.57 (binunionT_lem = $true)),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f86,plain,(
% 1.35/0.57 ($true = ((in @ sK13 @ (powerset @ sK14))))),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f87,plain,(
% 1.35/0.57 (((binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15))) != ((setminus @ sK14 @ (binunion @ sK13 @ sK15))))),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f88,plain,(
% 1.35/0.57 ($true = ((in @ sK15 @ (powerset @ sK14))))),
% 1.35/0.57 inference(cnf_transformation,[],[f44])).
% 1.35/0.57 thf(f92,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ X0 @ (powerset @ X1)))) | ($true = ((in @ (binunion @ X0 @ X2) @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1)))) | (binunionT_lem != $true)) )),
% 1.35/0.57 inference(cnf_transformation,[],[f47])).
% 1.35/0.57 thf(f95,plain,(
% 1.35/0.57 ( ! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | (complementT_lem != $true) | ($true != ((in @ X0 @ (powerset @ X1))))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f50])).
% 1.35/0.57 thf(f96,plain,(
% 1.35/0.57 ( ! [X3 : $i,X4 : $i,X5 : $i] : (($true != ((in @ X4 @ (powerset @ X3)))) | ($true = ((in @ (binintersect @ X4 @ X5) @ (powerset @ X3)))) | (binintersectT_lem != $true) | ($true != ((in @ X5 @ (powerset @ X3))))) )),
% 1.35/0.57 inference(cnf_transformation,[],[f53])).
% 1.35/0.57 thf(f102,definition,(
% 1.35/0.57 spl24_1 <=> (demorgan2b = $true)),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition])).
% 1.35/0.57 thf(f121,definition,(
% 1.35/0.57 spl24_5 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | (X5 = X7) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ X5 @ (powerset @ X6)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition])).
% 1.35/0.57 thf(f122,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | (X5 = X7)) ) | ~spl24_5),
% 1.35/0.57 inference(avatar_component_clause,[],[f121])).
% 1.35/0.57 thf(f124,definition,(
% 1.35/0.57 spl24_6 <=> (setextT = $true)),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition])).
% 1.35/0.57 thf(f127,plain,(
% 1.35/0.57 spl24_5 | ~spl24_6),
% 1.35/0.57 inference(avatar_split_clause,[],[f66,f124,f121])).
% 1.35/0.57 thf(f129,definition,(
% 1.35/0.57 spl24_7 <=> (complementT_lem = $true)),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition])).
% 1.35/0.57 thf(f137,plain,(
% 1.35/0.57 spl24_7),
% 1.35/0.57 inference(avatar_split_clause,[],[f84,f129])).
% 1.35/0.57 thf(f143,definition,(
% 1.35/0.57 spl24_10 <=> (demorgan2a = $true)),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_10])],[avatar_definition])).
% 1.35/0.57 thf(f148,definition,(
% 1.35/0.57 spl24_11 <=> (((binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15))) = ((setminus @ sK14 @ (binunion @ sK13 @ sK15))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_11])],[avatar_definition])).
% 1.35/0.57 thf(f150,plain,(
% 1.35/0.57 (((binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15))) != ((setminus @ sK14 @ (binunion @ sK13 @ sK15)))) | spl24_11),
% 1.35/0.57 inference(avatar_component_clause,[],[f148])).
% 1.35/0.57 thf(f151,plain,(
% 1.35/0.57 ~spl24_11),
% 1.35/0.57 inference(avatar_split_clause,[],[f87,f148])).
% 1.35/0.57 thf(f153,definition,(
% 1.35/0.57 spl24_12 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((X5 = X7) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X5 @ (powerset @ X6)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_12])],[avatar_definition])).
% 1.35/0.57 thf(f154,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | (X5 = X7) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ X7 @ (powerset @ X6))))) ) | ~spl24_12),
% 1.35/0.57 inference(avatar_component_clause,[],[f153])).
% 1.35/0.57 thf(f155,plain,(
% 1.35/0.57 spl24_12 | ~spl24_6),
% 1.35/0.57 inference(avatar_split_clause,[],[f65,f124,f153])).
% 1.35/0.57 thf(f166,definition,(
% 1.35/0.57 spl24_15 <=> (binunionT_lem = $true)),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition])).
% 1.35/0.57 thf(f176,definition,(
% 1.35/0.57 spl24_17 <=> ! [X5 : $i,X4 : $i,X7 : $i,X6 : $i] : (($true != ((in @ X7 @ X4))) | ($true != ((in @ X6 @ (powerset @ X4)))) | ($true = ((in @ X7 @ (setminus @ X4 @ (binunion @ X5 @ X6))))) | ($true != ((in @ X7 @ (binintersect @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6))))) | ($true != ((in @ X5 @ (powerset @ X4)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition])).
% 1.35/0.57 thf(f177,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true != ((in @ X7 @ (binintersect @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6))))) | ($true != ((in @ X7 @ X4))) | ($true != ((in @ X5 @ (powerset @ X4)))) | ($true != ((in @ X6 @ (powerset @ X4)))) | ($true = ((in @ X7 @ (setminus @ X4 @ (binunion @ X5 @ X6)))))) ) | ~spl24_17),
% 1.35/0.57 inference(avatar_component_clause,[],[f176])).
% 1.35/0.57 thf(f178,plain,(
% 1.35/0.57 spl24_17 | ~spl24_1),
% 1.35/0.57 inference(avatar_split_clause,[],[f74,f102,f176])).
% 1.35/0.57 thf(f190,definition,(
% 1.35/0.57 spl24_20 <=> ($true = ((in @ sK13 @ (powerset @ sK14))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition])).
% 1.35/0.57 thf(f192,plain,(
% 1.35/0.57 ($true = ((in @ sK13 @ (powerset @ sK14)))) | ~spl24_20),
% 1.35/0.57 inference(avatar_component_clause,[],[f190])).
% 1.35/0.57 thf(f193,plain,(
% 1.35/0.57 spl24_20),
% 1.35/0.57 inference(avatar_split_clause,[],[f86,f190])).
% 1.35/0.57 thf(f195,definition,(
% 1.35/0.57 spl24_21 <=> ! [X5 : $i,X4 : $i,X7 : $i,X6 : $i] : (($true = ((in @ X7 @ (binintersect @ (setminus @ X5 @ X4) @ (setminus @ X5 @ X6))))) | ($true != ((in @ X4 @ (powerset @ X5)))) | ($true != ((in @ X7 @ X5))) | ($true != ((in @ X6 @ (powerset @ X5)))) | ($true != ((in @ X7 @ (setminus @ X5 @ (binunion @ X4 @ X6))))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_21])],[avatar_definition])).
% 1.35/0.57 thf(f196,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : (($true = ((in @ X7 @ (binintersect @ (setminus @ X5 @ X4) @ (setminus @ X5 @ X6))))) | ($true != ((in @ X7 @ X5))) | ($true != ((in @ X4 @ (powerset @ X5)))) | ($true != ((in @ X7 @ (setminus @ X5 @ (binunion @ X4 @ X6))))) | ($true != ((in @ X6 @ (powerset @ X5))))) ) | ~spl24_21),
% 1.35/0.57 inference(avatar_component_clause,[],[f195])).
% 1.35/0.57 thf(f197,plain,(
% 1.35/0.57 spl24_21 | ~spl24_10),
% 1.35/0.57 inference(avatar_split_clause,[],[f54,f143,f195])).
% 1.35/0.57 thf(f199,definition,(
% 1.35/0.57 spl24_22 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | (X5 = X7))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition])).
% 1.35/0.57 thf(f200,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X7 @ (powerset @ X6)))) | (X5 = X7) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X5 @ (powerset @ X6))))) ) | ~spl24_22),
% 1.35/0.57 inference(avatar_component_clause,[],[f199])).
% 1.35/0.57 thf(f201,plain,(
% 1.35/0.57 ~spl24_6 | spl24_22),
% 1.35/0.57 inference(avatar_split_clause,[],[f61,f199,f124])).
% 1.35/0.57 thf(f202,plain,(
% 1.35/0.57 spl24_15),
% 1.35/0.57 inference(avatar_split_clause,[],[f85,f166])).
% 1.35/0.57 thf(f204,definition,(
% 1.35/0.57 spl24_23 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true != ((in @ X5 @ (powerset @ X6)))) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | (X5 = X7) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X7 @ (powerset @ X6)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition])).
% 1.35/0.57 thf(f205,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X5 @ (powerset @ X6)))) | (X5 = X7) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X7 @ (powerset @ X6))))) ) | ~spl24_23),
% 1.35/0.57 inference(avatar_component_clause,[],[f204])).
% 1.35/0.57 thf(f206,plain,(
% 1.35/0.57 ~spl24_6 | spl24_23),
% 1.35/0.57 inference(avatar_split_clause,[],[f64,f204,f124])).
% 1.35/0.57 thf(f208,definition,(
% 1.35/0.57 spl24_24 <=> (binintersectT_lem = $true)),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_24])],[avatar_definition])).
% 1.35/0.57 thf(f211,plain,(
% 1.35/0.57 spl24_24),
% 1.35/0.57 inference(avatar_split_clause,[],[f82,f208])).
% 1.35/0.57 thf(f216,plain,(
% 1.35/0.57 spl24_6),
% 1.35/0.57 inference(avatar_split_clause,[],[f80,f124])).
% 1.35/0.57 thf(f218,definition,(
% 1.35/0.57 spl24_26 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | (X5 = X7) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ X5 @ (powerset @ X6)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_26])],[avatar_definition])).
% 1.35/0.57 thf(f219,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X7 @ (powerset @ X6)))) | (X5 = X7) | ($true != ((in @ X5 @ (powerset @ X6))))) ) | ~spl24_26),
% 1.35/0.57 inference(avatar_component_clause,[],[f218])).
% 1.35/0.57 thf(f220,plain,(
% 1.35/0.57 spl24_26 | ~spl24_6),
% 1.35/0.57 inference(avatar_split_clause,[],[f62,f124,f218])).
% 1.35/0.57 thf(f222,definition,(
% 1.35/0.57 spl24_27 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true != ((in @ X7 @ (powerset @ X6)))) | (X5 = X7) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition])).
% 1.35/0.57 thf(f223,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | (X5 = X7) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ (sK8 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X7 @ (powerset @ X6))))) ) | ~spl24_27),
% 1.35/0.57 inference(avatar_component_clause,[],[f222])).
% 1.35/0.57 thf(f224,plain,(
% 1.35/0.57 ~spl24_6 | spl24_27),
% 1.35/0.57 inference(avatar_split_clause,[],[f67,f222,f124])).
% 1.35/0.57 thf(f226,definition,(
% 1.35/0.57 spl24_28 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | (X5 = X7) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ X5 @ (powerset @ X6)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition])).
% 1.35/0.57 thf(f227,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X6))) | (X5 = X7) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X7))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ X7 @ (powerset @ X6))))) ) | ~spl24_28),
% 1.35/0.57 inference(avatar_component_clause,[],[f226])).
% 1.35/0.57 thf(f228,plain,(
% 1.35/0.57 ~spl24_6 | spl24_28),
% 1.35/0.57 inference(avatar_split_clause,[],[f68,f226,f124])).
% 1.35/0.57 thf(f250,definition,(
% 1.35/0.57 spl24_33 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | (X5 = X7) | ($true != ((in @ X5 @ (powerset @ X6)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_33])],[avatar_definition])).
% 1.35/0.57 thf(f251,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | ($true = ((in @ (sK7 @ X7 @ X6 @ X5) @ X6))) | ($true != ((in @ X7 @ (powerset @ X6)))) | ($true != ((in @ X5 @ (powerset @ X6)))) | (X5 = X7)) ) | ~spl24_33),
% 1.35/0.57 inference(avatar_component_clause,[],[f250])).
% 1.35/0.57 thf(f252,plain,(
% 1.35/0.57 spl24_33 | ~spl24_6),
% 1.35/0.57 inference(avatar_split_clause,[],[f63,f124,f250])).
% 1.35/0.57 thf(f264,definition,(
% 1.35/0.57 spl24_36 <=> ! [X6 : $i,X5 : $i,X7 : $i] : (($true != ((in @ X7 @ (powerset @ X6)))) | (X5 = X7) | ($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X5 @ (powerset @ X6)))) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_36])],[avatar_definition])).
% 1.35/0.57 thf(f265,plain,(
% 1.35/0.57 ( ! [X6 : $i,X7 : $i,X5 : $i] : (($true = ((in @ (sK8 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ (sK7 @ X7 @ X6 @ X5) @ X5))) | ($true != ((in @ X5 @ (powerset @ X6)))) | (X5 = X7) | ($true != ((in @ X7 @ (powerset @ X6))))) ) | ~spl24_36),
% 1.35/0.57 inference(avatar_component_clause,[],[f264])).
% 1.35/0.57 thf(f266,plain,(
% 1.35/0.57 ~spl24_6 | spl24_36),
% 1.35/0.57 inference(avatar_split_clause,[],[f60,f264,f124])).
% 1.35/0.57 thf(f278,definition,(
% 1.35/0.57 spl24_39 <=> ! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_39])],[avatar_definition])).
% 1.35/0.57 thf(f279,plain,(
% 1.35/0.57 ( ! [X0 : $i,X1 : $i] : (($true = ((in @ (setminus @ X1 @ X0) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1))))) ) | ~spl24_39),
% 1.35/0.57 inference(avatar_component_clause,[],[f278])).
% 1.35/0.57 thf(f280,plain,(
% 1.35/0.57 ~spl24_7 | spl24_39),
% 1.35/0.57 inference(avatar_split_clause,[],[f95,f278,f129])).
% 1.35/0.57 thf(f282,definition,(
% 1.35/0.57 spl24_40 <=> ! [X4 : $i,X5 : $i,X3 : $i] : (($true != ((in @ X4 @ (powerset @ X3)))) | ($true != ((in @ X5 @ (powerset @ X3)))) | ($true = ((in @ (binintersect @ X4 @ X5) @ (powerset @ X3)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_40])],[avatar_definition])).
% 1.35/0.57 thf(f283,plain,(
% 1.35/0.57 ( ! [X3 : $i,X4 : $i,X5 : $i] : (($true = ((in @ (binintersect @ X4 @ X5) @ (powerset @ X3)))) | ($true != ((in @ X4 @ (powerset @ X3)))) | ($true != ((in @ X5 @ (powerset @ X3))))) ) | ~spl24_40),
% 1.35/0.57 inference(avatar_component_clause,[],[f282])).
% 1.35/0.57 thf(f284,plain,(
% 1.35/0.57 spl24_40 | ~spl24_24),
% 1.35/0.57 inference(avatar_split_clause,[],[f96,f208,f282])).
% 1.35/0.57 thf(f285,plain,(
% 1.35/0.57 spl24_10),
% 1.35/0.57 inference(avatar_split_clause,[],[f83,f143])).
% 1.35/0.57 thf(f296,definition,(
% 1.35/0.57 spl24_43 <=> ($true = ((in @ sK15 @ (powerset @ sK14))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_43])],[avatar_definition])).
% 1.35/0.57 thf(f298,plain,(
% 1.35/0.57 ($true = ((in @ sK15 @ (powerset @ sK14)))) | ~spl24_43),
% 1.35/0.57 inference(avatar_component_clause,[],[f296])).
% 1.35/0.57 thf(f299,plain,(
% 1.35/0.57 spl24_43),
% 1.35/0.57 inference(avatar_split_clause,[],[f88,f296])).
% 1.35/0.57 thf(f306,definition,(
% 1.35/0.57 spl24_45 <=> ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1)))) | ($true = ((in @ (binunion @ X0 @ X2) @ (powerset @ X1)))))),
% 1.35/0.57 introduced(definition,[new_symbols(definition,[spl24_45])],[avatar_definition])).
% 1.35/0.57 thf(f307,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (binunion @ X0 @ X2) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ X2 @ (powerset @ X1))))) ) | ~spl24_45),
% 1.35/0.57 inference(avatar_component_clause,[],[f306])).
% 1.35/0.57 thf(f308,plain,(
% 1.35/0.57 spl24_45 | ~spl24_15),
% 1.35/0.57 inference(avatar_split_clause,[],[f92,f166,f306])).
% 1.35/0.57 thf(f314,plain,(
% 1.35/0.57 spl24_1),
% 1.35/0.57 inference(avatar_split_clause,[],[f81,f102])).
% 1.35/0.57 thf(f335,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X4 @ (powerset @ X2)))) | ($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))))) | ($true != $true) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1))))) ) | (~spl24_17 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f177,f265])).
% 1.35/0.57 thf(f336,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1)))) | ($true != ((in @ X3 @ (powerset @ X2)))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true != ((in @ X4 @ (powerset @ X2)))) | ($true != $true) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true = ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X1)))) ) | (~spl24_17 | ~spl24_33)),
% 1.35/0.57 inference(superposition,[],[f177,f251])).
% 1.35/0.57 thf(f337,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1)))) | ($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true != $true) | ($true != ((in @ X4 @ (powerset @ X2)))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true = ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X0))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2)))) ) | (~spl24_5 | ~spl24_17)),
% 1.35/0.57 inference(superposition,[],[f177,f122])).
% 1.35/0.57 thf(f340,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))))) | ($true != ((in @ X4 @ (powerset @ X2)))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1))))) ) | (~spl24_17 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f335])).
% 1.35/0.57 thf(f342,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true = ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X0))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1)))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ X4 @ (powerset @ X2))))) ) | (~spl24_5 | ~spl24_17)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f337])).
% 1.35/0.57 thf(f343,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X4 @ (powerset @ X2)))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true = ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X1))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1))))) ) | (~spl24_17 | ~spl24_33)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f336])).
% 1.35/0.57 thf(f397,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ X4 @ (powerset @ X2)))) | ($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1)))) | ($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ X4 @ (powerset @ X2)))) | ($true != $true) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2)))) ) | (~spl24_17 | ~spl24_21 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f340,f196])).
% 1.35/0.57 thf(f401,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != $true) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ X4 @ (powerset @ X2)))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1)))) | ($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0)) ) | (~spl24_17 | ~spl24_21 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f397])).
% 1.35/0.57 thf(f402,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | ($true != ((in @ X4 @ (powerset @ X2)))) | ($true != ((in @ X3 @ (powerset @ X2)))) | ($true != ((in @ (sK8 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ X0 @ (powerset @ X1)))) | ($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ X2))) | ($true != ((in @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4)) @ (powerset @ X1)))) | ($true != ((in @ (sK7 @ X0 @ X1 @ (binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) @ (setminus @ X2 @ (binunion @ X3 @ X4))))) | (((binintersect @ (setminus @ X2 @ X3) @ (setminus @ X2 @ X4))) = X0)) ) | (~spl24_17 | ~spl24_21 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f401])).
% 1.35/0.57 thf(f485,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))))) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f200,f402])).
% 1.35/0.57 thf(f492,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != $true)) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f485])).
% 1.35/0.57 thf(f493,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))))) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f492])).
% 1.35/0.57 thf(f496,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0)))) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_36)),
% 1.35/0.57 inference(forward_subsumption_resolution,[],[f493,f196])).
% 1.35/0.57 thf(f539,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f496,f223])).
% 1.35/0.57 thf(f543,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))))) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f539])).
% 1.35/0.57 thf(f544,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f543])).
% 1.35/0.57 thf(f661,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f544,f342])).
% 1.35/0.57 thf(f669,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0)))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f661])).
% 1.35/0.57 thf(f670,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f669])).
% 1.35/0.57 thf(f686,plain,(
% 1.35/0.57 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X3)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X3 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0)))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(forward_subsumption_resolution,[],[f670,f496])).
% 1.35/0.57 thf(f696,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f686,f227])).
% 1.35/0.57 thf(f697,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f686,f219])).
% 1.35/0.57 thf(f703,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f696])).
% 1.35/0.57 thf(f704,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f703])).
% 1.35/0.57 thf(f712,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f697])).
% 1.35/0.57 thf(f713,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f712])).
% 1.35/0.57 thf(f744,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(superposition,[],[f713,f196])).
% 1.35/0.57 thf(f745,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(duplicate_literal_removal,[],[f744])).
% 1.35/0.57 thf(f746,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2))))) | ($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_36)),
% 1.35/0.57 inference(trivial_inequality_removal,[],[f745])).
% 1.35/0.57 thf(f747,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.57 inference(forward_subsumption_resolution,[],[f746,f704])).
% 1.35/0.57 thf(f766,plain,(
% 1.35/0.57 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2)))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.58 inference(superposition,[],[f747,f205])).
% 1.35/0.58 thf(f771,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != $true) | (((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2)))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.58 inference(duplicate_literal_removal,[],[f766])).
% 1.35/0.58 thf(f772,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ (setminus @ X0 @ (binunion @ X1 @ X2)))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_36)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f771])).
% 1.35/0.58 thf(f806,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | ($true != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(superposition,[],[f772,f343])).
% 1.35/0.58 thf(f812,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(duplicate_literal_removal,[],[f806])).
% 1.35/0.58 thf(f813,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != ((in @ (sK8 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0)))) ) | (~spl24_5 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f812])).
% 1.35/0.58 thf(f815,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true = ((in @ (sK7 @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ X0 @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) @ X0))) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0)))) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_12 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f813,f154])).
% 1.35/0.58 thf(f816,plain,(
% 1.35/0.58 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binunion @ X1 @ X2))) = ((binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != ((in @ (binintersect @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0)))) | ($true != ((in @ (setminus @ X0 @ (binunion @ X1 @ X2)) @ (powerset @ X0))))) ) | (~spl24_5 | ~spl24_12 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f815,f747])).
% 1.35/0.58 thf(f820,plain,(
% 1.35/0.58 ($true != ((in @ sK15 @ (powerset @ sK14)))) | ($true != ((in @ (binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ (setminus @ sK14 @ (binunion @ sK13 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ sK13 @ (powerset @ sK14)))) | (((setminus @ sK14 @ (binunion @ sK13 @ sK15))) != ((setminus @ sK14 @ (binunion @ sK13 @ sK15)))) | (~spl24_5 | spl24_11 | ~spl24_12 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(superposition,[],[f150,f816])).
% 1.35/0.58 thf(f912,plain,(
% 1.35/0.58 ($true != ((in @ (binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ sK15 @ (powerset @ sK14)))) | ($true != ((in @ (setminus @ sK14 @ (binunion @ sK13 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ sK13 @ (powerset @ sK14)))) | (~spl24_5 | spl24_11 | ~spl24_12 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f820])).
% 1.35/0.58 thf(f945,plain,(
% 1.35/0.58 ($true != ((in @ (binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ (setminus @ sK14 @ (binunion @ sK13 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ sK13 @ (powerset @ sK14)))) | (~spl24_5 | spl24_11 | ~spl24_12 | ~spl24_17 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36 | ~spl24_43)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f912,f298])).
% 1.35/0.58 thf(f946,plain,(
% 1.35/0.58 ($true != ((in @ (binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15)) @ (powerset @ sK14)))) | ($true != ((in @ (setminus @ sK14 @ (binunion @ sK13 @ sK15)) @ (powerset @ sK14)))) | (~spl24_5 | spl24_11 | ~spl24_12 | ~spl24_17 | ~spl24_20 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36 | ~spl24_43)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f945,f192])).
% 1.35/0.58 thf(f948,definition,(
% 1.35/0.58 spl24_47 <=> ($true = ((in @ (binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15)) @ (powerset @ sK14))))),
% 1.35/0.58 introduced(definition,[new_symbols(definition,[spl24_47])],[avatar_definition])).
% 1.35/0.58 thf(f950,plain,(
% 1.35/0.58 ($true != ((in @ (binintersect @ (setminus @ sK14 @ sK13) @ (setminus @ sK14 @ sK15)) @ (powerset @ sK14)))) | spl24_47),
% 1.35/0.58 inference(avatar_component_clause,[],[f948])).
% 1.35/0.58 thf(f952,definition,(
% 1.35/0.58 spl24_48 <=> ($true = ((in @ (setminus @ sK14 @ (binunion @ sK13 @ sK15)) @ (powerset @ sK14))))),
% 1.35/0.58 introduced(definition,[new_symbols(definition,[spl24_48])],[avatar_definition])).
% 1.35/0.58 thf(f954,plain,(
% 1.35/0.58 ($true != ((in @ (setminus @ sK14 @ (binunion @ sK13 @ sK15)) @ (powerset @ sK14)))) | spl24_48),
% 1.35/0.58 inference(avatar_component_clause,[],[f952])).
% 1.35/0.58 thf(f955,plain,(
% 1.35/0.58 ~spl24_47 | ~spl24_48 | ~spl24_5 | spl24_11 | ~spl24_12 | ~spl24_17 | ~spl24_20 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36 | ~spl24_43),
% 1.35/0.58 inference(avatar_split_clause,[],[f946,f296,f264,f250,f226,f222,f218,f204,f199,f195,f190,f176,f153,f148,f121,f952,f948])).
% 1.35/0.58 thf(f957,plain,(
% 1.35/0.58 ($true != ((in @ (setminus @ sK14 @ sK13) @ (powerset @ sK14)))) | ($true != $true) | ($true != ((in @ (setminus @ sK14 @ sK15) @ (powerset @ sK14)))) | (~spl24_40 | spl24_47)),
% 1.35/0.58 inference(superposition,[],[f950,f283])).
% 1.35/0.58 thf(f959,plain,(
% 1.35/0.58 ($true != ((in @ (setminus @ sK14 @ sK15) @ (powerset @ sK14)))) | ($true != ((in @ (setminus @ sK14 @ sK13) @ (powerset @ sK14)))) | (~spl24_40 | spl24_47)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f957])).
% 1.35/0.58 thf(f961,definition,(
% 1.35/0.58 spl24_49 <=> ($true = ((in @ (setminus @ sK14 @ sK15) @ (powerset @ sK14))))),
% 1.35/0.58 introduced(definition,[new_symbols(definition,[spl24_49])],[avatar_definition])).
% 1.35/0.58 thf(f963,plain,(
% 1.35/0.58 ($true != ((in @ (setminus @ sK14 @ sK15) @ (powerset @ sK14)))) | spl24_49),
% 1.35/0.58 inference(avatar_component_clause,[],[f961])).
% 1.35/0.58 thf(f965,definition,(
% 1.35/0.58 spl24_50 <=> ($true = ((in @ (setminus @ sK14 @ sK13) @ (powerset @ sK14))))),
% 1.35/0.58 introduced(definition,[new_symbols(definition,[spl24_50])],[avatar_definition])).
% 1.35/0.58 thf(f967,plain,(
% 1.35/0.58 ($true != ((in @ (setminus @ sK14 @ sK13) @ (powerset @ sK14)))) | spl24_50),
% 1.35/0.58 inference(avatar_component_clause,[],[f965])).
% 1.35/0.58 thf(f968,plain,(
% 1.35/0.58 ~spl24_49 | ~spl24_50 | ~spl24_40 | spl24_47),
% 1.35/0.58 inference(avatar_split_clause,[],[f959,f948,f282,f965,f961])).
% 1.35/0.58 thf(f980,plain,(
% 1.35/0.58 ($true != ((in @ sK15 @ (powerset @ sK14)))) | ($true != $true) | (~spl24_39 | spl24_49)),
% 1.35/0.58 inference(superposition,[],[f963,f279])).
% 1.35/0.58 thf(f981,plain,(
% 1.35/0.58 ($true != ((in @ sK15 @ (powerset @ sK14)))) | (~spl24_39 | spl24_49)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f980])).
% 1.35/0.58 thf(f982,plain,(
% 1.35/0.58 $false | (~spl24_39 | ~spl24_43 | spl24_49)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f981,f298])).
% 1.35/0.58 thf(f983,plain,(
% 1.35/0.58 ~spl24_39 | ~spl24_43 | spl24_49),
% 1.35/0.58 inference(avatar_contradiction_clause,[],[f982])).
% 1.35/0.58 thf(f1020,plain,(
% 1.35/0.58 ($true != ((in @ sK13 @ (powerset @ sK14)))) | ($true != $true) | (~spl24_39 | spl24_50)),
% 1.35/0.58 inference(superposition,[],[f967,f279])).
% 1.35/0.58 thf(f1021,plain,(
% 1.35/0.58 ($true != ((in @ sK13 @ (powerset @ sK14)))) | (~spl24_39 | spl24_50)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f1020])).
% 1.35/0.58 thf(f1022,plain,(
% 1.35/0.58 $false | (~spl24_20 | ~spl24_39 | spl24_50)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f1021,f192])).
% 1.35/0.58 thf(f1023,plain,(
% 1.35/0.58 ~spl24_20 | ~spl24_39 | spl24_50),
% 1.35/0.58 inference(avatar_contradiction_clause,[],[f1022])).
% 1.35/0.58 thf(f1024,plain,(
% 1.35/0.58 ($true != $true) | ($true != ((in @ (binunion @ sK13 @ sK15) @ (powerset @ sK14)))) | (~spl24_39 | spl24_48)),
% 1.35/0.58 inference(superposition,[],[f954,f279])).
% 1.35/0.58 thf(f1025,plain,(
% 1.35/0.58 ($true != ((in @ (binunion @ sK13 @ sK15) @ (powerset @ sK14)))) | (~spl24_39 | spl24_48)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f1024])).
% 1.35/0.58 thf(f1027,definition,(
% 1.35/0.58 spl24_51 <=> ($true = ((in @ (binunion @ sK13 @ sK15) @ (powerset @ sK14))))),
% 1.35/0.58 introduced(definition,[new_symbols(definition,[spl24_51])],[avatar_definition])).
% 1.35/0.58 thf(f1029,plain,(
% 1.35/0.58 ($true != ((in @ (binunion @ sK13 @ sK15) @ (powerset @ sK14)))) | spl24_51),
% 1.35/0.58 inference(avatar_component_clause,[],[f1027])).
% 1.35/0.58 thf(f1030,plain,(
% 1.35/0.58 ~spl24_51 | ~spl24_39 | spl24_48),
% 1.35/0.58 inference(avatar_split_clause,[],[f1025,f952,f278,f1027])).
% 1.35/0.58 thf(f1031,plain,(
% 1.35/0.58 ($true != ((in @ sK15 @ (powerset @ sK14)))) | ($true != ((in @ sK13 @ (powerset @ sK14)))) | ($true != $true) | (~spl24_45 | spl24_51)),
% 1.35/0.58 inference(superposition,[],[f1029,f307])).
% 1.35/0.58 thf(f1032,plain,(
% 1.35/0.58 ($true != ((in @ sK15 @ (powerset @ sK14)))) | ($true != ((in @ sK13 @ (powerset @ sK14)))) | (~spl24_45 | spl24_51)),
% 1.35/0.58 inference(trivial_inequality_removal,[],[f1031])).
% 1.35/0.58 thf(f1033,plain,(
% 1.35/0.58 ($true != ((in @ sK13 @ (powerset @ sK14)))) | (~spl24_43 | ~spl24_45 | spl24_51)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f1032,f298])).
% 1.35/0.58 thf(f1034,plain,(
% 1.35/0.58 $false | (~spl24_20 | ~spl24_43 | ~spl24_45 | spl24_51)),
% 1.35/0.58 inference(forward_subsumption_resolution,[],[f1033,f192])).
% 1.35/0.58 thf(f1035,plain,(
% 1.35/0.58 ~spl24_20 | ~spl24_43 | ~spl24_45 | spl24_51),
% 1.35/0.58 inference(avatar_contradiction_clause,[],[f1034])).
% 1.35/0.58 cnf(s4, plain, spl24_5 | ~spl24_6, inference(sat_conversion,[],[f127])).
% 1.35/0.58 cnf(s6, plain, spl24_7, inference(sat_conversion,[],[f137])).
% 1.35/0.58 cnf(s8, plain, ~spl24_11, inference(sat_conversion,[],[f151])).
% 1.35/0.58 cnf(s9, plain, ~spl24_6 | spl24_12, inference(sat_conversion,[],[f155])).
% 1.35/0.58 cnf(s13, plain, ~spl24_1 | spl24_17, inference(sat_conversion,[],[f178])).
% 1.35/0.58 cnf(s16, plain, spl24_20, inference(sat_conversion,[],[f193])).
% 1.35/0.58 cnf(s17, plain, ~spl24_10 | spl24_21, inference(sat_conversion,[],[f197])).
% 1.35/0.58 cnf(s18, plain, ~spl24_6 | spl24_22, inference(sat_conversion,[],[f201])).
% 1.35/0.58 cnf(s19, plain, spl24_15, inference(sat_conversion,[],[f202])).
% 1.35/0.58 cnf(s20, plain, ~spl24_6 | spl24_23, inference(sat_conversion,[],[f206])).
% 1.35/0.58 cnf(s21, plain, spl24_24, inference(sat_conversion,[],[f211])).
% 1.35/0.58 cnf(s23, plain, spl24_6, inference(sat_conversion,[],[f216])).
% 1.35/0.58 cnf(s24, plain, ~spl24_6 | spl24_26, inference(sat_conversion,[],[f220])).
% 1.35/0.58 cnf(s25, plain, ~spl24_6 | spl24_27, inference(sat_conversion,[],[f224])).
% 1.35/0.58 cnf(s26, plain, ~spl24_6 | spl24_28, inference(sat_conversion,[],[f228])).
% 1.35/0.58 cnf(s31, plain, ~spl24_6 | spl24_33, inference(sat_conversion,[],[f252])).
% 1.35/0.58 cnf(s34, plain, ~spl24_6 | spl24_36, inference(sat_conversion,[],[f266])).
% 1.35/0.58 cnf(s37, plain, ~spl24_7 | spl24_39, inference(sat_conversion,[],[f280])).
% 1.35/0.58 cnf(s38, plain, ~spl24_24 | spl24_40, inference(sat_conversion,[],[f284])).
% 1.35/0.58 cnf(s39, plain, spl24_10, inference(sat_conversion,[],[f285])).
% 1.35/0.58 cnf(s42, plain, spl24_43, inference(sat_conversion,[],[f299])).
% 1.35/0.58 cnf(s44, plain, ~spl24_15 | spl24_45, inference(sat_conversion,[],[f308])).
% 1.35/0.58 cnf(s46, plain, spl24_1, inference(sat_conversion,[],[f314])).
% 1.35/0.58 cnf(s47, plain, ~spl24_5 | spl24_11 | ~spl24_12 | ~spl24_17 | ~spl24_20 | ~spl24_21 | ~spl24_22 | ~spl24_23 | ~spl24_26 | ~spl24_27 | ~spl24_28 | ~spl24_33 | ~spl24_36 | ~spl24_43 | ~spl24_47 | ~spl24_48, inference(sat_conversion,[],[f955])).
% 1.35/0.58 cnf(s48, plain, ~spl24_40 | spl24_47 | ~spl24_49 | ~spl24_50, inference(sat_conversion,[],[f968])).
% 1.35/0.58 cnf(s49, plain, ~spl24_39 | ~spl24_43 | spl24_49, inference(sat_conversion,[],[f983])).
% 1.35/0.58 cnf(s50, plain, ~spl24_20 | ~spl24_39 | spl24_50, inference(sat_conversion,[],[f1023])).
% 1.35/0.58 cnf(s51, plain, ~spl24_39 | spl24_48 | ~spl24_51, inference(sat_conversion,[],[f1030])).
% 1.35/0.58 cnf(s52, plain, ~spl24_20 | ~spl24_43 | ~spl24_45 | spl24_51, inference(sat_conversion,[],[f1035])).
% 1.35/0.58 cnf(s53, plain, spl24_36, inference(rat,[],[s34,s23])).
% 1.35/0.58 cnf(s54, plain, spl24_33, inference(rat,[],[s31,s23])).
% 1.35/0.58 cnf(s55, plain, spl24_28, inference(rat,[],[s26,s23])).
% 1.35/0.58 cnf(s56, plain, spl24_27, inference(rat,[],[s25,s23])).
% 1.35/0.58 cnf(s57, plain, spl24_26, inference(rat,[],[s24,s23])).
% 1.35/0.58 cnf(s58, plain, spl24_40, inference(rat,[],[s38,s21])).
% 1.35/0.58 cnf(s59, plain, spl24_23, inference(rat,[],[s20,s23])).
% 1.35/0.58 cnf(s60, plain, spl24_45, inference(rat,[],[s44,s19])).
% 1.35/0.58 cnf(s61, plain, spl24_22, inference(rat,[],[s18,s23])).
% 1.35/0.58 cnf(s62, plain, spl24_21, inference(rat,[],[s17,s39])).
% 1.35/0.58 cnf(s63, plain, spl24_51, inference(rat,[],[s52,s60,s42,s16])).
% 1.35/0.58 cnf(s64, plain, spl24_17, inference(rat,[],[s13,s46])).
% 1.35/0.58 cnf(s65, plain, spl24_12, inference(rat,[],[s9,s23])).
% 1.35/0.58 cnf(s66, plain, spl24_39, inference(rat,[],[s37,s6])).
% 1.35/0.58 cnf(s67, plain, spl24_48, inference(rat,[],[s51,s63,s66])).
% 1.35/0.58 cnf(s68, plain, spl24_50, inference(rat,[],[s50,s16,s66])).
% 1.35/0.58 cnf(s69, plain, spl24_49, inference(rat,[],[s49,s42,s66])).
% 1.35/0.58 cnf(s70, plain, spl24_47, inference(rat,[],[s48,s68,s58,s69])).
% 1.35/0.58 cnf(s71, plain, ~spl24_5, inference(rat,[],[s47,s67,s8,s42,s53,s54,s55,s56,s57,s59,s61,s62,s16,s64,s65,s70])).
% 1.35/0.58 cnf(s72, plain, $false, inference(rat,[],[s4,s23,s71])).
% 1.35/0.58 thf(f1036,plain,(
% 1.35/0.58 $false),
% 1.35/0.58 inference(avatar_sat_refutation,[],[s72])).
% 1.35/0.58 % SZS output end Proof for theBenchmark
% 1.35/0.58 % (2934573)------------------------------
% 1.35/0.58 % (2934573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.35/0.58 % (2934573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.35/0.58 % (2934573)CaDiCaL version: 2.1.3
% 1.35/0.58 % (2934573)Termination reason: Refutation
% 1.35/0.58 % (2934573)Time elapsed: 0.221 s
% 1.35/0.58 % (2934573)Peak memory usage: 14 MB
% 1.35/0.58 % (2934573)Instructions burned: 308 (million)
% 1.35/0.58 % (2934565)Success in time 0.258 s
% 1.35/0.58 % Vampire exiting
%------------------------------------------------------------------------------