%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWB023+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 : n018.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:11 EDT 2022 % Result : Theorem 31.03s 31.27s % Output : Proof 31.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB023+2 : TPTP v8.1.0. Released v5.2.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n018.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 : Wed Jun 1 03:30:44 EDT 2022 % 0.13/0.34 % CPUTime : % 31.03/31.27 % SZS status Theorem % 31.03/31.27 (* PROOF-FOUND *) % 31.03/31.27 (* BEGIN-PROOF *) % 31.03/31.27 % SZS output start Proof % 31.03/31.27 1. ((uri_ex_u) != (uri_ex_u)) ### NotEqual % 31.03/31.27 2. (iext (uri_rdf_first) T_0 (uri_ex_u)) (-. (iext (uri_rdf_first) T_0 (uri_ex_u))) ### Axiom % 31.03/31.27 3. (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (-. (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) ### Axiom % 31.03/31.27 4. (iext (uri_owl_oneOf) T_1 T_0) (-. (iext (uri_owl_oneOf) T_1 T_0)) ### Axiom % 31.03/31.27 5. (-. (icext T_1 (uri_ex_u))) (icext T_1 (uri_ex_u)) ### Axiom % 31.03/31.27 6. ((icext T_1 (uri_ex_u)) <=> ((uri_ex_u) = (uri_ex_u))) (-. (icext T_1 (uri_ex_u))) ### Equiv 1 5 % 31.03/31.27 7. (All X, ((icext T_1 X) <=> (X = (uri_ex_u)))) (-. (icext T_1 (uri_ex_u))) ### All 6 % 31.03/31.27 8. ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_u))))) (-. (icext T_1 (uri_ex_u))) ### And 7 % 31.03/31.27 9. ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_u)))))) (-. (icext T_1 (uri_ex_u))) (iext (uri_owl_oneOf) T_1 T_0) ### Equiv 4 8 % 31.03/31.27 10. (((iext (uri_rdf_first) T_0 (uri_ex_u)) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_u))))))) (iext (uri_owl_oneOf) T_1 T_0) (-. (icext T_1 (uri_ex_u))) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) ### DisjTree 2 3 9 % 31.03/31.27 11. (All A1, (((iext (uri_rdf_first) T_0 A1) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1))))))) (iext (uri_rdf_first) T_0 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (-. (icext T_1 (uri_ex_u))) (iext (uri_owl_oneOf) T_1 T_0) ### All 10 % 31.03/31.27 12. (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 S1) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1)))))))) (iext (uri_owl_oneOf) T_1 T_0) (-. (icext T_1 (uri_ex_u))) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) ### All 11 % 31.03/31.27 13. (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (-. (icext T_1 (uri_ex_u))) (iext (uri_owl_oneOf) T_1 T_0) ### All 12 % 31.03/31.27 14. (iext (uri_rdf_first) T_0 (uri_ex_v)) (-. (iext (uri_rdf_first) T_0 (uri_ex_v))) ### Axiom % 31.03/31.27 15. (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (-. (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) ### Axiom % 31.03/31.27 16. (iext (uri_owl_oneOf) T_1 T_0) (-. (iext (uri_owl_oneOf) T_1 T_0)) ### Axiom % 31.03/31.27 17. (icext T_1 (uri_ex_u)) (-. (icext T_1 (uri_ex_u))) ### Axiom % 31.03/31.27 18. ((uri_ex_u) != (uri_ex_v)) ((uri_ex_u) = (uri_ex_v)) ### Axiom % 31.03/31.27 19. ((icext T_1 (uri_ex_u)) <=> ((uri_ex_u) = (uri_ex_v))) ((uri_ex_u) != (uri_ex_v)) (icext T_1 (uri_ex_u)) ### Equiv 17 18 % 31.03/31.27 20. (All X, ((icext T_1 X) <=> (X = (uri_ex_v)))) (icext T_1 (uri_ex_u)) ((uri_ex_u) != (uri_ex_v)) ### All 19 % 31.03/31.27 21. ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_v))))) ((uri_ex_u) != (uri_ex_v)) (icext T_1 (uri_ex_u)) ### And 20 % 31.03/31.27 22. ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_v)))))) (icext T_1 (uri_ex_u)) ((uri_ex_u) != (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) ### Equiv 16 21 % 31.03/31.27 23. (((iext (uri_rdf_first) T_0 (uri_ex_v)) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_v))))))) (iext (uri_owl_oneOf) T_1 T_0) ((uri_ex_u) != (uri_ex_v)) (icext T_1 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) ### DisjTree 14 15 22 % 31.03/31.27 24. (All A1, (((iext (uri_rdf_first) T_0 A1) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1))))))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (icext T_1 (uri_ex_u)) ((uri_ex_u) != (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) ### All 23 % 31.03/31.27 25. (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 S1) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1)))))))) (iext (uri_owl_oneOf) T_1 T_0) ((uri_ex_u) != (uri_ex_v)) (icext T_1 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) ### All 24 % 31.03/31.27 26. (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (icext T_1 (uri_ex_u)) ((uri_ex_u) != (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) ### All 25 % 31.03/31.27 27. ((iext (uri_rdf_type) (uri_ex_u) T_1) <=> (icext T_1 (uri_ex_u))) ((uri_ex_u) != (uri_ex_v)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) ### Equiv 13 26 % 31.03/31.27 28. (All C, ((iext (uri_rdf_type) (uri_ex_u) C) <=> (icext C (uri_ex_u)))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_first) T_0 (uri_ex_v)) ((uri_ex_u) != (uri_ex_v)) ### All 27 % 31.03/31.27 29. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ((uri_ex_u) != (uri_ex_v)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) ### All 28 % 31.03/31.27 30. ((uri_owl_sameAs) != (uri_owl_sameAs)) ### NotEqual % 31.03/31.27 31. (iext (uri_rdf_first) T_0 (uri_ex_v)) (-. (iext (uri_rdf_first) T_0 (uri_ex_v))) ### Axiom % 31.03/31.27 32. (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (-. (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) ### Axiom % 31.03/31.27 33. (iext (uri_owl_oneOf) T_1 T_0) (-. (iext (uri_owl_oneOf) T_1 T_0)) ### Axiom % 31.03/31.27 34. (iext (uri_rdf_type) (uri_ex_w) T_1) (-. (iext (uri_rdf_type) (uri_ex_w) T_1)) ### Axiom % 31.03/31.27 35. (-. (icext T_1 (uri_ex_w))) (icext T_1 (uri_ex_w)) ### Axiom % 31.03/31.27 36. ((iext (uri_rdf_type) (uri_ex_w) T_1) <=> (icext T_1 (uri_ex_w))) (-. (icext T_1 (uri_ex_w))) (iext (uri_rdf_type) (uri_ex_w) T_1) ### Equiv 34 35 % 31.03/31.27 37. (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) (iext (uri_rdf_type) (uri_ex_w) T_1) (-. (icext T_1 (uri_ex_w))) ### All 36 % 31.03/31.27 38. ((uri_ex_v) != (uri_ex_w)) ((uri_ex_w) = (uri_ex_v)) ### Sym(=) % 31.03/31.27 39. ((icext T_1 (uri_ex_w)) <=> ((uri_ex_w) = (uri_ex_v))) ((uri_ex_v) != (uri_ex_w)) (iext (uri_rdf_type) (uri_ex_w) T_1) (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) ### Equiv 37 38 % 31.03/31.27 40. (All X, ((icext T_1 X) <=> (X = (uri_ex_v)))) (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) (iext (uri_rdf_type) (uri_ex_w) T_1) ((uri_ex_v) != (uri_ex_w)) ### All 39 % 31.03/31.27 41. ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_v))))) ((uri_ex_v) != (uri_ex_w)) (iext (uri_rdf_type) (uri_ex_w) T_1) (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) ### And 40 % 31.03/31.27 42. ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_v)))))) (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) (iext (uri_rdf_type) (uri_ex_w) T_1) ((uri_ex_v) != (uri_ex_w)) (iext (uri_owl_oneOf) T_1 T_0) ### Equiv 33 41 % 31.03/31.27 43. (((iext (uri_rdf_first) T_0 (uri_ex_v)) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = (uri_ex_v))))))) (iext (uri_owl_oneOf) T_1 T_0) ((uri_ex_v) != (uri_ex_w)) (iext (uri_rdf_type) (uri_ex_w) T_1) (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) ### DisjTree 31 32 42 % 31.03/31.29 44. (All A1, (((iext (uri_rdf_first) T_0 A1) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1))))))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (All C, ((iext (uri_rdf_type) (uri_ex_w) C) <=> (icext C (uri_ex_w)))) (iext (uri_rdf_type) (uri_ex_w) T_1) ((uri_ex_v) != (uri_ex_w)) (iext (uri_owl_oneOf) T_1 T_0) ### All 43 % 31.03/31.29 45. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_oneOf) T_1 T_0) ((uri_ex_v) != (uri_ex_w)) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (All A1, (((iext (uri_rdf_first) T_0 A1) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1))))))) ### All 44 % 31.03/31.29 46. (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 S1) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1)))))))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_w) T_1) ((uri_ex_v) != (uri_ex_w)) (iext (uri_owl_oneOf) T_1 T_0) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### All 45 % 31.03/31.29 47. ((uri_ex_u) != (uri_ex_w)) ((uri_ex_u) = (uri_ex_v)) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 S1) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1)))))))) ### Trans 1 46 % 31.03/31.29 48. (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_owl_oneOf) T_1 T_0) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ((uri_ex_u) = (uri_ex_v)) ((uri_ex_u) != (uri_ex_w)) ### All 47 % 31.03/31.29 49. (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u))) (iext (uri_owl_sameAs) (uri_ex_u) (uri_ex_u)) ((uri_ex_u) = (uri_ex_v)) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) ### P-NotP 30 48 1 % 31.03/31.29 50. ((iext (uri_owl_sameAs) (uri_ex_u) (uri_ex_v)) <=> ((uri_ex_u) = (uri_ex_v))) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_owl_sameAs) (uri_ex_u) (uri_ex_u)) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_first) T_0 (uri_ex_v)) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### Equiv 29 49 % 31.03/31.29 51. (All Y, ((iext (uri_owl_sameAs) (uri_ex_u) Y) <=> ((uri_ex_u) = Y))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u))) (iext (uri_owl_sameAs) (uri_ex_u) (uri_ex_u)) (iext (uri_rdf_type) (uri_ex_w) T_1) ### All 50 % 31.03/31.29 52. ((iext (uri_owl_sameAs) (uri_ex_u) (uri_ex_u)) <=> ((uri_ex_u) = (uri_ex_u))) (iext (uri_rdf_type) (uri_ex_w) T_1) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_first) T_0 (uri_ex_v)) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (All Y, ((iext (uri_owl_sameAs) (uri_ex_u) Y) <=> ((uri_ex_u) = Y))) ### Equiv 1 51 % 31.03/31.29 53. (All Y, ((iext (uri_owl_sameAs) (uri_ex_u) Y) <=> ((uri_ex_u) = Y))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u))) (iext (uri_rdf_type) (uri_ex_w) T_1) ### All 52 % 31.03/31.29 54. (All X, (All Y, ((iext (uri_owl_sameAs) X Y) <=> (X = Y)))) (iext (uri_rdf_type) (uri_ex_w) T_1) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_first) T_0 (uri_ex_u)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_first) T_0 (uri_ex_v)) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### All 53 % 31.03/31.29 55. ((uri_ex_v) != (uri_ex_v)) ### NotEqual % 31.03/31.29 56. (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v))) (iext (uri_owl_sameAs) (uri_ex_v) (uri_ex_v)) (All A1, (((iext (uri_rdf_first) T_0 A1) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 T_0) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1))))))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_owl_oneOf) T_1 T_0) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### P-NotP 30 45 55 % 31.03/31.29 57. (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) T_1 S1) <=> ((ic T_1) /\ (All X, ((icext T_1 X) <=> (X = A1)))))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_owl_sameAs) (uri_ex_v) (uri_ex_v)) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v))) ### All 56 % 31.03/31.29 58. (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v))) (iext (uri_owl_sameAs) (uri_ex_v) (uri_ex_v)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_owl_oneOf) T_1 T_0) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### All 57 % 31.03/31.29 59. ((iext (uri_owl_sameAs) (uri_ex_v) (uri_ex_v)) <=> ((uri_ex_v) = (uri_ex_v))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) ### Equiv 55 58 % 31.03/31.29 60. (All Y, ((iext (uri_owl_sameAs) (uri_ex_v) Y) <=> ((uri_ex_v) = Y))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_owl_oneOf) T_1 T_0) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### All 59 % 31.03/31.29 61. (All X, (All Y, ((iext (uri_owl_sameAs) X Y) <=> (X = Y)))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_type) (uri_ex_w) T_1) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_v)) (-. (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) ### All 60 % 31.03/31.29 62. (-. ((iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u)) /\ (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v)))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_rdf_first) T_0 (uri_ex_v)) (iext (uri_owl_oneOf) T_1 T_0) (iext (uri_rdf_rest) T_0 (uri_rdf_nil)) (iext (uri_rdf_first) T_0 (uri_ex_u)) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (iext (uri_rdf_type) (uri_ex_w) T_1) (All X, (All Y, ((iext (uri_owl_sameAs) X Y) <=> (X = Y)))) ### NotAnd 54 61 % 31.03/31.29 63. ((iext (uri_rdf_type) (uri_rdf_first) (uri_owl_FunctionalProperty)) /\ ((iext (uri_rdf_type) (uri_ex_w) T_1) /\ ((iext (uri_rdf_type) T_1 (uri_owl_Class)) /\ ((iext (uri_owl_oneOf) T_1 T_0) /\ ((iext (uri_rdf_first) T_0 (uri_ex_u)) /\ ((iext (uri_rdf_first) T_0 (uri_ex_v)) /\ (iext (uri_rdf_rest) T_0 (uri_rdf_nil)))))))) (All X, (All Y, ((iext (uri_owl_sameAs) X Y) <=> (X = Y)))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. ((iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u)) /\ (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v)))) ### ConjTree 62 % 31.03/31.29 64. (Ex BNODE_l, ((iext (uri_rdf_type) (uri_rdf_first) (uri_owl_FunctionalProperty)) /\ ((iext (uri_rdf_type) (uri_ex_w) T_1) /\ ((iext (uri_rdf_type) T_1 (uri_owl_Class)) /\ ((iext (uri_owl_oneOf) T_1 BNODE_l) /\ ((iext (uri_rdf_first) BNODE_l (uri_ex_u)) /\ ((iext (uri_rdf_first) BNODE_l (uri_ex_v)) /\ (iext (uri_rdf_rest) BNODE_l (uri_rdf_nil))))))))) (-. ((iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u)) /\ (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v)))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (All X, (All Y, ((iext (uri_owl_sameAs) X Y) <=> (X = Y)))) ### Exists 63 % 31.03/31.29 65. (Ex BNODE_o, (Ex BNODE_l, ((iext (uri_rdf_type) (uri_rdf_first) (uri_owl_FunctionalProperty)) /\ ((iext (uri_rdf_type) (uri_ex_w) BNODE_o) /\ ((iext (uri_rdf_type) BNODE_o (uri_owl_Class)) /\ ((iext (uri_owl_oneOf) BNODE_o BNODE_l) /\ ((iext (uri_rdf_first) BNODE_l (uri_ex_u)) /\ ((iext (uri_rdf_first) BNODE_l (uri_ex_v)) /\ (iext (uri_rdf_rest) BNODE_l (uri_rdf_nil)))))))))) (All X, (All Y, ((iext (uri_owl_sameAs) X Y) <=> (X = Y)))) (All Z, (All S1, (All A1, (((iext (uri_rdf_first) S1 A1) /\ (iext (uri_rdf_rest) S1 (uri_rdf_nil))) => ((iext (uri_owl_oneOf) Z S1) <=> ((ic Z) /\ (All X, ((icext Z X) <=> (X = A1))))))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. ((iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_u)) /\ (iext (uri_owl_sameAs) (uri_ex_w) (uri_ex_v)))) ### Exists 64 % 31.03/31.29 % SZS output end Proof % 31.03/31.29 (* END-PROOF *) %------------------------------------------------------------------------------