%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : NUM635^4 : TPTP v9.2.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Oct 9 02:11:33 PM UTC 2025 % Result : Theorem 25.90s 25.97s % Output : Proof 25.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : NUM635^4 : TPTP v9.2.0. Released v7.1.0. % 0.12/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.13/0.35 % Computer : n014.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Oct 8 22:15:38 EDT 2025 % 0.13/0.35 % CPUTime : % 25.90/25.97 % SZS status Theorem % 25.90/25.97 % Mode: mode94:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=3.:SINE_DEPTH=0 % 25.90/25.97 % Inferences: 5 % 25.90/25.97 % SZS output start Proof % 25.90/25.97 thf(ty_univof, type, univof : ($i>$i)). % 25.90/25.97 thf(ty_power, type, power : ($i>$i)). % 25.90/25.97 thf(ty_eps, type, eps : (($i>$o)>$i)). % 25.90/25.97 thf(ty_union, type, union : ($i>$i)). % 25.90/25.97 thf(ty_eigen__1, type, eigen__1 : $i). % 25.90/25.97 thf(ty_eigen__0, type, eigen__0 : $i). % 25.90/25.97 thf(ty_emptyset, type, emptyset : $i). % 25.90/25.97 thf(ty_repl, type, repl : ($i>($i>$i)>$i)). % 25.90/25.97 thf(ty_in, type, in : ($i>$i>$o)). % 25.90/25.97 thf(sP1,plain,sP1 <=> ((in @ eigen__1) @ (eps @ (^[X1:$i]:(((~((![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) => (X2 = emptyset))))) => (~((X1 = ((repl @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (univof @ emptyset)) => (~((![X4:$i>$o]:((X4 @ emptyset) => ((![X5:$i]:((X4 @ X5) => (X4 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X6:$i]:(eps @ (^[X7:$i]:((((in @ emptyset) @ X6) => (~((X7 = X5)))) => (~(((~(((in @ emptyset) @ X6))) => (~((X7 = ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X5)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = X5)))))))))))))))))))))))))) => (X4 @ X3)))))))))) => (~((X2 = ((repl @ (univof @ emptyset)) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X3)))) => (~((X4 = X3)))) => (~(((~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X3)))))) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (univof @ emptyset)) => (~((![X4:$i>$o]:((X4 @ emptyset) => ((![X5:$i]:((X4 @ X5) => (X4 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X6:$i]:(eps @ (^[X7:$i]:((((in @ emptyset) @ X6) => (~((X7 = X5)))) => (~(((~(((in @ emptyset) @ X6))) => (~((X7 = ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X5)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = X5)))))))))))))))))))))))))) => (X4 @ X3)))))))) => (~((X2 = emptyset)))))))))) @ (^[X2:$i]:(eps @ (^[X3:$i]:(((~((X2 = emptyset))) => (~((X3 = X2)))) => (~(((X2 = emptyset) => (~((X3 = (eps @ (^[X4:$i]:(~((((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))))))))))))))))))))) => (~(((![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) => (X2 = emptyset))) => (~((X1 = emptyset)))))))))),introduced(definition,[new_symbols(definition,[sP1])])). % 25.90/25.97 thf(sP2,plain,sP2 <=> ((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X1:$i]:(eps @ (^[X2:$i]:((((in @ emptyset) @ X1) => (~((X2 = eigen__0)))) => (~(((~(((in @ emptyset) @ X1))) => (~((X2 = ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = eigen__0)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = eigen__0))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X1:$i]:(eps @ (^[X2:$i]:((((in @ emptyset) @ X1) => (~((X2 = eigen__1)))) => (~(((~(((in @ emptyset) @ X1))) => (~((X2 = ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = eigen__1)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = eigen__1)))))))))))))))))))))))),introduced(definition,[new_symbols(definition,[sP2])])). % 25.90/25.97 thf(sP3,plain,sP3 <=> (sP1 => (sP2 => (eigen__0 = eigen__1))),introduced(definition,[new_symbols(definition,[sP3])])). % 25.90/25.97 thf(sP4,plain,sP4 <=> (eigen__0 = eigen__1),introduced(definition,[new_symbols(definition,[sP4])])). % 25.90/25.97 thf(sP5,plain,sP5 <=> (![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((X3 = emptyset) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))) => (~((X6 = emptyset)))))))))) => (X5 = emptyset))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))) => (~((X2 = emptyset)))))))))) => (![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))))) => (~((X3 = ((repl @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((~((X4 = emptyset))) => (~((X5 = X4)))) => (~(((X4 = emptyset) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (eps @ (^[X7:$i]:(((~((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))) => (~((X7 = ((repl @ (univof @ emptyset)) @ (^[X8:$i]:(eps @ (^[X9:$i]:(((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))) => (~((X9 = X8)))) => (~(((~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))))) => (~((X9 = (eps @ (^[X10:$i]:(~((((in @ X10) @ (univof @ emptyset)) => (~((![X11:$i>$o]:((X11 @ emptyset) => ((![X12:$i]:((X11 @ X12) => (X11 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X12)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = ((repl @ (power @ (power @ emptyset))) @ (^[X15:$i]:(eps @ (^[X16:$i]:((((in @ emptyset) @ X15) => (~((X16 = X12)))) => (~(((~(((in @ emptyset) @ X15))) => (~((X16 = X12)))))))))))))))))))))))))) => (X11 @ X10)))))))))))))))))))))))))) => (~(((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))) => (~((X7 = emptyset)))))))))) => (X6 = emptyset))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))) => (~((X3 = emptyset)))))))))) => (((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X1)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X1)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X1))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X2)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X2)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X2)))))))))))))))))))))))) => (X1 = X2)))))),introduced(definition,[new_symbols(definition,[sP5])])). % 25.90/25.97 thf(sP6,plain,sP6 <=> (((in @ eigen__0) @ (eps @ (^[X1:$i]:(((~((![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) => (X2 = emptyset))))) => (~((X1 = ((repl @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (univof @ emptyset)) => (~((![X4:$i>$o]:((X4 @ emptyset) => ((![X5:$i]:((X4 @ X5) => (X4 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X6:$i]:(eps @ (^[X7:$i]:((((in @ emptyset) @ X6) => (~((X7 = X5)))) => (~(((~(((in @ emptyset) @ X6))) => (~((X7 = ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X5)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = X5)))))))))))))))))))))))))) => (X4 @ X3)))))))))) => (~((X2 = ((repl @ (univof @ emptyset)) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X3)))) => (~((X4 = X3)))) => (~(((~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X3)))))) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (univof @ emptyset)) => (~((![X4:$i>$o]:((X4 @ emptyset) => ((![X5:$i]:((X4 @ X5) => (X4 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X6:$i]:(eps @ (^[X7:$i]:((((in @ emptyset) @ X6) => (~((X7 = X5)))) => (~(((~(((in @ emptyset) @ X6))) => (~((X7 = ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X5)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = X5)))))))))))))))))))))))))) => (X4 @ X3)))))))) => (~((X2 = emptyset)))))))))) @ (^[X2:$i]:(eps @ (^[X3:$i]:(((~((X2 = emptyset))) => (~((X3 = X2)))) => (~(((X2 = emptyset) => (~((X3 = (eps @ (^[X4:$i]:(~((((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))))))))))))))))))))) => (~(((![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) => (X2 = emptyset))) => (~((X1 = emptyset)))))))))) => (![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((X3 = emptyset) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))) => (~((X6 = emptyset)))))))))) => (X5 = emptyset))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))) => (~((X2 = emptyset)))))))))) => (((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = eigen__0)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = eigen__0)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = eigen__0))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = X1)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = X1)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = X1)))))))))))))))))))))))) => (eigen__0 = X1))))),introduced(definition,[new_symbols(definition,[sP6])])). % 25.90/25.97 thf(sP7,plain,sP7 <=> ((in @ eigen__0) @ (eps @ (^[X1:$i]:(((~((![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) => (X2 = emptyset))))) => (~((X1 = ((repl @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (univof @ emptyset)) => (~((![X4:$i>$o]:((X4 @ emptyset) => ((![X5:$i]:((X4 @ X5) => (X4 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X6:$i]:(eps @ (^[X7:$i]:((((in @ emptyset) @ X6) => (~((X7 = X5)))) => (~(((~(((in @ emptyset) @ X6))) => (~((X7 = ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X5)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = X5)))))))))))))))))))))))))) => (X4 @ X3)))))))))) => (~((X2 = ((repl @ (univof @ emptyset)) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X3)))) => (~((X4 = X3)))) => (~(((~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X3)))))) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (univof @ emptyset)) => (~((![X4:$i>$o]:((X4 @ emptyset) => ((![X5:$i]:((X4 @ X5) => (X4 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X6:$i]:(eps @ (^[X7:$i]:((((in @ emptyset) @ X6) => (~((X7 = X5)))) => (~(((~(((in @ emptyset) @ X6))) => (~((X7 = ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X5)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = X5)))))))))))))))))))))))))) => (X4 @ X3)))))))) => (~((X2 = emptyset)))))))))) @ (^[X2:$i]:(eps @ (^[X3:$i]:(((~((X2 = emptyset))) => (~((X3 = X2)))) => (~(((X2 = emptyset) => (~((X3 = (eps @ (^[X4:$i]:(~((((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))))))))))))))))))))) => (~(((![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) => (X2 = emptyset))) => (~((X1 = emptyset)))))))))),introduced(definition,[new_symbols(definition,[sP7])])). % 25.96/25.98 thf(sP8,plain,sP8 <=> (sP2 => sP4),introduced(definition,[new_symbols(definition,[sP8])])). % 25.96/25.98 thf(sP9,plain,sP9 <=> (![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((X3 = emptyset) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))) => (~((X6 = emptyset)))))))))) => (X5 = emptyset))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))) => (~((X2 = emptyset)))))))))) => (((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = eigen__0)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = eigen__0)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = eigen__0))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = X1)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = X1)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = X1)))))))))))))))))))))))) => (eigen__0 = X1)))),introduced(definition,[new_symbols(definition,[sP9])])). % 25.96/25.98 thf(def_is_of,definition,(is_of = (^[X1:$i]:(^[X2:$i>$o]:(X2 @ X1))))). % 25.96/25.98 thf(def_all_of,definition,(all_of = (^[X1:$i>$o]:(^[X2:$i>$o]:(![X3:$i]:(((is_of @ X3) @ X1) => (X2 @ X3))))))). % 25.96/25.98 thf(def_if,definition,(if = (^[X1:$o]:(^[X2:$i]:(^[X3:$i]:(eps @ (^[X4:$i]:((X1 => (~((X4 = X2)))) => (~(((~(X1)) => (~((X4 = X3)))))))))))))). % 25.96/25.98 thf(def_d_UPair,definition,(d_UPair = (^[X1:$i]:(^[X2:$i]:((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(((if @ ((in @ emptyset) @ X3)) @ X1) @ X2))))))). % 25.96/25.98 thf(def_d_Sing,definition,(d_Sing = (^[X1:$i]:((d_UPair @ X1) @ X1)))). % 25.96/25.98 thf(def_binunion,definition,(binunion = (^[X1:$i]:(^[X2:$i]:(union @ ((d_UPair @ X1) @ X2)))))). % 25.96/25.98 thf(def_d_Sep,definition,(d_Sep = (^[X1:$i]:(^[X2:$i>$o]:(((if @ (~((![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3)))))))) @ ((repl @ X1) @ (^[X3:$i]:(((if @ (X2 @ X3)) @ X3) @ (eps @ (^[X4:$i]:(~((((in @ X4) @ X1) => (~((X2 @ X4)))))))))))) @ emptyset))))). % 25.96/25.98 thf(def_ordsucc,definition,(ordsucc = (^[X1:$i]:((binunion @ X1) @ (d_Sing @ X1))))). % 25.96/25.98 thf(def_nat_p,definition,(nat_p = (^[X1:$i]:(![X2:$i>$o]:((X2 @ emptyset) => ((![X3:$i]:((X2 @ X3) => (X2 @ (ordsucc @ X3)))) => (X2 @ X1))))))). % 25.96/25.98 thf(def_omega,definition,(omega = ((d_Sep @ (univof @ emptyset)) @ nat_p))). % 25.96/25.98 thf(def_imp,definition,(imp = (^[X1:$o]:(^[X2:$o]:(X1 => X2))))). % 25.96/25.98 thf(def_d_not,definition,(d_not = (^[X1:$o]:((imp @ X1) @ $false)))). % 25.96/25.98 thf(def_e_is,definition,(e_is = (^[X1:$i]:(=)))). % 25.96/25.98 thf(def_e_in,definition,(e_in = (^[X1:$i]:(^[X2:$i>$o]:(^[X3:$i]:X3))))). % 25.96/25.98 thf(def_nat,definition,(nat = ((d_Sep @ omega) @ (^[X1:$i]:(~((X1 = emptyset))))))). % 25.96/25.98 thf(def_n_is,definition,(n_is = (e_is @ nat))). % 25.96/25.98 thf(def_nis,definition,(nis = (^[X1:$i]:(^[X2:$i]:(d_not @ ((n_is @ X1) @ X2)))))). % 25.96/25.98 thf(def_n_1,definition,(n_1 = (ordsucc @ emptyset))). % 25.96/25.98 thf(satz1,conjecture,(![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((~((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))) => (~((X4 = emptyset)))))))))) => (~((~((X3 = emptyset))))))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((~((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((~((~((X3 = emptyset))))) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((~((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))) => (~((X6 = emptyset)))))))))) => (~((~((X5 = emptyset))))))))))))))))))))))))) => (~(((~((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((~((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))) => (~((X4 = emptyset)))))))))) => (~((~((X3 = emptyset))))))))))) => (~((X2 = emptyset)))))))))) => (![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((~((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))) => (~((X5 = emptyset)))))))))) => (~((~((X4 = emptyset))))))))) => (~((X3 = ((repl @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((~((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))) => (~((X4 = emptyset)))))))))) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((~((X4 = emptyset))) => (~((X5 = X4)))) => (~(((~((~((X4 = emptyset))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (eps @ (^[X7:$i]:(((~((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))) => (~((X7 = ((repl @ (univof @ emptyset)) @ (^[X8:$i]:(eps @ (^[X9:$i]:(((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))) => (~((X9 = X8)))) => (~(((~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))))) => (~((X9 = (eps @ (^[X10:$i]:(~((((in @ X10) @ (univof @ emptyset)) => (~((![X11:$i>$o]:((X11 @ emptyset) => ((![X12:$i]:((X11 @ X12) => (X11 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X12)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = ((repl @ (power @ (power @ emptyset))) @ (^[X15:$i]:(eps @ (^[X16:$i]:((((in @ emptyset) @ X15) => (~((X16 = X12)))) => (~(((~(((in @ emptyset) @ X15))) => (~((X16 = X12)))))))))))))))))))))))))) => (X11 @ X10)))))))))))))))))))))))))) => (~(((~((~((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))) => (~((X7 = emptyset)))))))))) => (~((~((X6 = emptyset))))))))))))))))))))))))) => (~(((~((~((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((~((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))) => (~((X5 = emptyset)))))))))) => (~((~((X4 = emptyset))))))))))) => (~((X3 = emptyset)))))))))) => ((~((X1 = X2))) => (~(((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X1)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X1)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X1))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X2)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X2)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X2)))))))))))))))))))))))))))))))). % 25.96/25.98 thf(h0,negated_conjecture,(~((![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((X3 = emptyset) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))) => (~((X6 = emptyset)))))))))) => (X5 = emptyset))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))) => (~((X2 = emptyset)))))))))) => (![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))))) => (~((X3 = ((repl @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((~((X4 = emptyset))) => (~((X5 = X4)))) => (~(((X4 = emptyset) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (eps @ (^[X7:$i]:(((~((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))) => (~((X7 = ((repl @ (univof @ emptyset)) @ (^[X8:$i]:(eps @ (^[X9:$i]:(((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))) => (~((X9 = X8)))) => (~(((~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))))) => (~((X9 = (eps @ (^[X10:$i]:(~((((in @ X10) @ (univof @ emptyset)) => (~((![X11:$i>$o]:((X11 @ emptyset) => ((![X12:$i]:((X11 @ X12) => (X11 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X12)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = ((repl @ (power @ (power @ emptyset))) @ (^[X15:$i]:(eps @ (^[X16:$i]:((((in @ emptyset) @ X15) => (~((X16 = X12)))) => (~(((~(((in @ emptyset) @ X15))) => (~((X16 = X12)))))))))))))))))))))))))) => (X11 @ X10)))))))))))))))))))))))))) => (~(((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))) => (~((X7 = emptyset)))))))))) => (X6 = emptyset))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))) => (~((X5 = emptyset)))))))))) => (X4 = emptyset))) => (~((X3 = emptyset)))))))))) => ((~((X1 = X2))) => (~(((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X1)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X1)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X1))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X2)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X2)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X2))))))))))))))))))))))))))))))))),inference(assume_negation,[status(cth)],[satz1])). % 25.96/25.98 thf(h1,assumption,(~((sP7 => (![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((X3 = emptyset) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))) => (~((X6 = emptyset)))))))))) => (X5 = emptyset))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))) => (~((X2 = emptyset)))))))))) => ((~((eigen__0 = X1))) => (~(((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = eigen__0)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = eigen__0)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = eigen__0))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = X1)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = X1)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = X1)))))))))))))))))))))))))))))))),introduced(assumption,[])). % 25.97/25.98 thf(h2,assumption,sP7,introduced(assumption,[])). % 25.97/25.98 thf(h3,assumption,(~((![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((X3 = emptyset) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))) => (~((X6 = emptyset)))))))))) => (X5 = emptyset))))))))))))))))))))) => (~(((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))) => (~((X4 = emptyset)))))))))) => (X3 = emptyset))) => (~((X2 = emptyset)))))))))) => ((~((eigen__0 = X1))) => (~(((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = eigen__0)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = eigen__0)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = eigen__0))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X2:$i]:(eps @ (^[X3:$i]:((((in @ emptyset) @ X2) => (~((X3 = X1)))) => (~(((~(((in @ emptyset) @ X2))) => (~((X3 = ((repl @ (power @ (power @ emptyset))) @ (^[X4:$i]:(eps @ (^[X5:$i]:((((in @ emptyset) @ X4) => (~((X5 = X1)))) => (~(((~(((in @ emptyset) @ X4))) => (~((X5 = X1))))))))))))))))))))))))))))))),introduced(assumption,[])). % 25.97/25.98 thf(h4,assumption,(~((sP1 => ((~(sP4)) => (~(sP2)))))),introduced(assumption,[])). % 25.97/25.98 thf(h5,assumption,sP1,introduced(assumption,[])). % 25.97/25.98 thf(h6,assumption,(~(((~(sP4)) => (~(sP2))))),introduced(assumption,[])). % 25.97/25.98 thf(h7,assumption,(~(sP4)),introduced(assumption,[])). % 25.97/25.98 thf(h8,assumption,sP2,introduced(assumption,[])). % 25.97/25.98 thf(1,plain,(~(sP9) | sP3),inference(all_rule,[status(thm)],[])). % 25.97/25.98 thf(2,plain,((~(sP3) | ~(sP1)) | sP8),inference(prop_rule,[status(thm)],[])). % 25.97/25.98 thf(3,plain,((~(sP8) | ~(sP2)) | sP4),inference(prop_rule,[status(thm)],[])). % 25.97/25.98 thf(4,plain,(~(sP5) | sP6),inference(all_rule,[status(thm)],[])). % 25.97/25.98 thf(5,plain,((~(sP6) | ~(sP7)) | sP9),inference(prop_rule,[status(thm)],[])). % 25.97/25.98 thf(n_ax4,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ nat))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ nat))) @ (^[X2:$i]:(((n_is @ (ordsucc @ X1)) @ (ordsucc @ X2)) => ((n_is @ X1) @ X2))))))). % 25.97/25.98 thf(6,plain,sP5,inference(preprocess,[status(thm)],[n_ax4]). % 25.97/25.98 thf(7,plain,$false,inference(prop_unsat,[status(thm),assumptions([h7,h8,h5,h6,h4,h2,h3,h1,h0])],[1,2,3,4,5,h2,h5,h7,h8,6])). % 25.97/25.98 thf(8,plain,$false,inference(tab_negimp,[status(thm),assumptions([h5,h6,h4,h2,h3,h1,h0]),tab_negimp(discharge,[h7,h8])],[h6,7,h7,h8])). % 25.97/25.98 thf(9,plain,$false,inference(tab_negimp,[status(thm),assumptions([h4,h2,h3,h1,h0]),tab_negimp(discharge,[h5,h6])],[h4,8,h5,h6])). % 25.97/25.98 thf(10,plain,$false,inference(tab_negall,[status(thm),assumptions([h2,h3,h1,h0]),tab_negall(discharge,[h4]),tab_negall(eigenvar,eigen__1)],[h3,9,h4])). % 25.97/25.98 thf(11,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h0]),tab_negimp(discharge,[h2,h3])],[h1,10,h2,h3])). % 25.97/25.98 thf(12,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[h0,11,h1])). % 25.97/25.98 thf(0,theorem,(![X1:$i]:(((in @ X1) @ (eps @ (^[X2:$i]:(((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((~((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))) => (~((X4 = emptyset)))))))))) => (~((~((X3 = emptyset))))))))) => (~((X2 = ((repl @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))) => (~((X3 = ((repl @ (univof @ emptyset)) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))) => (~((X5 = X4)))) => (~(((~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X4)))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))))))))))))))))) => (~(((~((~((![X4:$i]:(((in @ X4) @ (univof @ emptyset)) => (~((![X5:$i>$o]:((X5 @ emptyset) => ((![X6:$i]:((X5 @ X6) => (X5 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X7:$i]:(eps @ (^[X8:$i]:((((in @ emptyset) @ X7) => (~((X8 = X6)))) => (~(((~(((in @ emptyset) @ X7))) => (~((X8 = ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X6)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = X6)))))))))))))))))))))))))) => (X5 @ X4)))))))))))) => (~((X3 = emptyset)))))))))) @ (^[X3:$i]:(eps @ (^[X4:$i]:(((~((X3 = emptyset))) => (~((X4 = X3)))) => (~(((~((~((X3 = emptyset))))) => (~((X4 = (eps @ (^[X5:$i]:(~((((in @ X5) @ (eps @ (^[X6:$i]:(((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))) => (~((X6 = ((repl @ (univof @ emptyset)) @ (^[X7:$i]:(eps @ (^[X8:$i]:(((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))) => (~((X8 = X7)))) => (~(((~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X7)))))) => (~((X8 = (eps @ (^[X9:$i]:(~((((in @ X9) @ (univof @ emptyset)) => (~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X9)))))))))))))))))))))))))) => (~(((~((~((![X7:$i]:(((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))) => (~((X6 = emptyset)))))))))) => (~((~((X5 = emptyset))))))))))))))))))))))))) => (~(((~((~((![X3:$i]:(((in @ X3) @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((~((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))) => (~((X4 = emptyset)))))))))) => (~((~((X3 = emptyset))))))))))) => (~((X2 = emptyset)))))))))) => (![X2:$i]:(((in @ X2) @ (eps @ (^[X3:$i]:(((~((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((~((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))) => (~((X5 = emptyset)))))))))) => (~((~((X4 = emptyset))))))))) => (~((X3 = ((repl @ (eps @ (^[X4:$i]:(((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))) => (~((X4 = ((repl @ (univof @ emptyset)) @ (^[X5:$i]:(eps @ (^[X6:$i]:(((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))) => (~((X6 = X5)))) => (~(((~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X5)))))) => (~((X6 = (eps @ (^[X7:$i]:(~((((in @ X7) @ (univof @ emptyset)) => (~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X7)))))))))))))))))))))))))) => (~(((~((~((![X5:$i]:(((in @ X5) @ (univof @ emptyset)) => (~((![X6:$i>$o]:((X6 @ emptyset) => ((![X7:$i]:((X6 @ X7) => (X6 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X8:$i]:(eps @ (^[X9:$i]:((((in @ emptyset) @ X8) => (~((X9 = X7)))) => (~(((~(((in @ emptyset) @ X8))) => (~((X9 = ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X7)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = X7)))))))))))))))))))))))))) => (X6 @ X5)))))))))))) => (~((X4 = emptyset)))))))))) @ (^[X4:$i]:(eps @ (^[X5:$i]:(((~((X4 = emptyset))) => (~((X5 = X4)))) => (~(((~((~((X4 = emptyset))))) => (~((X5 = (eps @ (^[X6:$i]:(~((((in @ X6) @ (eps @ (^[X7:$i]:(((~((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))) => (~((X7 = ((repl @ (univof @ emptyset)) @ (^[X8:$i]:(eps @ (^[X9:$i]:(((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))) => (~((X9 = X8)))) => (~(((~((![X10:$i>$o]:((X10 @ emptyset) => ((![X11:$i]:((X10 @ X11) => (X10 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X11)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = ((repl @ (power @ (power @ emptyset))) @ (^[X14:$i]:(eps @ (^[X15:$i]:((((in @ emptyset) @ X14) => (~((X15 = X11)))) => (~(((~(((in @ emptyset) @ X14))) => (~((X15 = X11)))))))))))))))))))))))))) => (X10 @ X8)))))) => (~((X9 = (eps @ (^[X10:$i]:(~((((in @ X10) @ (univof @ emptyset)) => (~((![X11:$i>$o]:((X11 @ emptyset) => ((![X12:$i]:((X11 @ X12) => (X11 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X12)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = ((repl @ (power @ (power @ emptyset))) @ (^[X15:$i]:(eps @ (^[X16:$i]:((((in @ emptyset) @ X15) => (~((X16 = X12)))) => (~(((~(((in @ emptyset) @ X15))) => (~((X16 = X12)))))))))))))))))))))))))) => (X11 @ X10)))))))))))))))))))))))))) => (~(((~((~((![X8:$i]:(((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))) => (~((X7 = emptyset)))))))))) => (~((~((X6 = emptyset))))))))))))))))))))))))) => (~(((~((~((![X4:$i]:(((in @ X4) @ (eps @ (^[X5:$i]:(((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))) => (~((X5 = ((repl @ (univof @ emptyset)) @ (^[X6:$i]:(eps @ (^[X7:$i]:(((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))) => (~((X7 = X6)))) => (~(((~((![X8:$i>$o]:((X8 @ emptyset) => ((![X9:$i]:((X8 @ X9) => (X8 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X10:$i]:(eps @ (^[X11:$i]:((((in @ emptyset) @ X10) => (~((X11 = X9)))) => (~(((~(((in @ emptyset) @ X10))) => (~((X11 = ((repl @ (power @ (power @ emptyset))) @ (^[X12:$i]:(eps @ (^[X13:$i]:((((in @ emptyset) @ X12) => (~((X13 = X9)))) => (~(((~(((in @ emptyset) @ X12))) => (~((X13 = X9)))))))))))))))))))))))))) => (X8 @ X6)))))) => (~((X7 = (eps @ (^[X8:$i]:(~((((in @ X8) @ (univof @ emptyset)) => (~((![X9:$i>$o]:((X9 @ emptyset) => ((![X10:$i]:((X9 @ X10) => (X9 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X10)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = ((repl @ (power @ (power @ emptyset))) @ (^[X13:$i]:(eps @ (^[X14:$i]:((((in @ emptyset) @ X13) => (~((X14 = X10)))) => (~(((~(((in @ emptyset) @ X13))) => (~((X14 = X10)))))))))))))))))))))))))) => (X9 @ X8)))))))))))))))))))))))))) => (~(((~((~((![X6:$i]:(((in @ X6) @ (univof @ emptyset)) => (~((![X7:$i>$o]:((X7 @ emptyset) => ((![X8:$i]:((X7 @ X8) => (X7 @ (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X9:$i]:(eps @ (^[X10:$i]:((((in @ emptyset) @ X9) => (~((X10 = X8)))) => (~(((~(((in @ emptyset) @ X9))) => (~((X10 = ((repl @ (power @ (power @ emptyset))) @ (^[X11:$i]:(eps @ (^[X12:$i]:((((in @ emptyset) @ X11) => (~((X12 = X8)))) => (~(((~(((in @ emptyset) @ X11))) => (~((X12 = X8)))))))))))))))))))))))))) => (X7 @ X6)))))))))))) => (~((X5 = emptyset)))))))))) => (~((~((X4 = emptyset))))))))))) => (~((X3 = emptyset)))))))))) => ((~((X1 = X2))) => (~(((union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X1)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X1)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X1))))))))))))))))))))))) = (union @ ((repl @ (power @ (power @ emptyset))) @ (^[X3:$i]:(eps @ (^[X4:$i]:((((in @ emptyset) @ X3) => (~((X4 = X2)))) => (~(((~(((in @ emptyset) @ X3))) => (~((X4 = ((repl @ (power @ (power @ emptyset))) @ (^[X5:$i]:(eps @ (^[X6:$i]:((((in @ emptyset) @ X5) => (~((X6 = X2)))) => (~(((~(((in @ emptyset) @ X5))) => (~((X6 = X2))))))))))))))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[12,h0])). % 25.97/25.98 % SZS output end Proof %------------------------------------------------------------------------------