%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n013.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 14:50:16 EDT 2022 % Result : Theorem 2.75s 2.93s % Output : Proof 2.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.20/0.34 % CPULimit : 300 % 0.20/0.34 % WCLimit : 600 % 0.20/0.34 % DateTime : Sun Jun 19 19:04:44 EDT 2022 % 0.20/0.34 % CPUTime : % 2.75/2.93 % SZS status Theorem % 2.75/2.93 (* PROOF-FOUND *) % 2.75/2.93 (* BEGIN-PROOF *) % 2.75/2.93 % SZS output start Proof % 2.75/2.93 1. (element T_0 (powerset (powerset T_1))) (-. (element T_0 (powerset (powerset T_1)))) ### Axiom % 2.75/2.93 2. (T_0 != (empty_set)) (T_0 = (empty_set)) ### Axiom % 2.75/2.93 3. ((complements_of_subsets T_1 T_0) = (empty_set)) ((complements_of_subsets T_1 T_0) != (empty_set)) ### Axiom % 2.75/2.93 4. ((element T_0 (powerset (powerset T_1))) => (-. ((T_0 != (empty_set)) /\ ((complements_of_subsets T_1 T_0) = (empty_set))))) ((complements_of_subsets T_1 T_0) = (empty_set)) (T_0 != (empty_set)) (element T_0 (powerset (powerset T_1))) ### DisjTree 1 2 3 % 2.75/2.93 5. (All B, ((element B (powerset (powerset T_1))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets T_1 B) = (empty_set)))))) (element T_0 (powerset (powerset T_1))) (T_0 != (empty_set)) ((complements_of_subsets T_1 T_0) = (empty_set)) ### All 4 % 2.75/2.93 6. (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ((complements_of_subsets T_1 T_0) = (empty_set)) (T_0 != (empty_set)) (element T_0 (powerset (powerset T_1))) ### All 5 % 2.75/2.93 7. ((T_0 != (empty_set)) /\ ((complements_of_subsets T_1 T_0) = (empty_set))) (element T_0 (powerset (powerset T_1))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ### And 6 % 2.75/2.93 8. (-. (-. ((T_0 != (empty_set)) /\ ((complements_of_subsets T_1 T_0) = (empty_set))))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (element T_0 (powerset (powerset T_1))) ### NotNot 7 % 2.75/2.93 9. (empty T_2) (-. (empty T_2)) ### Axiom % 2.75/2.93 10. (element T_2 (powerset (powerset T_1))) (-. (element T_2 (powerset (powerset T_1)))) ### Axiom % 2.75/2.93 11. (T_1 != T_1) ### Refl(=) % 2.75/2.93 12. (T_0 != T_0) ### Refl(=) % 2.75/2.93 13. (element T_2 (powerset (powerset T_1))) (-. (element T_2 (powerset (powerset T_1)))) ### Axiom % 2.75/2.93 14. (-. (element (complements_of_subsets T_1 T_2) (powerset (powerset T_1)))) (element (complements_of_subsets T_1 T_2) (powerset (powerset T_1))) ### Axiom % 2.75/2.93 15. ((element T_2 (powerset (powerset T_1))) => (element (complements_of_subsets T_1 T_2) (powerset (powerset T_1)))) (-. (element (complements_of_subsets T_1 T_2) (powerset (powerset T_1)))) (element T_2 (powerset (powerset T_1))) ### Imply 13 14 % 2.75/2.93 16. (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (element T_2 (powerset (powerset T_1))) (-. (element (complements_of_subsets T_1 T_2) (powerset (powerset T_1)))) ### All 15 % 2.75/2.93 17. ((empty_set) != (complements_of_subsets T_1 T_2)) ((complements_of_subsets T_1 T_2) = (empty_set)) ### Sym(=) % 2.75/2.93 18. ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) != (complements_of_subsets T_1 (complements_of_subsets T_1 T_2))) ### Refl(=) % 2.75/2.93 19. (T_2 = (empty_set)) (T_2 != (empty_set)) ### Axiom % 2.75/2.93 20. ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) != (empty_set)) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) (T_2 = (empty_set)) ### Trans 18 19 % 2.75/2.93 21. ((element (complements_of_subsets T_1 T_2) (powerset (powerset T_1))) => (-. (((complements_of_subsets T_1 T_2) != (empty_set)) /\ ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = (empty_set))))) (T_2 = (empty_set)) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) ((empty_set) != (complements_of_subsets T_1 T_2)) (element T_2 (powerset (powerset T_1))) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) ### DisjTree 16 17 20 % 2.75/2.93 22. (All B, ((element B (powerset (powerset T_1))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets T_1 B) = (empty_set)))))) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (element T_2 (powerset (powerset T_1))) ((empty_set) != (complements_of_subsets T_1 T_2)) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) (T_2 = (empty_set)) ### All 21 % 2.75/2.93 23. (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (T_2 = (empty_set)) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) ((empty_set) != (complements_of_subsets T_1 T_2)) (element T_2 (powerset (powerset T_1))) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) ### All 22 % 2.75/2.93 24. (T_0 != (complements_of_subsets T_1 T_2)) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (element T_2 (powerset (powerset T_1))) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) (T_2 = (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ### Trans 12 23 % 2.75/2.93 25. ((complements_of_subsets T_1 T_0) != (complements_of_subsets T_1 (complements_of_subsets T_1 T_2))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (T_2 = (empty_set)) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) (element T_2 (powerset (powerset T_1))) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (T_0 = (empty_set)) ### NotEqual 11 24 % 2.75/2.93 26. (T_2 != T_2) ### Refl(=) % 2.75/2.93 27. (T_2 != T_2) ### Refl(=) % 2.75/2.93 28. ((complements_of_subsets T_1 T_0) != T_2) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (element T_2 (powerset (powerset T_1))) ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2) (T_2 = (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ### TransEq 25 26 27 % 2.75/2.93 29. ((element T_2 (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 T_2)) = T_2)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (T_2 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (T_0 = (empty_set)) ((complements_of_subsets T_1 T_0) != T_2) (element T_2 (powerset (powerset T_1))) ### Imply 10 28 % 2.75/2.93 30. (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) (element T_2 (powerset (powerset T_1))) ((complements_of_subsets T_1 T_0) != T_2) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (T_2 = (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ### All 29 % 2.75/2.93 31. ((empty_set) != (empty_set)) ### NotEqual % 2.75/2.93 32. ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (T_2 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (T_0 = (empty_set)) (element T_2 (powerset (powerset T_1))) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) ### TransEq 30 31 31 % 2.75/2.93 33. ((empty T_2) => (T_2 = (empty_set))) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) (element T_2 (powerset (powerset T_1))) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ((complements_of_subsets T_1 T_0) != (empty_set)) (empty T_2) ### Imply 9 32 % 2.75/2.95 34. (All A, ((empty A) => (A = (empty_set)))) (empty T_2) ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (T_0 = (empty_set)) (element T_2 (powerset (powerset T_1))) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) ### All 33 % 2.75/2.95 35. ((element T_2 (powerset (powerset T_1))) /\ (empty T_2)) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, ((empty A) => (A = (empty_set)))) ### And 34 % 2.75/2.95 36. (Ex B, ((element B (powerset (powerset T_1))) /\ (empty B))) (All A, ((empty A) => (A = (empty_set)))) ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) ### Exists 35 % 2.75/2.95 37. (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => (element (complements_of_subsets T_1 B) (powerset (powerset T_1))))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, ((empty A) => (A = (empty_set)))) ### All 36 % 2.75/2.95 38. (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) (All A, ((empty A) => (A = (empty_set)))) ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (T_0 = (empty_set)) (All B, ((element B (powerset (powerset T_1))) => ((complements_of_subsets T_1 (complements_of_subsets T_1 B)) = B))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) ### All 37 % 2.75/2.95 39. (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (T_0 = (empty_set)) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ((complements_of_subsets T_1 T_0) != (empty_set)) (All A, ((empty A) => (A = (empty_set)))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) ### All 38 % 2.75/2.95 40. (((complements_of_subsets T_1 T_0) != (empty_set)) /\ (T_0 = (empty_set))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) (All A, ((empty A) => (A = (empty_set)))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) ### And 39 % 2.75/2.95 41. (-. (-. (((complements_of_subsets T_1 T_0) != (empty_set)) /\ (T_0 = (empty_set))))) (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (All A, ((empty A) => (A = (empty_set)))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) ### NotNot 40 % 2.75/2.95 42. (-. ((-. ((T_0 != (empty_set)) /\ ((complements_of_subsets T_1 T_0) = (empty_set)))) /\ (-. (((complements_of_subsets T_1 T_0) != (empty_set)) /\ (T_0 = (empty_set)))))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) (All A, ((empty A) => (A = (empty_set)))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) (element T_0 (powerset (powerset T_1))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ### NotAnd 8 41 % 2.75/2.95 43. (-. ((element T_0 (powerset (powerset T_1))) => ((-. ((T_0 != (empty_set)) /\ ((complements_of_subsets T_1 T_0) = (empty_set)))) /\ (-. (((complements_of_subsets T_1 T_0) != (empty_set)) /\ (T_0 = (empty_set))))))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All A, ((empty A) => (A = (empty_set)))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) ### NotImply 42 % 2.75/2.95 44. (-. (All B, ((element B (powerset (powerset T_1))) => ((-. ((B != (empty_set)) /\ ((complements_of_subsets T_1 B) = (empty_set)))) /\ (-. (((complements_of_subsets T_1 B) != (empty_set)) /\ (B = (empty_set)))))))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) (All A, ((empty A) => (A = (empty_set)))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) ### NotAllEx 43 % 2.75/2.95 45. (-. (All A, (All B, ((element B (powerset (powerset A))) => ((-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set)))) /\ (-. (((complements_of_subsets A B) != (empty_set)) /\ (B = (empty_set))))))))) (All A, (All B, ((element B (powerset (powerset A))) => (-. ((B != (empty_set)) /\ ((complements_of_subsets A B) = (empty_set))))))) (All A, (All B, ((element B (powerset (powerset A))) => ((complements_of_subsets A (complements_of_subsets A B)) = B)))) (All A, (Ex B, ((element B (powerset A)) /\ (empty B)))) (All A, ((empty A) => (A = (empty_set)))) (All A, (All B, ((element B (powerset (powerset A))) => (element (complements_of_subsets A B) (powerset (powerset A)))))) ### NotAllEx 44 % 2.75/2.95 % SZS output end Proof % 2.75/2.95 (* END-PROOF *) %------------------------------------------------------------------------------