%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU373+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 : n011.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:39 EDT 2022 % Result : Theorem 2.75s 2.94s % Output : Proof 2.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEU373+1 : TPTP v8.1.0. Released v3.3.0. % 0.00/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.32 % Computer : n011.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % 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 Jun 20 01:59:54 EDT 2022 % 0.12/0.33 % CPUTime : % 2.75/2.94 % SZS status Theorem % 2.75/2.94 (* PROOF-FOUND *) % 2.75/2.94 (* BEGIN-PROOF *) % 2.75/2.94 % SZS output start Proof % 2.75/2.94 1. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 2.75/2.94 2. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 2.75/2.94 3. (-. (rel_str T_1)) (rel_str T_1) ### Axiom % 2.75/2.94 4. ((net_str T_1 T_0) => (rel_str T_1)) (-. (rel_str T_1)) (net_str T_1 T_0) ### Imply 2 3 % 2.75/2.94 5. (All B, ((net_str B T_0) => (rel_str B))) (net_str T_1 T_0) (-. (rel_str T_1)) ### All 4 % 2.75/2.94 6. ((one_sorted_str T_0) => (All B, ((net_str B T_0) => (rel_str B)))) (-. (rel_str T_1)) (net_str T_1 T_0) (one_sorted_str T_0) ### Imply 1 5 % 2.75/2.94 7. (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (one_sorted_str T_0) (net_str T_1 T_0) (-. (rel_str T_1)) ### All 6 % 2.75/2.94 8. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 2.75/2.94 9. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 2.75/2.94 10. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 2.75/2.94 11. (subnetstr T_2 T_0 T_1) (-. (subnetstr T_2 T_0 T_1)) ### Axiom % 2.75/2.94 12. (-. (net_str T_2 T_0)) (net_str T_2 T_0) ### Axiom % 2.75/2.94 13. ((subnetstr T_2 T_0 T_1) => (net_str T_2 T_0)) (-. (net_str T_2 T_0)) (subnetstr T_2 T_0 T_1) ### Imply 11 12 % 2.75/2.94 14. (All C, ((subnetstr C T_0 T_1) => (net_str C T_0))) (subnetstr T_2 T_0 T_1) (-. (net_str T_2 T_0)) ### All 13 % 2.75/2.94 15. (((one_sorted_str T_0) /\ (net_str T_1 T_0)) => (All C, ((subnetstr C T_0 T_1) => (net_str C T_0)))) (-. (net_str T_2 T_0)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (one_sorted_str T_0) ### DisjTree 9 10 14 % 2.75/2.94 16. (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (one_sorted_str T_0) (net_str T_1 T_0) (subnetstr T_2 T_0 T_1) (-. (net_str T_2 T_0)) ### All 15 % 2.75/2.94 17. (-. (rel_str T_2)) (rel_str T_2) ### Axiom % 2.75/2.94 18. ((net_str T_2 T_0) => (rel_str T_2)) (-. (rel_str T_2)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (one_sorted_str T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) ### Imply 16 17 % 2.75/2.94 19. (All B, ((net_str B T_0) => (rel_str B))) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (one_sorted_str T_0) (net_str T_1 T_0) (subnetstr T_2 T_0 T_1) (-. (rel_str T_2)) ### All 18 % 2.75/2.94 20. ((one_sorted_str T_0) => (All B, ((net_str B T_0) => (rel_str B)))) (-. (rel_str T_2)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (one_sorted_str T_0) ### Imply 8 19 % 2.75/2.94 21. (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (one_sorted_str T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (net_str T_1 T_0) (subnetstr T_2 T_0 T_1) (-. (rel_str T_2)) ### All 20 % 2.75/2.94 22. (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (-. (rel_str T_2)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (one_sorted_str T_0) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) ### All 21 % 2.75/2.94 23. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 2.75/2.94 24. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 2.75/2.94 25. (subnetstr T_2 T_0 T_1) (-. (subnetstr T_2 T_0 T_1)) ### Axiom % 2.75/2.94 26. (-. (subrelstr T_2 T_1)) (subrelstr T_2 T_1) ### Axiom % 2.75/2.94 27. ((subrelstr T_2 T_1) /\ ((the_mapping T_0 T_2) = (relation_dom_restr_as_relation_of (the_carrier T_1) (the_carrier T_0) (the_mapping T_0 T_1) (the_carrier T_2)))) (-. (subrelstr T_2 T_1)) ### And 26 % 2.75/2.94 28. ((subnetstr T_2 T_0 T_1) <=> ((subrelstr T_2 T_1) /\ ((the_mapping T_0 T_2) = (relation_dom_restr_as_relation_of (the_carrier T_1) (the_carrier T_0) (the_mapping T_0 T_1) (the_carrier T_2))))) (-. (subrelstr T_2 T_1)) (subnetstr T_2 T_0 T_1) ### Equiv 25 27 % 2.75/2.94 29. ((net_str T_2 T_0) => ((subnetstr T_2 T_0 T_1) <=> ((subrelstr T_2 T_1) /\ ((the_mapping T_0 T_2) = (relation_dom_restr_as_relation_of (the_carrier T_1) (the_carrier T_0) (the_mapping T_0 T_1) (the_carrier T_2)))))) (-. (subrelstr T_2 T_1)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (one_sorted_str T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) ### Imply 16 28 % 2.75/2.94 30. (All C, ((net_str C T_0) => ((subnetstr C T_0 T_1) <=> ((subrelstr C T_1) /\ ((the_mapping T_0 C) = (relation_dom_restr_as_relation_of (the_carrier T_1) (the_carrier T_0) (the_mapping T_0 T_1) (the_carrier C))))))) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (one_sorted_str T_0) (net_str T_1 T_0) (subnetstr T_2 T_0 T_1) (-. (subrelstr T_2 T_1)) ### All 29 % 2.75/2.94 31. ((net_str T_1 T_0) => (All C, ((net_str C T_0) => ((subnetstr C T_0 T_1) <=> ((subrelstr C T_1) /\ ((the_mapping T_0 C) = (relation_dom_restr_as_relation_of (the_carrier T_1) (the_carrier T_0) (the_mapping T_0 T_1) (the_carrier C)))))))) (-. (subrelstr T_2 T_1)) (subnetstr T_2 T_0 T_1) (one_sorted_str T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (net_str T_1 T_0) ### Imply 24 30 % 2.75/2.94 32. (All B, ((net_str B T_0) => (All C, ((net_str C T_0) => ((subnetstr C T_0 B) <=> ((subrelstr C B) /\ ((the_mapping T_0 C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier T_0) (the_mapping T_0 B) (the_carrier C))))))))) (net_str T_1 T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (one_sorted_str T_0) (subnetstr T_2 T_0 T_1) (-. (subrelstr T_2 T_1)) ### All 31 % 2.75/2.94 33. ((one_sorted_str T_0) => (All B, ((net_str B T_0) => (All C, ((net_str C T_0) => ((subnetstr C T_0 B) <=> ((subrelstr C B) /\ ((the_mapping T_0 C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier T_0) (the_mapping T_0 B) (the_carrier C)))))))))) (-. (subrelstr T_2 T_1)) (subnetstr T_2 T_0 T_1) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (net_str T_1 T_0) (one_sorted_str T_0) ### Imply 23 32 % 2.75/2.94 34. (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (one_sorted_str T_0) (net_str T_1 T_0) (All B, (((one_sorted_str T_0) /\ (net_str B T_0)) => (All C, ((subnetstr C T_0 B) => (net_str C T_0))))) (subnetstr T_2 T_0 T_1) (-. (subrelstr T_2 T_1)) ### All 33 % 2.75/2.94 35. (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (-. (subrelstr T_2 T_1)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (one_sorted_str T_0) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) ### All 34 % 2.75/2.94 36. (-. (subset (the_carrier T_2) (the_carrier T_1))) (subset (the_carrier T_2) (the_carrier T_1)) ### Axiom % 2.75/2.94 37. ((subset (the_carrier T_2) (the_carrier T_1)) /\ (subset (the_InternalRel T_2) (the_InternalRel T_1))) (-. (subset (the_carrier T_2) (the_carrier T_1))) ### And 36 % 2.75/2.94 38. ((subrelstr T_2 T_1) <=> ((subset (the_carrier T_2) (the_carrier T_1)) /\ (subset (the_InternalRel T_2) (the_InternalRel T_1)))) (-. (subset (the_carrier T_2) (the_carrier T_1))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (one_sorted_str T_0) (net_str T_1 T_0) (subnetstr T_2 T_0 T_1) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) ### Equiv 35 37 % 2.75/2.94 39. ((rel_str T_2) => ((subrelstr T_2 T_1) <=> ((subset (the_carrier T_2) (the_carrier T_1)) /\ (subset (the_InternalRel T_2) (the_InternalRel T_1))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (-. (subset (the_carrier T_2) (the_carrier T_1))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (one_sorted_str T_0) (net_str T_1 T_0) (subnetstr T_2 T_0 T_1) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) ### Imply 22 38 % 2.75/2.95 40. (All B, ((rel_str B) => ((subrelstr B T_1) <=> ((subset (the_carrier B) (the_carrier T_1)) /\ (subset (the_InternalRel B) (the_InternalRel T_1)))))) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (one_sorted_str T_0) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (-. (subset (the_carrier T_2) (the_carrier T_1))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) ### All 39 % 2.75/2.95 41. ((rel_str T_1) => (All B, ((rel_str B) => ((subrelstr B T_1) <=> ((subset (the_carrier B) (the_carrier T_1)) /\ (subset (the_InternalRel B) (the_InternalRel T_1))))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (-. (subset (the_carrier T_2) (the_carrier T_1))) (subnetstr T_2 T_0 T_1) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (net_str T_1 T_0) (one_sorted_str T_0) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) ### Imply 7 40 % 2.75/2.95 42. (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (one_sorted_str T_0) (net_str T_1 T_0) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (subnetstr T_2 T_0 T_1) (-. (subset (the_carrier T_2) (the_carrier T_1))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) ### All 41 % 2.75/2.95 43. (-. ((subnetstr T_2 T_0 T_1) => (subset (the_carrier T_2) (the_carrier T_1)))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (net_str T_1 T_0) (one_sorted_str T_0) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) ### NotImply 42 % 2.75/2.95 44. (-. (All C, ((subnetstr C T_0 T_1) => (subset (the_carrier C) (the_carrier T_1))))) (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (one_sorted_str T_0) (net_str T_1 T_0) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) ### NotAllEx 43 % 2.75/2.95 45. (-. ((net_str T_1 T_0) => (All C, ((subnetstr C T_0 T_1) => (subset (the_carrier C) (the_carrier T_1)))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (one_sorted_str T_0) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) ### NotImply 44 % 2.75/2.95 46. (-. (All B, ((net_str B T_0) => (All C, ((subnetstr C T_0 B) => (subset (the_carrier C) (the_carrier B))))))) (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (one_sorted_str T_0) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) ### NotAllEx 45 % 2.75/2.95 47. (-. ((one_sorted_str T_0) => (All B, ((net_str B T_0) => (All C, ((subnetstr C T_0 B) => (subset (the_carrier C) (the_carrier B)))))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) ### NotImply 46 % 2.75/2.95 48. (-. (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((subnetstr C A B) => (subset (the_carrier C) (the_carrier B))))))))) (All A, ((rel_str A) => (All B, ((rel_str B) => ((subrelstr B A) <=> ((subset (the_carrier B) (the_carrier A)) /\ (subset (the_InternalRel B) (the_InternalRel A)))))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (rel_str B))))) (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((net_str C A) => ((subnetstr C A B) <=> ((subrelstr C B) /\ ((the_mapping A C) = (relation_dom_restr_as_relation_of (the_carrier B) (the_carrier A) (the_mapping A B) (the_carrier C))))))))))) ### NotAllEx 47 % 2.75/2.95 % SZS output end Proof % 2.75/2.95 (* END-PROOF *) %------------------------------------------------------------------------------