% Mizar ND problem: t7_aff_4,aff_4,65,63 fof(dh_c1_7__aff_4,definition, ( ( ( ~ v3_struct_0(c1_7__aff_4) & ~ v3_realset2(c1_7__aff_4) & v1_diraf(c1_7__aff_4) & l1_analoaf(c1_7__aff_4) ) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,u1_struct_0(c1_7__aff_4)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(A,E) & r2_hidden(B,E) & r2_hidden(C,F) ) => ( ( ~ r4_aff_1(c1_7__aff_4,E,F) & ~ r4_aff_1(c1_7__aff_4,F,E) ) | A = B | ( ~ r2_analoaf(c1_7__aff_4,A,B,C,D) & ~ r2_analoaf(c1_7__aff_4,C,D,A,B) ) | r2_hidden(D,F) ) ) ) ) ) ) ) ) ) => ! [G] : ( ( ~ v3_struct_0(G) & ~ v3_realset2(G) & v1_diraf(G) & l1_analoaf(G) ) => ! [H] : ( m1_subset_1(H,u1_struct_0(G)) => ! [I] : ( m1_subset_1(I,u1_struct_0(G)) => ! [J] : ( m1_subset_1(J,u1_struct_0(G)) => ! [K] : ( m1_subset_1(K,u1_struct_0(G)) => ! [L] : ( m1_subset_1(L,k1_zfmisc_1(u1_struct_0(G))) => ! [M] : ( m1_subset_1(M,k1_zfmisc_1(u1_struct_0(G))) => ( ( r2_hidden(H,L) & r2_hidden(I,L) & r2_hidden(J,M) ) => ( ( ~ r4_aff_1(G,L,M) & ~ r4_aff_1(G,M,L) ) | H = I | ( ~ r2_analoaf(G,H,I,J,K) & ~ r2_analoaf(G,J,K,H,I) ) | r2_hidden(K,M) ) ) ) ) ) ) ) ) ) ), introduced(definition,[new_symbol(c1_7__aff_4),file(aff_4,c1_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c1_7__aff_4)]). fof(dh_c2_7__aff_4,definition, ( ( m1_subset_1(c2_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,D) & r2_hidden(A,D) & r2_hidden(B,E) ) => ( ( ~ r4_aff_1(c1_7__aff_4,D,E) & ~ r4_aff_1(c1_7__aff_4,E,D) ) | c2_7__aff_4 = A | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,A,B,C) & ~ r2_analoaf(c1_7__aff_4,B,C,c2_7__aff_4,A) ) | r2_hidden(C,E) ) ) ) ) ) ) ) ) => ! [F] : ( m1_subset_1(F,u1_struct_0(c1_7__aff_4)) => ! [G] : ( m1_subset_1(G,u1_struct_0(c1_7__aff_4)) => ! [H] : ( m1_subset_1(H,u1_struct_0(c1_7__aff_4)) => ! [I] : ( m1_subset_1(I,u1_struct_0(c1_7__aff_4)) => ! [J] : ( m1_subset_1(J,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [K] : ( m1_subset_1(K,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(F,J) & r2_hidden(G,J) & r2_hidden(H,K) ) => ( ( ~ r4_aff_1(c1_7__aff_4,J,K) & ~ r4_aff_1(c1_7__aff_4,K,J) ) | F = G | ( ~ r2_analoaf(c1_7__aff_4,F,G,H,I) & ~ r2_analoaf(c1_7__aff_4,H,I,F,G) ) | r2_hidden(I,K) ) ) ) ) ) ) ) ) ), introduced(definition,[new_symbol(c2_7__aff_4),file(aff_4,c2_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c2_7__aff_4)]). fof(dh_c3_7__aff_4,definition, ( ( m1_subset_1(c3_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,C) & r2_hidden(c3_7__aff_4,C) & r2_hidden(A,D) ) => ( ( ~ r4_aff_1(c1_7__aff_4,C,D) & ~ r4_aff_1(c1_7__aff_4,D,C) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,A,B) & ~ r2_analoaf(c1_7__aff_4,A,B,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(B,D) ) ) ) ) ) ) ) => ! [E] : ( m1_subset_1(E,u1_struct_0(c1_7__aff_4)) => ! [F] : ( m1_subset_1(F,u1_struct_0(c1_7__aff_4)) => ! [G] : ( m1_subset_1(G,u1_struct_0(c1_7__aff_4)) => ! [H] : ( m1_subset_1(H,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [I] : ( m1_subset_1(I,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,H) & r2_hidden(E,H) & r2_hidden(F,I) ) => ( ( ~ r4_aff_1(c1_7__aff_4,H,I) & ~ r4_aff_1(c1_7__aff_4,I,H) ) | c2_7__aff_4 = E | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,E,F,G) & ~ r2_analoaf(c1_7__aff_4,F,G,c2_7__aff_4,E) ) | r2_hidden(G,I) ) ) ) ) ) ) ) ), introduced(definition,[new_symbol(c3_7__aff_4),file(aff_4,c3_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c3_7__aff_4)]). fof(dh_c4_7__aff_4,definition, ( ( m1_subset_1(c4_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,B) & r2_hidden(c3_7__aff_4,B) & r2_hidden(c4_7__aff_4,C) ) => ( ( ~ r4_aff_1(c1_7__aff_4,B,C) & ~ r4_aff_1(c1_7__aff_4,C,B) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,A) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,A,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(A,C) ) ) ) ) ) ) => ! [D] : ( m1_subset_1(D,u1_struct_0(c1_7__aff_4)) => ! [E] : ( m1_subset_1(E,u1_struct_0(c1_7__aff_4)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,F) & r2_hidden(c3_7__aff_4,F) & r2_hidden(D,G) ) => ( ( ~ r4_aff_1(c1_7__aff_4,F,G) & ~ r4_aff_1(c1_7__aff_4,G,F) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,D,E) & ~ r2_analoaf(c1_7__aff_4,D,E,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(E,G) ) ) ) ) ) ) ), introduced(definition,[new_symbol(c4_7__aff_4),file(aff_4,c4_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c4_7__aff_4)]). fof(dh_c5_7__aff_4,definition, ( ( m1_subset_1(c5_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,A) & r2_hidden(c3_7__aff_4,A) & r2_hidden(c4_7__aff_4,B) ) => ( ( ~ r4_aff_1(c1_7__aff_4,A,B) & ~ r4_aff_1(c1_7__aff_4,B,A) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,B) ) ) ) ) ) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,D) & r2_hidden(c3_7__aff_4,D) & r2_hidden(c4_7__aff_4,E) ) => ( ( ~ r4_aff_1(c1_7__aff_4,D,E) & ~ r4_aff_1(c1_7__aff_4,E,D) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,C) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,C,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(C,E) ) ) ) ) ) ), introduced(definition,[new_symbol(c5_7__aff_4),file(aff_4,c5_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c5_7__aff_4)]). fof(dh_c6_7__aff_4,definition, ( ( m1_subset_1(c6_7__aff_4,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,A) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,A) & ~ r4_aff_1(c1_7__aff_4,A,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,A) ) ) ) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,B) & r2_hidden(c3_7__aff_4,B) & r2_hidden(c4_7__aff_4,C) ) => ( ( ~ r4_aff_1(c1_7__aff_4,B,C) & ~ r4_aff_1(c1_7__aff_4,C,B) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,C) ) ) ) ) ), introduced(definition,[new_symbol(c6_7__aff_4),file(aff_4,c6_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c6_7__aff_4)]). fof(dh_c7_7__aff_4,definition, ( ( m1_subset_1(c7_7__aff_4,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,c7_7__aff_4) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,c7_7__aff_4) & ~ r4_aff_1(c1_7__aff_4,c7_7__aff_4,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,c7_7__aff_4) ) ) ) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,A) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,A) & ~ r4_aff_1(c1_7__aff_4,A,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,A) ) ) ) ), introduced(definition,[new_symbol(c7_7__aff_4),file(aff_4,c7_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c7_7__aff_4)]). fof(e1_7__aff_4,assumption, ( ( r4_aff_1(c1_7__aff_4,c6_7__aff_4,c7_7__aff_4) | r4_aff_1(c1_7__aff_4,c7_7__aff_4,c6_7__aff_4) ) & c2_7__aff_4 != c3_7__aff_4 & ( r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) | r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) & r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,c7_7__aff_4) ), introduced(assumption,[file(aff_4,e1_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,e1_7__aff_4)]). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), [interesting(0.9),axiom,file(xboole_0,k1_xboole_0)]). fof(fc1_xboole_0,theorem,( v1_xboole_0(k1_xboole_0) ), file(xboole_0,fc1_xboole_0), [interesting(0.9),axiom,file(xboole_0,fc1_xboole_0)]). fof(reflexivity_r1_tarski,theorem,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), [interesting(0.9),axiom,file(tarski,r1_tarski)]). fof(existence_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), [interesting(0.9),axiom,file(struct_0,l1_struct_0)]). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), [interesting(0.9),axiom,file(struct_0,l1_struct_0)]). fof(fc1_struct_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ~ v1_xboole_0(u1_struct_0(A)) ) ), file(struct_0,fc1_struct_0), [interesting(0.9),axiom,file(struct_0,fc1_struct_0)]). fof(rc1_xboole_0,theorem,( ? [A] : v1_xboole_0(A) ), file(xboole_0,rc1_xboole_0), [interesting(0.9),axiom,file(xboole_0,rc1_xboole_0)]). fof(rc2_xboole_0,theorem,( ? [A] : ~ v1_xboole_0(A) ), file(xboole_0,rc2_xboole_0), [interesting(0.9),axiom,file(xboole_0,rc2_xboole_0)]). fof(rc3_struct_0,theorem,( ? [A] : ( l1_struct_0(A) & ~ v3_struct_0(A) ) ), file(struct_0,rc3_struct_0), [interesting(0.9),axiom,file(struct_0,rc3_struct_0)]). fof(rc5_struct_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & l1_struct_0(A) ) => ? [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & ~ v1_xboole_0(B) ) ) ), file(struct_0,rc5_struct_0), [interesting(0.9),axiom,file(struct_0,rc5_struct_0)]). fof(t2_subset,theorem,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), [interesting(0.9),axiom,file(subset,t2_subset)]). fof(t5_subset,theorem,( ! [A,B,C] : ~ ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) & v1_xboole_0(C) ) ), file(subset,t5_subset), [interesting(0.9),axiom,file(subset,t5_subset)]). fof(t6_boole,theorem,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), [interesting(0.9),axiom,file(boole,t6_boole)]). fof(t8_boole,theorem,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), [interesting(0.9),axiom,file(boole,t8_boole)]). fof(antisymmetry_r2_hidden,theorem,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), [interesting(0.9),axiom,file(hidden,r2_hidden)]). fof(symmetry_r4_aff_1,theorem,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( r4_aff_1(A,B,C) => r4_aff_1(A,C,B) ) ) ), file(aff_1,r4_aff_1), [interesting(0.9),axiom,file(aff_1,r4_aff_1)]). fof(existence_l1_analoaf,axiom,( ? [A] : l1_analoaf(A) ), file(analoaf,l1_analoaf), [interesting(0.9),axiom,file(analoaf,l1_analoaf)]). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(redefinition_r4_aff_1,definition,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( r4_aff_1(A,B,C) <=> r3_aff_1(A,B,C) ) ) ), file(aff_1,r4_aff_1), [interesting(0.9),axiom,file(aff_1,r4_aff_1)]). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), [interesting(0.9),axiom,file(zfmisc_1,k1_zfmisc_1)]). fof(dt_l1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => l1_struct_0(A) ) ), file(analoaf,l1_analoaf), [interesting(0.9),axiom,file(analoaf,l1_analoaf)]). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), [interesting(0.9),axiom,file(subset_1,m1_subset_1)]). fof(dt_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), [interesting(0.9),axiom,file(struct_0,u1_struct_0)]). fof(dt_c1_7__aff_4,assumption, ( ~ v3_struct_0(c1_7__aff_4) & ~ v3_realset2(c1_7__aff_4) & v1_diraf(c1_7__aff_4) & l1_analoaf(c1_7__aff_4) ), introduced(assumption,[file(aff_4,c1_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c1_7__aff_4)]). fof(dt_c2_7__aff_4,assumption,( m1_subset_1(c2_7__aff_4,u1_struct_0(c1_7__aff_4)) ), introduced(assumption,[file(aff_4,c2_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c2_7__aff_4)]). fof(dt_c3_7__aff_4,assumption,( m1_subset_1(c3_7__aff_4,u1_struct_0(c1_7__aff_4)) ), introduced(assumption,[file(aff_4,c3_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c3_7__aff_4)]). fof(dt_c4_7__aff_4,assumption,( m1_subset_1(c4_7__aff_4,u1_struct_0(c1_7__aff_4)) ), introduced(assumption,[file(aff_4,c4_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c4_7__aff_4)]). fof(dt_c5_7__aff_4,assumption,( m1_subset_1(c5_7__aff_4,u1_struct_0(c1_7__aff_4)) ), introduced(assumption,[file(aff_4,c5_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c5_7__aff_4)]). fof(dt_c6_7__aff_4,assumption,( m1_subset_1(c6_7__aff_4,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) ), introduced(assumption,[file(aff_4,c6_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c6_7__aff_4)]). fof(dt_c7_7__aff_4,assumption,( m1_subset_1(c7_7__aff_4,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) ), introduced(assumption,[file(aff_4,c7_7__aff_4)]), [interesting(0.8),axiom,file(aff_4,c7_7__aff_4)]). fof(t1_subset,theorem,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), [interesting(0.9),axiom,file(subset,t1_subset)]). fof(t3_subset,theorem,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), [interesting(0.9),axiom,file(subset,t3_subset)]). fof(t4_subset,theorem,( ! [A,B,C] : ( ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) ) => m1_subset_1(A,C) ) ), file(subset,t4_subset), [interesting(0.9),axiom,file(subset,t4_subset)]). fof(t7_boole,theorem,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), [interesting(0.9),axiom,file(boole,t7_boole)]). fof(t50_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r3_aff_1(A,B,C) => ( v1_aff_1(B,A) & v1_aff_1(C,A) ) ) ) ) ) ), file(aff_1,t50_aff_1), [interesting(0.9),axiom,file(aff_1,t50_aff_1)]). fof(e2_7__aff_4,plain, ( v1_aff_1(c6_7__aff_4,c1_7__aff_4) & v1_aff_1(c7_7__aff_4,c1_7__aff_4) ), inference(mizar_by,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,e1_7__aff_4])],[dt_k1_xboole_0,fc1_xboole_0,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,fc1_struct_0,rc1_xboole_0,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t6_boole,t8_boole,antisymmetry_r2_hidden,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,t1_subset,t3_subset,t4_subset,t7_boole,e1_7__aff_4,t50_aff_1]), [interesting(0.8),file(aff_4,e2_7__aff_4),[file(aff_4,e2_7__aff_4)]]). fof(t66_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(D,A) & r2_hidden(B,D) & r2_hidden(C,D) ) => r2_aff_1(A,B,C,D) ) ) ) ) ) ), file(aff_1,t66_aff_1), [interesting(0.9),axiom,file(aff_1,t66_aff_1)]). fof(e3_7__aff_4,plain,( r2_aff_1(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c6_7__aff_4) ), inference(mizar_by,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,e1_7__aff_4])],[dt_k1_xboole_0,fc1_xboole_0,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,fc1_struct_0,rc1_xboole_0,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t6_boole,t8_boole,antisymmetry_r2_hidden,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,t1_subset,t3_subset,t4_subset,t7_boole,e2_7__aff_4,e1_7__aff_4,t66_aff_1]), [interesting(0.8),file(aff_4,e3_7__aff_4),[file(aff_4,e3_7__aff_4)]]). fof(t4_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ~ ( ( r2_aff_1(A,B,C,F) | r2_aff_1(A,C,B,F) ) & ( r2_analoaf(A,B,C,D,E) | r2_analoaf(A,D,E,B,C) ) & B != C & ~ ( r2_aff_1(A,D,E,F) & r2_aff_1(A,E,D,F) ) ) ) ) ) ) ) ) ), file(aff_4,t4_aff_4), [interesting(0.9),axiom,file(aff_4,t4_aff_4)]). fof(e4_7__aff_4,plain,( r2_aff_1(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c6_7__aff_4) ), inference(mizar_by,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,e1_7__aff_4])],[dt_k1_xboole_0,fc1_xboole_0,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,fc1_struct_0,rc1_xboole_0,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t6_boole,t8_boole,antisymmetry_r2_hidden,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,t1_subset,t3_subset,t4_subset,t7_boole,e3_7__aff_4,e1_7__aff_4,t4_aff_4]), [interesting(0.8),file(aff_4,e4_7__aff_4),[file(aff_4,e4_7__aff_4)]]). fof(t3_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ~ ( ( r2_aff_1(A,B,C,D) | r2_aff_1(A,C,B,D) ) & ( r4_aff_1(A,D,E) | r4_aff_1(A,E,D) ) & ~ ( r2_aff_1(A,B,C,E) & r2_aff_1(A,C,B,E) ) ) ) ) ) ) ) ), file(aff_4,t3_aff_4), [interesting(0.9),axiom,file(aff_4,t3_aff_4)]). fof(e5_7__aff_4,plain,( r2_aff_1(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c7_7__aff_4) ), inference(mizar_by,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,e1_7__aff_4])],[dt_k1_xboole_0,fc1_xboole_0,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,fc1_struct_0,rc1_xboole_0,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t6_boole,t8_boole,antisymmetry_r2_hidden,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,t1_subset,t3_subset,t4_subset,t7_boole,e4_7__aff_4,e1_7__aff_4,t3_aff_4]), [interesting(0.8),file(aff_4,e5_7__aff_4),[file(aff_4,e5_7__aff_4)]]). fof(t2_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( r2_hidden(B,D) => ( ( ~ r2_aff_1(A,B,C,D) & ~ r2_aff_1(A,C,B,D) ) | r2_hidden(C,D) ) ) ) ) ) ) ), file(aff_4,t2_aff_4), [interesting(0.9),axiom,file(aff_4,t2_aff_4)]). fof(e6_7__aff_4,plain,( r2_hidden(c5_7__aff_4,c7_7__aff_4) ), inference(mizar_by,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,e1_7__aff_4])],[dt_k1_xboole_0,fc1_xboole_0,reflexivity_r1_tarski,existence_l1_struct_0,dt_l1_struct_0,fc1_struct_0,rc1_xboole_0,rc2_xboole_0,rc3_struct_0,rc5_struct_0,t2_subset,t5_subset,t6_boole,t8_boole,antisymmetry_r2_hidden,symmetry_r4_aff_1,existence_l1_analoaf,existence_m1_subset_1,redefinition_r4_aff_1,dt_k1_zfmisc_1,dt_l1_analoaf,dt_m1_subset_1,dt_u1_struct_0,dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,t1_subset,t3_subset,t4_subset,t7_boole,e5_7__aff_4,e1_7__aff_4,t2_aff_4]), [interesting(0.8),file(aff_4,e6_7__aff_4),[file(aff_4,e6_7__aff_4)]]). fof(i9_7__aff_4,theorem,( $true ), introduced(tautology,[file(aff_4,i9_7__aff_4)]), [interesting(0.8),trivial,file(aff_4,i9_7__aff_4)]). fof(i8_7__aff_4,plain,( r2_hidden(c5_7__aff_4,c7_7__aff_4) ), inference(conclusion,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4,e1_7__aff_4])],[e6_7__aff_4,i9_7__aff_4]), [interesting(0.8),file(aff_4,i8_7__aff_4),[file(aff_4,i8_7__aff_4)]]). fof(i7_7__aff_4,plain, ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,c7_7__aff_4) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,c7_7__aff_4) & ~ r4_aff_1(c1_7__aff_4,c7_7__aff_4,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,c7_7__aff_4) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4,dt_c7_7__aff_4]),discharge_asm(discharge,[e1_7__aff_4])],[e1_7__aff_4,i8_7__aff_4]), [interesting(0.8),file(aff_4,i7_7__aff_4),[file(aff_4,i7_7__aff_4)]]). fof(i7_7_tmp__aff_4,plain, ( m1_subset_1(c7_7__aff_4,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,c7_7__aff_4) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,c7_7__aff_4) & ~ r4_aff_1(c1_7__aff_4,c7_7__aff_4,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,c7_7__aff_4) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4]),discharge_asm(discharge,[dt_c7_7__aff_4])],[dt_c7_7__aff_4,i7_7__aff_4]), [interesting(0.8),i6_7__aff_4]). fof(i6_7__aff_4,plain,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,A) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,A) & ~ r4_aff_1(c1_7__aff_4,A,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,A) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4,dt_c6_7__aff_4])],[i7_7_tmp__aff_4,dh_c7_7__aff_4]), [interesting(0.8),file(aff_4,i6_7__aff_4),[file(aff_4,i6_7__aff_4)]]). fof(i6_7_tmp__aff_4,plain, ( m1_subset_1(c6_7__aff_4,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,c6_7__aff_4) & r2_hidden(c3_7__aff_4,c6_7__aff_4) & r2_hidden(c4_7__aff_4,A) ) => ( ( ~ r4_aff_1(c1_7__aff_4,c6_7__aff_4,A) & ~ r4_aff_1(c1_7__aff_4,A,c6_7__aff_4) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,A) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4]),discharge_asm(discharge,[dt_c6_7__aff_4])],[dt_c6_7__aff_4,i6_7__aff_4]), [interesting(0.8),i5_7__aff_4]). fof(i5_7__aff_4,plain,( ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,A) & r2_hidden(c3_7__aff_4,A) & r2_hidden(c4_7__aff_4,B) ) => ( ( ~ r4_aff_1(c1_7__aff_4,A,B) & ~ r4_aff_1(c1_7__aff_4,B,A) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,B) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4,dt_c5_7__aff_4])],[i6_7_tmp__aff_4,dh_c6_7__aff_4]), [interesting(0.8),file(aff_4,i5_7__aff_4),[file(aff_4,i5_7__aff_4)]]). fof(i5_7_tmp__aff_4,plain, ( m1_subset_1(c5_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,A) & r2_hidden(c3_7__aff_4,A) & r2_hidden(c4_7__aff_4,B) ) => ( ( ~ r4_aff_1(c1_7__aff_4,A,B) & ~ r4_aff_1(c1_7__aff_4,B,A) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,c5_7__aff_4) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,c5_7__aff_4,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(c5_7__aff_4,B) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4]),discharge_asm(discharge,[dt_c5_7__aff_4])],[dt_c5_7__aff_4,i5_7__aff_4]), [interesting(0.8),i4_7__aff_4]). fof(i4_7__aff_4,plain,( ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,B) & r2_hidden(c3_7__aff_4,B) & r2_hidden(c4_7__aff_4,C) ) => ( ( ~ r4_aff_1(c1_7__aff_4,B,C) & ~ r4_aff_1(c1_7__aff_4,C,B) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,A) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,A,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(A,C) ) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4,dt_c4_7__aff_4])],[i5_7_tmp__aff_4,dh_c5_7__aff_4]), [interesting(0.8),file(aff_4,i4_7__aff_4),[file(aff_4,i4_7__aff_4)]]). fof(i4_7_tmp__aff_4,plain, ( m1_subset_1(c4_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,B) & r2_hidden(c3_7__aff_4,B) & r2_hidden(c4_7__aff_4,C) ) => ( ( ~ r4_aff_1(c1_7__aff_4,B,C) & ~ r4_aff_1(c1_7__aff_4,C,B) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,c4_7__aff_4,A) & ~ r2_analoaf(c1_7__aff_4,c4_7__aff_4,A,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(A,C) ) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4]),discharge_asm(discharge,[dt_c4_7__aff_4])],[dt_c4_7__aff_4,i4_7__aff_4]), [interesting(0.8),i3_7__aff_4]). fof(i3_7__aff_4,plain,( ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,C) & r2_hidden(c3_7__aff_4,C) & r2_hidden(A,D) ) => ( ( ~ r4_aff_1(c1_7__aff_4,C,D) & ~ r4_aff_1(c1_7__aff_4,D,C) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,A,B) & ~ r2_analoaf(c1_7__aff_4,A,B,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(B,D) ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4,dt_c3_7__aff_4])],[i4_7_tmp__aff_4,dh_c4_7__aff_4]), [interesting(0.8),file(aff_4,i3_7__aff_4),[file(aff_4,i3_7__aff_4)]]). fof(i3_7_tmp__aff_4,plain, ( m1_subset_1(c3_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,C) & r2_hidden(c3_7__aff_4,C) & r2_hidden(A,D) ) => ( ( ~ r4_aff_1(c1_7__aff_4,C,D) & ~ r4_aff_1(c1_7__aff_4,D,C) ) | c2_7__aff_4 = c3_7__aff_4 | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,c3_7__aff_4,A,B) & ~ r2_analoaf(c1_7__aff_4,A,B,c2_7__aff_4,c3_7__aff_4) ) | r2_hidden(B,D) ) ) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4]),discharge_asm(discharge,[dt_c3_7__aff_4])],[dt_c3_7__aff_4,i3_7__aff_4]), [interesting(0.8),i2_7__aff_4]). fof(i2_7__aff_4,plain,( ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,D) & r2_hidden(A,D) & r2_hidden(B,E) ) => ( ( ~ r4_aff_1(c1_7__aff_4,D,E) & ~ r4_aff_1(c1_7__aff_4,E,D) ) | c2_7__aff_4 = A | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,A,B,C) & ~ r2_analoaf(c1_7__aff_4,B,C,c2_7__aff_4,A) ) | r2_hidden(C,E) ) ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_7__aff_4,dt_c2_7__aff_4])],[i3_7_tmp__aff_4,dh_c3_7__aff_4]), [interesting(0.8),file(aff_4,i2_7__aff_4),[file(aff_4,i2_7__aff_4)]]). fof(i2_7_tmp__aff_4,plain, ( m1_subset_1(c2_7__aff_4,u1_struct_0(c1_7__aff_4)) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(c2_7__aff_4,D) & r2_hidden(A,D) & r2_hidden(B,E) ) => ( ( ~ r4_aff_1(c1_7__aff_4,D,E) & ~ r4_aff_1(c1_7__aff_4,E,D) ) | c2_7__aff_4 = A | ( ~ r2_analoaf(c1_7__aff_4,c2_7__aff_4,A,B,C) & ~ r2_analoaf(c1_7__aff_4,B,C,c2_7__aff_4,A) ) | r2_hidden(C,E) ) ) ) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([dt_c1_7__aff_4]),discharge_asm(discharge,[dt_c2_7__aff_4])],[dt_c2_7__aff_4,i2_7__aff_4]), [interesting(0.8),i1_7__aff_4]). fof(i1_7__aff_4,plain,( ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,u1_struct_0(c1_7__aff_4)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(A,E) & r2_hidden(B,E) & r2_hidden(C,F) ) => ( ( ~ r4_aff_1(c1_7__aff_4,E,F) & ~ r4_aff_1(c1_7__aff_4,F,E) ) | A = B | ( ~ r2_analoaf(c1_7__aff_4,A,B,C,D) & ~ r2_analoaf(c1_7__aff_4,C,D,A,B) ) | r2_hidden(D,F) ) ) ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([dt_c1_7__aff_4])],[i2_7_tmp__aff_4,dh_c2_7__aff_4]), [interesting(0.8),file(aff_4,i1_7__aff_4),[file(aff_4,i1_7__aff_4)]]). fof(i1_7_tmp__aff_4,plain, ( ( ~ v3_struct_0(c1_7__aff_4) & ~ v3_realset2(c1_7__aff_4) & v1_diraf(c1_7__aff_4) & l1_analoaf(c1_7__aff_4) ) => ! [A] : ( m1_subset_1(A,u1_struct_0(c1_7__aff_4)) => ! [B] : ( m1_subset_1(B,u1_struct_0(c1_7__aff_4)) => ! [C] : ( m1_subset_1(C,u1_struct_0(c1_7__aff_4)) => ! [D] : ( m1_subset_1(D,u1_struct_0(c1_7__aff_4)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(c1_7__aff_4))) => ( ( r2_hidden(A,E) & r2_hidden(B,E) & r2_hidden(C,F) ) => ( ( ~ r4_aff_1(c1_7__aff_4,E,F) & ~ r4_aff_1(c1_7__aff_4,F,E) ) | A = B | ( ~ r2_analoaf(c1_7__aff_4,A,B,C,D) & ~ r2_analoaf(c1_7__aff_4,C,D,A,B) ) | r2_hidden(D,F) ) ) ) ) ) ) ) ) ), inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_7__aff_4])],[dt_c1_7__aff_4,i1_7__aff_4]), [interesting(1),t7_aff_4]). fof(t7_aff_4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,G) ) => ( ( ~ r4_aff_1(A,F,G) & ~ r4_aff_1(A,G,F) ) | B = C | ( ~ r2_analoaf(A,B,C,D,E) & ~ r2_analoaf(A,D,E,B,C) ) | r2_hidden(E,G) ) ) ) ) ) ) ) ) ) ), inference(let,[status(thm),assumptions([])],[i1_7_tmp__aff_4,dh_c1_7__aff_4]), [interesting(1),file(aff_4,t7_aff_4),[file(aff_4,t7_aff_4)]]).