%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : RNG108+1 : 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 : n029.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 20:42:00 EDT 2022 % Result : Theorem 8.39s 8.59s % Output : Proof 8.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : RNG108+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.11 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.32 % Computer : n029.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Mon May 30 19:41:29 EDT 2022 % 0.11/0.32 % CPUTime : % 8.39/8.59 % SZS status Theorem % 8.39/8.59 (* PROOF-FOUND *) % 8.39/8.59 (* BEGIN-PROOF *) % 8.39/8.59 % SZS output start Proof % 8.39/8.59 1. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 8.39/8.59 2. ((slsdtgt0 (xa)) != (slsdtgt0 (xa))) ### Refl(=) % 8.39/8.59 3. (aElement0 (sz00)) (-. (aElement0 (sz00))) ### Axiom % 8.39/8.59 4. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 8.39/8.59 5. ((sdtasdt0 (xa) (sz00)) != (sz00)) ((sdtasdt0 (xa) (sz00)) = (sz00)) ### Axiom % 8.39/8.59 6. (((sdtasdt0 (xa) (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) (xa)))) ((sdtasdt0 (xa) (sz00)) != (sz00)) ### And 5 % 8.39/8.59 7. ((aElement0 (xa)) => (((sdtasdt0 (xa) (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) (xa))))) ((sdtasdt0 (xa) (sz00)) != (sz00)) (aElement0 (xa)) ### Imply 4 6 % 8.39/8.59 8. (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xa)) ((sdtasdt0 (xa) (sz00)) != (sz00)) ### All 7 % 8.39/8.59 9. (-. ((aElement0 (sz00)) /\ ((sdtasdt0 (xa) (sz00)) = (sz00)))) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### NotAnd 3 8 % 8.39/8.59 10. (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (sz00))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xa)) ### NotExists 9 % 8.39/8.59 11. (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) (aElementOf0 (sz00) (slsdtgt0 (xa))) ### Axiom % 8.39/8.59 12. ((aElementOf0 (sz00) (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (sz00))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### Equiv 10 11 % 8.39/8.59 13. (All W2, ((aElementOf0 W2 (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xa)) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) ### All 12 % 8.39/8.59 14. ((aSet0 (slsdtgt0 (xa))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2)))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### And 13 % 8.39/8.59 15. (((slsdtgt0 (xa)) = (slsdtgt0 (xa))) <=> ((aSet0 (slsdtgt0 (xa))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2))))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xa)) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) ### Equiv 2 14 % 8.39/8.59 16. (All W1, ((W1 = (slsdtgt0 (xa))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2)))))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### All 15 % 8.39/8.59 17. ((aElement0 (xa)) => (All W1, ((W1 = (slsdtgt0 (xa))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2))))))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) (aElement0 (xa)) ### Imply 1 16 % 8.39/8.59 18. (All W0, ((aElement0 W0) => (All W1, ((W1 = (slsdtgt0 W0)) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 W0 W3) = W2)))))))))) (aElement0 (xa)) (-. (aElementOf0 (sz00) (slsdtgt0 (xa)))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### All 17 % 8.39/8.59 19. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 8.39/8.59 20. ((slsdtgt0 (xa)) != (slsdtgt0 (xa))) ### Refl(=) % 8.39/8.59 21. (aElement0 (xa)) (-. (aElement0 (xa))) ### Axiom % 8.39/8.59 22. (aElement0 (sz10)) (-. (aElement0 (sz10))) ### Axiom % 8.39/8.59 23. ((sdtasdt0 (xa) (sz10)) = (xa)) ((sdtasdt0 (xa) (sz10)) != (xa)) ### Axiom % 8.39/8.59 24. (-. ((aElement0 (sz10)) /\ ((sdtasdt0 (xa) (sz10)) = (xa)))) ((sdtasdt0 (xa) (sz10)) = (xa)) (aElement0 (sz10)) ### NotAnd 22 23 % 8.39/8.59 25. (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (xa))))) (aElement0 (sz10)) ((sdtasdt0 (xa) (sz10)) = (xa)) ### NotExists 24 % 8.39/8.59 26. (((sdtasdt0 (xa) (sz10)) = (xa)) /\ ((xa) = (sdtasdt0 (sz10) (xa)))) (aElement0 (sz10)) (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (xa))))) ### And 25 % 8.39/8.59 27. ((aElement0 (xa)) => (((sdtasdt0 (xa) (sz10)) = (xa)) /\ ((xa) = (sdtasdt0 (sz10) (xa))))) (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (xa))))) (aElement0 (sz10)) (aElement0 (xa)) ### Imply 21 26 % 8.39/8.59 28. (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (xa)) (aElement0 (sz10)) (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (xa))))) ### All 27 % 8.39/8.59 29. (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) (aElementOf0 (xa) (slsdtgt0 (xa))) ### Axiom % 8.39/8.59 30. ((aElementOf0 (xa) (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = (xa))))) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) (aElement0 (sz10)) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### Equiv 28 29 % 8.39/8.59 31. (All W2, ((aElementOf0 W2 (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (xa)) (aElement0 (sz10)) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) ### All 30 % 8.39/8.59 32. ((aSet0 (slsdtgt0 (xa))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2)))))) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) (aElement0 (sz10)) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### And 31 % 8.39/8.59 33. (((slsdtgt0 (xa)) = (slsdtgt0 (xa))) <=> ((aSet0 (slsdtgt0 (xa))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xa))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2))))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (xa)) (aElement0 (sz10)) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) ### Equiv 20 32 % 8.39/8.59 34. (All W1, ((W1 = (slsdtgt0 (xa))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2)))))))) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) (aElement0 (sz10)) (aElement0 (xa)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### All 33 % 8.39/8.59 35. ((aElement0 (xa)) => (All W1, ((W1 = (slsdtgt0 (xa))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xa) W3) = W2))))))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (sz10)) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) (aElement0 (xa)) ### Imply 19 34 % 8.39/8.59 36. (All W0, ((aElement0 W0) => (All W1, ((W1 = (slsdtgt0 W0)) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 W0 W3) = W2)))))))))) (aElement0 (xa)) (-. (aElementOf0 (xa) (slsdtgt0 (xa)))) (aElement0 (sz10)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### All 35 % 8.39/8.59 37. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 8.39/8.59 38. ((slsdtgt0 (xb)) != (slsdtgt0 (xb))) ### Refl(=) % 8.39/8.59 39. (aElement0 (sz00)) (-. (aElement0 (sz00))) ### Axiom % 8.39/8.59 40. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 8.39/8.59 41. ((sdtasdt0 (xb) (sz00)) != (sz00)) ((sdtasdt0 (xb) (sz00)) = (sz00)) ### Axiom % 8.39/8.59 42. (((sdtasdt0 (xb) (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) (xb)))) ((sdtasdt0 (xb) (sz00)) != (sz00)) ### And 41 % 8.39/8.59 43. ((aElement0 (xb)) => (((sdtasdt0 (xb) (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) (xb))))) ((sdtasdt0 (xb) (sz00)) != (sz00)) (aElement0 (xb)) ### Imply 40 42 % 8.39/8.59 44. (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xb)) ((sdtasdt0 (xb) (sz00)) != (sz00)) ### All 43 % 8.39/8.59 45. (-. ((aElement0 (sz00)) /\ ((sdtasdt0 (xb) (sz00)) = (sz00)))) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### NotAnd 39 44 % 8.39/8.59 46. (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (sz00))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xb)) ### NotExists 45 % 8.39/8.59 47. (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) (aElementOf0 (sz00) (slsdtgt0 (xb))) ### Axiom % 8.39/8.59 48. ((aElementOf0 (sz00) (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (sz00))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### Equiv 46 47 % 8.39/8.59 49. (All W2, ((aElementOf0 W2 (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xb)) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) ### All 48 % 8.39/8.59 50. ((aSet0 (slsdtgt0 (xb))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2)))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### And 49 % 8.39/8.59 51. (((slsdtgt0 (xb)) = (slsdtgt0 (xb))) <=> ((aSet0 (slsdtgt0 (xb))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2))))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xb)) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) ### Equiv 38 50 % 8.39/8.59 52. (All W1, ((W1 = (slsdtgt0 (xb))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2)))))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### All 51 % 8.39/8.59 53. ((aElement0 (xb)) => (All W1, ((W1 = (slsdtgt0 (xb))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2))))))))) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) (aElement0 (xb)) ### Imply 37 52 % 8.39/8.59 54. (All W0, ((aElement0 W0) => (All W1, ((W1 = (slsdtgt0 W0)) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 W0 W3) = W2)))))))))) (aElement0 (xb)) (-. (aElementOf0 (sz00) (slsdtgt0 (xb)))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) ### All 53 % 8.39/8.59 55. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 8.39/8.59 56. ((slsdtgt0 (xb)) != (slsdtgt0 (xb))) ### Refl(=) % 8.39/8.59 57. (aElement0 (xb)) (-. (aElement0 (xb))) ### Axiom % 8.39/8.59 58. (aElement0 (sz10)) (-. (aElement0 (sz10))) ### Axiom % 8.39/8.59 59. ((sdtasdt0 (xb) (sz10)) = (xb)) ((sdtasdt0 (xb) (sz10)) != (xb)) ### Axiom % 8.39/8.59 60. (-. ((aElement0 (sz10)) /\ ((sdtasdt0 (xb) (sz10)) = (xb)))) ((sdtasdt0 (xb) (sz10)) = (xb)) (aElement0 (sz10)) ### NotAnd 58 59 % 8.39/8.59 61. (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (xb))))) (aElement0 (sz10)) ((sdtasdt0 (xb) (sz10)) = (xb)) ### NotExists 60 % 8.39/8.59 62. (((sdtasdt0 (xb) (sz10)) = (xb)) /\ ((xb) = (sdtasdt0 (sz10) (xb)))) (aElement0 (sz10)) (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (xb))))) ### And 61 % 8.39/8.59 63. ((aElement0 (xb)) => (((sdtasdt0 (xb) (sz10)) = (xb)) /\ ((xb) = (sdtasdt0 (sz10) (xb))))) (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (xb))))) (aElement0 (sz10)) (aElement0 (xb)) ### Imply 57 62 % 8.39/8.59 64. (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (xb)) (aElement0 (sz10)) (-. (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (xb))))) ### All 63 % 8.39/8.59 65. (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) (aElementOf0 (xb) (slsdtgt0 (xb))) ### Axiom % 8.39/8.59 66. ((aElementOf0 (xb) (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = (xb))))) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) (aElement0 (sz10)) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### Equiv 64 65 % 8.39/8.59 67. (All W2, ((aElementOf0 W2 (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (xb)) (aElement0 (sz10)) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) ### All 66 % 8.39/8.59 68. ((aSet0 (slsdtgt0 (xb))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2)))))) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) (aElement0 (sz10)) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### And 67 % 8.39/8.59 69. (((slsdtgt0 (xb)) = (slsdtgt0 (xb))) <=> ((aSet0 (slsdtgt0 (xb))) /\ (All W2, ((aElementOf0 W2 (slsdtgt0 (xb))) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2))))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (xb)) (aElement0 (sz10)) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) ### Equiv 56 68 % 8.39/8.59 70. (All W1, ((W1 = (slsdtgt0 (xb))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2)))))))) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) (aElement0 (sz10)) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### All 69 % 8.39/8.59 71. ((aElement0 (xb)) => (All W1, ((W1 = (slsdtgt0 (xb))) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 (xb) W3) = W2))))))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (sz10)) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) (aElement0 (xb)) ### Imply 55 70 % 8.39/8.59 72. (All W0, ((aElement0 W0) => (All W1, ((W1 = (slsdtgt0 W0)) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 W0 W3) = W2)))))))))) (aElement0 (xb)) (-. (aElementOf0 (xb) (slsdtgt0 (xb)))) (aElement0 (sz10)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) ### All 71 % 8.39/8.59 73. (-. ((aElementOf0 (sz00) (slsdtgt0 (xa))) /\ ((aElementOf0 (xa) (slsdtgt0 (xa))) /\ ((aElementOf0 (sz00) (slsdtgt0 (xb))) /\ (aElementOf0 (xb) (slsdtgt0 (xb))))))) (aElement0 (xb)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (aElement0 (sz10)) (aElement0 (sz00)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (xa)) (All W0, ((aElement0 W0) => (All W1, ((W1 = (slsdtgt0 W0)) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 W0 W3) = W2)))))))))) ### DisjTree 18 36 54 72 % 8.39/8.59 74. ((aElement0 (xa)) /\ (aElement0 (xb))) (All W0, ((aElement0 W0) => (All W1, ((W1 = (slsdtgt0 W0)) <=> ((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) <=> (Ex W3, ((aElement0 W3) /\ ((sdtasdt0 W0 W3) = W2)))))))))) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz00)) = (sz00)) /\ ((sz00) = (sdtasdt0 (sz00) W0))))) (aElement0 (sz00)) (aElement0 (sz10)) (All W0, ((aElement0 W0) => (((sdtasdt0 W0 (sz10)) = W0) /\ (W0 = (sdtasdt0 (sz10) W0))))) (-. ((aElementOf0 (sz00) (slsdtgt0 (xa))) /\ ((aElementOf0 (xa) (slsdtgt0 (xa))) /\ ((aElementOf0 (sz00) (slsdtgt0 (xb))) /\ (aElementOf0 (xb) (slsdtgt0 (xb))))))) ### And 73 % 8.39/8.59 % SZS output end Proof % 8.39/8.59 (* END-PROOF *) %------------------------------------------------------------------------------