%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU189+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 : n003.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:49:03 EDT 2022 % Result : Theorem 0.19s 0.41s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU189+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n003.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 20 11:18:44 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.41 % SZS status Theorem % 0.19/0.41 (* PROOF-FOUND *) % 0.19/0.41 (* BEGIN-PROOF *) % 0.19/0.41 % SZS output start Proof % 0.19/0.41 1. ((relation_rng T_0) != (empty_set)) ((relation_rng T_0) = (empty_set)) ### Axiom % 0.19/0.41 2. ((relation_dom T_0) != (empty_set)) ((relation_dom T_0) = (empty_set)) ### Axiom % 0.19/0.41 3. (-. (((relation_dom T_0) = (empty_set)) <=> ((relation_rng T_0) = (empty_set)))) ((relation_dom T_0) != (empty_set)) ((relation_rng T_0) != (empty_set)) ### NotEquiv 1 2 % 0.19/0.41 4. (T_0 = (empty_set)) (T_0 != (empty_set)) ### Axiom % 0.19/0.41 5. ((relation_dom T_0) != (relation_dom (empty_set))) (T_0 = (empty_set)) ### NotEqual 4 % 0.19/0.41 6. ((empty_set) != (empty_set)) ### NotEqual % 0.19/0.41 7. ((relation_dom T_0) != (empty_set)) ((relation_dom (empty_set)) = (empty_set)) (T_0 = (empty_set)) ### Trans 5 6 % 0.19/0.41 8. (T_0 = (empty_set)) (T_0 != (empty_set)) ### Axiom % 0.19/0.41 9. ((relation_rng T_0) != (relation_rng (empty_set))) (T_0 = (empty_set)) ### NotEqual 8 % 0.19/0.41 10. ((relation_rng T_0) != (empty_set)) ((relation_rng (empty_set)) = (empty_set)) (T_0 = (empty_set)) ### Trans 9 6 % 0.19/0.41 11. (-. (((relation_dom T_0) = (empty_set)) <=> ((relation_rng T_0) = (empty_set)))) ((relation_rng (empty_set)) = (empty_set)) (T_0 = (empty_set)) ((relation_dom (empty_set)) = (empty_set)) ### NotEquiv 7 10 % 0.19/0.41 12. (relation T_0) ((relation_dom (empty_set)) = (empty_set)) ((relation_rng (empty_set)) = (empty_set)) (-. (((relation_dom T_0) = (empty_set)) <=> ((relation_rng T_0) = (empty_set)))) ### Extension/test/t64_relat_1 3 11 % 0.19/0.41 13. (-. ((relation T_0) => (((relation_dom T_0) = (empty_set)) <=> ((relation_rng T_0) = (empty_set))))) ((relation_rng (empty_set)) = (empty_set)) ((relation_dom (empty_set)) = (empty_set)) ### NotImply 12 % 0.19/0.41 14. (-. (All A, ((relation A) => (((relation_dom A) = (empty_set)) <=> ((relation_rng A) = (empty_set)))))) ((relation_dom (empty_set)) = (empty_set)) ((relation_rng (empty_set)) = (empty_set)) ### NotAllEx 13 % 0.19/0.41 15. (((relation_dom (empty_set)) = (empty_set)) /\ ((relation_rng (empty_set)) = (empty_set))) (-. (All A, ((relation A) => (((relation_dom A) = (empty_set)) <=> ((relation_rng A) = (empty_set)))))) ### And 14 % 0.19/0.41 % SZS output end Proof % 0.19/0.41 (* END-PROOF *) %------------------------------------------------------------------------------