%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SET020+1 : TPTP v8.1.0. Bugfixed v5.4.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 05:38:11 EDT 2022 % Result : Theorem 9.29s 9.52s % Output : Proof 9.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SET020+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.06/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 : Mon Jul 11 01:32:47 EDT 2022 % 0.12/0.33 % CPUTime : % 9.29/9.52 % SZS status Theorem % 9.29/9.52 (* PROOF-FOUND *) % 9.29/9.52 (* BEGIN-PROOF *) % 9.29/9.52 % SZS output start Proof % 9.29/9.52 1. (member T_0 (universal_class)) (-. (member T_0 (universal_class))) ### Axiom % 9.29/9.52 2. (member T_1 (universal_class)) (-. (member T_1 (universal_class))) ### Axiom % 9.29/9.52 3. (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (T_2 != (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ### Axiom % 9.29/9.52 4. (T_2 != (ordered_pair T_0 T_1)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ### Definition-Pseudo(ordered_pair) 3 % 9.29/9.52 5. ((first T_2) != (first (ordered_pair T_0 T_1))) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ### NotEqual 4 % 9.29/9.52 6. (T_0 != T_0) ### Refl(=) % 9.29/9.52 7. (T_0 != T_0) ### Refl(=) % 9.29/9.52 8. ((first T_2) != T_0) ((first (ordered_pair T_0 T_1)) = T_0) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ### TransEq 5 6 7 % 9.29/9.52 9. (((first (ordered_pair T_0 T_1)) = T_0) /\ ((second (ordered_pair T_0 T_1)) = T_1)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((first T_2) != T_0) ### And 8 % 9.29/9.52 10. (((member T_0 (universal_class)) /\ (member T_1 (universal_class))) => (((first (ordered_pair T_0 T_1)) = T_0) /\ ((second (ordered_pair T_0 T_1)) = T_1))) ((first T_2) != T_0) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (member T_1 (universal_class)) (member T_0 (universal_class)) ### DisjTree 1 2 9 % 9.29/9.52 11. (All Y, (((member T_0 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_0 Y)) = T_0) /\ ((second (ordered_pair T_0 Y)) = Y)))) (member T_0 (universal_class)) (member T_1 (universal_class)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((first T_2) != T_0) ### All 10 % 9.29/9.52 12. (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ((first T_2) != T_0) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (member T_1 (universal_class)) (member T_0 (universal_class)) ### All 11 % 9.29/9.52 13. (member T_1 (universal_class)) (-. (member T_1 (universal_class))) ### Axiom % 9.29/9.52 14. (member T_1 (universal_class)) (-. (member T_1 (universal_class))) ### Axiom % 9.29/9.52 15. (member T_0 (universal_class)) (-. (member T_0 (universal_class))) ### Axiom % 9.29/9.52 16. (member T_1 (universal_class)) (-. (member T_1 (universal_class))) ### Axiom % 9.29/9.52 17. ((second T_2) != (second (ordered_pair T_0 T_1))) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ### NotEqual 4 % 9.29/9.52 18. ((first (ordered_pair T_1 T_1)) = T_1) (T_1 != (first (ordered_pair T_1 T_1))) ### Sym(=) % 9.29/9.52 19. ((first (ordered_pair T_1 T_1)) = T_1) (T_1 != (first (ordered_pair T_1 T_1))) ### Sym(=) % 9.29/9.52 20. ((second T_2) != (first (ordered_pair T_1 T_1))) ((second (ordered_pair T_0 T_1)) = T_1) ((first (ordered_pair T_1 T_1)) = T_1) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ### TransEq 17 18 19 % 9.29/9.52 21. (((first (ordered_pair T_0 T_1)) = T_0) /\ ((second (ordered_pair T_0 T_1)) = T_1)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((first (ordered_pair T_1 T_1)) = T_1) ((second T_2) != (first (ordered_pair T_1 T_1))) ### And 20 % 9.29/9.52 22. (((member T_0 (universal_class)) /\ (member T_1 (universal_class))) => (((first (ordered_pair T_0 T_1)) = T_0) /\ ((second (ordered_pair T_0 T_1)) = T_1))) ((second T_2) != (first (ordered_pair T_1 T_1))) ((first (ordered_pair T_1 T_1)) = T_1) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (member T_1 (universal_class)) (member T_0 (universal_class)) ### DisjTree 15 16 21 % 9.29/9.52 23. (All Y, (((member T_0 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_0 Y)) = T_0) /\ ((second (ordered_pair T_0 Y)) = Y)))) (member T_0 (universal_class)) (member T_1 (universal_class)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((first (ordered_pair T_1 T_1)) = T_1) ((second T_2) != (first (ordered_pair T_1 T_1))) ### All 22 % 9.29/9.52 24. (T_1 != T_1) ### Refl(=) % 9.29/9.52 25. (T_1 != T_1) ### Refl(=) % 9.29/9.52 26. ((second T_2) != T_1) ((first (ordered_pair T_1 T_1)) = T_1) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (member T_1 (universal_class)) (member T_0 (universal_class)) (All Y, (((member T_0 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_0 Y)) = T_0) /\ ((second (ordered_pair T_0 Y)) = Y)))) ### TransEq 23 24 25 % 9.29/9.52 27. (((first (ordered_pair T_1 T_1)) = T_1) /\ ((second (ordered_pair T_1 T_1)) = T_1)) (All Y, (((member T_0 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_0 Y)) = T_0) /\ ((second (ordered_pair T_0 Y)) = Y)))) (member T_0 (universal_class)) (member T_1 (universal_class)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((second T_2) != T_1) ### And 26 % 9.29/9.52 28. (((member T_1 (universal_class)) /\ (member T_1 (universal_class))) => (((first (ordered_pair T_1 T_1)) = T_1) /\ ((second (ordered_pair T_1 T_1)) = T_1))) ((second T_2) != T_1) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (member T_0 (universal_class)) (All Y, (((member T_0 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_0 Y)) = T_0) /\ ((second (ordered_pair T_0 Y)) = Y)))) (member T_1 (universal_class)) ### DisjTree 13 14 27 % 9.29/9.52 29. (All Y, (((member T_1 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_1 Y)) = T_1) /\ ((second (ordered_pair T_1 Y)) = Y)))) (member T_1 (universal_class)) (All Y, (((member T_0 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_0 Y)) = T_0) /\ ((second (ordered_pair T_0 Y)) = Y)))) (member T_0 (universal_class)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((second T_2) != T_1) ### All 28 % 9.29/9.52 30. (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ((second T_2) != T_1) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (member T_0 (universal_class)) (member T_1 (universal_class)) (All Y, (((member T_1 (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair T_1 Y)) = T_1) /\ ((second (ordered_pair T_1 Y)) = Y)))) ### All 29 % 9.29/9.52 31. (member T_1 (universal_class)) (member T_0 (universal_class)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) ((second T_2) != T_1) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ### All 30 % 9.29/9.52 32. (-. (((first T_2) = T_0) /\ ((second T_2) = T_1))) (member T_0 (universal_class)) (member T_1 (universal_class)) (T_2 = (unordered_pair (singleton T_0) (unordered_pair T_0 (singleton T_1)))) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ### NotAnd 12 31 % 9.29/9.52 33. (T_2 = (ordered_pair T_0 T_1)) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) (member T_1 (universal_class)) (member T_0 (universal_class)) (-. (((first T_2) = T_0) /\ ((second T_2) = T_1))) ### Definition-Pseudo(ordered_pair) 32 % 9.29/9.52 34. (-. (((member T_0 (universal_class)) /\ ((member T_1 (universal_class)) /\ (T_2 = (ordered_pair T_0 T_1)))) => (((first T_2) = T_0) /\ ((second T_2) = T_1)))) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ### ConjTree 33 % 9.29/9.52 35. (-. (All X, (((member T_0 (universal_class)) /\ ((member T_1 (universal_class)) /\ (X = (ordered_pair T_0 T_1)))) => (((first X) = T_0) /\ ((second X) = T_1))))) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ### NotAllEx 34 % 9.29/9.53 36. (-. (All V, (All X, (((member T_0 (universal_class)) /\ ((member V (universal_class)) /\ (X = (ordered_pair T_0 V)))) => (((first X) = T_0) /\ ((second X) = V)))))) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ### NotAllEx 35 % 9.29/9.53 37. (-. (All U, (All V, (All X, (((member U (universal_class)) /\ ((member V (universal_class)) /\ (X = (ordered_pair U V)))) => (((first X) = U) /\ ((second X) = V))))))) (All X, (All Y, (((member X (universal_class)) /\ (member Y (universal_class))) => (((first (ordered_pair X Y)) = X) /\ ((second (ordered_pair X Y)) = Y))))) ### NotAllEx 36 % 9.29/9.53 % SZS output end Proof % 9.29/9.53 (* END-PROOF *) %------------------------------------------------------------------------------