%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB022+2 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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 : 300s % DateTime : Fri Oct 3 08:03:27 PM UTC 2025 % Result : Theorem 25.68s 25.90s % Output : Proof 26.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB022+2 : TPTP v9.2.0. Released v5.2.0. % 0.03/0.13 % Command : duper %s % 0.13/0.35 % Computer : n021.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 11:49:08 EDT 2025 % 0.13/0.35 % CPUTime : % 25.68/25.90 SZS status Theorem for theBenchmark.p % 25.68/25.90 SZS output start Proof for theBenchmark.p % 25.68/25.90 Clause #0 (by assumption #[]): Eq (∀ (P Q : Iota), iext uri_rdfs_subPropertyOf P Q → And (And (ip P) (ip Q)) (∀ (X Y : Iota), iext P X Y → iext Q X Y)) % 25.68/25.90 True % 25.68/25.90 Clause #1 (by assumption #[]): Eq % 25.68/25.90 (∀ (P S1 P1 S2 P2 : Iota), % 25.68/25.90 And (And (And (iext uri_rdf_first S1 P1) (iext uri_rdf_rest S1 S2)) (iext uri_rdf_first S2 P2)) % 25.68/25.90 (iext uri_rdf_rest S2 uri_rdf_nil) → % 25.68/25.90 Iff (iext uri_owl_propertyChainAxiom P S1) % 25.68/25.90 (And (And (And (ip P) (ip P1)) (ip P2)) % 25.68/25.90 (∀ (Y0 Y1 Y2 : Iota), And (iext P1 Y0 Y1) (iext P2 Y1 Y2) → iext P Y0 Y2))) % 25.68/25.90 True % 25.68/25.90 Clause #2 (by assumption #[]): Eq % 25.68/25.90 (Not % 25.68/25.90 (And % 25.68/25.90 (And (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_X) % 25.68/25.90 (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y)) % 25.68/25.90 (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z))) % 25.68/25.90 True % 25.68/25.90 Clause #3 (by assumption #[]): Eq % 25.68/25.90 (Exists fun BNODE_pL => % 25.68/25.90 Exists fun BNODE_l11 => % 25.68/25.90 Exists fun BNODE_l12 => % 25.68/25.90 Exists fun BNODE_l21 => % 25.68/25.90 Exists fun BNODE_l22 => % 25.68/25.90 Exists fun BNODE_l31 => % 25.68/25.90 Exists fun BNODE_l32 => % 25.68/25.90 Exists fun BNODE_l33 => % 25.68/25.90 And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And % 25.68/25.90 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList BNODE_pL) % 25.68/25.90 (iext uri_owl_propertyChainAxiom uri_skos_member BNODE_l11)) % 25.68/25.90 (iext uri_rdf_first BNODE_l11 BNODE_pL)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l11 BNODE_l12)) % 25.68/25.90 (iext uri_rdf_first BNODE_l12 uri_rdf_first)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l12 uri_rdf_nil)) % 25.68/25.90 (iext uri_owl_propertyChainAxiom BNODE_pL BNODE_l21)) % 25.68/25.90 (iext uri_rdf_first BNODE_l21 BNODE_pL)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 25.68/25.90 (iext uri_rdf_first BNODE_l22 uri_rdf_rest)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 25.68/25.90 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.68/25.90 (iext uri_skos_memberList uri_ex_MyOrderedCollection BNODE_l31)) % 25.68/25.90 (iext uri_rdf_first BNODE_l31 uri_ex_X)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l31 BNODE_l32)) % 25.68/25.90 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.68/25.90 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.68/25.90 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.68/25.90 True % 25.68/25.90 Clause #4 (by clausification #[2]): Eq % 25.68/25.90 (And % 25.68/25.90 (And (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_X) % 25.68/25.90 (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y)) % 25.68/25.90 (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z)) % 25.68/25.90 False % 25.68/25.90 Clause #5 (by clausification #[4]): Or % 25.68/25.90 (Eq % 25.68/25.90 (And (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_X) % 25.68/25.90 (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y)) % 25.68/25.90 False) % 25.68/25.90 (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z) False) % 25.68/25.90 Clause #6 (by clausification #[5]): Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z) False) % 25.68/25.94 (Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_X) False) % 25.68/25.94 (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) False)) % 25.68/25.94 Clause #7 (by clausification #[0]): ∀ (a : Iota), % 25.68/25.94 Eq (∀ (Q : Iota), iext uri_rdfs_subPropertyOf a Q → And (And (ip a) (ip Q)) (∀ (X Y : Iota), iext a X Y → iext Q X Y)) % 25.68/25.94 True % 25.68/25.94 Clause #8 (by clausification #[7]): ∀ (a a_1 : Iota), % 25.68/25.94 Eq (iext uri_rdfs_subPropertyOf a a_1 → And (And (ip a) (ip a_1)) (∀ (X Y : Iota), iext a X Y → iext a_1 X Y)) True % 25.68/25.94 Clause #9 (by clausification #[8]): ∀ (a a_1 : Iota), % 25.68/25.94 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) % 25.68/25.94 (Eq (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), iext a X Y → iext a_1 X Y)) True) % 25.68/25.94 Clause #10 (by clausification #[9]): ∀ (a a_1 : Iota), % 25.68/25.94 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) (Eq (∀ (X Y : Iota), iext a X Y → iext a_1 X Y) True) % 25.68/25.94 Clause #12 (by clausification #[10]): ∀ (a a_1 a_2 : Iota), % 25.68/25.94 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) (Eq (∀ (Y : Iota), iext a a_2 Y → iext a_1 a_2 Y) True) % 25.68/25.94 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 : Iota), % 25.68/25.94 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) (Eq (iext a a_2 a_3 → iext a_1 a_2 a_3) True) % 25.68/25.94 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 : Iota), % 25.68/25.94 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) (Or (Eq (iext a a_2 a_3) False) (Eq (iext a_1 a_2 a_3) True)) % 25.68/25.94 Clause #17 (by clausification #[1]): ∀ (a : Iota), % 25.68/25.94 Eq % 25.68/25.94 (∀ (S1 P1 S2 P2 : Iota), % 25.68/25.94 And (And (And (iext uri_rdf_first S1 P1) (iext uri_rdf_rest S1 S2)) (iext uri_rdf_first S2 P2)) % 25.68/25.94 (iext uri_rdf_rest S2 uri_rdf_nil) → % 25.68/25.94 Iff (iext uri_owl_propertyChainAxiom a S1) % 25.68/25.94 (And (And (And (ip a) (ip P1)) (ip P2)) % 25.68/25.94 (∀ (Y0 Y1 Y2 : Iota), And (iext P1 Y0 Y1) (iext P2 Y1 Y2) → iext a Y0 Y2))) % 25.68/25.94 True % 25.68/25.94 Clause #18 (by clausification #[17]): ∀ (a a_1 : Iota), % 25.68/25.94 Eq % 25.68/25.94 (∀ (P1 S2 P2 : Iota), % 25.68/25.94 And (And (And (iext uri_rdf_first a P1) (iext uri_rdf_rest a S2)) (iext uri_rdf_first S2 P2)) % 25.68/25.94 (iext uri_rdf_rest S2 uri_rdf_nil) → % 25.68/25.94 Iff (iext uri_owl_propertyChainAxiom a_1 a) % 25.68/25.94 (And (And (And (ip a_1) (ip P1)) (ip P2)) % 25.68/25.94 (∀ (Y0 Y1 Y2 : Iota), And (iext P1 Y0 Y1) (iext P2 Y1 Y2) → iext a_1 Y0 Y2))) % 25.68/25.94 True % 25.68/25.94 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), % 25.68/25.94 Eq % 25.68/25.94 (∀ (S2 P2 : Iota), % 25.68/25.94 And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a S2)) (iext uri_rdf_first S2 P2)) % 25.68/25.94 (iext uri_rdf_rest S2 uri_rdf_nil) → % 25.68/25.94 Iff (iext uri_owl_propertyChainAxiom a_2 a) % 25.68/25.94 (And (And (And (ip a_2) (ip a_1)) (ip P2)) % 25.68/25.94 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext P2 Y1 Y2) → iext a_2 Y0 Y2))) % 25.68/25.94 True % 25.68/25.94 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 : Iota), % 25.68/25.94 Eq % 25.68/25.94 (∀ (P2 : Iota), % 25.68/25.94 And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a a_2)) (iext uri_rdf_first a_2 P2)) % 25.68/25.94 (iext uri_rdf_rest a_2 uri_rdf_nil) → % 25.68/25.94 Iff (iext uri_owl_propertyChainAxiom a_3 a) % 25.68/25.94 (And (And (And (ip a_3) (ip a_1)) (ip P2)) % 25.68/25.94 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext P2 Y1 Y2) → iext a_3 Y0 Y2))) % 25.68/25.94 True % 25.68/25.94 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.68/25.94 Eq % 25.68/25.94 (And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a a_2)) (iext uri_rdf_first a_2 a_3)) % 25.68/25.94 (iext uri_rdf_rest a_2 uri_rdf_nil) → % 25.68/25.94 Iff (iext uri_owl_propertyChainAxiom a_4 a) % 25.68/25.94 (And (And (And (ip a_4) (ip a_1)) (ip a_3)) % 25.68/25.94 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2) → iext a_4 Y0 Y2))) % 25.68/25.94 True % 25.68/25.94 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.68/25.94 Or % 25.68/25.94 (Eq % 25.68/25.94 (And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a a_2)) (iext uri_rdf_first a_2 a_3)) % 25.68/25.94 (iext uri_rdf_rest a_2 uri_rdf_nil)) % 25.68/25.94 False) % 25.68/25.94 (Eq % 25.68/25.94 (Iff (iext uri_owl_propertyChainAxiom a_4 a) % 25.68/25.94 (And (And (And (ip a_4) (ip a_1)) (ip a_3)) % 25.68/25.94 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2) → iext a_4 Y0 Y2))) % 25.68/25.98 True) % 25.68/25.98 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.68/25.98 Or % 25.68/25.98 (Eq % 25.68/25.98 (Iff (iext uri_owl_propertyChainAxiom a a_1) % 25.68/25.98 (And (And (And (ip a) (ip a_2)) (ip a_3)) % 25.68/25.98 (∀ (Y0 Y1 Y2 : Iota), And (iext a_2 Y0 Y1) (iext a_3 Y1 Y2) → iext a Y0 Y2))) % 25.68/25.98 True) % 25.68/25.98 (Or (Eq (And (And (iext uri_rdf_first a_1 a_2) (iext uri_rdf_rest a_1 a_4)) (iext uri_rdf_first a_4 a_3)) False) % 25.68/25.98 (Eq (iext uri_rdf_rest a_4 uri_rdf_nil) False)) % 25.68/25.98 Clause #25 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.68/25.98 Or (Eq (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a a_2)) (iext uri_rdf_first a_2 a_3)) False) % 25.68/25.98 (Or (Eq (iext uri_rdf_rest a_2 uri_rdf_nil) False) % 25.68/25.98 (Or (Eq (iext uri_owl_propertyChainAxiom a_4 a) False) % 25.68/25.98 (Eq % 25.68/25.98 (And (And (And (ip a_4) (ip a_1)) (ip a_3)) % 25.68/25.98 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2) → iext a_4 Y0 Y2)) % 25.68/25.98 True))) % 25.68/25.98 Clause #41 (by clausification #[3]): ∀ (a : Iota), % 25.68/25.98 Eq % 25.68/25.98 (Exists fun BNODE_l11 => % 25.68/25.98 Exists fun BNODE_l12 => % 25.68/25.98 Exists fun BNODE_l21 => % 25.68/25.98 Exists fun BNODE_l22 => % 25.68/25.98 Exists fun BNODE_l31 => % 25.68/25.98 Exists fun BNODE_l32 => % 25.68/25.98 Exists fun BNODE_l33 => % 25.68/25.98 And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.68/25.98 (iext uri_owl_propertyChainAxiom uri_skos_member BNODE_l11)) % 25.68/25.98 (iext uri_rdf_first BNODE_l11 (skS.0 3 a))) % 25.68/25.98 (iext uri_rdf_rest BNODE_l11 BNODE_l12)) % 25.68/25.98 (iext uri_rdf_first BNODE_l12 uri_rdf_first)) % 25.68/25.98 (iext uri_rdf_rest BNODE_l12 uri_rdf_nil)) % 25.68/25.98 (iext uri_owl_propertyChainAxiom (skS.0 3 a) BNODE_l21)) % 25.68/25.98 (iext uri_rdf_first BNODE_l21 (skS.0 3 a))) % 25.68/25.98 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 25.68/25.98 (iext uri_rdf_first BNODE_l22 uri_rdf_rest)) % 25.68/25.98 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 25.68/25.98 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.68/25.98 (iext uri_skos_memberList uri_ex_MyOrderedCollection BNODE_l31)) % 25.68/25.98 (iext uri_rdf_first BNODE_l31 uri_ex_X)) % 25.68/25.98 (iext uri_rdf_rest BNODE_l31 BNODE_l32)) % 25.68/25.98 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.68/25.98 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.68/25.98 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.68/25.98 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.68/25.98 True % 25.68/25.98 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 25.68/25.98 Eq % 25.68/25.98 (Exists fun BNODE_l12 => % 25.68/25.98 Exists fun BNODE_l21 => % 25.68/25.98 Exists fun BNODE_l22 => % 25.68/25.98 Exists fun BNODE_l31 => % 25.68/25.98 Exists fun BNODE_l32 => % 25.68/25.98 Exists fun BNODE_l33 => % 25.68/25.98 And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.68/25.98 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.77/25.99 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.77/25.99 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.77/25.99 (iext uri_rdf_rest (skS.0 4 a a_1) BNODE_l12)) % 25.77/25.99 (iext uri_rdf_first BNODE_l12 uri_rdf_first)) % 25.77/25.99 (iext uri_rdf_rest BNODE_l12 uri_rdf_nil)) % 25.77/25.99 (iext uri_owl_propertyChainAxiom (skS.0 3 a) BNODE_l21)) % 25.77/25.99 (iext uri_rdf_first BNODE_l21 (skS.0 3 a))) % 25.77/25.99 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 25.77/25.99 (iext uri_rdf_first BNODE_l22 uri_rdf_rest)) % 25.77/25.99 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 25.77/25.99 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.77/25.99 (iext uri_skos_memberList uri_ex_MyOrderedCollection BNODE_l31)) % 25.77/25.99 (iext uri_rdf_first BNODE_l31 uri_ex_X)) % 25.77/25.99 (iext uri_rdf_rest BNODE_l31 BNODE_l32)) % 25.77/25.99 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.77/25.99 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.77/25.99 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.77/25.99 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.77/25.99 True % 25.77/25.99 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 25.77/25.99 Eq % 25.77/25.99 (Exists fun BNODE_l21 => % 25.77/25.99 Exists fun BNODE_l22 => % 25.77/25.99 Exists fun BNODE_l31 => % 25.77/25.99 Exists fun BNODE_l32 => % 25.77/25.99 Exists fun BNODE_l33 => % 25.77/25.99 And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And % 25.77/25.99 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.77/25.99 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.77/25.99 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.77/25.99 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.77/25.99 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.77/25.99 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.77/25.99 (iext uri_owl_propertyChainAxiom (skS.0 3 a) BNODE_l21)) % 25.77/25.99 (iext uri_rdf_first BNODE_l21 (skS.0 3 a))) % 25.77/25.99 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 25.77/25.99 (iext uri_rdf_first BNODE_l22 uri_rdf_rest)) % 25.77/25.99 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 25.77/25.99 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.77/25.99 (iext uri_skos_memberList uri_ex_MyOrderedCollection BNODE_l31)) % 25.77/25.99 (iext uri_rdf_first BNODE_l31 uri_ex_X)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l31 BNODE_l32)) % 25.80/26.02 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.80/26.02 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.80/26.02 True % 25.80/26.02 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 : Iota), % 25.80/26.02 Eq % 25.80/26.02 (Exists fun BNODE_l22 => % 25.80/26.02 Exists fun BNODE_l31 => % 25.80/26.02 Exists fun BNODE_l32 => % 25.80/26.02 Exists fun BNODE_l33 => % 25.80/26.02 And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.80/26.02 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.80/26.02 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.80/26.02 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.80/26.02 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.80/26.02 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.80/26.02 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.80/26.02 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.80/26.02 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) BNODE_l22)) % 25.80/26.02 (iext uri_rdf_first BNODE_l22 uri_rdf_rest)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 25.80/26.02 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.80/26.02 (iext uri_skos_memberList uri_ex_MyOrderedCollection BNODE_l31)) % 25.80/26.02 (iext uri_rdf_first BNODE_l31 uri_ex_X)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l31 BNODE_l32)) % 25.80/26.02 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.80/26.02 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.80/26.02 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.80/26.02 True % 25.80/26.02 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.80/26.02 Eq % 25.80/26.02 (Exists fun BNODE_l31 => % 25.80/26.02 Exists fun BNODE_l32 => % 25.80/26.02 Exists fun BNODE_l33 => % 25.80/26.02 And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And % 25.80/26.02 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.80/26.02 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.80/26.02 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.80/26.02 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.80/26.02 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.80/26.02 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.80/26.02 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.80/26.05 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.80/26.05 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.80/26.05 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.80/26.05 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.80/26.05 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.80/26.05 (iext uri_skos_memberList uri_ex_MyOrderedCollection BNODE_l31)) % 25.80/26.05 (iext uri_rdf_first BNODE_l31 uri_ex_X)) % 25.80/26.05 (iext uri_rdf_rest BNODE_l31 BNODE_l32)) % 25.80/26.05 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.80/26.05 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.80/26.05 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.80/26.05 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.80/26.05 True % 25.80/26.05 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 25.80/26.05 Eq % 25.80/26.05 (Exists fun BNODE_l32 => % 25.80/26.05 Exists fun BNODE_l33 => % 25.80/26.05 And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.80/26.05 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.80/26.05 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.80/26.05 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.80/26.05 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.80/26.05 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.80/26.05 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.80/26.05 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.80/26.05 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.80/26.05 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.80/26.05 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.80/26.05 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.80/26.05 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.80/26.05 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.80/26.05 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) BNODE_l32)) % 25.80/26.05 (iext uri_rdf_first BNODE_l32 uri_ex_Y)) % 25.80/26.05 (iext uri_rdf_rest BNODE_l32 BNODE_l33)) % 25.80/26.05 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.80/26.05 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.80/26.05 True % 25.80/26.05 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 25.80/26.05 Eq % 25.80/26.05 (Exists fun BNODE_l33 => % 25.80/26.05 And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And % 25.80/26.05 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.80/26.05 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.80/26.05 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.80/26.09 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.80/26.09 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.80/26.09 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.80/26.09 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.80/26.09 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.80/26.09 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.80/26.09 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.80/26.09 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.80/26.09 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 25.80/26.09 (iext uri_rdf_first (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) uri_ex_Y)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) BNODE_l33)) % 25.80/26.09 (iext uri_rdf_first BNODE_l33 uri_ex_Z)) % 25.80/26.09 (iext uri_rdf_rest BNODE_l33 uri_rdf_nil)) % 25.80/26.09 True % 25.80/26.09 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.80/26.09 Eq % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.80/26.09 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.80/26.09 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.80/26.09 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.80/26.09 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.80/26.09 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.80/26.09 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.80/26.09 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.80/26.09 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.80/26.09 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.80/26.09 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.80/26.09 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 25.80/26.09 (iext uri_rdf_first (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) uri_ex_Y)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 25.80/26.09 (iext uri_rdf_first (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) uri_ex_Z)) % 25.80/26.09 (iext uri_rdf_rest (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) uri_rdf_nil)) % 25.80/26.09 True % 25.80/26.09 Clause #50 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.80/26.09 Eq % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.09 (And % 25.80/26.12 (And % 25.80/26.12 (And % 25.80/26.12 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.80/26.12 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.80/26.12 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.80/26.12 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.80/26.12 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.80/26.12 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.80/26.12 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.80/26.12 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.80/26.12 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.80/26.12 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.80/26.12 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.80/26.12 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.80/26.12 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.80/26.12 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.80/26.12 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 25.80/26.12 (iext uri_rdf_first (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) uri_ex_Y)) % 25.80/26.12 (iext uri_rdf_rest (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 25.80/26.12 (iext uri_rdf_first (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) uri_ex_Z)) % 25.80/26.12 True % 25.80/26.12 Clause #52 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.80/26.12 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.80/26.12 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.80/26.12 (Or % 25.80/26.12 (Eq % 25.80/26.12 (And (And (And (ip a_1) (ip a_3)) (ip a_4)) % 25.80/26.12 (∀ (Y0 Y1 Y2 : Iota), And (iext a_3 Y0 Y1) (iext a_4 Y1 Y2) → iext a_1 Y0 Y2)) % 25.80/26.12 True) % 25.80/26.12 (Or (Eq (And (iext uri_rdf_first a_2 a_3) (iext uri_rdf_rest a_2 a)) False) % 25.80/26.12 (Eq (iext uri_rdf_first a a_4) False)))) % 25.80/26.12 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.80/26.12 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.80/26.12 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.80/26.12 (Or (Eq (And (iext uri_rdf_first a_2 a_3) (iext uri_rdf_rest a_2 a)) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a a_4) False) % 25.80/26.12 (Eq (∀ (Y0 Y1 Y2 : Iota), And (iext a_3 Y0 Y1) (iext a_4 Y1 Y2) → iext a_1 Y0 Y2) True)))) % 25.80/26.12 Clause #55 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.80/26.12 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.80/26.12 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a a_3) False) % 25.80/26.12 (Or (Eq (∀ (Y0 Y1 Y2 : Iota), And (iext a_4 Y0 Y1) (iext a_3 Y1 Y2) → iext a_1 Y0 Y2) True) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a_2 a_4) False) (Eq (iext uri_rdf_rest a_2 a) False))))) % 25.80/26.12 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 25.80/26.12 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.80/26.12 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a a_3) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 25.80/26.12 (Eq (∀ (Y1 Y2 : Iota), And (iext a_4 a_5 Y1) (iext a_3 Y1 Y2) → iext a_1 a_5 Y2) True))))) % 25.80/26.12 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 25.80/26.12 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.80/26.12 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a a_3) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 25.80/26.12 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 25.80/26.12 (Eq (∀ (Y2 : Iota), And (iext a_4 a_5 a_6) (iext a_3 a_6 Y2) → iext a_1 a_5 Y2) True))))) % 25.80/26.12 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.80/26.12 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.91/26.16 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_first a a_3) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 25.91/26.16 (Eq (And (iext a_4 a_5 a_6) (iext a_3 a_6 a_7) → iext a_1 a_5 a_7) True))))) % 25.91/26.16 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.91/26.16 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.91/26.16 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_first a a_3) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 25.91/26.16 (Or (Eq (And (iext a_4 a_5 a_6) (iext a_3 a_6 a_7)) False) (Eq (iext a_1 a_5 a_7) True)))))) % 25.91/26.16 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.91/26.16 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 25.91/26.16 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_first a a_3) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 25.91/26.16 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 25.91/26.16 (Or (Eq (iext a_1 a_5 a_6) True) (Or (Eq (iext a_4 a_5 a_7) False) (Eq (iext a_3 a_7 a_6) False))))))) % 25.91/26.16 Clause #77 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (iext uri_rdf_first (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) uri_ex_Z) True % 25.91/26.16 Clause #78 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.91/26.16 Eq % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.91/26.16 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.91/26.16 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.91/26.16 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.91/26.16 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.91/26.16 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.91/26.16 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.91/26.16 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.91/26.16 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.91/26.16 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.91/26.16 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.91/26.16 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.91/26.16 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.91/26.16 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.91/26.16 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 25.91/26.16 (iext uri_rdf_first (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) uri_ex_Y)) % 25.91/26.16 (iext uri_rdf_rest (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 25.91/26.16 True % 25.91/26.16 Clause #90 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 25.91/26.16 Eq (iext uri_rdf_rest (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 25.91/26.16 Clause #91 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 25.91/26.16 Eq % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And % 25.91/26.16 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.91/26.16 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.91/26.19 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.91/26.19 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.91/26.19 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.91/26.19 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.91/26.19 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.91/26.19 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.91/26.19 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.91/26.19 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.91/26.19 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.91/26.19 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 25.91/26.19 (iext uri_rdf_first (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) uri_ex_Y)) % 25.91/26.19 True % 25.91/26.19 Clause #98 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (iext uri_rdf_first (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) uri_ex_Y) True % 25.91/26.19 Clause #99 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 25.91/26.19 Eq % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.91/26.19 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.91/26.19 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.91/26.19 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.91/26.19 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.91/26.19 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.91/26.19 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.91/26.19 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.91/26.19 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.91/26.19 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.91/26.19 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.91/26.19 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 25.91/26.19 True % 25.91/26.19 Clause #105 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 25.91/26.19 Eq (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6)) True % 25.91/26.19 Clause #106 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 25.91/26.19 Eq % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And % 25.91/26.19 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.91/26.19 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.91/26.19 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.91/26.19 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.91/26.19 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.91/26.19 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.91/26.19 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.99/26.22 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.99/26.22 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.99/26.22 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.99/26.22 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.99/26.22 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.99/26.22 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.99/26.22 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X)) % 25.99/26.22 True % 25.99/26.22 Clause #114 (by clausification #[106]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3 a_4 a_5) uri_ex_X) True % 25.99/26.22 Clause #115 (by clausification #[106]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 25.99/26.22 Eq % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.99/26.22 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.99/26.22 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.99/26.22 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.99/26.22 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.99/26.22 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.99/26.22 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.99/26.22 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.99/26.22 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.99/26.22 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.99/26.22 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.99/26.22 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.99/26.22 (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 25.99/26.22 True % 25.99/26.22 Clause #122 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 25.99/26.22 Eq (iext uri_skos_memberList uri_ex_MyOrderedCollection (skS.0 8 a a_1 a_2 a_3 a_4 a_5)) True % 25.99/26.22 Clause #123 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.99/26.22 Eq % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.99/26.22 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.99/26.22 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.99/26.22 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.99/26.22 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.99/26.22 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.99/26.22 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.99/26.22 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.99/26.22 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.99/26.22 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.99/26.22 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.99/26.22 (iext uri_rdf_type uri_ex_MyOrderedCollection uri_skos_OrderedCollection)) % 25.99/26.22 True % 25.99/26.22 Clause #125 (by clausification #[123]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.99/26.22 Eq % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And % 25.99/26.22 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.99/26.22 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.99/26.22 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.99/26.22 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.99/26.22 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.99/26.26 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.99/26.26 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.99/26.26 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.99/26.26 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.99/26.26 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.99/26.26 (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 25.99/26.26 True % 25.99/26.26 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_rest (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_nil) True % 25.99/26.26 Clause #127 (by clausification #[125]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.99/26.26 Eq % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.99/26.26 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.99/26.26 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.99/26.26 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.99/26.26 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.99/26.26 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.99/26.26 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.99/26.26 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.99/26.26 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.99/26.26 (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest)) % 25.99/26.26 True % 25.99/26.26 Clause #129 (by superposition #[126, 60]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 25.99/26.26 Or (Eq True False) % 25.99/26.26 (Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 25.99/26.26 (Or (Eq (iext uri_rdf_first (skS.0 7 a_2 a_3 a_4 a_5 a_6) a_7) False) % 25.99/26.26 (Or (Eq (iext uri_rdf_first a_1 a_8) False) % 25.99/26.26 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 7 a_2 a_3 a_4 a_5 a_6)) False) % 25.99/26.26 (Or (Eq (iext a a_9 a_10) True) (Or (Eq (iext a_8 a_9 a_11) False) (Eq (iext a_7 a_11 a_10) False))))))) % 25.99/26.26 Clause #138 (by clausification #[129]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 25.99/26.26 Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 25.99/26.26 (Or (Eq (iext uri_rdf_first (skS.0 7 a_2 a_3 a_4 a_5 a_6) a_7) False) % 25.99/26.26 (Or (Eq (iext uri_rdf_first a_1 a_8) False) % 25.99/26.26 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 7 a_2 a_3 a_4 a_5 a_6)) False) % 25.99/26.26 (Or (Eq (iext a a_9 a_10) True) (Or (Eq (iext a_8 a_9 a_11) False) (Eq (iext a_7 a_11 a_10) False)))))) % 25.99/26.26 Clause #140 (by clausification #[127]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) uri_rdf_rest) True % 25.99/26.26 Clause #141 (by clausification #[127]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 25.99/26.26 Eq % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.99/26.26 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.99/26.26 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 25.99/26.26 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 25.99/26.26 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 25.99/26.26 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 25.99/26.26 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 25.99/26.26 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 25.99/26.26 (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4))) % 25.99/26.26 True % 25.99/26.26 Clause #162 (by clausification #[141]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3 a_4)) True % 25.99/26.26 Clause #163 (by clausification #[141]): ∀ (a a_1 a_2 a_3 : Iota), % 25.99/26.26 Eq % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And % 25.99/26.26 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 25.99/26.26 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 25.99/26.26 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 26.08/26.31 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 26.08/26.31 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 26.08/26.31 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 26.08/26.31 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 26.08/26.31 (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a))) % 26.08/26.31 True % 26.08/26.31 Clause #185 (by clausification #[163]): ∀ (a a_1 a_2 a_3 : Iota), Eq (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) (skS.0 3 a)) True % 26.08/26.31 Clause #186 (by clausification #[163]): ∀ (a a_1 a_2 a_3 : Iota), % 26.08/26.31 Eq % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 26.08/26.31 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 26.08/26.31 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 26.08/26.31 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 26.08/26.31 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 26.08/26.31 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 26.08/26.31 (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 26.08/26.31 True % 26.08/26.31 Clause #195 (by clausification #[186]): ∀ (a a_1 a_2 a_3 : Iota), Eq (iext uri_owl_propertyChainAxiom (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3)) True % 26.08/26.31 Clause #196 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), % 26.08/26.31 Eq % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 26.08/26.31 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 26.08/26.31 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 26.08/26.31 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 26.08/26.31 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 26.08/26.31 (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil)) % 26.08/26.31 True % 26.08/26.31 Clause #204 (by superposition #[195, 138]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota), % 26.08/26.31 Or (Eq True False) % 26.08/26.31 (Or (Eq (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) a_5) False) % 26.08/26.31 (Or (Eq (iext uri_rdf_first (skS.0 6 a_6 a_7 a_8 a_9) a_10) False) % 26.08/26.31 (Or (Eq (iext uri_rdf_rest (skS.0 6 a_6 a_7 a_8 a_9) (skS.0 7 a a_1 a_2 a_3 a_4)) False) % 26.08/26.31 (Or (Eq (iext (skS.0 3 a_6) a_11 a_12) True) % 26.08/26.31 (Or (Eq (iext a_10 a_11 a_13) False) (Eq (iext a_5 a_13 a_12) False)))))) % 26.08/26.31 Clause #341 (by clausification #[204]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota), % 26.08/26.31 Or (Eq (iext uri_rdf_first (skS.0 7 a a_1 a_2 a_3 a_4) a_5) False) % 26.08/26.31 (Or (Eq (iext uri_rdf_first (skS.0 6 a_6 a_7 a_8 a_9) a_10) False) % 26.08/26.31 (Or (Eq (iext uri_rdf_rest (skS.0 6 a_6 a_7 a_8 a_9) (skS.0 7 a a_1 a_2 a_3 a_4)) False) % 26.08/26.31 (Or (Eq (iext (skS.0 3 a_6) a_11 a_12) True) % 26.08/26.31 (Or (Eq (iext a_10 a_11 a_13) False) (Eq (iext a_5 a_13 a_12) False))))) % 26.08/26.31 Clause #342 (by superposition #[341, 140]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 26.08/26.31 Or (Eq (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) a_4) False) % 26.08/26.31 (Or (Eq (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a_5 a_6 a_7 a_8 a_9)) False) % 26.08/26.31 (Or (Eq (iext (skS.0 3 a) a_10 a_11) True) % 26.08/26.31 (Or (Eq (iext a_4 a_10 a_12) False) (Or (Eq (iext uri_rdf_rest a_12 a_11) False) (Eq False True))))) % 26.08/26.31 Clause #343 (by clausification #[196]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_rdf_rest (skS.0 5 a a_1 a_2) uri_rdf_nil) True % 26.08/26.31 Clause #344 (by clausification #[196]): ∀ (a a_1 a_2 : Iota), % 26.08/26.31 Eq % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And % 26.08/26.31 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 26.08/26.31 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 26.08/26.31 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 26.08/26.31 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 26.08/26.31 (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first)) % 26.08/26.31 True % 26.08/26.31 Clause #346 (by superposition #[343, 60]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 26.08/26.31 Or (Eq True False) % 26.08/26.31 (Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 26.08/26.31 (Or (Eq (iext uri_rdf_first (skS.0 5 a_2 a_3 a_4) a_5) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_first a_1 a_6) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 5 a_2 a_3 a_4)) False) % 26.08/26.36 (Or (Eq (iext a a_7 a_8) True) (Or (Eq (iext a_6 a_7 a_9) False) (Eq (iext a_5 a_9 a_8) False))))))) % 26.08/26.36 Clause #370 (by clausification #[346]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 26.08/26.36 Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_first (skS.0 5 a_2 a_3 a_4) a_5) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_first a_1 a_6) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 5 a_2 a_3 a_4)) False) % 26.08/26.36 (Or (Eq (iext a a_7 a_8) True) (Or (Eq (iext a_6 a_7 a_9) False) (Eq (iext a_5 a_9 a_8) False)))))) % 26.08/26.36 Clause #382 (by clausification #[342]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 26.08/26.36 Or (Eq (iext uri_rdf_first (skS.0 6 a a_1 a_2 a_3) a_4) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a_5 a_6 a_7 a_8 a_9)) False) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_10 a_11) True) % 26.08/26.36 (Or (Eq (iext a_4 a_10 a_12) False) (Eq (iext uri_rdf_rest a_12 a_11) False)))) % 26.08/26.36 Clause #383 (by superposition #[382, 185]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 26.08/26.36 Or (Eq (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a_4 a_5 a_6 a_7 a_8)) False) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_9 a_10) True) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_9 a_11) False) (Or (Eq (iext uri_rdf_rest a_11 a_10) False) (Eq False True)))) % 26.08/26.36 Clause #384 (by clausification #[383]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 26.08/26.36 Or (Eq (iext uri_rdf_rest (skS.0 6 a a_1 a_2 a_3) (skS.0 7 a_4 a_5 a_6 a_7 a_8)) False) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_9 a_10) True) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_9 a_11) False) (Eq (iext uri_rdf_rest a_11 a_10) False))) % 26.08/26.36 Clause #385 (by superposition #[384, 162]): ∀ (a a_1 a_2 a_3 : Iota), % 26.08/26.36 Or (Eq (iext (skS.0 3 a) a_1 a_2) True) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_1 a_3) False) (Or (Eq (iext uri_rdf_rest a_3 a_2) False) (Eq False True))) % 26.08/26.36 Clause #386 (by clausification #[385]): ∀ (a a_1 a_2 a_3 : Iota), % 26.08/26.36 Or (Eq (iext (skS.0 3 a) a_1 a_2) True) % 26.08/26.36 (Or (Eq (iext (skS.0 3 a) a_1 a_3) False) (Eq (iext uri_rdf_rest a_3 a_2) False)) % 26.08/26.36 Clause #396 (by clausification #[344]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_rdf_first (skS.0 5 a a_1 a_2) uri_rdf_first) True % 26.08/26.36 Clause #397 (by clausification #[344]): ∀ (a a_1 a_2 : Iota), % 26.08/26.36 Eq % 26.08/26.36 (And % 26.08/26.36 (And % 26.08/26.36 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 26.08/26.36 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 26.08/26.36 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 26.08/26.36 (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2))) % 26.08/26.36 True % 26.08/26.36 Clause #414 (by clausification #[397]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a a_1 a_2)) True % 26.08/26.36 Clause #415 (by clausification #[397]): ∀ (a a_1 : Iota), % 26.08/26.36 Eq % 26.08/26.36 (And % 26.08/26.36 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 26.08/26.36 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 26.08/26.36 (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a))) % 26.08/26.36 True % 26.08/26.36 Clause #416 (by clausification #[415]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_first (skS.0 4 a a_1) (skS.0 3 a)) True % 26.08/26.36 Clause #417 (by clausification #[415]): ∀ (a a_1 : Iota), % 26.08/26.36 Eq % 26.08/26.36 (And (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) % 26.08/26.36 (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1))) % 26.08/26.36 True % 26.08/26.36 Clause #425 (by clausification #[417]): ∀ (a a_1 : Iota), Eq (iext uri_owl_propertyChainAxiom uri_skos_member (skS.0 4 a a_1)) True % 26.08/26.36 Clause #426 (by clausification #[417]): ∀ (a : Iota), Eq (iext uri_rdfs_subPropertyOf uri_skos_memberList (skS.0 3 a)) True % 26.08/26.36 Clause #438 (by superposition #[425, 370]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 26.08/26.36 Or (Eq True False) % 26.08/26.36 (Or (Eq (iext uri_rdf_first (skS.0 5 a a_1 a_2) a_3) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_first (skS.0 4 a_4 a_5) a_6) False) % 26.08/26.36 (Or (Eq (iext uri_rdf_rest (skS.0 4 a_4 a_5) (skS.0 5 a a_1 a_2)) False) % 26.08/26.36 (Or (Eq (iext uri_skos_member a_7 a_8) True) % 26.08/26.36 (Or (Eq (iext a_6 a_7 a_9) False) (Eq (iext a_3 a_9 a_8) False)))))) % 26.17/26.41 Clause #439 (by superposition #[426, 14]): ∀ (a a_1 a_2 : Iota), % 26.17/26.41 Or (Eq True False) (Or (Eq (iext uri_skos_memberList a a_1) False) (Eq (iext (skS.0 3 a_2) a a_1) True)) % 26.17/26.41 Clause #446 (by clausification #[439]): ∀ (a a_1 a_2 : Iota), Or (Eq (iext uri_skos_memberList a a_1) False) (Eq (iext (skS.0 3 a_2) a a_1) True) % 26.17/26.41 Clause #447 (by superposition #[446, 122]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection (skS.0 8 a_1 a_2 a_3 a_4 a_5 a_6)) True) (Eq False True) % 26.17/26.41 Clause #449 (by clausification #[447]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 26.17/26.41 Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection (skS.0 8 a_1 a_2 a_3 a_4 a_5 a_6)) True % 26.17/26.41 Clause #450 (by superposition #[449, 386]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection a_1) True) % 26.17/26.41 (Or (Eq True False) (Eq (iext uri_rdf_rest (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7) a_1) False)) % 26.17/26.41 Clause #451 (by clausification #[450]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection a_1) True) % 26.17/26.41 (Eq (iext uri_rdf_rest (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7) a_1) False) % 26.17/26.41 Clause #452 (by superposition #[451, 105]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True) (Eq False True) % 26.17/26.41 Clause #453 (by clausification #[452]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.41 Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 26.17/26.41 Clause #454 (by superposition #[453, 386]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection a_1) True) % 26.17/26.41 (Or (Eq True False) (Eq (iext uri_rdf_rest (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_1) False)) % 26.17/26.41 Clause #455 (by clausification #[454]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection a_1) True) % 26.17/26.41 (Eq (iext uri_rdf_rest (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_1) False) % 26.17/26.41 Clause #456 (by superposition #[455, 90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.41 Or (Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True) (Eq False True) % 26.17/26.41 Clause #457 (by clausification #[456]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.41 Eq (iext (skS.0 3 a) uri_ex_MyOrderedCollection (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True % 26.17/26.41 Clause #593 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 26.17/26.41 Or (Eq (iext uri_rdf_first (skS.0 5 a a_1 a_2) a_3) False) % 26.17/26.41 (Or (Eq (iext uri_rdf_first (skS.0 4 a_4 a_5) a_6) False) % 26.17/26.41 (Or (Eq (iext uri_rdf_rest (skS.0 4 a_4 a_5) (skS.0 5 a a_1 a_2)) False) % 26.17/26.41 (Or (Eq (iext uri_skos_member a_7 a_8) True) (Or (Eq (iext a_6 a_7 a_9) False) (Eq (iext a_3 a_9 a_8) False))))) % 26.17/26.41 Clause #594 (by superposition #[593, 396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.41 Or (Eq (iext uri_rdf_first (skS.0 4 a a_1) a_2) False) % 26.17/26.41 (Or (Eq (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a_3 a_4 a_5)) False) % 26.17/26.41 (Or (Eq (iext uri_skos_member a_6 a_7) True) % 26.17/26.41 (Or (Eq (iext a_2 a_6 a_8) False) (Or (Eq (iext uri_rdf_first a_8 a_7) False) (Eq False True))))) % 26.17/26.41 Clause #595 (by clausification #[594]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.41 Or (Eq (iext uri_rdf_first (skS.0 4 a a_1) a_2) False) % 26.17/26.41 (Or (Eq (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a_3 a_4 a_5)) False) % 26.17/26.41 (Or (Eq (iext uri_skos_member a_6 a_7) True) % 26.17/26.41 (Or (Eq (iext a_2 a_6 a_8) False) (Eq (iext uri_rdf_first a_8 a_7) False)))) % 26.17/26.41 Clause #596 (by superposition #[595, 416]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.41 Or (Eq (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a_2 a_3 a_4)) False) % 26.17/26.41 (Or (Eq (iext uri_skos_member a_5 a_6) True) % 26.17/26.41 (Or (Eq (iext (skS.0 3 a) a_5 a_7) False) (Or (Eq (iext uri_rdf_first a_7 a_6) False) (Eq False True)))) % 26.17/26.41 Clause #597 (by clausification #[596]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.41 Or (Eq (iext uri_rdf_rest (skS.0 4 a a_1) (skS.0 5 a_2 a_3 a_4)) False) % 26.17/26.45 (Or (Eq (iext uri_skos_member a_5 a_6) True) % 26.17/26.45 (Or (Eq (iext (skS.0 3 a) a_5 a_7) False) (Eq (iext uri_rdf_first a_7 a_6) False))) % 26.17/26.45 Clause #598 (by superposition #[597, 414]): ∀ (a a_1 a_2 a_3 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member a a_1) True) % 26.17/26.45 (Or (Eq (iext (skS.0 3 a_2) a a_3) False) (Or (Eq (iext uri_rdf_first a_3 a_1) False) (Eq False True))) % 26.17/26.45 Clause #599 (by clausification #[598]): ∀ (a a_1 a_2 a_3 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member a a_1) True) % 26.17/26.45 (Or (Eq (iext (skS.0 3 a_2) a a_3) False) (Eq (iext uri_rdf_first a_3 a_1) False)) % 26.17/26.45 Clause #602 (by superposition #[599, 449]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection a) True) % 26.17/26.45 (Or (Eq (iext uri_rdf_first (skS.0 8 a_1 a_2 a_3 a_4 a_5 a_6) a) False) (Eq False True)) % 26.17/26.45 Clause #603 (by superposition #[599, 453]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection a) True) % 26.17/26.45 (Or (Eq (iext uri_rdf_first (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6 a_7) a) False) (Eq False True)) % 26.17/26.45 Clause #604 (by superposition #[599, 457]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection a) True) % 26.17/26.45 (Or (Eq (iext uri_rdf_first (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a) False) (Eq False True)) % 26.17/26.45 Clause #611 (by clausification #[602]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection a) True) % 26.17/26.45 (Eq (iext uri_rdf_first (skS.0 8 a_1 a_2 a_3 a_4 a_5 a_6) a) False) % 26.17/26.45 Clause #612 (by superposition #[611, 114]): Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_X) True) (Eq False True) % 26.17/26.45 Clause #613 (by clausification #[612]): Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_X) True % 26.17/26.45 Clause #614 (by backward demodulation #[613, 6]): Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z) False) % 26.17/26.45 (Or (Eq True False) (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) False)) % 26.17/26.45 Clause #615 (by clausification #[614]): Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z) False) % 26.17/26.45 (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) False) % 26.17/26.45 Clause #616 (by clausification #[603]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection a) True) % 26.17/26.45 (Eq (iext uri_rdf_first (skS.0 9 a_1 a_2 a_3 a_4 a_5 a_6 a_7) a) False) % 26.17/26.45 Clause #617 (by superposition #[616, 98]): Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) True) (Eq False True) % 26.17/26.45 Clause #618 (by clausification #[617]): Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) True % 26.17/26.45 Clause #620 (by clausification #[604]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 26.17/26.45 Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection a) True) % 26.17/26.45 (Eq (iext uri_rdf_first (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a) False) % 26.17/26.45 Clause #621 (by superposition #[620, 77]): Or (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z) True) (Eq False True) % 26.17/26.45 Clause #622 (by clausification #[621]): Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Z) True % 26.17/26.45 Clause #623 (by backward demodulation #[622, 615]): Or (Eq True False) (Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) False) % 26.17/26.45 Clause #624 (by clausification #[623]): Eq (iext uri_skos_member uri_ex_MyOrderedCollection uri_ex_Y) False % 26.17/26.45 Clause #625 (by superposition #[624, 618]): Eq False True % 26.17/26.45 Clause #626 (by clausification #[625]): False % 26.17/26.45 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------