%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM537+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n025.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 : 600s % DateTime : Mon Jul 18 14:43:24 EDT 2022 % Result : Theorem 1.40s 1.63s % Output : Proof 1.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : NUM537+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jul 6 00:30:27 EDT 2022 % 0.12/0.33 % CPUTime : % 1.40/1.63 % SZS status Theorem % 1.40/1.63 (* PROOF-FOUND *) % 1.40/1.63 (* BEGIN-PROOF *) % 1.40/1.63 % SZS output start Proof % 1.40/1.63 1. (aSet0 (xS)) (-. (aSet0 (xS))) ### Axiom % 1.40/1.63 2. (aSet0 (sdtpldt0 (xS) (xx))) (-. (aSet0 (sdtpldt0 (xS) (xx)))) ### Axiom % 1.40/1.63 3. (aSet0 (xS)) (-. (aSet0 (xS))) ### Axiom % 1.40/1.63 4. (aElementOf0 T_0 (xS)) (-. (aElementOf0 T_0 (xS))) ### Axiom % 1.40/1.63 5. (-. (aElement0 T_0)) (aElement0 T_0) ### Axiom % 1.40/1.63 6. ((aElementOf0 T_0 (xS)) => (aElement0 T_0)) (-. (aElement0 T_0)) (aElementOf0 T_0 (xS)) ### Imply 4 5 % 1.40/1.63 7. (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (aElementOf0 T_0 (xS)) (-. (aElement0 T_0)) ### All 6 % 1.40/1.63 8. (aElementOf0 T_0 (xS)) (-. (aElementOf0 T_0 (xS))) ### Axiom % 1.40/1.63 9. (-. ((aElementOf0 T_0 (xS)) \/ (T_0 = (xx)))) (aElementOf0 T_0 (xS)) ### NotOr 8 % 1.40/1.63 10. (-. ((aElement0 T_0) /\ ((aElementOf0 T_0 (xS)) \/ (T_0 = (xx))))) (aElementOf0 T_0 (xS)) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) ### NotAnd 7 9 % 1.40/1.63 11. (-. (aElementOf0 T_0 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_0 (sdtpldt0 (xS) (xx))) ### Axiom % 1.40/1.63 12. ((aElementOf0 T_0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 T_0) /\ ((aElementOf0 T_0 (xS)) \/ (T_0 = (xx))))) (-. (aElementOf0 T_0 (sdtpldt0 (xS) (xx)))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (aElementOf0 T_0 (xS)) ### Equiv 10 11 % 1.40/1.63 13. (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aElementOf0 T_0 (xS)) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (-. (aElementOf0 T_0 (sdtpldt0 (xS) (xx)))) ### All 12 % 1.40/1.63 14. (-. ((aElementOf0 T_0 (xS)) => (aElementOf0 T_0 (sdtpldt0 (xS) (xx))))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) ### NotImply 13 % 1.40/1.63 15. (-. (All W2, ((aElementOf0 W2 (xS)) => (aElementOf0 W2 (sdtpldt0 (xS) (xx)))))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) ### NotAllEx 14 % 1.40/1.63 16. (-. ((aSet0 (xS)) /\ (All W2, ((aElementOf0 W2 (xS)) => (aElementOf0 W2 (sdtpldt0 (xS) (xx))))))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (xS)) ### NotAnd 3 15 % 1.40/1.63 17. (aElementOf0 T_1 (xS)) (-. (aElementOf0 T_1 (xS))) ### Axiom % 1.40/1.63 18. (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_1 (sdtpldt0 (xS) (xx))) ### Axiom % 1.40/1.63 19. ((aElementOf0 T_1 (xS)) => (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_1 (xS)) ### Imply 17 18 % 1.40/1.63 20. (All W2, ((aElementOf0 W2 (xS)) => (aElementOf0 W2 (sdtpldt0 (xS) (xx))))) (aElementOf0 T_1 (xS)) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) ### All 19 % 1.40/1.63 21. ((aSet0 (xS)) /\ (All W2, ((aElementOf0 W2 (xS)) => (aElementOf0 W2 (sdtpldt0 (xS) (xx)))))) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_1 (xS)) ### And 20 % 1.40/1.63 22. ((aSubsetOf0 (xS) (sdtpldt0 (xS) (xx))) <=> ((aSet0 (xS)) /\ (All W2, ((aElementOf0 W2 (xS)) => (aElementOf0 W2 (sdtpldt0 (xS) (xx))))))) (aElementOf0 T_1 (xS)) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aSet0 (xS)) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) ### Equiv 16 21 % 1.40/1.63 23. (All W1, ((aSubsetOf0 W1 (sdtpldt0 (xS) (xx))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (sdtpldt0 (xS) (xx)))))))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (xS)) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_1 (xS)) ### All 22 % 1.40/1.63 24. ((aSet0 (sdtpldt0 (xS) (xx))) => (All W1, ((aSubsetOf0 W1 (sdtpldt0 (xS) (xx))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (sdtpldt0 (xS) (xx))))))))) (aElementOf0 T_1 (xS)) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aSet0 (xS)) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (aSet0 (sdtpldt0 (xS) (xx))) ### Imply 2 23 % 1.40/1.63 25. (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (xS)) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_1 (xS)) ### All 24 % 1.40/1.63 26. ((aSet0 (xS)) => (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1)))) (aElementOf0 T_1 (xS)) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (xS)) ### Imply 1 25 % 1.40/1.63 27. (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (-. (aElementOf0 T_1 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_1 (xS)) ### All 26 % 1.40/1.63 28. (-. (aElement0 T_1)) (aElement0 T_1) ### Axiom % 1.40/1.63 29. ((aElement0 T_1) /\ ((aElementOf0 T_1 (xS)) \/ (T_1 = (xx)))) (-. (aElement0 T_1)) ### And 28 % 1.40/1.63 30. ((aElementOf0 T_1 (sdtpldt0 (xS) (xx))) <=> ((aElement0 T_1) /\ ((aElementOf0 T_1 (xS)) \/ (T_1 = (xx))))) (-. (aElement0 T_1)) (aElementOf0 T_1 (xS)) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) ### Equiv 27 29 % 1.40/1.63 31. (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aElementOf0 T_1 (xS)) (-. (aElement0 T_1)) ### All 30 % 1.40/1.63 32. (T_1 = (xx)) (T_1 != (xx)) ### Axiom % 1.40/1.63 33. ((xS) != (xS)) ### NotEqual % 1.40/1.63 34. (-. (aElementOf0 (xx) (xS))) (aElementOf0 T_1 (xS)) (T_1 = (xx)) ### P-NotP 32 33 % 1.40/1.63 35. (-. ((aElement0 T_1) /\ ((aElementOf0 T_1 (sdtpldt0 (xS) (xx))) /\ (T_1 != (xx))))) (-. (aElementOf0 (xx) (xS))) (aElementOf0 T_1 (xS)) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) ### DisjTree 31 27 34 % 1.40/1.63 36. (-. (aElementOf0 T_1 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))) (aElementOf0 T_1 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) ### Axiom % 1.40/1.63 37. ((aElementOf0 T_1 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 T_1) /\ ((aElementOf0 T_1 (sdtpldt0 (xS) (xx))) /\ (T_1 != (xx))))) (-. (aElementOf0 T_1 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aElementOf0 T_1 (xS)) (-. (aElementOf0 (xx) (xS))) ### Equiv 35 36 % 1.40/1.63 38. (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (-. (aElementOf0 (xx) (xS))) (aElementOf0 T_1 (xS)) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 T_1 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))) ### All 37 % 1.40/1.63 39. (-. ((aElementOf0 T_1 (xS)) => (aElementOf0 T_1 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (-. (aElementOf0 (xx) (xS))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) ### NotImply 38 % 1.40/1.63 40. (-. (All W0, ((aElementOf0 W0 (xS)) => (aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (-. (aElementOf0 (xx) (xS))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (aSet0 (sdtpldt0 (xS) (xx))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) ### NotAllEx 39 % 1.40/1.63 41. (-. (((aSet0 (sdtpldt0 (xS) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx))))))) => (((aSet0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx))))))) => ((All W0, ((aElementOf0 W0 (xS)) => (aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))))) \/ (aSubsetOf0 (xS) (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))))))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (-. (aElementOf0 (xx) (xS))) ### ConjTree 40 % 1.40/1.63 42. (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (-. (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))) ### Axiom % 1.40/1.63 43. (-. (aElementOf0 T_2 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_2 (sdtpldt0 (xS) (xx))) ### Axiom % 1.40/1.63 44. ((aElement0 T_2) /\ ((aElementOf0 T_2 (sdtpldt0 (xS) (xx))) /\ (T_2 != (xx)))) (-. (aElementOf0 T_2 (sdtpldt0 (xS) (xx)))) ### ConjTree 43 % 1.40/1.63 45. ((aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 T_2) /\ ((aElementOf0 T_2 (sdtpldt0 (xS) (xx))) /\ (T_2 != (xx))))) (-. (aElementOf0 T_2 (sdtpldt0 (xS) (xx)))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) ### Equiv 42 44 % 1.40/1.63 46. (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (-. (aElementOf0 T_2 (sdtpldt0 (xS) (xx)))) ### All 45 % 1.40/1.63 47. (-. (aElementOf0 T_2 (xS))) (aElementOf0 T_2 (xS)) ### Axiom % 1.40/1.63 48. (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (-. (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))) ### Axiom % 1.40/1.63 49. (T_2 = (xx)) (T_2 != (xx)) ### Axiom % 1.40/1.63 50. ((aElement0 T_2) /\ ((aElementOf0 T_2 (sdtpldt0 (xS) (xx))) /\ (T_2 != (xx)))) (T_2 = (xx)) ### ConjTree 49 % 1.40/1.63 51. ((aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 T_2) /\ ((aElementOf0 T_2 (sdtpldt0 (xS) (xx))) /\ (T_2 != (xx))))) (T_2 = (xx)) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) ### Equiv 48 50 % 1.40/1.63 52. (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (T_2 = (xx)) ### All 51 % 1.40/1.63 53. ((aElementOf0 T_2 (xS)) \/ (T_2 = (xx))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (-. (aElementOf0 T_2 (xS))) ### Or 47 52 % 1.40/1.63 54. ((aElement0 T_2) /\ ((aElementOf0 T_2 (xS)) \/ (T_2 = (xx)))) (-. (aElementOf0 T_2 (xS))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) ### And 53 % 1.40/1.63 55. ((aElementOf0 T_2 (sdtpldt0 (xS) (xx))) <=> ((aElement0 T_2) /\ ((aElementOf0 T_2 (xS)) \/ (T_2 = (xx))))) (-. (aElementOf0 T_2 (xS))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) ### Equiv 46 54 % 1.40/1.63 56. (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) (-. (aElementOf0 T_2 (xS))) ### All 55 % 1.40/1.63 57. (-. ((aElementOf0 T_2 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) => (aElementOf0 T_2 (xS)))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) ### NotImply 56 % 1.40/1.63 58. (-. (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) => (aElementOf0 W0 (xS))))) (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx)))))) (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx)))))) ### NotAllEx 57 % 1.40/1.63 59. (-. (((aSet0 (sdtpldt0 (xS) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx))))))) => (((aSet0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx))))))) => ((All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) => (aElementOf0 W0 (xS)))) \/ (aSubsetOf0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)) (xS)))))) ### ConjTree 58 % 1.40/1.63 60. (-. ((((aSet0 (sdtpldt0 (xS) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx))))))) => (((aSet0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx))))))) => ((All W0, ((aElementOf0 W0 (xS)) => (aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))))) \/ (aSubsetOf0 (xS) (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))))) /\ (((aSet0 (sdtpldt0 (xS) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx))))))) => (((aSet0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx))))))) => ((All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) => (aElementOf0 W0 (xS)))) \/ (aSubsetOf0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)) (xS))))))) (-. (aElementOf0 (xx) (xS))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) ### NotAnd 41 59 % 1.40/1.63 61. ((aElement0 (xx)) /\ (aSet0 (xS))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (All W0, ((aSet0 W0) => (All W1, ((aSubsetOf0 W1 W0) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 W0)))))))) (-. (aElementOf0 (xx) (xS))) (-. ((((aSet0 (sdtpldt0 (xS) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx))))))) => (((aSet0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx))))))) => ((All W0, ((aElementOf0 W0 (xS)) => (aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))))) \/ (aSubsetOf0 (xS) (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)))))) /\ (((aSet0 (sdtpldt0 (xS) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xS)) \/ (W0 = (xx))))))) => (((aSet0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) /\ (All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtpldt0 (xS) (xx))) /\ (W0 != (xx))))))) => ((All W0, ((aElementOf0 W0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx))) => (aElementOf0 W0 (xS)))) \/ (aSubsetOf0 (sdtmndt0 (sdtpldt0 (xS) (xx)) (xx)) (xS))))))) ### And 60 % 1.40/1.63 % SZS output end Proof % 1.40/1.63 (* END-PROOF *) %------------------------------------------------------------------------------