%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWB014+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:08 EDT 2022 % Result : Theorem 4.94s 5.17s % Output : Proof 4.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWB014+2 : TPTP v8.1.0. Released v5.2.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n018.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 08:42:59 EDT 2022 % 0.12/0.33 % CPUTime : % 4.94/5.17 % SZS status Theorem % 4.94/5.17 (* PROOF-FOUND *) % 4.94/5.17 (* BEGIN-PROOF *) % 4.94/5.17 % SZS output start Proof % 4.94/5.17 1. (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (-. (iext (uri_rdf_first) T_0 (uri_ex_Eagle))) ### Axiom % 4.94/5.17 2. (iext (uri_rdf_rest) T_0 T_1) (-. (iext (uri_rdf_rest) T_0 T_1)) ### Axiom % 4.94/5.17 3. (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (-. (iext (uri_rdf_first) T_1 (uri_ex_Falcon))) ### Axiom % 4.94/5.17 4. (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (-. (iext (uri_rdf_rest) T_1 (uri_rdf_nil))) ### Axiom % 4.94/5.17 5. (iext (uri_owl_unionOf) T_2 T_0) (-. (iext (uri_owl_unionOf) T_2 T_0)) ### Axiom % 4.94/5.17 6. (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (iext (uri_rdf_type) (uri_ex_harry) T_2)) ### Axiom % 4.94/5.17 7. (-. (icext T_2 (uri_ex_harry))) (icext T_2 (uri_ex_harry)) ### Axiom % 4.94/5.17 8. ((iext (uri_rdf_type) (uri_ex_harry) T_2) <=> (icext T_2 (uri_ex_harry))) (-. (icext T_2 (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) ### Equiv 6 7 % 4.94/5.17 9. (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext T_2 (uri_ex_harry))) ### All 8 % 4.94/5.17 10. (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (icext (uri_ex_Eagle) (uri_ex_harry)) ### Axiom % 4.94/5.17 11. (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (icext (uri_ex_Falcon) (uri_ex_harry)) ### Axiom % 4.94/5.17 12. ((icext (uri_ex_Eagle) (uri_ex_harry)) \/ (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) ### Or 10 11 % 4.94/5.17 13. ((icext T_2 (uri_ex_harry)) <=> ((icext (uri_ex_Eagle) (uri_ex_harry)) \/ (icext (uri_ex_Falcon) (uri_ex_harry)))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) ### Equiv 9 12 % 4.94/5.17 14. (All X, ((icext T_2 X) <=> ((icext (uri_ex_Eagle) X) \/ (icext (uri_ex_Falcon) X)))) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) ### All 13 % 4.94/5.17 15. ((ic T_2) /\ ((ic (uri_ex_Eagle)) /\ ((ic (uri_ex_Falcon)) /\ (All X, ((icext T_2 X) <=> ((icext (uri_ex_Eagle) X) \/ (icext (uri_ex_Falcon) X))))))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) ### ConjTree 14 % 4.94/5.17 16. ((iext (uri_owl_unionOf) T_2 T_0) <=> ((ic T_2) /\ ((ic (uri_ex_Eagle)) /\ ((ic (uri_ex_Falcon)) /\ (All X, ((icext T_2 X) <=> ((icext (uri_ex_Eagle) X) \/ (icext (uri_ex_Falcon) X)))))))) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (iext (uri_owl_unionOf) T_2 T_0) ### Equiv 5 15 % 4.94/5.17 17. (((iext (uri_rdf_first) T_0 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) T_0 T_1) /\ ((iext (uri_rdf_first) T_1 (uri_ex_Falcon)) /\ (iext (uri_rdf_rest) T_1 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) T_2 T_0) <=> ((ic T_2) /\ ((ic (uri_ex_Eagle)) /\ ((ic (uri_ex_Falcon)) /\ (All X, ((icext T_2 X) <=> ((icext (uri_ex_Eagle) X) \/ (icext (uri_ex_Falcon) X))))))))) (iext (uri_owl_unionOf) T_2 T_0) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) ### DisjTree 1 2 3 4 16 % 4.94/5.17 18. (All C2, (((iext (uri_rdf_first) T_0 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) T_0 T_1) /\ ((iext (uri_rdf_first) T_1 C2) /\ (iext (uri_rdf_rest) T_1 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) T_2 T_0) <=> ((ic T_2) /\ ((ic (uri_ex_Eagle)) /\ ((ic C2) /\ (All X, ((icext T_2 X) <=> ((icext (uri_ex_Eagle) X) \/ (icext C2 X)))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (iext (uri_owl_unionOf) T_2 T_0) ### All 17 % 4.94/5.17 19. (All S2, (All C2, (((iext (uri_rdf_first) T_0 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) T_0 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) T_2 T_0) <=> ((ic T_2) /\ ((ic (uri_ex_Eagle)) /\ ((ic C2) /\ (All X, ((icext T_2 X) <=> ((icext (uri_ex_Eagle) X) \/ (icext C2 X))))))))))) (iext (uri_owl_unionOf) T_2 T_0) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) ### All 18 % 4.94/5.17 20. (All C1, (All S2, (All C2, (((iext (uri_rdf_first) T_0 C1) /\ ((iext (uri_rdf_rest) T_0 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) T_2 T_0) <=> ((ic T_2) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext T_2 X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (iext (uri_owl_unionOf) T_2 T_0) ### All 19 % 4.94/5.17 21. (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) T_2 S1) <=> ((ic T_2) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext T_2 X) <=> ((icext C1 X) \/ (icext C2 X))))))))))))) (iext (uri_owl_unionOf) T_2 T_0) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) ### All 20 % 4.94/5.17 22. (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (icext (uri_ex_Eagle) (uri_ex_harry))) (iext (uri_owl_unionOf) T_2 T_0) ### All 21 % 4.94/5.17 23. (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle))) (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle)) ### Axiom % 4.94/5.17 24. ((iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle)) <=> (icext (uri_ex_Eagle) (uri_ex_harry))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle))) (iext (uri_owl_unionOf) T_2 T_0) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) ### Equiv 22 23 % 4.94/5.18 25. (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (-. (icext (uri_ex_Falcon) (uri_ex_harry))) (iext (uri_owl_unionOf) T_2 T_0) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle))) ### All 24 % 4.94/5.18 26. (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon))) (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon)) ### Axiom % 4.94/5.18 27. ((iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon)) <=> (icext (uri_ex_Falcon) (uri_ex_harry))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle))) (iext (uri_owl_unionOf) T_2 T_0) (iext (uri_rdf_type) (uri_ex_harry) T_2) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) ### Equiv 25 26 % 4.94/5.18 28. (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (All C, ((iext (uri_rdf_type) (uri_ex_harry) C) <=> (icext C (uri_ex_harry)))) (iext (uri_rdf_type) (uri_ex_harry) T_2) (iext (uri_owl_unionOf) T_2 T_0) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon))) ### All 27 % 4.94/5.18 29. (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle))) (iext (uri_owl_unionOf) T_2 T_0) (iext (uri_rdf_type) (uri_ex_harry) T_2) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) ### All 28 % 4.94/5.18 30. (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) (-. (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species))) ### Axiom % 4.94/5.18 31. (-. ((iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Eagle)) /\ (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)))) (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_harry) T_2) (iext (uri_owl_unionOf) T_2 T_0) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) ### NotAnd 29 30 % 4.94/5.18 32. (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon))) (iext (uri_owl_unionOf) T_2 T_0) (iext (uri_rdf_type) (uri_ex_harry) T_2) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) ### NotExists 31 % 4.94/5.18 33. (iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) (-. (iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species))) ### Axiom % 4.94/5.18 34. (-. ((iext (uri_rdf_type) (uri_ex_harry) (uri_ex_Falcon)) /\ (iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)))) (iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_type) (uri_ex_harry) T_2) (iext (uri_owl_unionOf) T_2 T_0) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) ### NotAnd 32 33 % 4.94/5.18 35. (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (iext (uri_owl_unionOf) T_2 T_0) (iext (uri_rdf_type) (uri_ex_harry) T_2) (iext (uri_rdf_rest) T_1 (uri_rdf_nil)) (iext (uri_rdf_first) T_1 (uri_ex_Falcon)) (iext (uri_rdf_rest) T_0 T_1) (iext (uri_rdf_first) T_0 (uri_ex_Eagle)) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) (iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) ### NotExists 34 % 4.94/5.18 36. ((iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_harry) T_2) /\ ((iext (uri_owl_unionOf) T_2 T_0) /\ ((iext (uri_rdf_first) T_0 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) T_0 T_1) /\ ((iext (uri_rdf_first) T_1 (uri_ex_Falcon)) /\ (iext (uri_rdf_rest) T_1 (uri_rdf_nil))))))))) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) ### ConjTree 35 % 4.94/5.18 37. (Ex BNODE_l2, ((iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_harry) T_2) /\ ((iext (uri_owl_unionOf) T_2 T_0) /\ ((iext (uri_rdf_first) T_0 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) T_0 BNODE_l2) /\ ((iext (uri_rdf_first) BNODE_l2 (uri_ex_Falcon)) /\ (iext (uri_rdf_rest) BNODE_l2 (uri_rdf_nil)))))))))) (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) ### Exists 36 % 4.94/5.18 38. (Ex BNODE_l1, (Ex BNODE_l2, ((iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_harry) T_2) /\ ((iext (uri_owl_unionOf) T_2 BNODE_l1) /\ ((iext (uri_rdf_first) BNODE_l1 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) BNODE_l1 BNODE_l2) /\ ((iext (uri_rdf_first) BNODE_l2 (uri_ex_Falcon)) /\ (iext (uri_rdf_rest) BNODE_l2 (uri_rdf_nil))))))))))) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) ### Exists 37 % 4.94/5.18 39. (Ex BNODE_u, (Ex BNODE_l1, (Ex BNODE_l2, ((iext (uri_rdf_type) (uri_ex_Eagle) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_Falcon) (uri_ex_Species)) /\ ((iext (uri_rdf_type) (uri_ex_harry) BNODE_u) /\ ((iext (uri_owl_unionOf) BNODE_u BNODE_l1) /\ ((iext (uri_rdf_first) BNODE_l1 (uri_ex_Eagle)) /\ ((iext (uri_rdf_rest) BNODE_l1 BNODE_l2) /\ ((iext (uri_rdf_first) BNODE_l2 (uri_ex_Falcon)) /\ (iext (uri_rdf_rest) BNODE_l2 (uri_rdf_nil)))))))))))) (-. (Ex BNODE_x, ((iext (uri_rdf_type) (uri_ex_harry) BNODE_x) /\ (iext (uri_rdf_type) BNODE_x (uri_ex_Species))))) (All X, (All C, ((iext (uri_rdf_type) X C) <=> (icext C X)))) (All Z, (All S1, (All C1, (All S2, (All C2, (((iext (uri_rdf_first) S1 C1) /\ ((iext (uri_rdf_rest) S1 S2) /\ ((iext (uri_rdf_first) S2 C2) /\ (iext (uri_rdf_rest) S2 (uri_rdf_nil))))) => ((iext (uri_owl_unionOf) Z S1) <=> ((ic Z) /\ ((ic C1) /\ ((ic C2) /\ (All X, ((icext Z X) <=> ((icext C1 X) \/ (icext C2 X)))))))))))))) ### Exists 38 % 4.94/5.18 % SZS output end Proof % 4.94/5.18 (* END-PROOF *) %------------------------------------------------------------------------------