%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET579+3 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n019.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 : Tue Jul 19 05:42:22 EDT 2022 % Result : Theorem 4.43s 4.61s % Output : Proof 4.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET579+3 : TPTP v8.1.0. Released v2.2.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n019.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 : Mon Jul 11 04:40:08 EDT 2022 % 0.12/0.33 % CPUTime : % 4.43/4.61 % SZS status Theorem % 4.43/4.61 (* PROOF-FOUND *) % 4.43/4.61 (* BEGIN-PROOF *) % 4.43/4.61 % SZS output start Proof % 4.43/4.61 1. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 4.43/4.61 2. (-. (member T_0 T_2)) (member T_0 T_2) ### Axiom % 4.43/4.61 3. ((member T_0 T_2) /\ (-. (member T_0 T_3))) (-. (member T_0 T_2)) ### And 2 % 4.43/4.61 4. ((member T_0 T_1) <=> ((member T_0 T_2) /\ (-. (member T_0 T_3)))) (-. (member T_0 T_2)) (member T_0 T_1) ### Equiv 1 3 % 4.43/4.61 5. (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (member T_0 T_1) (-. (member T_0 T_2)) ### All 4 % 4.43/4.61 6. (member T_0 T_1) (-. (member T_0 T_1)) ### Axiom % 4.43/4.61 7. (member T_0 T_3) (-. (member T_0 T_3)) ### Axiom % 4.43/4.61 8. ((member T_0 T_2) /\ (-. (member T_0 T_3))) (member T_0 T_3) ### And 7 % 4.43/4.61 9. ((member T_0 T_1) <=> ((member T_0 T_2) /\ (-. (member T_0 T_3)))) (member T_0 T_3) (member T_0 T_1) ### Equiv 6 8 % 4.43/4.61 10. (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (member T_0 T_1) (member T_0 T_3) ### All 9 % 4.43/4.61 11. (-. (-. (member T_0 T_3))) (member T_0 T_1) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) ### NotNot 10 % 4.43/4.61 12. (-. ((member T_0 T_2) /\ (-. (member T_0 T_3)))) (member T_0 T_1) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) ### NotAnd 5 11 % 4.43/4.61 13. (-. (member T_0 (difference T_2 T_3))) (member T_0 (difference T_2 T_3)) ### Axiom % 4.43/4.61 14. ((member T_0 (difference T_2 T_3)) <=> ((member T_0 T_2) /\ (-. (member T_0 T_3)))) (-. (member T_0 (difference T_2 T_3))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (member T_0 T_1) ### Equiv 12 13 % 4.43/4.61 15. (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (member T_0 T_1) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (-. (member T_0 (difference T_2 T_3))) ### All 14 % 4.43/4.61 16. (-. ((member T_0 T_1) => (member T_0 (difference T_2 T_3)))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) ### NotImply 15 % 4.43/4.61 17. (-. (All D, ((member D T_1) => (member D (difference T_2 T_3))))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) ### NotAllEx 16 % 4.43/4.61 18. (-. (subset T_1 (difference T_2 T_3))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) ### Definition-Pseudo(subset) 17 % 4.43/4.61 19. (member T_4 (difference T_2 T_3)) (-. (member T_4 (difference T_2 T_3))) ### Axiom % 4.43/4.61 20. (-. (member T_4 T_2)) (member T_4 T_2) ### Axiom % 4.43/4.61 21. ((member T_4 T_2) /\ (-. (member T_4 T_3))) (-. (member T_4 T_2)) ### And 20 % 4.43/4.61 22. ((member T_4 (difference T_2 T_3)) <=> ((member T_4 T_2) /\ (-. (member T_4 T_3)))) (-. (member T_4 T_2)) (member T_4 (difference T_2 T_3)) ### Equiv 19 21 % 4.43/4.61 23. (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (member T_4 (difference T_2 T_3)) (-. (member T_4 T_2)) ### All 22 % 4.43/4.61 24. (member T_4 (difference T_2 T_3)) (-. (member T_4 (difference T_2 T_3))) ### Axiom % 4.43/4.61 25. (member T_4 T_3) (-. (member T_4 T_3)) ### Axiom % 4.43/4.61 26. ((member T_4 T_2) /\ (-. (member T_4 T_3))) (member T_4 T_3) ### And 25 % 4.43/4.61 27. ((member T_4 (difference T_2 T_3)) <=> ((member T_4 T_2) /\ (-. (member T_4 T_3)))) (member T_4 T_3) (member T_4 (difference T_2 T_3)) ### Equiv 24 26 % 4.43/4.61 28. (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (member T_4 (difference T_2 T_3)) (member T_4 T_3) ### All 27 % 4.43/4.61 29. (-. (-. (member T_4 T_3))) (member T_4 (difference T_2 T_3)) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) ### NotNot 28 % 4.43/4.61 30. (-. ((member T_4 T_2) /\ (-. (member T_4 T_3)))) (member T_4 (difference T_2 T_3)) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) ### NotAnd 23 29 % 4.43/4.61 31. (-. (member T_4 T_1)) (member T_4 T_1) ### Axiom % 4.43/4.61 32. ((member T_4 T_1) <=> ((member T_4 T_2) /\ (-. (member T_4 T_3)))) (-. (member T_4 T_1)) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (member T_4 (difference T_2 T_3)) ### Equiv 30 31 % 4.43/4.61 33. (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (member T_4 (difference T_2 T_3)) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (-. (member T_4 T_1)) ### All 32 % 4.43/4.61 34. (-. ((member T_4 (difference T_2 T_3)) => (member T_4 T_1))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) ### NotImply 33 % 4.43/4.61 35. (-. (All D, ((member D (difference T_2 T_3)) => (member D T_1)))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) ### NotAllEx 34 % 4.43/4.61 36. (-. (subset (difference T_2 T_3) T_1)) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) ### Definition-Pseudo(subset) 35 % 4.43/4.61 37. (-. ((subset T_1 (difference T_2 T_3)) /\ (subset (difference T_2 T_3) T_1))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) ### NotAnd 18 36 % 4.43/4.61 38. (T_1 != (difference T_2 T_3)) (T_1 = (difference T_2 T_3)) ### Axiom % 4.43/4.61 39. ((T_1 = (difference T_2 T_3)) <=> ((subset T_1 (difference T_2 T_3)) /\ (subset (difference T_2 T_3) T_1))) (T_1 != (difference T_2 T_3)) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) ### Equiv 37 38 % 4.43/4.61 40. (All C, ((T_1 = C) <=> ((subset T_1 C) /\ (subset C T_1)))) (All D, ((member D (difference T_2 T_3)) <=> ((member D T_2) /\ (-. (member D T_3))))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (T_1 != (difference T_2 T_3)) ### All 39 % 4.43/4.61 41. (All C, (All D, ((member D (difference T_2 C)) <=> ((member D T_2) /\ (-. (member D C)))))) (T_1 != (difference T_2 T_3)) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (All C, ((T_1 = C) <=> ((subset T_1 C) /\ (subset C T_1)))) ### All 40 % 4.43/4.61 42. (All B, (All C, (All D, ((member D (difference B C)) <=> ((member D B) /\ (-. (member D C))))))) (All C, ((T_1 = C) <=> ((subset T_1 C) /\ (subset C T_1)))) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (T_1 != (difference T_2 T_3)) ### All 41 % 4.43/4.61 43. (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (T_1 != (difference T_2 T_3)) (All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) (All B, (All C, (All D, ((member D (difference B C)) <=> ((member D B) /\ (-. (member D C))))))) ### All 42 % 4.43/4.61 44. (-. ((All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E T_3))))) => (T_1 = (difference T_2 T_3)))) (All B, (All C, (All D, ((member D (difference B C)) <=> ((member D B) /\ (-. (member D C))))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### NotImply 43 % 4.43/4.61 45. (-. (All D, ((All E, ((member E T_1) <=> ((member E T_2) /\ (-. (member E D))))) => (T_1 = (difference T_2 D))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (difference B C)) <=> ((member D B) /\ (-. (member D C))))))) ### NotAllEx 44 % 4.43/4.61 46. (-. (All C, (All D, ((All E, ((member E T_1) <=> ((member E C) /\ (-. (member E D))))) => (T_1 = (difference C D)))))) (All B, (All C, (All D, ((member D (difference B C)) <=> ((member D B) /\ (-. (member D C))))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) ### NotAllEx 45 % 4.43/4.61 47. (-. (All B, (All C, (All D, ((All E, ((member E B) <=> ((member E C) /\ (-. (member E D))))) => (B = (difference C D))))))) (All B, (All C, ((B = C) <=> ((subset B C) /\ (subset C B))))) (All B, (All C, (All D, ((member D (difference B C)) <=> ((member D B) /\ (-. (member D C))))))) ### NotAllEx 46 % 4.43/4.61 % SZS output end Proof % 4.43/4.61 (* END-PROOF *) %------------------------------------------------------------------------------