%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWB005+2 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n027.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 19:22:05 EDT 2022 % Result : Theorem 0.18s 0.40s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWB005+2 : TPTP v8.1.0. Released v5.2.0. % 0.12/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n027.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 : Wed Jun 1 06:13:03 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.40 % SZS status Theorem % 0.18/0.40 (* PROOF-FOUND *) % 0.18/0.40 (* BEGIN-PROOF *) % 0.18/0.40 % SZS output start Proof % 0.18/0.40 1. (-. (icext (uri_rdfs_Resource) (uri_ex_s))) (icext (uri_rdfs_Resource) (uri_ex_s)) ### Axiom % 0.18/0.40 2. (ir (uri_ex_s)) (-. (icext (uri_rdfs_Resource) (uri_ex_s))) ### Definition-Pseudo(ir) 1 % 0.18/0.40 3. (All X, (ir X)) (-. (icext (uri_rdfs_Resource) (uri_ex_s))) ### All 2 % 0.18/0.40 4. (-. (iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource))) (iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource)) ### Axiom % 0.18/0.40 5. ((iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource)) <=> (icext (uri_rdfs_Resource) (uri_ex_s))) (-. (iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource))) (All X, (ir X)) ### Equiv 3 4 % 0.18/0.40 6. (All C, ((iext (uri_rdf_type) (uri_ex_s) C) <=> (icext C (uri_ex_s)))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource))) ### All 5 % 0.18/0.40 7. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource))) (All X, (ir X)) ### All 6 % 0.18/0.40 8. (-. (ir (uri_ex_s))) (All X, (ir X)) ### Definition-Pseudo(ir) 3 % 0.18/0.40 9. (-. (icext (uri_owl_Thing) (uri_ex_s))) (icext (uri_owl_Thing) (uri_ex_s)) ### Axiom % 0.18/0.40 10. ((icext (uri_owl_Thing) (uri_ex_s)) <=> (ir (uri_ex_s))) (-. (icext (uri_owl_Thing) (uri_ex_s))) (All X, (ir X)) ### Equiv 8 9 % 0.18/0.40 11. (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (icext (uri_owl_Thing) (uri_ex_s))) ### All 10 % 0.18/0.40 12. (-. (iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing))) (iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing)) ### Axiom % 0.18/0.40 13. ((iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing)) <=> (icext (uri_owl_Thing) (uri_ex_s))) (-. (iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### Equiv 11 12 % 0.18/0.40 14. (All C, ((iext (uri_rdf_type) (uri_ex_s) C) <=> (icext C (uri_ex_s)))) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing))) ### All 13 % 0.18/0.40 15. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### All 14 % 0.18/0.40 16. (-. (icext (uri_rdfs_Resource) (uri_ex_p))) (icext (uri_rdfs_Resource) (uri_ex_p)) ### Axiom % 0.18/0.40 17. (ir (uri_ex_p)) (-. (icext (uri_rdfs_Resource) (uri_ex_p))) ### Definition-Pseudo(ir) 16 % 0.18/0.40 18. (All X, (ir X)) (-. (icext (uri_rdfs_Resource) (uri_ex_p))) ### All 17 % 0.18/0.40 19. (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource))) (iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource)) ### Axiom % 0.18/0.40 20. ((iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource)) <=> (icext (uri_rdfs_Resource) (uri_ex_p))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource))) (All X, (ir X)) ### Equiv 18 19 % 0.18/0.40 21. (All C, ((iext (uri_rdf_type) (uri_ex_p) C) <=> (icext C (uri_ex_p)))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource))) ### All 20 % 0.18/0.40 22. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource))) (All X, (ir X)) ### All 21 % 0.18/0.40 23. (-. (ir (uri_ex_p))) (All X, (ir X)) ### Definition-Pseudo(ir) 18 % 0.18/0.40 24. (-. (icext (uri_owl_Thing) (uri_ex_p))) (icext (uri_owl_Thing) (uri_ex_p)) ### Axiom % 0.18/0.40 25. ((icext (uri_owl_Thing) (uri_ex_p)) <=> (ir (uri_ex_p))) (-. (icext (uri_owl_Thing) (uri_ex_p))) (All X, (ir X)) ### Equiv 23 24 % 0.18/0.40 26. (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (icext (uri_owl_Thing) (uri_ex_p))) ### All 25 % 0.18/0.40 27. (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing))) (iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing)) ### Axiom % 0.18/0.40 28. ((iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing)) <=> (icext (uri_owl_Thing) (uri_ex_p))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### Equiv 26 27 % 0.18/0.40 29. (All C, ((iext (uri_rdf_type) (uri_ex_p) C) <=> (icext C (uri_ex_p)))) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing))) ### All 28 % 0.18/0.40 30. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### All 29 % 0.18/0.40 31. (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (-. (iext (uri_ex_p) (uri_ex_s) (uri_ex_o))) ### Axiom % 0.18/0.40 32. (-. (ip (uri_ex_p))) (ip (uri_ex_p)) ### Axiom % 0.18/0.40 33. ((iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) => (ip (uri_ex_p))) (-. (ip (uri_ex_p))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) ### Imply 31 32 % 0.18/0.40 34. (All O, ((iext (uri_ex_p) (uri_ex_s) O) => (ip (uri_ex_p)))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (-. (ip (uri_ex_p))) ### All 33 % 0.18/0.40 35. (All P, (All O, ((iext P (uri_ex_s) O) => (ip P)))) (-. (ip (uri_ex_p))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) ### All 34 % 0.18/0.40 36. (All S, (All P, (All O, ((iext P S O) => (ip P))))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (-. (ip (uri_ex_p))) ### All 35 % 0.18/0.40 37. (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdf_Property))) (iext (uri_rdf_type) (uri_ex_p) (uri_rdf_Property)) ### Axiom % 0.18/0.40 38. ((iext (uri_rdf_type) (uri_ex_p) (uri_rdf_Property)) <=> (ip (uri_ex_p))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdf_Property))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (All S, (All P, (All O, ((iext P S O) => (ip P))))) ### Equiv 36 37 % 0.18/0.40 39. (All P, ((iext (uri_rdf_type) P (uri_rdf_Property)) <=> (ip P))) (All S, (All P, (All O, ((iext P S O) => (ip P))))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_rdf_Property))) ### All 38 % 0.18/0.40 40. (-. (icext (uri_owl_ObjectProperty) (uri_ex_p))) (icext (uri_owl_ObjectProperty) (uri_ex_p)) ### Axiom % 0.18/0.40 41. ((icext (uri_owl_ObjectProperty) (uri_ex_p)) <=> (ip (uri_ex_p))) (-. (icext (uri_owl_ObjectProperty) (uri_ex_p))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (All S, (All P, (All O, ((iext P S O) => (ip P))))) ### Equiv 36 40 % 0.18/0.40 42. (All X, ((icext (uri_owl_ObjectProperty) X) <=> (ip X))) (All S, (All P, (All O, ((iext P S O) => (ip P))))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (-. (icext (uri_owl_ObjectProperty) (uri_ex_p))) ### All 41 % 0.18/0.40 43. (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty)) ### Axiom % 0.18/0.40 44. ((iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty)) <=> (icext (uri_owl_ObjectProperty) (uri_ex_p))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (All S, (All P, (All O, ((iext P S O) => (ip P))))) (All X, ((icext (uri_owl_ObjectProperty) X) <=> (ip X))) ### Equiv 42 43 % 0.18/0.40 45. (All C, ((iext (uri_rdf_type) (uri_ex_p) C) <=> (icext C (uri_ex_p)))) (All X, ((icext (uri_owl_ObjectProperty) X) <=> (ip X))) (All S, (All P, (All O, ((iext P S O) => (ip P))))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) ### All 44 % 0.18/0.40 46. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (All S, (All P, (All O, ((iext P S O) => (ip P))))) (All X, ((icext (uri_owl_ObjectProperty) X) <=> (ip X))) ### All 45 % 0.18/0.40 47. (-. (icext (uri_rdfs_Resource) (uri_ex_o))) (icext (uri_rdfs_Resource) (uri_ex_o)) ### Axiom % 0.18/0.40 48. (ir (uri_ex_o)) (-. (icext (uri_rdfs_Resource) (uri_ex_o))) ### Definition-Pseudo(ir) 47 % 0.18/0.40 49. (All X, (ir X)) (-. (icext (uri_rdfs_Resource) (uri_ex_o))) ### All 48 % 0.18/0.40 50. (-. (iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource))) (iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource)) ### Axiom % 0.18/0.40 51. ((iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource)) <=> (icext (uri_rdfs_Resource) (uri_ex_o))) (-. (iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource))) (All X, (ir X)) ### Equiv 49 50 % 0.18/0.40 52. (All C, ((iext (uri_rdf_type) (uri_ex_o) C) <=> (icext C (uri_ex_o)))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource))) ### All 51 % 0.18/0.40 53. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource))) (All X, (ir X)) ### All 52 % 0.18/0.40 54. (-. (ir (uri_ex_o))) (All X, (ir X)) ### Definition-Pseudo(ir) 49 % 0.18/0.40 55. (-. (icext (uri_owl_Thing) (uri_ex_o))) (icext (uri_owl_Thing) (uri_ex_o)) ### Axiom % 0.18/0.40 56. ((icext (uri_owl_Thing) (uri_ex_o)) <=> (ir (uri_ex_o))) (-. (icext (uri_owl_Thing) (uri_ex_o))) (All X, (ir X)) ### Equiv 54 55 % 0.18/0.40 57. (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (icext (uri_owl_Thing) (uri_ex_o))) ### All 56 % 0.18/0.40 58. (-. (iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing))) (iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing)) ### Axiom % 0.18/0.40 59. ((iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing)) <=> (icext (uri_owl_Thing) (uri_ex_o))) (-. (iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### Equiv 57 58 % 0.18/0.40 60. (All C, ((iext (uri_rdf_type) (uri_ex_o) C) <=> (icext C (uri_ex_o)))) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing))) ### All 59 % 0.18/0.40 61. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### All 60 % 0.18/0.40 62. (-. ((iext (uri_rdf_type) (uri_ex_s) (uri_rdfs_Resource)) /\ ((iext (uri_rdf_type) (uri_ex_s) (uri_owl_Thing)) /\ ((iext (uri_rdf_type) (uri_ex_p) (uri_rdfs_Resource)) /\ ((iext (uri_rdf_type) (uri_ex_p) (uri_owl_Thing)) /\ ((iext (uri_rdf_type) (uri_ex_p) (uri_rdf_Property)) /\ ((iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty)) /\ ((iext (uri_rdf_type) (uri_ex_o) (uri_rdfs_Resource)) /\ (iext (uri_rdf_type) (uri_ex_o) (uri_owl_Thing)))))))))) (All X, ((icext (uri_owl_ObjectProperty) X) <=> (ip X))) (iext (uri_ex_p) (uri_ex_s) (uri_ex_o)) (All S, (All P, (All O, ((iext P S O) => (ip P))))) (All P, ((iext (uri_rdf_type) P (uri_rdf_Property)) <=> (ip P))) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### DisjTree 7 15 22 30 39 46 53 61 % 0.18/0.40 % SZS output end Proof % 0.18/0.40 (* END-PROOF *) %------------------------------------------------------------------------------