%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU753^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 : n019.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:09 AM UTC 2026
% Result : Theorem 0.88s 0.43s
% Output : Refutation 0.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU753^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n019.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 14:21:48 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.08/0.23 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.88/0.37 % (848559)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.88/0.37 % (848567)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=4278044534: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.88/0.37 % (848566)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1420421666:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.88/0.37 % (848564)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1675130711:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.88/0.37 % (848565)lrs+10_16_si=on:nwc=1.5:random_seed=3874936695:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.88/0.37 % (848569)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3152039140:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.88/0.37 % (848566)Instruction limit reached!
% 0.88/0.37 % (848566)------------------------------
% 0.88/0.37 % (848566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.37 % (848566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.37 % (848566)CaDiCaL version: 2.1.3
% 0.88/0.37 % (848566)Termination reason: Instruction limit
% 0.88/0.37 % (848566)Termination phase: Property scanning
% 0.88/0.37 % (848566)Time elapsed: 0.002 s
% 0.88/0.37 % (848566)Peak memory usage: 10 MB
% 0.88/0.37 % (848566)Instructions burned: 3 (million)
% 0.88/0.37 % (848565)Instruction limit reached!
% 0.88/0.37 % (848565)------------------------------
% 0.88/0.37 % (848565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.37 % (848565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.37 % (848565)CaDiCaL version: 2.1.3
% 0.88/0.37 % (848565)Termination reason: Instruction limit
% 0.88/0.37 % (848565)Termination phase: Saturation
% 0.88/0.37 % (848565)Time elapsed: 0.009 s
% 0.88/0.37 % (848565)Peak memory usage: 12 MB
% 0.88/0.37 % (848565)Instructions burned: 19 (million)
% 0.88/0.37 % (848570)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.88/0.37 % (848570)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.88/0.37 % (848570)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=146085376:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.88/0.37 % (848568)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3314588474:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.88/0.37 % (848576)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3446203750:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.88/0.37 % (848576)Instruction limit reached!
% 0.88/0.37 % (848576)------------------------------
% 0.88/0.37 % (848576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.37 % (848576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.37 % (848576)CaDiCaL version: 2.1.3
% 0.88/0.37 % (848576)Termination reason: Instruction limit
% 0.88/0.37 % (848576)Termination phase: Saturation
% 0.88/0.37 % (848576)Time elapsed: 0.003 s
% 0.88/0.37 % (848576)Peak memory usage: 11 MB
% 0.88/0.37 % (848576)Instructions burned: 6 (million)
% 0.88/0.37 % (848577)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3000525769:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.88/0.37 % (848577)Instruction limit reached!
% 0.88/0.37 % (848577)------------------------------
% 0.88/0.37 % (848577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.37 % (848577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.37 % (848577)CaDiCaL version: 2.1.3
% 0.88/0.37 % (848577)Termination reason: Instruction limit
% 0.88/0.37 % (848577)Termination phase: Saturation
% 0.88/0.37 % (848577)Time elapsed: 0.003 s
% 0.88/0.37 % (848577)Peak memory usage: 11 MB
% 0.88/0.37 % (848577)Instructions burned: 6 (million)
% 0.88/0.37 % (848568)Instruction limit reached!
% 0.88/0.42 % (848568)------------------------------
% 0.88/0.42 % (848568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.42 % (848568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.42 % (848568)CaDiCaL version: 2.1.3
% 0.88/0.42 % (848568)Termination reason: Instruction limit
% 0.88/0.42 % (848568)Termination phase: Saturation
% 0.88/0.42 % (848568)Time elapsed: 0.020 s
% 0.88/0.42 % (848568)Peak memory usage: 12 MB
% 0.88/0.42 % (848568)Instructions burned: 24 (million)
% 0.88/0.42 % (848569)Instruction limit reached!
% 0.88/0.42 % (848569)------------------------------
% 0.88/0.42 % (848569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.42 % (848569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.42 % (848569)CaDiCaL version: 2.1.3
% 0.88/0.42 % (848569)Termination reason: Instruction limit
% 0.88/0.42 % (848569)Termination phase: Saturation
% 0.88/0.42 % (848569)Time elapsed: 0.039 s
% 0.88/0.42 % (848569)Peak memory usage: 12 MB
% 0.88/0.42 % (848569)Instructions burned: 75 (million)
% 0.88/0.42 % (848564)Instruction limit reached!
% 0.88/0.42 % (848564)------------------------------
% 0.88/0.42 % (848564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.42 % (848564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.42 % (848564)CaDiCaL version: 2.1.3
% 0.88/0.42 % (848564)Termination reason: Instruction limit
% 0.88/0.42 % (848564)Termination phase: Saturation
% 0.88/0.42 % (848564)Time elapsed: 0.042 s
% 0.88/0.42 % (848564)Peak memory usage: 13 MB
% 0.88/0.42 % (848564)Instructions burned: 89 (million)
% 0.88/0.42 % (848581)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.88/0.42 % (848581)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=296719093:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.88/0.42 % (848583)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2718576397:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.88/0.42 % (848581)Instruction limit reached!
% 0.88/0.42 % (848581)------------------------------
% 0.88/0.42 % (848581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.42 % (848581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.42 % (848581)CaDiCaL version: 2.1.3
% 0.88/0.42 % (848581)Termination reason: Instruction limit
% 0.88/0.42 % (848581)Termination phase: Saturation
% 0.88/0.42 % (848581)Time elapsed: 0.004 s
% 0.88/0.42 % (848581)Peak memory usage: 12 MB
% 0.88/0.42 % (848581)Instructions burned: 8 (million)
% 0.88/0.42 % (848585)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=991852745:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.88/0.42 % (848584)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.88/0.42 % (848584)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.88/0.42 % (848586)lrs+10_1_si=on:cs=on:random_seed=3596464808:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.88/0.42 % (848584)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3802942968:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.88/0.42 % (848583)Instruction limit reached!
% 0.88/0.42 % (848583)------------------------------
% 0.88/0.42 % (848583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.42 % (848583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.42 % (848583)CaDiCaL version: 2.1.3
% 0.88/0.42 % (848583)Termination reason: Instruction limit
% 0.88/0.42 % (848583)Termination phase: Saturation
% 0.88/0.42 % (848583)Time elapsed: 0.009 s
% 0.88/0.42 % (848583)Peak memory usage: 12 MB
% 0.88/0.42 % (848583)Instructions burned: 13 (million)
% 0.88/0.42 % (848586)Instruction limit reached!
% 0.88/0.42 % (848586)------------------------------
% 0.88/0.42 % (848586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848586)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848586)Termination reason: Instruction limit
% 0.88/0.43 % (848586)Termination phase: Saturation
% 0.88/0.43 % (848586)Time elapsed: 0.004 s
% 0.88/0.43 % (848586)Peak memory usage: 11 MB
% 0.88/0.43 % (848586)Instructions burned: 10 (million)
% 0.88/0.43 % (848589)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.88/0.43 % (848570)Instruction limit reached!
% 0.88/0.43 % (848570)------------------------------
% 0.88/0.43 % (848570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848570)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848570)Termination reason: Instruction limit
% 0.88/0.43 % (848570)Termination phase: Saturation
% 0.88/0.43 % (848570)Time elapsed: 0.059 s
% 0.88/0.43 % (848570)Peak memory usage: 13 MB
% 0.88/0.43 % (848570)Instructions burned: 159 (million)
% 0.88/0.43 % (848589)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=2207588448:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.88/0.43 % (848584)Instruction limit reached!
% 0.88/0.43 % (848584)------------------------------
% 0.88/0.43 % (848584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848584)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848584)Termination reason: Instruction limit
% 0.88/0.43 % (848584)Termination phase: Saturation
% 0.88/0.43 % (848584)Time elapsed: 0.015 s
% 0.88/0.43 % (848584)Peak memory usage: 12 MB
% 0.88/0.43 % (848584)Instructions burned: 32 (million)
% 0.88/0.43 % (848589)Instruction limit reached!
% 0.88/0.43 % (848589)------------------------------
% 0.88/0.43 % (848589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848589)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848589)Termination reason: Instruction limit
% 0.88/0.43 % (848589)Termination phase: Saturation
% 0.88/0.43 % (848589)Time elapsed: 0.003 s
% 0.88/0.43 % (848589)Peak memory usage: 12 MB
% 0.88/0.43 % (848589)Instructions burned: 6 (million)
% 0.88/0.43 % (848594)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2338541030:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.88/0.43 % (848593)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2774685551:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.88/0.43 % (848595)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=299639608:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.88/0.43 % (848598)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=4244027817:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 0.88/0.43 % (848597)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=61130012:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.88/0.43 % (848585)Instruction limit reached!
% 0.88/0.43 % (848585)------------------------------
% 0.88/0.43 % (848585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848585)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848585)Termination reason: Instruction limit
% 0.88/0.43 % (848585)Termination phase: Saturation
% 0.88/0.43 % (848585)Time elapsed: 0.041 s
% 0.88/0.43 % (848585)Peak memory usage: 12 MB
% 0.88/0.43 % (848585)Instructions burned: 87 (million)
% 0.88/0.43 % (848597)Instruction limit reached!
% 0.88/0.43 % (848597)------------------------------
% 0.88/0.43 % (848597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848597)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848597)Termination reason: Instruction limit
% 0.88/0.43 % (848597)Termination phase: Saturation
% 0.88/0.43 % (848597)Time elapsed: 0.007 s
% 0.88/0.43 % (848597)Peak memory usage: 12 MB
% 0.88/0.43 % (848597)Instructions burned: 14 (million)
% 0.88/0.43 % (848593)Instruction limit reached!
% 0.88/0.43 % (848593)------------------------------
% 0.88/0.43 % (848593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848593)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848593)Termination reason: Instruction limit
% 0.88/0.43 % (848593)Termination phase: Saturation
% 0.88/0.43 % (848593)Time elapsed: 0.019 s
% 0.88/0.43 % (848593)Peak memory usage: 12 MB
% 0.88/0.43 % (848593)Instructions burned: 38 (million)
% 0.88/0.43 % (848595)Instruction limit reached!
% 0.88/0.43 % (848595)------------------------------
% 0.88/0.43 % (848595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848595)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848595)Termination reason: Instruction limit
% 0.88/0.43 % (848595)Termination phase: Saturation
% 0.88/0.43 % (848595)Time elapsed: 0.026 s
% 0.88/0.43 % (848595)Peak memory usage: 12 MB
% 0.88/0.43 % (848595)Instructions burned: 26 (million)
% 0.88/0.43 % (848606)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=702698711:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.88/0.43 % (848605)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1477593979:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 0.88/0.43 % (848605)Instruction limit reached!
% 0.88/0.43 % (848605)------------------------------
% 0.88/0.43 % (848605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848605)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848605)Termination reason: Instruction limit
% 0.88/0.43 % (848605)Termination phase: Function definition elimination
% 0.88/0.43 % (848605)Time elapsed: 0.002 s
% 0.88/0.43 % (848605)Peak memory usage: 11 MB
% 0.88/0.43 % (848605)Instructions burned: 4 (million)
% 0.88/0.43 % (848604)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=3500326668:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.88/0.43 % (848607)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1416464070:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.88/0.43 % (848606)Instruction limit reached!
% 0.88/0.43 % (848606)------------------------------
% 0.88/0.43 % (848606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848606)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848606)Termination reason: Instruction limit
% 0.88/0.43 % (848606)Termination phase: Saturation
% 0.88/0.43 % (848606)Time elapsed: 0.014 s
% 0.88/0.43 % (848606)Peak memory usage: 12 MB
% 0.88/0.43 % (848606)Instructions burned: 26 (million)
% 0.88/0.43 % (848604)Instruction limit reached!
% 0.88/0.43 % (848604)------------------------------
% 0.88/0.43 % (848604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848604)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848604)Termination reason: Instruction limit
% 0.88/0.43 % (848604)Termination phase: Saturation
% 0.88/0.43 % (848604)Time elapsed: 0.007 s
% 0.88/0.43 % (848604)Peak memory usage: 12 MB
% 0.88/0.43 % (848604)Instructions burned: 14 (million)
% 0.88/0.43 % (848607)Instruction limit reached!
% 0.88/0.43 % (848607)------------------------------
% 0.88/0.43 % (848607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.43 % (848607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.43 % (848607)CaDiCaL version: 2.1.3
% 0.88/0.43 % (848607)Termination reason: Instruction limit
% 0.88/0.43 % (848607)Termination phase: Saturation
% 0.88/0.43 % (848607)Time elapsed: 0.012 s
% 0.88/0.43 % (848607)Peak memory usage: 12 MB
% 0.88/0.43 % (848607)Instructions burned: 24 (million)
% 0.88/0.43 % (848567) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-848559-848567"...
% 0.88/0.43 % (848610)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=4081299529:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.88/0.43 % (848613)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.88/0.43 % (848613)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.88/0.43 % (848614)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.88/0.43 % (848613)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=151150547:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.88/0.43 % (848614)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=4083334425:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.88/0.43 % (848567)...printing done.
% 0.88/0.43 % (848567)Refutation found. Thanks to Tanya!
% 0.88/0.43 % SZS status Theorem for theBenchmark
% 0.88/0.43 % SZS output start Proof for theBenchmark
% 0.88/0.43 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.88/0.43 thf(func_def_0, type, in: ($i > $i > $o)).
% 0.88/0.43 thf(func_def_1, type, powerset: ($i > $i)).
% 0.88/0.43 thf(func_def_2, type, binunion: ($i > $i > $i)).
% 0.88/0.43 thf(func_def_3, type, binintersect: ($i > $i > $i)).
% 0.88/0.43 thf(func_def_4, type, setminus: ($i > $i > $i)).
% 0.88/0.43 thf(func_def_5, type, binintersectT_lem: $o).
% 0.88/0.43 thf(func_def_7, type, binunionT_lem: $o).
% 0.88/0.43 thf(func_def_8, type, complementT_lem: $o).
% 0.88/0.43 thf(func_def_9, type, setextT: $o).
% 0.88/0.43 thf(func_def_10, type, demorgan1a: $o).
% 0.88/0.43 thf(func_def_11, type, demorgan1b: $o).
% 0.88/0.43 thf(func_def_20, type, sK6: ($i > $i > $i > $i)).
% 0.88/0.43 thf(func_def_21, type, sK7: ($i > $i > $i > $i)).
% 0.88/0.43 thf(f1,axiom,(
% 0.88/0.43 (! [X1 : $i,X0 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (in @ (binintersect @ X1 @ X2) @ (powerset @ X0)))) = binintersectT_lem)),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',binintersectT_lem)).
% 0.88/0.43 thf(f2,axiom,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (in @ (binunion @ X1 @ X2) @ (powerset @ X0)))) = binunionT_lem)),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',binunionT_lem)).
% 0.88/0.43 thf(f3,axiom,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => (in @ (setminus @ X0 @ X1) @ (powerset @ X0))) = complementT_lem)),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complementT_lem)).
% 0.88/0.43 thf(f4,axiom,(
% 0.88/0.43 (! [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)),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setextT)).
% 0.88/0.43 thf(f5,axiom,(
% 0.88/0.43 (demorgan1a = ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) => (in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan1a)).
% 0.88/0.43 thf(f6,axiom,(
% 0.88/0.43 (demorgan1b = ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) => (in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))))))))),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan1b)).
% 0.88/0.43 thf(f7,conjecture,(
% 0.88/0.43 binintersectT_lem => (binunionT_lem => (complementT_lem => (setextT => (demorgan1a => (demorgan1b => ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))))))))))),
% 0.88/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan1)).
% 0.88/0.43 thf(f8,negated_conjecture,(
% 0.88/0.43 ~(binintersectT_lem => (binunionT_lem => (complementT_lem => (setextT => (demorgan1a => (demorgan1b => ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))))))),
% 0.88/0.43 inference(negated_conjecture,[status(cth)],[f7])).
% 0.88/0.43 thf(f9,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((in @ X0 @ (powerset @ X1)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X1)) => (in @ (binintersect @ X0 @ X2) @ (powerset @ X1)))) = binintersectT_lem)),
% 0.88/0.43 inference(rectify,[],[f1])).
% 0.88/0.43 thf(f10,plain,(
% 0.88/0.43 ! [X1 : $i,X0 : $i] : ((((in @ X0 @ (powerset @ X1))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X1))) = $true) => (((in @ (binintersect @ X0 @ X2) @ (powerset @ X1))) = $true))) <=> (binintersectT_lem = $true)),
% 0.88/0.43 inference(fool_elimination,[],[f9])).
% 0.88/0.43 thf(f11,plain,(
% 0.88/0.43 ~(binintersectT_lem => (binunionT_lem => (complementT_lem => (setextT => (demorgan1a => (demorgan1b => ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))))))),
% 0.88/0.43 inference(rectify,[],[f8])).
% 0.88/0.43 thf(f12,plain,(
% 0.88/0.43 ~((binintersectT_lem = $true) => ((binunionT_lem = $true) => ((complementT_lem = $true) => ((setextT = $true) => ((demorgan1a = $true) => ((demorgan1b = $true) => ! [X1 : $i,X0 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))))))),
% 0.88/0.43 inference(fool_elimination,[],[f11])).
% 0.88/0.43 thf(f13,plain,(
% 0.88/0.43 (demorgan1a = ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) => (in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))))))),
% 0.88/0.43 inference(rectify,[],[f5])).
% 0.88/0.43 thf(f14,plain,(
% 0.88/0.43 ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => ((((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) => (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true))))) <=> (demorgan1a = $true)),
% 0.88/0.43 inference(fool_elimination,[],[f13])).
% 0.88/0.43 thf(f15,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => (in @ (setminus @ X0 @ X1) @ (powerset @ X0))) = complementT_lem)),
% 0.88/0.43 inference(rectify,[],[f3])).
% 0.88/0.43 thf(f16,plain,(
% 0.88/0.43 (complementT_lem = $true) <=> ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => (((in @ (setminus @ X0 @ X1) @ (powerset @ X0))) = $true))),
% 0.88/0.43 inference(fool_elimination,[],[f15])).
% 0.88/0.43 thf(f17,plain,(
% 0.88/0.43 (demorgan1b = ! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => ! [X3 : $i] : ((in @ X3 @ X0) => ((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) => (in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))))))))),
% 0.88/0.43 inference(rectify,[],[f6])).
% 0.88/0.43 thf(f18,plain,(
% 0.88/0.43 ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => ((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) => (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true))))) <=> (demorgan1b = $true)),
% 0.88/0.43 inference(fool_elimination,[],[f17])).
% 0.88/0.43 thf(f19,plain,(
% 0.88/0.43 (! [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)),
% 0.88/0.43 inference(rectify,[],[f4])).
% 0.88/0.43 thf(f20,plain,(
% 0.88/0.43 ! [X1 : $i,X0 : $i] : ((((in @ X0 @ (powerset @ X1))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X1))) = $true) => (! [X3 : $i] : ((((in @ X3 @ X1)) = $true) => ((((in @ X3 @ X0)) = $true) => (((in @ X3 @ X2)) = $true))) => (! [X4 : $i] : ((((in @ X4 @ X1)) = $true) => ((((in @ X4 @ X2)) = $true) => (((in @ X4 @ X0)) = $true))) => (X0 = X2))))) <=> (setextT = $true)),
% 0.88/0.43 inference(fool_elimination,[],[f19])).
% 0.88/0.43 thf(f21,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((in @ X1 @ (powerset @ X0)) => ! [X2 : $i] : ((in @ X2 @ (powerset @ X0)) => (in @ (binunion @ X1 @ X2) @ (powerset @ X0)))) = binunionT_lem)),
% 0.88/0.43 inference(rectify,[],[f2])).
% 0.88/0.43 thf(f22,plain,(
% 0.88/0.43 ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) => ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) => (((in @ (binunion @ X1 @ X2) @ (powerset @ X0))) = $true))) <=> (binunionT_lem = $true)),
% 0.88/0.43 inference(fool_elimination,[],[f21])).
% 0.88/0.43 thf(f23,plain,(
% 0.88/0.43 ! [X1 : $i,X0 : $i] : ((((in @ (setminus @ X0 @ X1) @ (powerset @ X0))) = $true) | (((in @ X1 @ (powerset @ X0))) != $true)) <=> (complementT_lem = $true)),
% 0.88/0.43 inference(ennf_transformation,[],[f16])).
% 0.88/0.43 thf(f24,plain,(
% 0.88/0.43 (((((? [X1 : $i,X0 : $i] : (? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & (((setminus @ X0 @ (binintersect @ X1 @ X2))) != ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) & (((in @ X1 @ (powerset @ X0))) = $true)) & (demorgan1b = $true)) & (demorgan1a = $true)) & (setextT = $true)) & (complementT_lem = $true)) & (binunionT_lem = $true)) & (binintersectT_lem = $true)),
% 0.88/0.43 inference(ennf_transformation,[],[f12])).
% 0.88/0.43 thf(f25,plain,(
% 0.88/0.43 (binunionT_lem = $true) & (binintersectT_lem = $true) & ? [X1 : $i,X0 : $i] : (? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & (((setminus @ X0 @ (binintersect @ X1 @ X2))) != ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) & (((in @ X1 @ (powerset @ X0))) = $true)) & (demorgan1b = $true) & (demorgan1a = $true) & (setextT = $true) & (complementT_lem = $true)),
% 0.88/0.43 inference(flattening,[],[f24])).
% 0.88/0.43 thf(f26,plain,(
% 0.88/0.43 ! [X1 : $i,X0 : $i] : (! [X2 : $i] : ((((X0 = X2) | ? [X4 : $i] : (((((in @ X4 @ X0)) != $true) & (((in @ X4 @ X2)) = $true)) & (((in @ X4 @ X1)) = $true))) | ? [X3 : $i] : (((((in @ X3 @ X2)) != $true) & (((in @ X3 @ X0)) = $true)) & (((in @ X3 @ X1)) = $true))) | (((in @ X2 @ (powerset @ X1))) != $true)) | (((in @ X0 @ (powerset @ X1))) != $true)) <=> (setextT = $true)),
% 0.88/0.43 inference(ennf_transformation,[],[f20])).
% 0.88/0.43 thf(f27,plain,(
% 0.88/0.43 (setextT = $true) <=> ! [X0 : $i,X1 : $i] : ((((in @ X0 @ (powerset @ X1))) != $true) | ! [X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ X2)) != $true) & (((in @ X3 @ X0)) = $true) & (((in @ X3 @ X1)) = $true)) | (((in @ X2 @ (powerset @ X1))) != $true) | ? [X4 : $i] : ((((in @ X4 @ X2)) = $true) & (((in @ X4 @ X0)) != $true) & (((in @ X4 @ X1)) = $true)) | (X0 = X2)))),
% 0.88/0.43 inference(flattening,[],[f26])).
% 0.88/0.43 thf(f28,plain,(
% 0.88/0.43 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true)) | (((in @ X3 @ X0)) != $true)) | (((in @ X2 @ (powerset @ X0))) != $true)) | (((in @ X1 @ (powerset @ X0))) != $true)) <=> (demorgan1a = $true)),
% 0.88/0.43 inference(ennf_transformation,[],[f14])).
% 0.88/0.43 thf(f29,plain,(
% 0.88/0.43 ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true)) | (((in @ X2 @ (powerset @ X0))) != $true))) <=> (demorgan1a = $true)),
% 0.88/0.43 inference(flattening,[],[f28])).
% 0.88/0.43 thf(f30,plain,(
% 0.88/0.43 (binintersectT_lem = $true) <=> ! [X1 : $i,X0 : $i] : ((((in @ X0 @ (powerset @ X1))) != $true) | ! [X2 : $i] : ((((in @ X2 @ (powerset @ X1))) != $true) | (((in @ (binintersect @ X0 @ X2) @ (powerset @ X1))) = $true)))),
% 0.88/0.43 inference(ennf_transformation,[],[f10])).
% 0.88/0.43 thf(f31,plain,(
% 0.88/0.43 (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)))),
% 0.88/0.43 inference(ennf_transformation,[],[f22])).
% 0.88/0.43 thf(f32,plain,(
% 0.88/0.43 ! [X0 : $i,X1 : $i] : (! [X2 : $i] : (! [X3 : $i] : (((((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true)) | (((in @ X3 @ X0)) != $true)) | (((in @ X2 @ (powerset @ X0))) != $true)) | (((in @ X1 @ (powerset @ X0))) != $true)) <=> (demorgan1b = $true)),
% 0.88/0.43 inference(ennf_transformation,[],[f18])).
% 0.88/0.43 thf(f33,plain,(
% 0.88/0.43 (demorgan1b = $true) <=> ! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | ! [X3 : $i] : ((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true))))),
% 0.88/0.43 inference(flattening,[],[f32])).
% 0.88/0.43 thf(f34,plain,(
% 0.88/0.43 ((binintersectT_lem = $true) | ? [X1 : $i,X0 : $i] : ((((in @ X0 @ (powerset @ X1))) = $true) & ? [X2 : $i] : ((((in @ X2 @ (powerset @ X1))) = $true) & (((in @ (binintersect @ X0 @ X2) @ (powerset @ X1))) != $true)))) & (! [X1 : $i,X0 : $i] : ((((in @ X0 @ (powerset @ X1))) != $true) | ! [X2 : $i] : ((((in @ X2 @ (powerset @ X1))) != $true) | (((in @ (binintersect @ X0 @ X2) @ (powerset @ X1))) = $true))) | (binintersectT_lem != $true))),
% 0.88/0.43 inference(nnf_transformation,[],[f30])).
% 0.88/0.43 thf(f35,plain,(
% 0.88/0.43 ((binintersectT_lem = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & (((in @ (binintersect @ X1 @ X2) @ (powerset @ X0))) != $true)))) & (! [X3 : $i,X4 : $i] : ((((in @ X4 @ (powerset @ X3))) != $true) | ! [X5 : $i] : ((((in @ X5 @ (powerset @ X3))) != $true) | (((in @ (binintersect @ X4 @ X5) @ (powerset @ X3))) = $true))) | (binintersectT_lem != $true))),
% 0.88/0.43 inference(rectify,[],[f34])).
% 0.88/0.43 thf(f36,plain,(
% 0.88/0.43 ((binintersectT_lem = $true) | (($true = ((in @ sK1 @ (powerset @ sK0)))) & ((((in @ sK2 @ (powerset @ sK0))) = $true) & ($true != ((in @ (binintersect @ sK1 @ sK2) @ (powerset @ sK0))))))) & (! [X3 : $i,X4 : $i] : ((((in @ X4 @ (powerset @ X3))) != $true) | ! [X5 : $i] : ((((in @ X5 @ (powerset @ X3))) != $true) | (((in @ (binintersect @ X4 @ X5) @ (powerset @ X3))) = $true))) | (binintersectT_lem != $true))),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f35])).
% 0.88/0.43 thf(f37,plain,(
% 0.88/0.43 ((setextT = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X0 @ (powerset @ X1))) = $true) & ? [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X2)) = $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ X1)) != $true)) & (((in @ X2 @ (powerset @ X1))) = $true) & ! [X4 : $i] : ((((in @ X4 @ X2)) != $true) | (((in @ X4 @ X0)) = $true) | (((in @ X4 @ X1)) != $true)) & (X0 != X2)))) & (! [X0 : $i,X1 : $i] : ((((in @ X0 @ (powerset @ X1))) != $true) | ! [X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ X2)) != $true) & (((in @ X3 @ X0)) = $true) & (((in @ X3 @ X1)) = $true)) | (((in @ X2 @ (powerset @ X1))) != $true) | ? [X4 : $i] : ((((in @ X4 @ X2)) = $true) & (((in @ X4 @ X0)) != $true) & (((in @ X4 @ X1)) = $true)) | (X0 = X2))) | (setextT != $true))),
% 0.88/0.43 inference(nnf_transformation,[],[f27])).
% 0.88/0.43 thf(f38,plain,(
% 0.88/0.43 ((setextT = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X0 @ (powerset @ X1))) = $true) & ? [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X2)) = $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ X1)) != $true)) & (((in @ X2 @ (powerset @ X1))) = $true) & ! [X4 : $i] : ((((in @ X4 @ X2)) != $true) | (((in @ X4 @ X0)) = $true) | (((in @ X4 @ X1)) != $true)) & (X0 != X2)))) & (! [X5 : $i,X6 : $i] : ((((in @ X5 @ (powerset @ X6))) != $true) | ! [X7 : $i] : (? [X8 : $i] : ((((in @ X8 @ X7)) != $true) & (((in @ X8 @ X5)) = $true) & (((in @ X8 @ X6)) = $true)) | (((in @ X7 @ (powerset @ X6))) != $true) | ? [X9 : $i] : ((((in @ X9 @ X7)) = $true) & (((in @ X9 @ X5)) != $true) & (((in @ X9 @ X6)) = $true)) | (X5 = X7))) | (setextT != $true))),
% 0.88/0.43 inference(rectify,[],[f37])).
% 0.88/0.43 thf(f39,plain,(
% 0.88/0.43 ((setextT = $true) | ((((in @ sK3 @ (powerset @ sK4))) = $true) & (! [X3 : $i] : ((((in @ X3 @ sK5)) = $true) | (((in @ X3 @ sK3)) != $true) | (((in @ X3 @ sK4)) != $true)) & (((in @ sK5 @ (powerset @ sK4))) = $true) & ! [X4 : $i] : ((((in @ X4 @ sK5)) != $true) | ($true = ((in @ X4 @ sK3))) | (((in @ X4 @ sK4)) != $true)) & (sK5 != sK3)))) & (! [X5 : $i,X6 : $i] : ((((in @ X5 @ (powerset @ X6))) != $true) | ! [X7 : $i] : (((((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) & (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) & (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true)) | (((in @ X7 @ (powerset @ X6))) != $true) | ((((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) & (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) & (((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true)) | (X5 = X7))) | (setextT != $true))),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,vAPP,vAPP]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X9,sK7 @ X7 @ X6 @ X5),skolemize(X9,sK7 @ X7 @ X6 @ X5)],[f38])).
% 0.88/0.43 thf(f40,plain,(
% 0.88/0.43 ((demorgan1b = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & ? [X3 : $i] : ((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) & (((in @ X3 @ X0)) = $true) & (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true))))) & (! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | ! [X3 : $i] : ((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true)))) | (demorgan1b != $true))),
% 0.88/0.43 inference(nnf_transformation,[],[f33])).
% 0.88/0.43 thf(f41,plain,(
% 0.88/0.43 ((demorgan1b = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : ((((in @ X2 @ (powerset @ X0))) = $true) & ? [X3 : $i] : ((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) & (((in @ X3 @ X0)) = $true) & (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true))))) & (! [X4 : $i,X5 : $i] : ((((in @ X5 @ (powerset @ X4))) != $true) | ! [X6 : $i] : ((((in @ X6 @ (powerset @ X4))) != $true) | ! [X7 : $i] : ((((in @ X7 @ (binunion @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))) != $true) | (((in @ X7 @ X4)) != $true) | (((in @ X7 @ (setminus @ X4 @ (binintersect @ X5 @ X6)))) = $true)))) | (demorgan1b != $true))),
% 0.88/0.43 inference(rectify,[],[f40])).
% 0.88/0.43 thf(f42,plain,(
% 0.88/0.43 ((demorgan1b = $true) | ((((in @ sK9 @ (powerset @ sK8))) = $true) & ((((in @ sK10 @ (powerset @ sK8))) = $true) & (($true = ((in @ sK11 @ (binunion @ (setminus @ sK8 @ sK9) @ (setminus @ sK8 @ sK10))))) & (((in @ sK11 @ sK8)) = $true) & ($true != ((in @ sK11 @ (setminus @ sK8 @ (binintersect @ sK9 @ sK10))))))))) & (! [X4 : $i,X5 : $i] : ((((in @ X5 @ (powerset @ X4))) != $true) | ! [X6 : $i] : ((((in @ X6 @ (powerset @ X4))) != $true) | ! [X7 : $i] : ((((in @ X7 @ (binunion @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))) != $true) | (((in @ X7 @ X4)) != $true) | (((in @ X7 @ (setminus @ X4 @ (binintersect @ X5 @ X6)))) = $true)))) | (demorgan1b != $true))),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X3,sK11)],[f41])).
% 0.88/0.43 thf(f43,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true)) | (((in @ X2 @ (powerset @ X0))) != $true))) | (demorgan1a != $true)) & ((demorgan1a = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) = $true) & ? [X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ X0)) = $true) & (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) & (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true)) & (((in @ X2 @ (powerset @ X0))) = $true))))),
% 0.88/0.43 inference(nnf_transformation,[],[f29])).
% 0.88/0.43 thf(f44,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true)) | (((in @ X2 @ (powerset @ X0))) != $true))) | (demorgan1a != $true)) & ((demorgan1a = $true) | ? [X4 : $i,X5 : $i] : ((((in @ X5 @ (powerset @ X4))) = $true) & ? [X6 : $i] : (? [X7 : $i] : ((((in @ X7 @ X4)) = $true) & (((in @ X7 @ (setminus @ X4 @ (binintersect @ X5 @ X6)))) = $true) & (((in @ X7 @ (binunion @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))) != $true)) & (((in @ X6 @ (powerset @ X4))) = $true))))),
% 0.88/0.43 inference(rectify,[],[f43])).
% 0.88/0.43 thf(f45,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ! [X2 : $i] : (! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true)) | (((in @ X2 @ (powerset @ X0))) != $true))) | (demorgan1a != $true)) & ((demorgan1a = $true) | (($true = ((in @ sK13 @ (powerset @ sK12)))) & (((((in @ sK15 @ sK12)) = $true) & (((in @ sK15 @ (setminus @ sK12 @ (binintersect @ sK13 @ sK14)))) = $true) & (((in @ sK15 @ (binunion @ (setminus @ sK12 @ sK13) @ (setminus @ sK12 @ sK14)))) != $true)) & (((in @ sK14 @ (powerset @ sK12))) = $true))))),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15]),skolemize(X4,sK12),skolemize(X5,sK13),skolemize(X6,sK14),skolemize(X7,sK15)],[f44])).
% 0.88/0.43 thf(f46,plain,(
% 0.88/0.43 (! [X1 : $i,X0 : $i] : ((((in @ (setminus @ X0 @ X1) @ (powerset @ X0))) = $true) | (((in @ X1 @ (powerset @ X0))) != $true)) | (complementT_lem != $true)) & ((complementT_lem = $true) | ? [X1 : $i,X0 : $i] : ((((in @ (setminus @ X0 @ X1) @ (powerset @ X0))) != $true) & (((in @ X1 @ (powerset @ X0))) = $true)))),
% 0.88/0.43 inference(nnf_transformation,[],[f23])).
% 0.88/0.43 thf(f47,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((((in @ (setminus @ X1 @ X0) @ (powerset @ X1))) = $true) | (((in @ X0 @ (powerset @ X1))) != $true)) | (complementT_lem != $true)) & ((complementT_lem = $true) | ? [X2 : $i,X3 : $i] : (($true != ((in @ (setminus @ X3 @ X2) @ (powerset @ X3)))) & (((in @ X2 @ (powerset @ X3))) = $true)))),
% 0.88/0.43 inference(rectify,[],[f46])).
% 0.88/0.43 thf(f48,plain,(
% 0.88/0.43 (! [X0 : $i,X1 : $i] : ((((in @ (setminus @ X1 @ X0) @ (powerset @ X1))) = $true) | (((in @ X0 @ (powerset @ X1))) != $true)) | (complementT_lem != $true)) & ((complementT_lem = $true) | ((((in @ (setminus @ sK17 @ sK16) @ (powerset @ sK17))) != $true) & (((in @ sK16 @ (powerset @ sK17))) = $true)))),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X2,sK16),skolemize(X3,sK17)],[f47])).
% 0.88/0.43 thf(f49,plain,(
% 0.88/0.43 (binunionT_lem = $true) & (binintersectT_lem = $true) & ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((in @ X2 @ (powerset @ X1))) = $true) & (((binunion @ (setminus @ X1 @ X0) @ (setminus @ X1 @ X2))) != ((setminus @ X1 @ (binintersect @ X0 @ X2))))) & (((in @ X0 @ (powerset @ X1))) = $true)) & (demorgan1b = $true) & (demorgan1a = $true) & (setextT = $true) & (complementT_lem = $true)),
% 0.88/0.43 inference(rectify,[],[f25])).
% 0.88/0.43 thf(f50,plain,(
% 0.88/0.43 (binunionT_lem = $true) & (binintersectT_lem = $true) & ((($true = ((in @ sK20 @ (powerset @ sK19)))) & (((setminus @ sK19 @ (binintersect @ sK18 @ sK20))) != ((binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20))))) & (((in @ sK18 @ (powerset @ sK19))) = $true)) & (demorgan1b = $true) & (demorgan1a = $true) & (setextT = $true) & (complementT_lem = $true)),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20]),skolemize(X0,sK18),skolemize(X1,sK19),skolemize(X2,sK20)],[f49])).
% 0.88/0.43 thf(f51,plain,(
% 0.88/0.43 ((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)))) & (! [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))),
% 0.88/0.43 inference(nnf_transformation,[],[f31])).
% 0.88/0.43 thf(f52,plain,(
% 0.88/0.43 ((binunionT_lem = $true) | ? [X0 : $i,X1 : $i] : ((((in @ X0 @ (powerset @ X1))) = $true) & ? [X2 : $i] : ((((in @ (binunion @ X0 @ X2) @ (powerset @ X1))) != $true) & (((in @ X2 @ (powerset @ X1))) = $true)))) & (! [X3 : $i,X4 : $i] : ((((in @ X3 @ (powerset @ X4))) != $true) | ! [X5 : $i] : ((((in @ (binunion @ X3 @ X5) @ (powerset @ X4))) = $true) | (((in @ X5 @ (powerset @ X4))) != $true))) | (binunionT_lem != $true))),
% 0.88/0.43 inference(rectify,[],[f51])).
% 0.88/0.43 thf(f53,plain,(
% 0.88/0.43 ((binunionT_lem = $true) | ((((in @ sK21 @ (powerset @ sK22))) = $true) & ((((in @ (binunion @ sK21 @ sK23) @ (powerset @ sK22))) != $true) & (((in @ sK23 @ (powerset @ sK22))) = $true)))) & (! [X3 : $i,X4 : $i] : ((((in @ X3 @ (powerset @ X4))) != $true) | ! [X5 : $i] : ((((in @ (binunion @ X3 @ X5) @ (powerset @ X4))) = $true) | (((in @ X5 @ (powerset @ X4))) != $true))) | (binunionT_lem != $true))),
% 0.88/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23]),skolemize(X0,sK21),skolemize(X1,sK22),skolemize(X2,sK23)],[f52])).
% 0.88/0.43 thf(f54,plain,(
% 0.88/0.43 ( ! [X3 : $i,X4 : $i,X5 : $i] : ((binintersectT_lem != $true) | (((in @ X5 @ (powerset @ X3))) != $true) | (((in @ (binintersect @ X4 @ X5) @ (powerset @ X3))) = $true) | (((in @ X4 @ (powerset @ X3))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f36])).
% 0.88/0.43 thf(f58,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (X5 = X7) | (((in @ X7 @ (powerset @ X6))) != $true) | (setextT != $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f59,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (X5 = X7) | (setextT != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f60,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (setextT != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f61,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (setextT != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ X5 @ (powerset @ X6))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f62,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ X7 @ (powerset @ X6))) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (X5 = X7) | (((in @ X5 @ (powerset @ X6))) != $true) | (setextT != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f63,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ X5 @ (powerset @ X6))) != $true) | (setextT != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (X5 = X7)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f64,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (setextT != $true) | (((in @ X5 @ (powerset @ X6))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f65,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (setextT != $true) | (((in @ X5 @ (powerset @ X6))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f66,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7) | (setextT != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f39])).
% 0.88/0.43 thf(f72,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : ((((in @ X6 @ (powerset @ X4))) != $true) | (demorgan1b != $true) | (((in @ X7 @ X4)) != $true) | (((in @ X5 @ (powerset @ X4))) != $true) | (((in @ X7 @ (setminus @ X4 @ (binintersect @ X5 @ X6)))) = $true) | (((in @ X7 @ (binunion @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f42])).
% 0.88/0.43 thf(f83,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((demorgan1a != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) | (((in @ X3 @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f45])).
% 0.88/0.43 thf(f86,plain,(
% 0.88/0.43 ( ! [X0 : $i,X1 : $i] : ((((in @ (setminus @ X1 @ X0) @ (powerset @ X1))) = $true) | (complementT_lem != $true) | (((in @ X0 @ (powerset @ X1))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f48])).
% 0.88/0.43 thf(f87,plain,(
% 0.88/0.43 (complementT_lem = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f88,plain,(
% 0.88/0.43 (setextT = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f89,plain,(
% 0.88/0.43 (demorgan1a = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f90,plain,(
% 0.88/0.43 (demorgan1b = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f91,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f92,plain,(
% 0.88/0.43 (((setminus @ sK19 @ (binintersect @ sK18 @ sK20))) != ((binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20))))),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f93,plain,(
% 0.88/0.43 ($true = ((in @ sK20 @ (powerset @ sK19))))),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f94,plain,(
% 0.88/0.43 (binintersectT_lem = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f95,plain,(
% 0.88/0.43 (binunionT_lem = $true)),
% 0.88/0.43 inference(cnf_transformation,[],[f50])).
% 0.88/0.43 thf(f96,plain,(
% 0.88/0.43 ( ! [X3 : $i,X4 : $i,X5 : $i] : ((binunionT_lem != $true) | (((in @ (binunion @ X3 @ X5) @ (powerset @ X4))) = $true) | (((in @ X3 @ (powerset @ X4))) != $true) | (((in @ X5 @ (powerset @ X4))) != $true)) )),
% 0.88/0.43 inference(cnf_transformation,[],[f53])).
% 0.88/0.43 thf(f105,definition,(
% 0.88/0.43 spl24_2 <=> (setextT = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition])).
% 0.88/0.43 thf(f114,definition,(
% 0.88/0.43 spl24_4 <=> (demorgan1a = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition])).
% 0.88/0.43 thf(f119,definition,(
% 0.88/0.43 spl24_5 <=> ! [X5 : $i,X4 : $i,X7 : $i,X6 : $i] : ((((in @ X6 @ (powerset @ X4))) != $true) | (((in @ X7 @ (binunion @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))) != $true) | (((in @ X7 @ (setminus @ X4 @ (binintersect @ X5 @ X6)))) = $true) | (((in @ X5 @ (powerset @ X4))) != $true) | (((in @ X7 @ X4)) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition])).
% 0.88/0.43 thf(f120,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $i] : ((((in @ X7 @ (binunion @ (setminus @ X4 @ X5) @ (setminus @ X4 @ X6)))) != $true) | (((in @ X6 @ (powerset @ X4))) != $true) | (((in @ X5 @ (powerset @ X4))) != $true) | (((in @ X7 @ X4)) != $true) | (((in @ X7 @ (setminus @ X4 @ (binintersect @ X5 @ X6)))) = $true)) ) | ~spl24_5),
% 0.88/0.43 inference(avatar_component_clause,[],[f119])).
% 0.88/0.43 thf(f122,definition,(
% 0.88/0.43 spl24_6 <=> (demorgan1b = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition])).
% 0.88/0.43 thf(f125,plain,(
% 0.88/0.43 spl24_5 | ~spl24_6),
% 0.88/0.43 inference(avatar_split_clause,[],[f72,f122,f119])).
% 0.88/0.43 thf(f127,definition,(
% 0.88/0.43 spl24_7 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (X5 = X7) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition])).
% 0.88/0.43 thf(f128,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (X5 = X7)) ) | ~spl24_7),
% 0.88/0.43 inference(avatar_component_clause,[],[f127])).
% 0.88/0.43 thf(f129,plain,(
% 0.88/0.43 spl24_7 | ~spl24_2),
% 0.88/0.43 inference(avatar_split_clause,[],[f66,f105,f127])).
% 0.88/0.43 thf(f131,definition,(
% 0.88/0.43 spl24_8 <=> ! [X4 : $i,X5 : $i,X3 : $i] : ((((in @ X5 @ (powerset @ X3))) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ (binintersect @ X4 @ X5) @ (powerset @ X3))) = $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition])).
% 0.88/0.43 thf(f132,plain,(
% 0.88/0.43 ( ! [X3 : $i,X4 : $i,X5 : $i] : ((((in @ (binintersect @ X4 @ X5) @ (powerset @ X3))) = $true) | (((in @ X5 @ (powerset @ X3))) != $true) | (((in @ X4 @ (powerset @ X3))) != $true)) ) | ~spl24_8),
% 0.88/0.43 inference(avatar_component_clause,[],[f131])).
% 0.88/0.43 thf(f134,definition,(
% 0.88/0.43 spl24_9 <=> (binintersectT_lem = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition])).
% 0.88/0.43 thf(f137,plain,(
% 0.88/0.43 spl24_8 | ~spl24_9),
% 0.88/0.43 inference(avatar_split_clause,[],[f54,f134,f131])).
% 0.88/0.43 thf(f153,definition,(
% 0.88/0.43 spl24_13 <=> (binunionT_lem = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition])).
% 0.88/0.43 thf(f168,definition,(
% 0.88/0.43 spl24_16 <=> (complementT_lem = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_16])],[avatar_definition])).
% 0.88/0.43 thf(f171,plain,(
% 0.88/0.43 spl24_16),
% 0.88/0.43 inference(avatar_split_clause,[],[f87,f168])).
% 0.88/0.43 thf(f173,definition,(
% 0.88/0.43 spl24_17 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ X5 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition])).
% 0.88/0.43 thf(f174,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ X5 @ (powerset @ X6))) != $true)) ) | ~spl24_17),
% 0.88/0.43 inference(avatar_component_clause,[],[f173])).
% 0.88/0.43 thf(f175,plain,(
% 0.88/0.43 spl24_17 | ~spl24_2),
% 0.88/0.43 inference(avatar_split_clause,[],[f63,f105,f173])).
% 0.88/0.43 thf(f177,definition,(
% 0.88/0.43 spl24_18 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((X5 = X7) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition])).
% 0.88/0.43 thf(f178,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true)) ) | ~spl24_18),
% 0.88/0.43 inference(avatar_component_clause,[],[f177])).
% 0.88/0.43 thf(f179,plain,(
% 0.88/0.43 ~spl24_2 | spl24_18),
% 0.88/0.43 inference(avatar_split_clause,[],[f64,f177,f105])).
% 0.88/0.43 thf(f181,definition,(
% 0.88/0.43 spl24_19 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_19])],[avatar_definition])).
% 0.88/0.43 thf(f182,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (X5 = X7)) ) | ~spl24_19),
% 0.88/0.43 inference(avatar_component_clause,[],[f181])).
% 0.88/0.43 thf(f183,plain,(
% 0.88/0.43 ~spl24_2 | spl24_19),
% 0.88/0.43 inference(avatar_split_clause,[],[f61,f181,f105])).
% 0.88/0.43 thf(f185,definition,(
% 0.88/0.43 spl24_20 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (X5 = X7) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition])).
% 0.88/0.43 thf(f186,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (X5 = X7) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (((in @ X7 @ (powerset @ X6))) != $true)) ) | ~spl24_20),
% 0.88/0.43 inference(avatar_component_clause,[],[f185])).
% 0.88/0.43 thf(f187,plain,(
% 0.88/0.43 spl24_20 | ~spl24_2),
% 0.88/0.43 inference(avatar_split_clause,[],[f59,f105,f185])).
% 0.88/0.43 thf(f198,plain,(
% 0.88/0.43 spl24_6),
% 0.88/0.43 inference(avatar_split_clause,[],[f90,f122])).
% 0.88/0.43 thf(f200,definition,(
% 0.88/0.43 spl24_23 <=> ! [X0 : $i,X1 : $i] : ((((in @ (setminus @ X1 @ X0) @ (powerset @ X1))) = $true) | (((in @ X0 @ (powerset @ X1))) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition])).
% 0.88/0.43 thf(f201,plain,(
% 0.88/0.43 ( ! [X0 : $i,X1 : $i] : ((((in @ (setminus @ X1 @ X0) @ (powerset @ X1))) = $true) | (((in @ X0 @ (powerset @ X1))) != $true)) ) | ~spl24_23),
% 0.88/0.43 inference(avatar_component_clause,[],[f200])).
% 0.88/0.43 thf(f202,plain,(
% 0.88/0.43 ~spl24_16 | spl24_23),
% 0.88/0.43 inference(avatar_split_clause,[],[f86,f200,f168])).
% 0.88/0.43 thf(f209,definition,(
% 0.88/0.43 spl24_25 <=> (((setminus @ sK19 @ (binintersect @ sK18 @ sK20))) = ((binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20))))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition])).
% 0.88/0.43 thf(f211,plain,(
% 0.88/0.43 (((setminus @ sK19 @ (binintersect @ sK18 @ sK20))) != ((binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)))) | spl24_25),
% 0.88/0.43 inference(avatar_component_clause,[],[f209])).
% 0.88/0.43 thf(f212,plain,(
% 0.88/0.43 ~spl24_25),
% 0.88/0.43 inference(avatar_split_clause,[],[f92,f209])).
% 0.88/0.43 thf(f224,definition,(
% 0.88/0.43 spl24_28 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((X5 = X7) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition])).
% 0.88/0.43 thf(f225,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X7)) = $true) | (X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true)) ) | ~spl24_28),
% 0.88/0.43 inference(avatar_component_clause,[],[f224])).
% 0.88/0.43 thf(f226,plain,(
% 0.88/0.43 spl24_28 | ~spl24_2),
% 0.88/0.43 inference(avatar_split_clause,[],[f60,f105,f224])).
% 0.88/0.43 thf(f227,plain,(
% 0.88/0.43 spl24_4),
% 0.88/0.43 inference(avatar_split_clause,[],[f89,f114])).
% 0.88/0.43 thf(f239,definition,(
% 0.88/0.43 spl24_31 <=> (((in @ sK18 @ (powerset @ sK19))) = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_31])],[avatar_definition])).
% 0.88/0.43 thf(f241,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) = $true) | ~spl24_31),
% 0.88/0.43 inference(avatar_component_clause,[],[f239])).
% 0.88/0.43 thf(f242,plain,(
% 0.88/0.43 spl24_31),
% 0.88/0.43 inference(avatar_split_clause,[],[f91,f239])).
% 0.88/0.43 thf(f253,plain,(
% 0.88/0.43 spl24_2),
% 0.88/0.43 inference(avatar_split_clause,[],[f88,f105])).
% 0.88/0.43 thf(f260,definition,(
% 0.88/0.43 spl24_35 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ X7 @ (powerset @ X6))) != $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_35])],[avatar_definition])).
% 0.88/0.43 thf(f261,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK6 @ X7 @ X6 @ X5) @ X5)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true)) ) | ~spl24_35),
% 0.88/0.43 inference(avatar_component_clause,[],[f260])).
% 0.88/0.43 thf(f262,plain,(
% 0.88/0.43 ~spl24_2 | spl24_35),
% 0.88/0.43 inference(avatar_split_clause,[],[f62,f260,f105])).
% 0.88/0.43 thf(f289,definition,(
% 0.88/0.43 spl24_41 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (X5 = X7))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_41])],[avatar_definition])).
% 0.88/0.43 thf(f290,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X6)) = $true) | (X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X6)) = $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ X5 @ (powerset @ X6))) != $true)) ) | ~spl24_41),
% 0.88/0.43 inference(avatar_component_clause,[],[f289])).
% 0.88/0.43 thf(f291,plain,(
% 0.88/0.43 spl24_41 | ~spl24_2),
% 0.88/0.43 inference(avatar_split_clause,[],[f58,f105,f289])).
% 0.88/0.43 thf(f296,plain,(
% 0.88/0.43 spl24_13),
% 0.88/0.43 inference(avatar_split_clause,[],[f95,f153])).
% 0.88/0.43 thf(f298,definition,(
% 0.88/0.43 spl24_43 <=> ! [X6 : $i,X5 : $i,X7 : $i] : ((((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (((in @ X5 @ (powerset @ X6))) != $true) | (((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (X5 = X7) | (((in @ X7 @ (powerset @ X6))) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_43])],[avatar_definition])).
% 0.88/0.43 thf(f299,plain,(
% 0.88/0.43 ( ! [X6 : $i,X7 : $i,X5 : $i] : ((((in @ (sK7 @ X7 @ X6 @ X5) @ X5)) != $true) | (X5 = X7) | (((in @ (sK6 @ X7 @ X6 @ X5) @ X7)) != $true) | (((in @ X7 @ (powerset @ X6))) != $true) | (((in @ X5 @ (powerset @ X6))) != $true)) ) | ~spl24_43),
% 0.88/0.43 inference(avatar_component_clause,[],[f298])).
% 0.88/0.43 thf(f300,plain,(
% 0.88/0.43 ~spl24_2 | spl24_43),
% 0.88/0.43 inference(avatar_split_clause,[],[f65,f298,f105])).
% 0.88/0.43 thf(f302,definition,(
% 0.88/0.43 spl24_44 <=> ! [X4 : $i,X5 : $i,X3 : $i] : ((((in @ (binunion @ X3 @ X5) @ (powerset @ X4))) = $true) | (((in @ X5 @ (powerset @ X4))) != $true) | (((in @ X3 @ (powerset @ X4))) != $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_44])],[avatar_definition])).
% 0.88/0.43 thf(f303,plain,(
% 0.88/0.43 ( ! [X3 : $i,X4 : $i,X5 : $i] : ((((in @ (binunion @ X3 @ X5) @ (powerset @ X4))) = $true) | (((in @ X5 @ (powerset @ X4))) != $true) | (((in @ X3 @ (powerset @ X4))) != $true)) ) | ~spl24_44),
% 0.88/0.43 inference(avatar_component_clause,[],[f302])).
% 0.88/0.43 thf(f304,plain,(
% 0.88/0.43 spl24_44 | ~spl24_13),
% 0.88/0.43 inference(avatar_split_clause,[],[f96,f153,f302])).
% 0.88/0.43 thf(f306,definition,(
% 0.88/0.43 spl24_45 <=> ($true = ((in @ sK20 @ (powerset @ sK19))))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_45])],[avatar_definition])).
% 0.88/0.43 thf(f308,plain,(
% 0.88/0.43 ($true = ((in @ sK20 @ (powerset @ sK19)))) | ~spl24_45),
% 0.88/0.43 inference(avatar_component_clause,[],[f306])).
% 0.88/0.43 thf(f309,plain,(
% 0.88/0.43 spl24_45),
% 0.88/0.43 inference(avatar_split_clause,[],[f93,f306])).
% 0.88/0.43 thf(f311,definition,(
% 0.88/0.43 spl24_46 <=> ! [X0 : $i,X3 : $i,X2 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_46])],[avatar_definition])).
% 0.88/0.43 thf(f312,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X3 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) = $true) | (((in @ X3 @ X0)) != $true) | (((in @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | ~spl24_46),
% 0.88/0.43 inference(avatar_component_clause,[],[f311])).
% 0.88/0.43 thf(f313,plain,(
% 0.88/0.43 spl24_46 | ~spl24_4),
% 0.88/0.43 inference(avatar_split_clause,[],[f83,f114,f311])).
% 0.88/0.43 thf(f314,plain,(
% 0.88/0.43 spl24_9),
% 0.88/0.43 inference(avatar_split_clause,[],[f94,f134])).
% 0.88/0.43 thf(f330,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | ($true != $true) | ($true = ((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X3))) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | ($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_28)),
% 0.88/0.43 inference(superposition,[],[f120,f225])).
% 0.88/0.43 thf(f331,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((in @ X4 @ (powerset @ X3))) != $true) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | ($true != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X4)) = $true) | ($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))))) ) | (~spl24_5 | ~spl24_17)),
% 0.88/0.43 inference(superposition,[],[f120,f174])).
% 0.88/0.43 thf(f332,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | ($true != ((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | ($true != $true) | ($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | (((in @ X4 @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7)),
% 0.88/0.43 inference(superposition,[],[f120,f128])).
% 0.88/0.43 thf(f339,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X4)) = $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_17)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f331])).
% 0.88/0.43 thf(f340,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | ($true = ((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X3))) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_28)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f330])).
% 0.88/0.43 thf(f343,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true != ((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4)) ) | (~spl24_5 | ~spl24_7)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f332])).
% 0.88/0.43 thf(f428,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | ($true != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | ($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f343,f312])).
% 0.88/0.43 thf(f430,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | ($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | ($true != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f428])).
% 0.88/0.43 thf(f431,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2))))) | (((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))) = X4) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X4 @ (powerset @ X3))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ X4) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f430])).
% 0.88/0.43 thf(f483,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | ($true != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f299,f431])).
% 0.88/0.43 thf(f484,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | ($true != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f483])).
% 0.88/0.43 thf(f485,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f484])).
% 0.88/0.43 thf(f488,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f485,f120])).
% 0.88/0.43 thf(f556,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | ($true != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f488,f312])).
% 0.88/0.43 thf(f560,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | ($true != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f556])).
% 0.88/0.43 thf(f561,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f560])).
% 0.88/0.43 thf(f646,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | ($true != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f561,f261])).
% 0.88/0.43 thf(f650,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f646])).
% 0.88/0.43 thf(f651,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f650])).
% 0.88/0.43 thf(f693,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | ($true != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f651,f339])).
% 0.88/0.43 thf(f716,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | ($true != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f693])).
% 0.88/0.43 thf(f717,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f716])).
% 0.88/0.43 thf(f721,plain,(
% 0.88/0.43 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : ((((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X3))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X3))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X3 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f717,f561])).
% 0.88/0.43 thf(f723,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | ($true != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_19 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f721,f182])).
% 0.88/0.43 thf(f724,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | ($true != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f721,f178])).
% 0.88/0.43 thf(f734,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_19 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f723])).
% 0.88/0.43 thf(f735,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) = $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_19 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f734])).
% 0.88/0.43 thf(f738,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f724])).
% 0.88/0.43 thf(f739,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f738])).
% 0.88/0.43 thf(f785,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f739,f312])).
% 0.88/0.43 thf(f786,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f785])).
% 0.88/0.43 thf(f787,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f786])).
% 0.88/0.43 thf(f788,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f787,f735])).
% 0.88/0.43 thf(f798,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | ($true != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f788,f186])).
% 0.88/0.43 thf(f805,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | ($true != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f798])).
% 0.88/0.43 thf(f806,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ (setminus @ X0 @ (binintersect @ X1 @ X2)))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f805])).
% 0.88/0.43 thf(f851,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) = $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | ($true != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_28 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f806,f340])).
% 0.88/0.43 thf(f853,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) = $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2))))) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_28 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(duplicate_literal_removal,[],[f851])).
% 0.88/0.43 thf(f854,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true) | (((in @ (sK7 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) = $true) | (((in @ X1 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_28 | ~spl24_35 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f853])).
% 0.88/0.43 thf(f859,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ (sK6 @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ X0 @ (setminus @ X0 @ (binintersect @ X1 @ X2))) @ X0)) = $true) | (((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_28 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f854,f290])).
% 0.88/0.43 thf(f861,plain,(
% 0.88/0.43 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((setminus @ X0 @ (binintersect @ X1 @ X2))) = ((binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)))) | (((in @ (binunion @ (setminus @ X0 @ X1) @ (setminus @ X0 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X1 @ (powerset @ X0))) != $true) | (((in @ (setminus @ X0 @ (binintersect @ X1 @ X2)) @ (powerset @ X0))) != $true) | (((in @ X2 @ (powerset @ X0))) != $true)) ) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | ~spl24_28 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f859,f788])).
% 0.88/0.43 thf(f938,plain,(
% 0.88/0.43 (((setminus @ sK19 @ (binintersect @ sK18 @ sK20))) != ((setminus @ sK19 @ (binintersect @ sK18 @ sK20)))) | (((in @ (setminus @ sK19 @ (binintersect @ sK18 @ sK20)) @ (powerset @ sK19))) != $true) | ($true != ((in @ sK20 @ (powerset @ sK19)))) | (((in @ (binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)) @ (powerset @ sK19))) != $true) | (((in @ sK18 @ (powerset @ sK19))) != $true) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | spl24_25 | ~spl24_28 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(superposition,[],[f211,f861])).
% 0.88/0.43 thf(f1005,plain,(
% 0.88/0.43 ($true != ((in @ sK20 @ (powerset @ sK19)))) | (((in @ (binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)) @ (powerset @ sK19))) != $true) | (((in @ (setminus @ sK19 @ (binintersect @ sK18 @ sK20)) @ (powerset @ sK19))) != $true) | (((in @ sK18 @ (powerset @ sK19))) != $true) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | spl24_25 | ~spl24_28 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_46)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f938])).
% 0.88/0.43 thf(f1067,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) != $true) | (((in @ (setminus @ sK19 @ (binintersect @ sK18 @ sK20)) @ (powerset @ sK19))) != $true) | (((in @ (binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)) @ (powerset @ sK19))) != $true) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | spl24_25 | ~spl24_28 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_45 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f1005,f308])).
% 0.88/0.43 thf(f1068,plain,(
% 0.88/0.43 (((in @ (setminus @ sK19 @ (binintersect @ sK18 @ sK20)) @ (powerset @ sK19))) != $true) | (((in @ (binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)) @ (powerset @ sK19))) != $true) | (~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | spl24_25 | ~spl24_28 | ~spl24_31 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_45 | ~spl24_46)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f1067,f241])).
% 0.88/0.43 thf(f1070,definition,(
% 0.88/0.43 spl24_47 <=> (((in @ (binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)) @ (powerset @ sK19))) = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_47])],[avatar_definition])).
% 0.88/0.43 thf(f1072,plain,(
% 0.88/0.43 (((in @ (binunion @ (setminus @ sK19 @ sK18) @ (setminus @ sK19 @ sK20)) @ (powerset @ sK19))) != $true) | spl24_47),
% 0.88/0.43 inference(avatar_component_clause,[],[f1070])).
% 0.88/0.43 thf(f1074,definition,(
% 0.88/0.43 spl24_48 <=> (((in @ (setminus @ sK19 @ (binintersect @ sK18 @ sK20)) @ (powerset @ sK19))) = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_48])],[avatar_definition])).
% 0.88/0.43 thf(f1076,plain,(
% 0.88/0.43 (((in @ (setminus @ sK19 @ (binintersect @ sK18 @ sK20)) @ (powerset @ sK19))) != $true) | spl24_48),
% 0.88/0.43 inference(avatar_component_clause,[],[f1074])).
% 0.88/0.43 thf(f1077,plain,(
% 0.88/0.43 ~spl24_47 | ~spl24_48 | ~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | spl24_25 | ~spl24_28 | ~spl24_31 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_45 | ~spl24_46),
% 0.88/0.43 inference(avatar_split_clause,[],[f1068,f311,f306,f298,f289,f260,f239,f224,f209,f185,f181,f177,f173,f127,f119,f1074,f1070])).
% 0.88/0.43 thf(f1090,plain,(
% 0.88/0.43 (((in @ (setminus @ sK19 @ sK18) @ (powerset @ sK19))) != $true) | ($true != ((in @ (setminus @ sK19 @ sK20) @ (powerset @ sK19)))) | ($true != $true) | (~spl24_44 | spl24_47)),
% 0.88/0.43 inference(superposition,[],[f1072,f303])).
% 0.88/0.43 thf(f1091,plain,(
% 0.88/0.43 ($true != ((in @ (setminus @ sK19 @ sK20) @ (powerset @ sK19)))) | (((in @ (setminus @ sK19 @ sK18) @ (powerset @ sK19))) != $true) | (~spl24_44 | spl24_47)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f1090])).
% 0.88/0.43 thf(f1094,definition,(
% 0.88/0.43 spl24_49 <=> (((in @ (setminus @ sK19 @ sK18) @ (powerset @ sK19))) = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_49])],[avatar_definition])).
% 0.88/0.43 thf(f1096,plain,(
% 0.88/0.43 (((in @ (setminus @ sK19 @ sK18) @ (powerset @ sK19))) != $true) | spl24_49),
% 0.88/0.43 inference(avatar_component_clause,[],[f1094])).
% 0.88/0.43 thf(f1098,definition,(
% 0.88/0.43 spl24_50 <=> ($true = ((in @ (setminus @ sK19 @ sK20) @ (powerset @ sK19))))),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_50])],[avatar_definition])).
% 0.88/0.43 thf(f1100,plain,(
% 0.88/0.43 ($true != ((in @ (setminus @ sK19 @ sK20) @ (powerset @ sK19)))) | spl24_50),
% 0.88/0.43 inference(avatar_component_clause,[],[f1098])).
% 0.88/0.43 thf(f1101,plain,(
% 0.88/0.43 ~spl24_49 | ~spl24_50 | ~spl24_44 | spl24_47),
% 0.88/0.43 inference(avatar_split_clause,[],[f1091,f1070,f302,f1098,f1094])).
% 0.88/0.43 thf(f1114,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) != $true) | ($true != $true) | (~spl24_23 | spl24_49)),
% 0.88/0.43 inference(superposition,[],[f1096,f201])).
% 0.88/0.43 thf(f1115,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) != $true) | (~spl24_23 | spl24_49)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f1114])).
% 0.88/0.43 thf(f1116,plain,(
% 0.88/0.43 $false | (~spl24_23 | ~spl24_31 | spl24_49)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f1115,f241])).
% 0.88/0.43 thf(f1117,plain,(
% 0.88/0.43 ~spl24_23 | ~spl24_31 | spl24_49),
% 0.88/0.43 inference(avatar_contradiction_clause,[],[f1116])).
% 0.88/0.43 thf(f1118,plain,(
% 0.88/0.43 ($true != $true) | ($true != ((in @ sK20 @ (powerset @ sK19)))) | (~spl24_23 | spl24_50)),
% 0.88/0.43 inference(superposition,[],[f1100,f201])).
% 0.88/0.43 thf(f1119,plain,(
% 0.88/0.43 ($true != ((in @ sK20 @ (powerset @ sK19)))) | (~spl24_23 | spl24_50)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f1118])).
% 0.88/0.43 thf(f1120,plain,(
% 0.88/0.43 $false | (~spl24_23 | ~spl24_45 | spl24_50)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f1119,f308])).
% 0.88/0.43 thf(f1121,plain,(
% 0.88/0.43 ~spl24_23 | ~spl24_45 | spl24_50),
% 0.88/0.43 inference(avatar_contradiction_clause,[],[f1120])).
% 0.88/0.43 thf(f1122,plain,(
% 0.88/0.43 (((in @ (binintersect @ sK18 @ sK20) @ (powerset @ sK19))) != $true) | ($true != $true) | (~spl24_23 | spl24_48)),
% 0.88/0.43 inference(superposition,[],[f1076,f201])).
% 0.88/0.43 thf(f1123,plain,(
% 0.88/0.43 (((in @ (binintersect @ sK18 @ sK20) @ (powerset @ sK19))) != $true) | (~spl24_23 | spl24_48)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f1122])).
% 0.88/0.43 thf(f1125,definition,(
% 0.88/0.43 spl24_51 <=> (((in @ (binintersect @ sK18 @ sK20) @ (powerset @ sK19))) = $true)),
% 0.88/0.43 introduced(definition,[new_symbols(definition,[spl24_51])],[avatar_definition])).
% 0.88/0.43 thf(f1127,plain,(
% 0.88/0.43 (((in @ (binintersect @ sK18 @ sK20) @ (powerset @ sK19))) != $true) | spl24_51),
% 0.88/0.43 inference(avatar_component_clause,[],[f1125])).
% 0.88/0.43 thf(f1128,plain,(
% 0.88/0.43 ~spl24_51 | ~spl24_23 | spl24_48),
% 0.88/0.43 inference(avatar_split_clause,[],[f1123,f1074,f200,f1125])).
% 0.88/0.43 thf(f1176,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) != $true) | ($true != ((in @ sK20 @ (powerset @ sK19)))) | ($true != $true) | (~spl24_8 | spl24_51)),
% 0.88/0.43 inference(superposition,[],[f1127,f132])).
% 0.88/0.43 thf(f1177,plain,(
% 0.88/0.43 (((in @ sK18 @ (powerset @ sK19))) != $true) | ($true != ((in @ sK20 @ (powerset @ sK19)))) | (~spl24_8 | spl24_51)),
% 0.88/0.43 inference(trivial_inequality_removal,[],[f1176])).
% 0.88/0.43 thf(f1178,plain,(
% 0.88/0.43 ($true != ((in @ sK20 @ (powerset @ sK19)))) | (~spl24_8 | ~spl24_31 | spl24_51)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f1177,f241])).
% 0.88/0.43 thf(f1179,plain,(
% 0.88/0.43 $false | (~spl24_8 | ~spl24_31 | ~spl24_45 | spl24_51)),
% 0.88/0.43 inference(forward_subsumption_resolution,[],[f1178,f308])).
% 0.88/0.43 thf(f1180,plain,(
% 0.88/0.43 ~spl24_8 | ~spl24_31 | ~spl24_45 | spl24_51),
% 0.88/0.43 inference(avatar_contradiction_clause,[],[f1179])).
% 0.88/0.43 cnf(s3, plain, spl24_5 | ~spl24_6, inference(sat_conversion,[],[f125])).
% 0.88/0.43 cnf(s4, plain, ~spl24_2 | spl24_7, inference(sat_conversion,[],[f129])).
% 0.88/0.43 cnf(s5, plain, spl24_8 | ~spl24_9, inference(sat_conversion,[],[f137])).
% 0.88/0.43 cnf(s11, plain, spl24_16, inference(sat_conversion,[],[f171])).
% 0.88/0.43 cnf(s12, plain, ~spl24_2 | spl24_17, inference(sat_conversion,[],[f175])).
% 0.88/0.43 cnf(s13, plain, ~spl24_2 | spl24_18, inference(sat_conversion,[],[f179])).
% 0.88/0.43 cnf(s14, plain, ~spl24_2 | spl24_19, inference(sat_conversion,[],[f183])).
% 0.88/0.43 cnf(s15, plain, ~spl24_2 | spl24_20, inference(sat_conversion,[],[f187])).
% 0.88/0.43 cnf(s18, plain, spl24_6, inference(sat_conversion,[],[f198])).
% 0.88/0.43 cnf(s19, plain, ~spl24_16 | spl24_23, inference(sat_conversion,[],[f202])).
% 0.88/0.43 cnf(s21, plain, ~spl24_25, inference(sat_conversion,[],[f212])).
% 0.88/0.43 cnf(s24, plain, ~spl24_2 | spl24_28, inference(sat_conversion,[],[f226])).
% 0.88/0.43 cnf(s25, plain, spl24_4, inference(sat_conversion,[],[f227])).
% 0.88/0.43 cnf(s28, plain, spl24_31, inference(sat_conversion,[],[f242])).
% 0.88/0.43 cnf(s31, plain, spl24_2, inference(sat_conversion,[],[f253])).
% 0.88/0.43 cnf(s33, plain, ~spl24_2 | spl24_35, inference(sat_conversion,[],[f262])).
% 0.88/0.43 cnf(s39, plain, ~spl24_2 | spl24_41, inference(sat_conversion,[],[f291])).
% 0.88/0.43 cnf(s41, plain, spl24_13, inference(sat_conversion,[],[f296])).
% 0.88/0.43 cnf(s42, plain, ~spl24_2 | spl24_43, inference(sat_conversion,[],[f300])).
% 0.88/0.43 cnf(s43, plain, ~spl24_13 | spl24_44, inference(sat_conversion,[],[f304])).
% 0.88/0.43 cnf(s44, plain, spl24_45, inference(sat_conversion,[],[f309])).
% 0.88/0.43 cnf(s45, plain, ~spl24_4 | spl24_46, inference(sat_conversion,[],[f313])).
% 0.88/0.43 cnf(s46, plain, spl24_9, inference(sat_conversion,[],[f314])).
% 0.88/0.43 cnf(s47, plain, ~spl24_5 | ~spl24_7 | ~spl24_17 | ~spl24_18 | ~spl24_19 | ~spl24_20 | spl24_25 | ~spl24_28 | ~spl24_31 | ~spl24_35 | ~spl24_41 | ~spl24_43 | ~spl24_45 | ~spl24_46 | ~spl24_47 | ~spl24_48, inference(sat_conversion,[],[f1077])).
% 0.88/0.43 cnf(s48, plain, ~spl24_44 | spl24_47 | ~spl24_49 | ~spl24_50, inference(sat_conversion,[],[f1101])).
% 0.88/0.43 cnf(s49, plain, ~spl24_23 | ~spl24_31 | spl24_49, inference(sat_conversion,[],[f1117])).
% 0.88/0.43 cnf(s50, plain, ~spl24_23 | ~spl24_45 | spl24_50, inference(sat_conversion,[],[f1121])).
% 0.88/0.43 cnf(s51, plain, ~spl24_23 | spl24_48 | ~spl24_51, inference(sat_conversion,[],[f1128])).
% 0.88/0.43 cnf(s52, plain, ~spl24_8 | ~spl24_31 | ~spl24_45 | spl24_51, inference(sat_conversion,[],[f1180])).
% 0.88/0.43 cnf(s53, plain, spl24_44, inference(rat,[],[s43,s41])).
% 0.88/0.44 cnf(s54, plain, spl24_43, inference(rat,[],[s42,s31])).
% 0.88/0.44 cnf(s55, plain, spl24_41, inference(rat,[],[s39,s31])).
% 0.88/0.44 cnf(s56, plain, spl24_35, inference(rat,[],[s33,s31])).
% 0.88/0.44 cnf(s57, plain, spl24_46, inference(rat,[],[s45,s25])).
% 0.88/0.44 cnf(s58, plain, spl24_28, inference(rat,[],[s24,s31])).
% 0.88/0.44 cnf(s59, plain, spl24_20, inference(rat,[],[s15,s31])).
% 0.88/0.44 cnf(s60, plain, spl24_19, inference(rat,[],[s14,s31])).
% 0.88/0.44 cnf(s61, plain, spl24_18, inference(rat,[],[s13,s31])).
% 0.88/0.44 cnf(s62, plain, spl24_17, inference(rat,[],[s12,s31])).
% 0.88/0.44 cnf(s63, plain, spl24_23, inference(rat,[],[s19,s11])).
% 0.88/0.44 cnf(s64, plain, spl24_50, inference(rat,[],[s50,s44,s63])).
% 0.88/0.44 cnf(s65, plain, spl24_49, inference(rat,[],[s49,s28,s63])).
% 0.88/0.44 cnf(s66, plain, spl24_47, inference(rat,[],[s48,s64,s53,s65])).
% 0.88/0.44 cnf(s67, plain, spl24_8, inference(rat,[],[s5,s46])).
% 0.88/0.44 cnf(s68, plain, spl24_51, inference(rat,[],[s52,s28,s44,s67])).
% 0.88/0.44 cnf(s69, plain, spl24_48, inference(rat,[],[s51,s63,s68])).
% 0.88/0.44 cnf(s70, plain, spl24_7, inference(rat,[],[s4,s31])).
% 0.88/0.44 cnf(s71, plain, ~spl24_5, inference(rat,[],[s47,s69,s66,s57,s44,s54,s55,s56,s28,s58,s21,s59,s60,s61,s62,s70])).
% 0.88/0.44 cnf(s72, plain, $false, inference(rat,[],[s3,s18,s71])).
% 0.88/0.44 thf(f1181,plain,(
% 0.88/0.44 $false),
% 0.88/0.44 inference(avatar_sat_refutation,[],[s72])).
% 0.88/0.44 % SZS output end Proof for theBenchmark
% 0.88/0.44 % (848567)------------------------------
% 0.88/0.44 % (848567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.44 % (848567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.44 % (848567)CaDiCaL version: 2.1.3
% 0.88/0.44 % (848567)Termination reason: Refutation
% 0.88/0.44 % (848567)Time elapsed: 0.169 s
% 0.88/0.44 % (848567)Peak memory usage: 14 MB
% 0.88/0.44 % (848567)Instructions burned: 393 (million)
% 0.88/0.44 % (848559)Success in time 0.194 s
% 0.88/0.44 % Vampire exiting
%------------------------------------------------------------------------------