%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU374+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 : n029.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 3.16s 3.33s % Output : Proof 3.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n029.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.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jun 19 00:34:59 EDT 2022 % 0.13/0.34 % CPUTime : % 3.16/3.33 % SZS status Theorem % 3.16/3.33 (* PROOF-FOUND *) % 3.16/3.33 (* BEGIN-PROOF *) % 3.16/3.33 % SZS output start Proof % 3.16/3.33 1. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 3.16/3.33 2. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 3.16/3.33 3. (-. (rel_str T_1)) (rel_str T_1) ### Axiom % 3.16/3.33 4. ((net_str T_1 T_0) => (rel_str T_1)) (-. (rel_str T_1)) (net_str T_1 T_0) ### Imply 2 3 % 3.16/3.33 5. (All B, ((net_str B T_0) => (rel_str B))) (net_str T_1 T_0) (-. (rel_str T_1)) ### All 4 % 3.16/3.33 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 % 3.16/3.33 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 % 3.16/3.33 8. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 3.16/3.33 9. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 3.16/3.33 10. (one_sorted_str T_0) (-. (one_sorted_str T_0)) ### Axiom % 3.16/3.33 11. (net_str T_1 T_0) (-. (net_str T_1 T_0)) ### Axiom % 3.16/3.33 12. (subnetstr T_2 T_0 T_1) (-. (subnetstr T_2 T_0 T_1)) ### Axiom % 3.16/3.33 13. (-. (net_str T_2 T_0)) (net_str T_2 T_0) ### Axiom % 3.16/3.33 14. ((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 12 13 % 3.16/3.33 15. (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 14 % 3.16/3.33 16. (((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 10 11 15 % 3.16/3.33 17. (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 16 % 3.16/3.33 18. (subnetstr T_2 T_0 T_1) (-. (subnetstr T_2 T_0 T_1)) ### Axiom % 3.16/3.33 19. (-. (subrelstr T_2 T_1)) (subrelstr T_2 T_1) ### Axiom % 3.16/3.33 20. ((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 19 % 3.16/3.33 21. ((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 18 20 % 3.16/3.33 22. ((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 17 21 % 3.16/3.33 23. (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 22 % 3.16/3.33 24. ((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 9 23 % 3.16/3.33 25. (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 24 % 3.16/3.33 26. (element T_3 (the_carrier T_1)) (-. (element T_3 (the_carrier T_1))) ### Axiom % 3.16/3.33 27. (element T_4 (the_carrier T_1)) (-. (element T_4 (the_carrier T_1))) ### Axiom % 3.16/3.33 28. (element T_5 (the_carrier T_2)) (-. (element T_5 (the_carrier T_2))) ### Axiom % 3.16/3.33 29. (element T_6 (the_carrier T_2)) (-. (element T_6 (the_carrier T_2))) ### Axiom % 3.16/3.33 30. (T_3 = T_5) (T_5 != T_3) ### Sym(=) % 3.16/3.33 31. (T_4 = T_6) (T_6 != T_4) ### Sym(=) % 3.16/3.33 32. (related T_2 T_5 T_6) (-. (related T_2 T_5 T_6)) ### Axiom % 3.16/3.33 33. (-. (related T_1 T_3 T_4)) (related T_1 T_3 T_4) ### Axiom % 3.16/3.33 34. ((element T_6 (the_carrier T_2)) => (((T_5 = T_3) /\ ((T_6 = T_4) /\ (related T_2 T_5 T_6))) => (related T_1 T_3 T_4))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) ### DisjTree 29 30 31 32 33 % 3.16/3.33 35. (All F, ((element F (the_carrier T_2)) => (((T_5 = T_3) /\ ((F = T_4) /\ (related T_2 T_5 F))) => (related T_1 T_3 T_4)))) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) ### All 34 % 3.16/3.33 36. ((element T_5 (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((T_5 = T_3) /\ ((F = T_4) /\ (related T_2 T_5 F))) => (related T_1 T_3 T_4))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) ### Imply 28 35 % 3.16/3.33 37. (All E, ((element E (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((E = T_3) /\ ((F = T_4) /\ (related T_2 E F))) => (related T_1 T_3 T_4)))))) (element T_5 (the_carrier T_2)) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) ### All 36 % 3.16/3.33 38. ((element T_4 (the_carrier T_1)) => (All E, ((element E (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((E = T_3) /\ ((F = T_4) /\ (related T_2 E F))) => (related T_1 T_3 T_4))))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) ### Imply 27 37 % 3.16/3.33 39. (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((E = T_3) /\ ((F = D) /\ (related T_2 E F))) => (related T_1 T_3 D)))))))) (element T_4 (the_carrier T_1)) (element T_5 (the_carrier T_2)) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) ### All 38 % 3.16/3.33 40. ((element T_3 (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((E = T_3) /\ ((F = D) /\ (related T_2 E F))) => (related T_1 T_3 D))))))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier T_1)) ### Imply 26 39 % 3.16/3.33 41. (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((E = C) /\ ((F = D) /\ (related T_2 E F))) => (related T_1 C D)))))))))) (element T_3 (the_carrier T_1)) (element T_4 (the_carrier T_1)) (element T_5 (the_carrier T_2)) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) ### All 40 % 3.16/3.33 42. ((subrelstr T_2 T_1) => (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_2)) => (All F, ((element F (the_carrier T_2)) => (((E = C) /\ ((F = D) /\ (related T_2 E F))) => (related T_1 C D))))))))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier 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) (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))))))))) ### Imply 25 41 % 3.25/3.42 43. (All B, ((subrelstr B T_1) => (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related T_1 C D)))))))))))) (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) (element T_3 (the_carrier T_1)) (element T_4 (the_carrier T_1)) (element T_5 (the_carrier T_2)) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) ### All 42 % 3.25/3.42 44. ((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)))))))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier 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) (All B, ((subrelstr B T_1) => (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related T_1 C D)))))))))))) (one_sorted_str T_0) ### Imply 8 43 % 3.25/3.42 45. (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) (All B, ((subrelstr B T_1) => (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related T_1 C D)))))))))))) (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) (element T_3 (the_carrier T_1)) (element T_4 (the_carrier T_1)) (element T_5 (the_carrier T_2)) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) ### All 44 % 3.25/3.42 46. (All A, (All B, (((one_sorted_str A) /\ (net_str B A)) => (All C, ((subnetstr C A B) => (net_str C A)))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier T_1)) (subnetstr T_2 T_0 T_1) (net_str T_1 T_0) (All B, ((subrelstr B T_1) => (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related T_1 C D)))))))))))) (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 45 % 3.25/3.42 47. ((rel_str T_1) => (All B, ((subrelstr B T_1) => (All C, ((element C (the_carrier T_1)) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related T_1 C D))))))))))))) (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))))))))))) (subnetstr T_2 T_0 T_1) (element T_3 (the_carrier T_1)) (element T_4 (the_carrier T_1)) (element T_5 (the_carrier T_2)) (element T_6 (the_carrier T_2)) (T_3 = T_5) (T_4 = T_6) (related T_2 T_5 T_6) (-. (related T_1 T_3 T_4)) (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 46 % 3.25/3.42 48. (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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)))))) (-. (related T_1 T_3 T_4)) (related T_2 T_5 T_6) (T_4 = T_6) (T_3 = T_5) (element T_6 (the_carrier T_2)) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier T_1)) (subnetstr T_2 T_0 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 47 % 3.25/3.42 49. (-. ((element T_6 (the_carrier T_2)) => (((T_3 = T_5) /\ ((T_4 = T_6) /\ (related T_2 T_5 T_6))) => (related T_1 T_3 T_4)))) (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))))))))))) (subnetstr T_2 T_0 T_1) (element T_3 (the_carrier T_1)) (element T_4 (the_carrier T_1)) (element T_5 (the_carrier T_2)) (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, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### ConjTree 48 % 3.25/3.42 50. (-. (All G, ((element G (the_carrier T_2)) => (((T_3 = T_5) /\ ((T_4 = G) /\ (related T_2 T_5 G))) => (related T_1 T_3 T_4))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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)))))) (element T_5 (the_carrier T_2)) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier T_1)) (subnetstr T_2 T_0 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))))))))))) ### NotAllEx 49 % 3.25/3.42 51. (-. ((element T_5 (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((T_3 = T_5) /\ ((T_4 = G) /\ (related T_2 T_5 G))) => (related T_1 T_3 T_4)))))) (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))))))))))) (subnetstr T_2 T_0 T_1) (element T_3 (the_carrier T_1)) (element T_4 (the_carrier 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))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### NotImply 50 % 3.25/3.44 52. (-. (All F, ((element F (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((T_3 = F) /\ ((T_4 = G) /\ (related T_2 F G))) => (related T_1 T_3 T_4))))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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)))))) (element T_4 (the_carrier T_1)) (element T_3 (the_carrier T_1)) (subnetstr T_2 T_0 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))))))))))) ### NotAllEx 51 % 3.25/3.44 53. (-. ((element T_4 (the_carrier T_1)) => (All F, ((element F (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((T_3 = F) /\ ((T_4 = G) /\ (related T_2 F G))) => (related T_1 T_3 T_4)))))))) (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))))))))))) (subnetstr T_2 T_0 T_1) (element T_3 (the_carrier 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))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### NotImply 52 % 3.25/3.44 54. (-. (All E, ((element E (the_carrier T_1)) => (All F, ((element F (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((T_3 = F) /\ ((E = G) /\ (related T_2 F G))) => (related T_1 T_3 E))))))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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)))))) (element T_3 (the_carrier T_1)) (subnetstr T_2 T_0 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))))))))))) ### NotAllEx 53 % 3.25/3.44 55. (-. ((element T_3 (the_carrier T_1)) => (All E, ((element E (the_carrier T_1)) => (All F, ((element F (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((T_3 = F) /\ ((E = G) /\ (related T_2 F G))) => (related T_1 T_3 E)))))))))) (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))))))))))) (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))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### NotImply 54 % 3.25/3.44 56. (-. (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_1)) => (All F, ((element F (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((D = F) /\ ((E = G) /\ (related T_2 F G))) => (related T_1 D E))))))))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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) (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 55 % 3.25/3.44 57. (-. ((subnetstr T_2 T_0 T_1) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_1)) => (All F, ((element F (the_carrier T_2)) => (All G, ((element G (the_carrier T_2)) => (((D = F) /\ ((E = G) /\ (related T_2 F G))) => (related T_1 D E)))))))))))) (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, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### NotImply 56 % 3.25/3.44 58. (-. (All C, ((subnetstr C T_0 T_1) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_1)) => (All F, ((element F (the_carrier C)) => (All G, ((element G (the_carrier C)) => (((D = F) /\ ((E = G) /\ (related C F G))) => (related T_1 D E))))))))))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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 57 % 3.25/3.44 59. (-. ((net_str T_1 T_0) => (All C, ((subnetstr C T_0 T_1) => (All D, ((element D (the_carrier T_1)) => (All E, ((element E (the_carrier T_1)) => (All F, ((element F (the_carrier C)) => (All G, ((element G (the_carrier C)) => (((D = F) /\ ((E = G) /\ (related C F G))) => (related T_1 D E)))))))))))))) (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, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### NotImply 58 % 3.25/3.45 60. (-. (All B, ((net_str B T_0) => (All C, ((subnetstr C T_0 B) => (All D, ((element D (the_carrier B)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier C)) => (All G, ((element G (the_carrier C)) => (((D = F) /\ ((E = G) /\ (related C F G))) => (related B D E))))))))))))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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 59 % 3.25/3.45 61. (-. ((one_sorted_str T_0) => (All B, ((net_str B T_0) => (All C, ((subnetstr C T_0 B) => (All D, ((element D (the_carrier B)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier C)) => (All G, ((element G (the_carrier C)) => (((D = F) /\ ((E = G) /\ (related C F G))) => (related B D E)))))))))))))))) (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, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) ### NotImply 60 % 3.25/3.45 62. (-. (All A, ((one_sorted_str A) => (All B, ((net_str B A) => (All C, ((subnetstr C A B) => (All D, ((element D (the_carrier B)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier C)) => (All G, ((element G (the_carrier C)) => (((D = F) /\ ((E = G) /\ (related C F G))) => (related B D E))))))))))))))))) (All A, ((rel_str A) => (All B, ((subrelstr B A) => (All C, ((element C (the_carrier A)) => (All D, ((element D (the_carrier A)) => (All E, ((element E (the_carrier B)) => (All F, ((element F (the_carrier B)) => (((E = C) /\ ((F = D) /\ (related B E F))) => (related A C D)))))))))))))) (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 61 % 3.25/3.45 % SZS output end Proof % 3.25/3.45 (* END-PROOF *) %------------------------------------------------------------------------------