%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU354+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 : 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 : Tue Jul 19 14:50:30 EDT 2022 % Result : Theorem 5.12s 5.31s % Output : Proof 5.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SEU354+1 : TPTP v8.1.0. Released v3.3.0. % 0.00/0.09 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.09/0.29 % Computer : n025.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 600 % 0.09/0.29 % DateTime : Sat Jun 18 21:32:58 EDT 2022 % 0.09/0.29 % CPUTime : % 5.12/5.31 % SZS status Theorem % 5.12/5.31 (* PROOF-FOUND *) % 5.12/5.31 (* BEGIN-PROOF *) % 5.12/5.31 % SZS output start Proof % 5.12/5.31 1. (element T_0 (powerset T_1)) (-. (element T_0 (powerset T_1))) ### Axiom % 5.12/5.31 2. (T_0 != T_0) ### Refl(=) % 5.12/5.31 3. (T_0 != T_0) ### Refl(=) % 5.12/5.31 4. ((union (powerset T_1)) != T_1) ((union (powerset T_1)) = T_1) ### Axiom % 5.12/5.31 5. (All A, ((union (powerset A)) = A)) ((union (powerset T_1)) != T_1) ### All 4 % 5.12/5.31 6. (T_0 != T_1) (T_0 = (union (powerset T_1))) (All A, ((union (powerset A)) = A)) ### TransEq 2 3 5 % 5.12/5.31 7. (-. (T_0 != (union (powerset T_1)))) (All A, ((union (powerset A)) = A)) (T_0 != T_1) ### NotNot 6 % 5.12/5.31 8. (-. (proper_element T_0 (powerset T_1))) (proper_element T_0 (powerset T_1)) ### Axiom % 5.12/5.31 9. ((proper_element T_0 (powerset T_1)) <=> (T_0 != (union (powerset T_1)))) (-. (proper_element T_0 (powerset T_1))) (T_0 != T_1) (All A, ((union (powerset A)) = A)) ### Equiv 7 8 % 5.12/5.31 10. ((element T_0 (powerset T_1)) => ((proper_element T_0 (powerset T_1)) <=> (T_0 != (union (powerset T_1))))) (All A, ((union (powerset A)) = A)) (T_0 != T_1) (-. (proper_element T_0 (powerset T_1))) (element T_0 (powerset T_1)) ### Imply 1 9 % 5.12/5.31 11. (All B, ((element B (powerset T_1)) => ((proper_element B (powerset T_1)) <=> (B != (union (powerset T_1)))))) (element T_0 (powerset T_1)) (-. (proper_element T_0 (powerset T_1))) (T_0 != T_1) (All A, ((union (powerset A)) = A)) ### All 10 % 5.12/5.31 12. (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (All A, ((union (powerset A)) = A)) (T_0 != T_1) (-. (proper_element T_0 (powerset T_1))) (element T_0 (powerset T_1)) ### All 11 % 5.12/5.31 13. (T_2 != T_2) ### Refl(=) % 5.12/5.31 14. (T_0 = T_1) (T_1 != T_0) ### Sym(=) % 5.12/5.31 15. ((powerset T_1) != (powerset T_0)) (T_0 = T_1) ### NotEqual 14 % 5.12/5.31 16. (-. (element T_2 (powerset T_0))) (element T_2 (powerset T_1)) (T_0 = T_1) ### P-NotP 13 15 % 5.12/5.31 17. (T_2 = (union (powerset T_0))) (T_2 != (union (powerset T_0))) ### Axiom % 5.12/5.31 18. (T_0 != T_0) ### Refl(=) % 5.12/5.31 19. (T_0 != T_2) ((union (powerset T_0)) = T_0) (T_2 = (union (powerset T_0))) ### Trans-sym 17 18 % 5.12/5.31 20. (-. (T_2 != (union (powerset T_0)))) ((union (powerset T_0)) = T_0) (T_0 != T_2) ### NotNot 19 % 5.12/5.31 21. (T_2 != T_2) ### Refl(=) % 5.12/5.31 22. (T_0 = T_1) (T_0 != T_1) ### Axiom % 5.12/5.31 23. ((powerset T_0) != (powerset T_1)) (T_0 = T_1) ### NotEqual 22 % 5.12/5.31 24. (-. (proper_element T_2 (powerset T_1))) (proper_element T_2 (powerset T_0)) (T_0 = T_1) ### P-NotP 21 23 % 5.12/5.31 25. ((proper_element T_2 (powerset T_0)) <=> (T_2 != (union (powerset T_0)))) (T_0 = T_1) (-. (proper_element T_2 (powerset T_1))) (T_0 != T_2) ((union (powerset T_0)) = T_0) ### Equiv 20 24 % 5.12/5.31 26. ((element T_2 (powerset T_0)) => ((proper_element T_2 (powerset T_0)) <=> (T_2 != (union (powerset T_0))))) ((union (powerset T_0)) = T_0) (T_0 != T_2) (-. (proper_element T_2 (powerset T_1))) (T_0 = T_1) (element T_2 (powerset T_1)) ### Imply 16 25 % 5.12/5.31 27. (All B, ((element B (powerset T_0)) => ((proper_element B (powerset T_0)) <=> (B != (union (powerset T_0)))))) (element T_2 (powerset T_1)) (T_0 = T_1) (-. (proper_element T_2 (powerset T_1))) (T_0 != T_2) ((union (powerset T_0)) = T_0) ### All 26 % 5.12/5.31 28. (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) ((union (powerset T_0)) = T_0) (T_0 != T_2) (-. (proper_element T_2 (powerset T_1))) (T_0 = T_1) (element T_2 (powerset T_1)) ### All 27 % 5.12/5.31 29. ((powerset T_1) != (powerset T_1)) ### Refl(=) % 5.12/5.31 30. (proper_element T_0 (powerset T_1)) (element T_2 (powerset T_1)) (T_0 = T_1) (-. (proper_element T_2 (powerset T_1))) ((union (powerset T_0)) = T_0) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) ### P-NotP 28 29 % 5.12/5.31 31. (All A, ((union (powerset A)) = A)) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (-. (proper_element T_2 (powerset T_1))) (T_0 = T_1) (element T_2 (powerset T_1)) (proper_element T_0 (powerset T_1)) ### All 30 % 5.12/5.31 32. ((element T_2 (powerset T_1)) /\ (-. (proper_element T_2 (powerset T_1)))) (proper_element T_0 (powerset T_1)) (T_0 = T_1) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (All A, ((union (powerset A)) = A)) ### And 31 % 5.12/5.31 33. (Ex B, ((element B (powerset T_1)) /\ (-. (proper_element B (powerset T_1))))) (All A, ((union (powerset A)) = A)) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (T_0 = T_1) (proper_element T_0 (powerset T_1)) ### Exists 32 % 5.12/5.31 34. (All A, (Ex B, ((element B (powerset A)) /\ (-. (proper_element B (powerset A)))))) (proper_element T_0 (powerset T_1)) (T_0 = T_1) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (All A, ((union (powerset A)) = A)) ### All 33 % 5.12/5.31 35. (-. (T_0 != T_1)) (All A, ((union (powerset A)) = A)) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (proper_element T_0 (powerset T_1)) (All A, (Ex B, ((element B (powerset A)) /\ (-. (proper_element B (powerset A)))))) ### NotNot 34 % 5.12/5.31 36. (-. ((proper_element T_0 (powerset T_1)) <=> (T_0 != T_1))) (All A, (Ex B, ((element B (powerset A)) /\ (-. (proper_element B (powerset A)))))) (element T_0 (powerset T_1)) (All A, ((union (powerset A)) = A)) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) ### NotEquiv 12 35 % 5.12/5.31 37. (-. ((element T_0 (powerset T_1)) => ((proper_element T_0 (powerset T_1)) <=> (T_0 != T_1)))) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (All A, ((union (powerset A)) = A)) (All A, (Ex B, ((element B (powerset A)) /\ (-. (proper_element B (powerset A)))))) ### NotImply 36 % 5.12/5.31 38. (-. (All B, ((element B (powerset T_1)) => ((proper_element B (powerset T_1)) <=> (B != T_1))))) (All A, (Ex B, ((element B (powerset A)) /\ (-. (proper_element B (powerset A)))))) (All A, ((union (powerset A)) = A)) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) ### NotAllEx 37 % 5.12/5.31 39. (-. (All A, (All B, ((element B (powerset A)) => ((proper_element B (powerset A)) <=> (B != A)))))) (All A, (All B, ((element B A) => ((proper_element B A) <=> (B != (union A)))))) (All A, ((union (powerset A)) = A)) (All A, (Ex B, ((element B (powerset A)) /\ (-. (proper_element B (powerset A)))))) ### NotAllEx 38 % 5.12/5.31 % SZS output end Proof % 5.12/5.31 (* END-PROOF *) %------------------------------------------------------------------------------