%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWB004+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 : n032.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.14s 0.36s % Output : Proof 0.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SWB004+2 : TPTP v8.1.0. Released v5.2.0. % 0.03/0.11 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.09/0.30 % Computer : n032.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 600 % 0.09/0.30 % DateTime : Wed Jun 1 11:36:14 EDT 2022 % 0.09/0.30 % CPUTime : % 0.14/0.36 % SZS status Theorem % 0.14/0.36 (* PROOF-FOUND *) % 0.14/0.36 (* BEGIN-PROOF *) % 0.14/0.36 % SZS output start Proof % 0.14/0.36 1. (-. (ir (uri_owl_Class))) (ir (uri_owl_Class)) ### Axiom % 0.14/0.36 2. (All X, (ir X)) (-. (ir (uri_owl_Class))) ### All 1 % 0.14/0.36 3. (-. (icext (uri_owl_Thing) (uri_owl_Class))) (icext (uri_owl_Thing) (uri_owl_Class)) ### Axiom % 0.14/0.36 4. ((icext (uri_owl_Thing) (uri_owl_Class)) <=> (ir (uri_owl_Class))) (-. (icext (uri_owl_Thing) (uri_owl_Class))) (All X, (ir X)) ### Equiv 2 3 % 0.14/0.36 5. (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (icext (uri_owl_Thing) (uri_owl_Class))) ### All 4 % 0.14/0.36 6. (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing))) (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing)) ### Axiom % 0.14/0.36 7. ((iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing)) <=> (icext (uri_owl_Thing) (uri_owl_Class))) (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### Equiv 5 6 % 0.14/0.36 8. (All C, ((iext (uri_rdf_type) (uri_owl_Class) C) <=> (icext C (uri_owl_Class)))) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing))) ### All 7 % 0.14/0.36 9. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### All 8 % 0.14/0.36 10. (ic (uri_owl_Class)) (-. (ic (uri_owl_Class))) ### Axiom % 0.14/0.36 11. (-. (icext (uri_owl_Class) (uri_owl_Class))) (icext (uri_owl_Class) (uri_owl_Class)) ### Axiom % 0.14/0.36 12. ((icext (uri_owl_Class) (uri_owl_Class)) <=> (ic (uri_owl_Class))) (-. (icext (uri_owl_Class) (uri_owl_Class))) (ic (uri_owl_Class)) ### Equiv 10 11 % 0.14/0.36 13. (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_owl_Class)) (-. (icext (uri_owl_Class) (uri_owl_Class))) ### All 12 % 0.14/0.36 14. (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class))) (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class)) ### Axiom % 0.14/0.36 15. ((iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class)) <=> (icext (uri_owl_Class) (uri_owl_Class))) (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class))) (ic (uri_owl_Class)) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) ### Equiv 13 14 % 0.14/0.36 16. (All C, ((iext (uri_rdf_type) (uri_owl_Class) C) <=> (icext C (uri_owl_Class)))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_owl_Class)) (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class))) ### All 15 % 0.14/0.36 17. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class))) (ic (uri_owl_Class)) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) ### All 16 % 0.14/0.36 18. (ic (uri_owl_Class)) (-. (ic (uri_owl_Class))) ### Axiom % 0.14/0.36 19. (ic (uri_owl_Thing)) (-. (ic (uri_owl_Thing))) ### Axiom % 0.14/0.36 20. (-. (ir T_0)) (ir T_0) ### Axiom % 0.14/0.36 21. (All X, (ir X)) (-. (ir T_0)) ### All 20 % 0.14/0.36 22. (-. (icext (uri_owl_Thing) T_0)) (icext (uri_owl_Thing) T_0) ### Axiom % 0.14/0.36 23. ((icext (uri_owl_Thing) T_0) <=> (ir T_0)) (-. (icext (uri_owl_Thing) T_0)) (All X, (ir X)) ### Equiv 21 22 % 0.14/0.36 24. (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) (-. (icext (uri_owl_Thing) T_0)) ### All 23 % 0.14/0.36 25. (-. ((icext (uri_owl_Class) T_0) => (icext (uri_owl_Thing) T_0))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) ### NotImply 24 % 0.14/0.36 26. (-. (All X, ((icext (uri_owl_Class) X) => (icext (uri_owl_Thing) X)))) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) ### NotAllEx 25 % 0.14/0.36 27. (-. ((ic (uri_owl_Class)) /\ ((ic (uri_owl_Thing)) /\ (All X, ((icext (uri_owl_Class) X) => (icext (uri_owl_Thing) X)))))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (ic (uri_owl_Thing)) (ic (uri_owl_Class)) ### DisjTree 18 19 26 % 0.14/0.36 28. (-. (iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing))) (iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing)) ### Axiom % 0.14/0.36 29. ((iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing)) <=> ((ic (uri_owl_Class)) /\ ((ic (uri_owl_Thing)) /\ (All X, ((icext (uri_owl_Class) X) => (icext (uri_owl_Thing) X)))))) (-. (iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing))) (ic (uri_owl_Class)) (ic (uri_owl_Thing)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) ### Equiv 27 28 % 0.14/0.36 30. (All C2, ((iext (uri_rdfs_subClassOf) (uri_owl_Class) C2) <=> ((ic (uri_owl_Class)) /\ ((ic C2) /\ (All X, ((icext (uri_owl_Class) X) => (icext C2 X))))))) (All X, (ir X)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (ic (uri_owl_Thing)) (ic (uri_owl_Class)) (-. (iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing))) ### All 29 % 0.14/0.36 31. (All C1, (All C2, ((iext (uri_rdfs_subClassOf) C1 C2) <=> ((ic C1) /\ ((ic C2) /\ (All X, ((icext C1 X) => (icext C2 X)))))))) (-. (iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing))) (ic (uri_owl_Class)) (ic (uri_owl_Thing)) (All X, ((icext (uri_owl_Thing) X) <=> (ir X))) (All X, (ir X)) ### All 30 % 0.14/0.36 32. (ic (uri_owl_Class)) (-. (ic (uri_owl_Class))) ### Axiom % 0.14/0.36 33. (ic (uri_rdfs_Class)) (-. (ic (uri_rdfs_Class))) ### Axiom % 0.14/0.36 34. (icext (uri_rdfs_Class) T_1) (-. (icext (uri_rdfs_Class) T_1)) ### Axiom % 0.14/0.36 35. (-. (ic T_1)) (ic T_1) ### Axiom % 0.14/0.36 36. ((icext (uri_rdfs_Class) T_1) <=> (ic T_1)) (-. (ic T_1)) (icext (uri_rdfs_Class) T_1) ### Equiv 34 35 % 0.14/0.36 37. (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (icext (uri_rdfs_Class) T_1) (-. (ic T_1)) ### All 36 % 0.14/0.36 38. (-. (icext (uri_owl_Class) T_1)) (icext (uri_owl_Class) T_1) ### Axiom % 0.14/0.36 39. ((icext (uri_owl_Class) T_1) <=> (ic T_1)) (-. (icext (uri_owl_Class) T_1)) (icext (uri_rdfs_Class) T_1) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) ### Equiv 37 38 % 0.14/0.36 40. (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (icext (uri_rdfs_Class) T_1) (-. (icext (uri_owl_Class) T_1)) ### All 39 % 0.14/0.36 41. (icext (uri_owl_Class) T_1) (-. (icext (uri_owl_Class) T_1)) ### Axiom % 0.14/0.36 42. (-. (ic T_1)) (ic T_1) ### Axiom % 0.14/0.36 43. ((icext (uri_owl_Class) T_1) <=> (ic T_1)) (-. (ic T_1)) (icext (uri_owl_Class) T_1) ### Equiv 41 42 % 0.14/0.36 44. (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (icext (uri_owl_Class) T_1) (-. (ic T_1)) ### All 43 % 0.14/0.36 45. (-. (icext (uri_rdfs_Class) T_1)) (icext (uri_rdfs_Class) T_1) ### Axiom % 0.14/0.36 46. ((icext (uri_rdfs_Class) T_1) <=> (ic T_1)) (-. (icext (uri_rdfs_Class) T_1)) (icext (uri_owl_Class) T_1) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) ### Equiv 44 45 % 0.14/0.36 47. (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (icext (uri_owl_Class) T_1) (-. (icext (uri_rdfs_Class) T_1)) ### All 46 % 0.14/0.36 48. (-. ((icext (uri_owl_Class) T_1) <=> (icext (uri_rdfs_Class) T_1))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) ### NotEquiv 40 47 % 0.14/0.36 49. (-. (All X, ((icext (uri_owl_Class) X) <=> (icext (uri_rdfs_Class) X)))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) ### NotAllEx 48 % 0.14/0.36 50. (-. ((ic (uri_owl_Class)) /\ ((ic (uri_rdfs_Class)) /\ (All X, ((icext (uri_owl_Class) X) <=> (icext (uri_rdfs_Class) X)))))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_rdfs_Class)) (ic (uri_owl_Class)) ### DisjTree 32 33 49 % 0.14/0.36 51. (-. (iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class))) (iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class)) ### Axiom % 0.14/0.36 52. ((iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class)) <=> ((ic (uri_owl_Class)) /\ ((ic (uri_rdfs_Class)) /\ (All X, ((icext (uri_owl_Class) X) <=> (icext (uri_rdfs_Class) X)))))) (-. (iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class))) (ic (uri_owl_Class)) (ic (uri_rdfs_Class)) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) ### Equiv 50 51 % 0.14/0.36 53. (All C2, ((iext (uri_owl_equivalentClass) (uri_owl_Class) C2) <=> ((ic (uri_owl_Class)) /\ ((ic C2) /\ (All X, ((icext (uri_owl_Class) X) <=> (icext C2 X))))))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_rdfs_Class)) (ic (uri_owl_Class)) (-. (iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class))) ### All 52 % 0.14/0.36 54. (All C1, (All C2, ((iext (uri_owl_equivalentClass) C1 C2) <=> ((ic C1) /\ ((ic C2) /\ (All X, ((icext C1 X) <=> (icext C2 X)))))))) (-. (iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class))) (ic (uri_owl_Class)) (ic (uri_rdfs_Class)) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) ### All 53 % 0.14/0.36 55. (ic (uri_rdfs_Datatype)) (-. (ic (uri_rdfs_Datatype))) ### Axiom % 0.14/0.36 56. (ic (uri_owl_Class)) (-. (ic (uri_owl_Class))) ### Axiom % 0.14/0.36 57. (icext (uri_rdfs_Datatype) T_2) (-. (icext (uri_rdfs_Datatype) T_2)) ### Axiom % 0.14/0.36 58. (-. (idc T_2)) (idc T_2) ### Axiom % 0.14/0.36 59. ((icext (uri_rdfs_Datatype) T_2) <=> (idc T_2)) (-. (idc T_2)) (icext (uri_rdfs_Datatype) T_2) ### Equiv 57 58 % 0.14/0.36 60. (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (icext (uri_rdfs_Datatype) T_2) (-. (idc T_2)) ### All 59 % 0.14/0.36 61. (-. (ic T_2)) (ic T_2) ### Axiom % 0.14/0.36 62. ((idc T_2) => (ic T_2)) (-. (ic T_2)) (icext (uri_rdfs_Datatype) T_2) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) ### Imply 60 61 % 0.14/0.36 63. (All X, ((idc X) => (ic X))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (icext (uri_rdfs_Datatype) T_2) (-. (ic T_2)) ### All 62 % 0.14/0.36 64. (-. (icext (uri_owl_Class) T_2)) (icext (uri_owl_Class) T_2) ### Axiom % 0.14/0.36 65. ((icext (uri_owl_Class) T_2) <=> (ic T_2)) (-. (icext (uri_owl_Class) T_2)) (icext (uri_rdfs_Datatype) T_2) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (All X, ((idc X) => (ic X))) ### Equiv 63 64 % 0.14/0.36 66. (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (icext (uri_rdfs_Datatype) T_2) (-. (icext (uri_owl_Class) T_2)) ### All 65 % 0.14/0.36 67. (-. ((icext (uri_rdfs_Datatype) T_2) => (icext (uri_owl_Class) T_2))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) ### NotImply 66 % 0.14/0.36 68. (-. (All X, ((icext (uri_rdfs_Datatype) X) => (icext (uri_owl_Class) X)))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) ### NotAllEx 67 % 0.14/0.36 69. (-. ((ic (uri_rdfs_Datatype)) /\ ((ic (uri_owl_Class)) /\ (All X, ((icext (uri_rdfs_Datatype) X) => (icext (uri_owl_Class) X)))))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_owl_Class)) (ic (uri_rdfs_Datatype)) ### DisjTree 55 56 68 % 0.14/0.36 70. (-. (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class))) (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class)) ### Axiom % 0.14/0.36 71. ((iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class)) <=> ((ic (uri_rdfs_Datatype)) /\ ((ic (uri_owl_Class)) /\ (All X, ((icext (uri_rdfs_Datatype) X) => (icext (uri_owl_Class) X)))))) (-. (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class))) (ic (uri_rdfs_Datatype)) (ic (uri_owl_Class)) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) ### Equiv 69 70 % 0.14/0.36 72. (All C2, ((iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) C2) <=> ((ic (uri_rdfs_Datatype)) /\ ((ic C2) /\ (All X, ((icext (uri_rdfs_Datatype) X) => (icext C2 X))))))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_owl_Class)) (ic (uri_rdfs_Datatype)) (-. (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class))) ### All 71 % 0.14/0.36 73. (All C1, (All C2, ((iext (uri_rdfs_subClassOf) C1 C2) <=> ((ic C1) /\ ((ic C2) /\ (All X, ((icext C1 X) => (icext C2 X)))))))) (-. (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class))) (ic (uri_rdfs_Datatype)) (ic (uri_owl_Class)) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (All X, ((idc X) => (ic X))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) ### All 72 % 0.14/0.36 74. (-. ((iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Thing)) /\ ((iext (uri_rdf_type) (uri_owl_Class) (uri_owl_Class)) /\ ((iext (uri_rdfs_subClassOf) (uri_owl_Class) (uri_owl_Thing)) /\ ((iext (uri_owl_equivalentClass) (uri_owl_Class) (uri_rdfs_Class)) /\ (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_owl_Class))))))) (All X, ((icext (uri_rdfs_Datatype) X) <=> (idc X))) (All X, ((idc X) => (ic X))) (ic (uri_rdfs_Datatype)) (All X, ((icext (uri_rdfs_Class) X) <=> (ic X))) (ic (uri_rdfs_Class)) (All C1, (All C2, ((iext (uri_owl_equivalentClass) C1 C2) <=> ((ic C1) /\ ((ic C2) /\ (All X, ((icext C1 X) <=> (icext C2 X)))))))) (ic (uri_owl_Thing)) (All C1, (All C2, ((iext (uri_rdfs_subClassOf) C1 C2) <=> ((ic C1) /\ ((ic C2) /\ (All X, ((icext C1 X) => (icext C2 X)))))))) (All X, ((icext (uri_owl_Class) X) <=> (ic X))) (ic (uri_owl_Class)) (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 9 17 31 54 73 % 0.14/0.36 % SZS output end Proof % 0.14/0.36 (* END-PROOF *) %------------------------------------------------------------------------------