%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB025+2 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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:28 PM UTC 2025 % Result : Theorem 12.50s 12.67s % Output : Proof 12.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWB025+2 : TPTP v9.2.0. Released v5.2.0. % 0.14/0.14 % Command : duper %s % 0.15/0.35 % Computer : n026.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 11:47:53 EDT 2025 % 0.15/0.35 % CPUTime : % 12.50/12.67 SZS status Theorem for theBenchmark.p % 12.50/12.67 SZS output start Proof for theBenchmark.p % 12.50/12.67 Clause #0 (by assumption #[]): Eq % 12.50/12.67 (∀ (P S1 P1 S2 P2 : Iota), % 12.50/12.67 And (And (And (iext uri_rdf_first S1 P1) (iext uri_rdf_rest S1 S2)) (iext uri_rdf_first S2 P2)) % 12.50/12.67 (iext uri_rdf_rest S2 uri_rdf_nil) → % 12.50/12.67 Iff (iext uri_owl_propertyChainAxiom P S1) % 12.50/12.67 (And (And (And (ip P) (ip P1)) (ip P2)) % 12.50/12.67 (∀ (Y0 Y1 Y2 : Iota), And (iext P1 Y0 Y1) (iext P2 Y1 Y2) → iext P Y0 Y2))) % 12.50/12.67 True % 12.50/12.67 Clause #1 (by assumption #[]): Eq % 12.50/12.67 (∀ (P1 P2 : Iota), % 12.50/12.67 Iff (iext uri_owl_inverseOf P1 P2) (And (And (ip P1) (ip P2)) (∀ (X Y : Iota), Iff (iext P1 X Y) (iext P2 Y X)))) % 12.50/12.67 True % 12.50/12.67 Clause #2 (by assumption #[]): Eq (Not (And (iext uri_ex_hasUncle uri_ex_alice uri_ex_charly) (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice))) True % 12.50/12.67 Clause #3 (by assumption #[]): Eq % 12.50/12.67 (Exists fun BNODE_l11 => % 12.50/12.67 Exists fun BNODE_l12 => % 12.50/12.67 Exists fun BNODE_l21 => % 12.50/12.67 Exists fun BNODE_l22 => % 12.50/12.67 Exists fun BNODE_l3 => % 12.50/12.67 And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And % 12.50/12.67 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle BNODE_l11) % 12.50/12.67 (iext uri_rdf_first BNODE_l11 uri_ex_hasCousin)) % 12.50/12.67 (iext uri_rdf_rest BNODE_l11 BNODE_l12)) % 12.50/12.67 (iext uri_rdf_first BNODE_l12 uri_ex_hasFather)) % 12.50/12.67 (iext uri_rdf_rest BNODE_l12 uri_rdf_nil)) % 12.50/12.67 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin BNODE_l21)) % 12.50/12.67 (iext uri_rdf_first BNODE_l21 uri_ex_hasUncle)) % 12.50/12.67 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 12.50/12.67 (iext uri_rdf_first BNODE_l22 BNODE_l3)) % 12.50/12.67 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 12.50/12.67 (iext uri_owl_inverseOf BNODE_l3 uri_ex_hasFather)) % 12.50/12.67 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.50/12.67 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.50/12.67 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.50/12.67 (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave)) % 12.50/12.67 True % 12.50/12.67 Clause #4 (by clausification #[2]): Eq (And (iext uri_ex_hasUncle uri_ex_alice uri_ex_charly) (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice)) False % 12.50/12.67 Clause #5 (by clausification #[4]): Or (Eq (iext uri_ex_hasUncle uri_ex_alice uri_ex_charly) False) % 12.50/12.67 (Eq (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice) False) % 12.50/12.67 Clause #6 (by clausification #[1]): ∀ (a : Iota), % 12.50/12.67 Eq % 12.50/12.67 (∀ (P2 : Iota), % 12.50/12.67 Iff (iext uri_owl_inverseOf a P2) (And (And (ip a) (ip P2)) (∀ (X Y : Iota), Iff (iext a X Y) (iext P2 Y X)))) % 12.50/12.67 True % 12.50/12.67 Clause #7 (by clausification #[6]): ∀ (a a_1 : Iota), % 12.50/12.67 Eq (Iff (iext uri_owl_inverseOf a a_1) (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), Iff (iext a X Y) (iext a_1 Y X)))) % 12.50/12.67 True % 12.50/12.67 Clause #9 (by clausification #[7]): ∀ (a a_1 : Iota), % 12.50/12.67 Or (Eq (iext uri_owl_inverseOf a a_1) False) % 12.50/12.67 (Eq (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), Iff (iext a X Y) (iext a_1 Y X))) True) % 12.50/12.67 Clause #18 (by clausification #[9]): ∀ (a a_1 : Iota), % 12.50/12.67 Or (Eq (iext uri_owl_inverseOf a a_1) False) (Eq (∀ (X Y : Iota), Iff (iext a X Y) (iext a_1 Y X)) True) % 12.50/12.67 Clause #20 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), % 12.50/12.67 Or (Eq (iext uri_owl_inverseOf a a_1) False) (Eq (∀ (Y : Iota), Iff (iext a a_2 Y) (iext a_1 Y a_2)) True) % 12.50/12.67 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 : Iota), % 12.50/12.67 Or (Eq (iext uri_owl_inverseOf a a_1) False) (Eq (Iff (iext a a_2 a_3) (iext a_1 a_3 a_2)) True) % 12.50/12.67 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 : Iota), % 12.50/12.67 Or (Eq (iext uri_owl_inverseOf a a_1) False) (Or (Eq (iext a a_2 a_3) True) (Eq (iext a_1 a_3 a_2) False)) % 12.50/12.69 Clause #26 (by clausification #[0]): ∀ (a : Iota), % 12.50/12.69 Eq % 12.50/12.69 (∀ (S1 P1 S2 P2 : Iota), % 12.50/12.69 And (And (And (iext uri_rdf_first S1 P1) (iext uri_rdf_rest S1 S2)) (iext uri_rdf_first S2 P2)) % 12.50/12.69 (iext uri_rdf_rest S2 uri_rdf_nil) → % 12.50/12.69 Iff (iext uri_owl_propertyChainAxiom a S1) % 12.50/12.69 (And (And (And (ip a) (ip P1)) (ip P2)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext P1 Y0 Y1) (iext P2 Y1 Y2) → iext a Y0 Y2))) % 12.50/12.69 True % 12.50/12.69 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), % 12.50/12.69 Eq % 12.50/12.69 (∀ (P1 S2 P2 : Iota), % 12.50/12.69 And (And (And (iext uri_rdf_first a P1) (iext uri_rdf_rest a S2)) (iext uri_rdf_first S2 P2)) % 12.50/12.69 (iext uri_rdf_rest S2 uri_rdf_nil) → % 12.50/12.69 Iff (iext uri_owl_propertyChainAxiom a_1 a) % 12.50/12.69 (And (And (And (ip a_1) (ip P1)) (ip P2)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext P1 Y0 Y1) (iext P2 Y1 Y2) → iext a_1 Y0 Y2))) % 12.50/12.69 True % 12.50/12.69 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), % 12.50/12.69 Eq % 12.50/12.69 (∀ (S2 P2 : Iota), % 12.50/12.69 And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a S2)) (iext uri_rdf_first S2 P2)) % 12.50/12.69 (iext uri_rdf_rest S2 uri_rdf_nil) → % 12.50/12.69 Iff (iext uri_owl_propertyChainAxiom a_2 a) % 12.50/12.69 (And (And (And (ip a_2) (ip a_1)) (ip P2)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext P2 Y1 Y2) → iext a_2 Y0 Y2))) % 12.50/12.69 True % 12.50/12.69 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 : Iota), % 12.50/12.69 Eq % 12.50/12.69 (∀ (P2 : Iota), % 12.50/12.69 And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a a_2)) (iext uri_rdf_first a_2 P2)) % 12.50/12.69 (iext uri_rdf_rest a_2 uri_rdf_nil) → % 12.50/12.69 Iff (iext uri_owl_propertyChainAxiom a_3 a) % 12.50/12.69 (And (And (And (ip a_3) (ip a_1)) (ip P2)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext P2 Y1 Y2) → iext a_3 Y0 Y2))) % 12.50/12.69 True % 12.50/12.69 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.69 Eq % 12.50/12.69 (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)) % 12.50/12.69 (iext uri_rdf_rest a_2 uri_rdf_nil) → % 12.50/12.69 Iff (iext uri_owl_propertyChainAxiom a_4 a) % 12.50/12.69 (And (And (And (ip a_4) (ip a_1)) (ip a_3)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2) → iext a_4 Y0 Y2))) % 12.50/12.69 True % 12.50/12.69 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.69 Or % 12.50/12.69 (Eq % 12.50/12.69 (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)) % 12.50/12.69 (iext uri_rdf_rest a_2 uri_rdf_nil)) % 12.50/12.69 False) % 12.50/12.69 (Eq % 12.50/12.69 (Iff (iext uri_owl_propertyChainAxiom a_4 a) % 12.50/12.69 (And (And (And (ip a_4) (ip a_1)) (ip a_3)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2) → iext a_4 Y0 Y2))) % 12.50/12.69 True) % 12.50/12.69 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.69 Or % 12.50/12.69 (Eq % 12.50/12.69 (Iff (iext uri_owl_propertyChainAxiom a a_1) % 12.50/12.69 (And (And (And (ip a) (ip a_2)) (ip a_3)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_2 Y0 Y1) (iext a_3 Y1 Y2) → iext a Y0 Y2))) % 12.50/12.69 True) % 12.50/12.69 (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) % 12.50/12.69 (Eq (iext uri_rdf_rest a_4 uri_rdf_nil) False)) % 12.50/12.69 Clause #34 (by clausification #[32]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.69 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) % 12.50/12.69 (Or (Eq (iext uri_rdf_rest a_2 uri_rdf_nil) False) % 12.50/12.69 (Or (Eq (iext uri_owl_propertyChainAxiom a_4 a) False) % 12.50/12.69 (Eq % 12.50/12.69 (And (And (And (ip a_4) (ip a_1)) (ip a_3)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2) → iext a_4 Y0 Y2)) % 12.50/12.69 True))) % 12.50/12.69 Clause #50 (by clausification #[34]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.69 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.69 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.69 (Or % 12.50/12.69 (Eq % 12.50/12.69 (And (And (And (ip a_1) (ip a_3)) (ip a_4)) % 12.50/12.69 (∀ (Y0 Y1 Y2 : Iota), And (iext a_3 Y0 Y1) (iext a_4 Y1 Y2) → iext a_1 Y0 Y2)) % 12.50/12.69 True) % 12.50/12.69 (Or (Eq (And (iext uri_rdf_first a_2 a_3) (iext uri_rdf_rest a_2 a)) False) % 12.50/12.69 (Eq (iext uri_rdf_first a a_4) False)))) % 12.50/12.71 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (And (iext uri_rdf_first a_2 a_3) (iext uri_rdf_rest a_2 a)) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_4) False) % 12.50/12.71 (Eq (∀ (Y0 Y1 Y2 : Iota), And (iext a_3 Y0 Y1) (iext a_4 Y1 Y2) → iext a_1 Y0 Y2) True)))) % 12.50/12.71 Clause #53 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_3) False) % 12.50/12.71 (Or (Eq (∀ (Y0 Y1 Y2 : Iota), And (iext a_4 Y0 Y1) (iext a_3 Y1 Y2) → iext a_1 Y0 Y2) True) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a_2 a_4) False) (Eq (iext uri_rdf_rest a_2 a) False))))) % 12.50/12.71 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_3) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 12.50/12.71 (Eq (∀ (Y1 Y2 : Iota), And (iext a_4 a_5 Y1) (iext a_3 Y1 Y2) → iext a_1 a_5 Y2) True))))) % 12.50/12.71 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_3) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 12.50/12.71 (Eq (∀ (Y2 : Iota), And (iext a_4 a_5 a_6) (iext a_3 a_6 Y2) → iext a_1 a_5 Y2) True))))) % 12.50/12.71 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_3) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 12.50/12.71 (Eq (And (iext a_4 a_5 a_6) (iext a_3 a_6 a_7) → iext a_1 a_5 a_7) True))))) % 12.50/12.71 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_3) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 12.50/12.71 (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)))))) % 12.50/12.71 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.50/12.71 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 12.50/12.71 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a a_3) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_first a_2 a_4) False) % 12.50/12.71 (Or (Eq (iext uri_rdf_rest a_2 a) False) % 12.50/12.71 (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))))))) % 12.50/12.71 Clause #64 (by clausification #[3]): ∀ (a : Iota), % 12.50/12.71 Eq % 12.50/12.71 (Exists fun BNODE_l12 => % 12.50/12.71 Exists fun BNODE_l21 => % 12.50/12.71 Exists fun BNODE_l22 => % 12.50/12.71 Exists fun BNODE_l3 => % 12.50/12.71 And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And % 12.50/12.71 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.50/12.71 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.50/12.71 (iext uri_rdf_rest (skS.0 5 a) BNODE_l12)) % 12.50/12.71 (iext uri_rdf_first BNODE_l12 uri_ex_hasFather)) % 12.50/12.71 (iext uri_rdf_rest BNODE_l12 uri_rdf_nil)) % 12.50/12.72 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin BNODE_l21)) % 12.50/12.72 (iext uri_rdf_first BNODE_l21 uri_ex_hasUncle)) % 12.50/12.72 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 12.50/12.72 (iext uri_rdf_first BNODE_l22 BNODE_l3)) % 12.50/12.72 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 12.50/12.72 (iext uri_owl_inverseOf BNODE_l3 uri_ex_hasFather)) % 12.50/12.72 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.50/12.72 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.50/12.72 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.50/12.72 (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave)) % 12.50/12.72 True % 12.50/12.72 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), % 12.50/12.72 Eq % 12.50/12.72 (Exists fun BNODE_l21 => % 12.50/12.72 Exists fun BNODE_l22 => % 12.50/12.72 Exists fun BNODE_l3 => % 12.50/12.72 And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.50/12.72 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.50/12.72 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.50/12.72 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.50/12.72 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.50/12.72 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin BNODE_l21)) % 12.50/12.72 (iext uri_rdf_first BNODE_l21 uri_ex_hasUncle)) % 12.50/12.72 (iext uri_rdf_rest BNODE_l21 BNODE_l22)) % 12.50/12.72 (iext uri_rdf_first BNODE_l22 BNODE_l3)) % 12.50/12.72 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 12.50/12.72 (iext uri_owl_inverseOf BNODE_l3 uri_ex_hasFather)) % 12.50/12.72 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.50/12.72 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.50/12.72 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.50/12.72 (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave)) % 12.50/12.72 True % 12.50/12.72 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 : Iota), % 12.50/12.72 Eq % 12.50/12.72 (Exists fun BNODE_l22 => % 12.50/12.72 Exists fun BNODE_l3 => % 12.50/12.72 And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And % 12.50/12.72 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.50/12.72 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.50/12.72 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.50/12.72 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.50/12.72 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.50/12.72 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.50/12.72 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.50/12.72 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) BNODE_l22)) % 12.50/12.72 (iext uri_rdf_first BNODE_l22 BNODE_l3)) % 12.50/12.72 (iext uri_rdf_rest BNODE_l22 uri_rdf_nil)) % 12.50/12.72 (iext uri_owl_inverseOf BNODE_l3 uri_ex_hasFather)) % 12.50/12.72 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.50/12.72 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.50/12.72 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.50/12.72 (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave)) % 12.50/12.72 True % 12.50/12.72 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 : Iota), % 12.50/12.72 Eq % 12.50/12.72 (Exists fun BNODE_l3 => % 12.50/12.73 And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.50/12.73 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.50/12.73 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.50/12.73 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.50/12.73 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.50/12.73 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) BNODE_l3)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.50/12.73 (iext uri_owl_inverseOf BNODE_l3 uri_ex_hasFather)) % 12.50/12.73 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.50/12.73 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.50/12.73 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.50/12.73 (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave)) % 12.50/12.73 True % 12.50/12.73 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.73 Eq % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.50/12.73 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.50/12.73 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.50/12.73 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.50/12.73 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.50/12.73 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.50/12.73 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.50/12.73 (iext uri_owl_inverseOf (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_hasFather)) % 12.50/12.73 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.50/12.73 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.50/12.73 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.50/12.73 (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave)) % 12.50/12.73 True % 12.50/12.73 Clause #69 (by clausification #[68]): Eq (iext uri_ex_hasUncle uri_ex_bob uri_ex_dave) True % 12.50/12.73 Clause #70 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.50/12.73 Eq % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And % 12.50/12.73 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.50/12.73 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.50/12.73 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.50/12.73 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.50/12.73 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.50/12.73 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.50/12.73 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.58/12.74 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.58/12.74 (iext uri_owl_inverseOf (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_hasFather)) % 12.58/12.74 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.58/12.74 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.58/12.74 (iext uri_ex_hasFather uri_ex_bob uri_ex_charly)) % 12.58/12.74 True % 12.58/12.74 Clause #71 (by clausification #[70]): Eq (iext uri_ex_hasFather uri_ex_bob uri_ex_charly) True % 12.58/12.74 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.58/12.74 Eq % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.74 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.74 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.74 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.74 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.58/12.74 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.58/12.74 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.58/12.74 (iext uri_owl_inverseOf (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_hasFather)) % 12.58/12.74 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.58/12.74 (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob)) % 12.58/12.74 True % 12.58/12.74 Clause #73 (by clausification #[72]): Eq (iext uri_ex_hasCousin uri_ex_alice uri_ex_bob) True % 12.58/12.74 Clause #74 (by clausification #[72]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.58/12.74 Eq % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.74 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.74 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.74 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.74 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.58/12.74 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.58/12.74 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.58/12.74 (iext uri_owl_inverseOf (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_hasFather)) % 12.58/12.74 (iext uri_ex_hasFather uri_ex_alice uri_ex_dave)) % 12.58/12.74 True % 12.58/12.74 Clause #75 (by clausification #[74]): Eq (iext uri_ex_hasFather uri_ex_alice uri_ex_dave) True % 12.58/12.74 Clause #76 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.58/12.74 Eq % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And % 12.58/12.74 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.74 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.74 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.74 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.74 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.74 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.58/12.74 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.58/12.74 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.58/12.76 (iext uri_owl_inverseOf (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_hasFather)) % 12.58/12.76 True % 12.58/12.76 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_owl_inverseOf (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_hasFather) True % 12.58/12.76 Clause #78 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.58/12.76 Eq % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.76 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.76 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.76 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.76 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.76 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.76 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.76 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.58/12.76 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.58/12.76 (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil)) % 12.58/12.76 True % 12.58/12.76 Clause #79 (by superposition #[77, 22]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.58/12.76 Or (Eq True False) % 12.58/12.76 (Or (Eq (iext (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6) True) (Eq (iext uri_ex_hasFather a_6 a_5) False)) % 12.58/12.76 Clause #89 (by clausification #[79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.58/12.76 Or (Eq (iext (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6) True) (Eq (iext uri_ex_hasFather a_6 a_5) False) % 12.58/12.76 Clause #91 (by superposition #[89, 75]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (iext (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_dave uri_ex_alice) True) (Eq False True) % 12.58/12.76 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext (skS.0 9 a a_1 a_2 a_3 a_4) uri_ex_dave uri_ex_alice) True % 12.58/12.76 Clause #93 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), Eq (iext uri_rdf_rest (skS.0 8 a a_1 a_2 a_3) uri_rdf_nil) True % 12.58/12.76 Clause #94 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.58/12.76 Eq % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.76 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.76 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.76 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.76 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.76 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.76 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.76 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.58/12.76 (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.58/12.76 True % 12.58/12.76 Clause #96 (by superposition #[93, 58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 12.58/12.76 Or (Eq True False) % 12.58/12.76 (Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 12.58/12.76 (Or (Eq (iext uri_rdf_first (skS.0 8 a_2 a_3 a_4 a_5) a_6) False) % 12.58/12.76 (Or (Eq (iext uri_rdf_first a_1 a_7) False) % 12.58/12.76 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 8 a_2 a_3 a_4 a_5)) False) % 12.58/12.76 (Or (Eq (iext a a_8 a_9) True) (Or (Eq (iext a_7 a_8 a_10) False) (Eq (iext a_6 a_10 a_9) False))))))) % 12.58/12.76 Clause #113 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 12.58/12.76 Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 12.58/12.76 (Or (Eq (iext uri_rdf_first (skS.0 8 a_2 a_3 a_4 a_5) a_6) False) % 12.58/12.76 (Or (Eq (iext uri_rdf_first a_1 a_7) False) % 12.58/12.76 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 8 a_2 a_3 a_4 a_5)) False) % 12.58/12.76 (Or (Eq (iext a a_8 a_9) True) (Or (Eq (iext a_7 a_8 a_10) False) (Eq (iext a_6 a_10 a_9) False)))))) % 12.58/12.76 Clause #139 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4)) True % 12.58/12.76 Clause #140 (by clausification #[94]): ∀ (a a_1 a_2 a_3 : Iota), % 12.58/12.76 Eq % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.76 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.78 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.78 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.78 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.78 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 12.58/12.78 True % 12.58/12.78 Clause #152 (by clausification #[140]): ∀ (a a_1 a_2 a_3 : Iota), Eq (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) True % 12.58/12.78 Clause #153 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), % 12.58/12.78 Eq % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.78 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.78 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.78 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.78 (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle)) % 12.58/12.78 True % 12.58/12.78 Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_rdf_first (skS.0 7 a a_1 a_2) uri_ex_hasUncle) True % 12.58/12.78 Clause #155 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), % 12.58/12.78 Eq % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.78 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.78 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.78 (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2))) % 12.58/12.78 True % 12.58/12.78 Clause #160 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_owl_propertyChainAxiom uri_ex_hasCousin (skS.0 7 a a_1 a_2)) True % 12.58/12.78 Clause #161 (by clausification #[155]): ∀ (a a_1 : Iota), % 12.58/12.78 Eq % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.78 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.78 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil)) % 12.58/12.78 True % 12.58/12.78 Clause #165 (by superposition #[160, 113]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 12.58/12.78 Or (Eq True False) % 12.58/12.78 (Or (Eq (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) a_4) False) % 12.58/12.78 (Or (Eq (iext uri_rdf_first (skS.0 7 a_5 a_6 a_7) a_8) False) % 12.58/12.78 (Or (Eq (iext uri_rdf_rest (skS.0 7 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3)) False) % 12.58/12.78 (Or (Eq (iext uri_ex_hasCousin a_9 a_10) True) % 12.58/12.78 (Or (Eq (iext a_8 a_9 a_11) False) (Eq (iext a_4 a_11 a_10) False)))))) % 12.58/12.78 Clause #257 (by clausification #[161]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_rest (skS.0 6 a a_1) uri_rdf_nil) True % 12.58/12.78 Clause #258 (by clausification #[161]): ∀ (a a_1 : Iota), % 12.58/12.78 Eq % 12.58/12.78 (And % 12.58/12.78 (And % 12.58/12.78 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.58/12.78 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.58/12.78 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.58/12.78 (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather)) % 12.58/12.78 True % 12.58/12.78 Clause #260 (by superposition #[257, 58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.58/12.78 Or (Eq True False) % 12.58/12.78 (Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 12.58/12.78 (Or (Eq (iext uri_rdf_first (skS.0 6 a_2 a_3) a_4) False) % 12.58/12.78 (Or (Eq (iext uri_rdf_first a_1 a_5) False) % 12.58/12.78 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 6 a_2 a_3)) False) % 12.58/12.78 (Or (Eq (iext a a_6 a_7) True) (Or (Eq (iext a_5 a_6 a_8) False) (Eq (iext a_4 a_8 a_7) False))))))) % 12.58/12.78 Clause #276 (by clausification #[258]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_first (skS.0 6 a a_1) uri_ex_hasFather) True % 12.64/12.80 Clause #277 (by clausification #[258]): ∀ (a a_1 : Iota), % 12.64/12.80 Eq % 12.64/12.80 (And % 12.64/12.80 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.64/12.80 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.64/12.80 (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1))) % 12.64/12.80 True % 12.64/12.80 Clause #281 (by clausification #[277]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a a_1)) True % 12.64/12.80 Clause #282 (by clausification #[277]): ∀ (a : Iota), % 12.64/12.80 Eq % 12.64/12.80 (And (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) % 12.64/12.80 (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin)) % 12.64/12.80 True % 12.64/12.80 Clause #283 (by clausification #[282]): ∀ (a : Iota), Eq (iext uri_rdf_first (skS.0 5 a) uri_ex_hasCousin) True % 12.64/12.80 Clause #284 (by clausification #[282]): ∀ (a : Iota), Eq (iext uri_owl_propertyChainAxiom uri_ex_hasUncle (skS.0 5 a)) True % 12.64/12.80 Clause #323 (by clausification #[260]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.64/12.80 Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_first (skS.0 6 a_2 a_3) a_4) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_first a_1 a_5) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest a_1 (skS.0 6 a_2 a_3)) False) % 12.64/12.80 (Or (Eq (iext a a_6 a_7) True) (Or (Eq (iext a_5 a_6 a_8) False) (Eq (iext a_4 a_8 a_7) False)))))) % 12.64/12.80 Clause #325 (by superposition #[323, 284]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_first (skS.0 6 a a_1) a_2) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_first (skS.0 5 a_3) a_4) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest (skS.0 5 a_3) (skS.0 6 a a_1)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasUncle a_5 a_6) True) % 12.64/12.80 (Or (Eq (iext a_4 a_5 a_7) False) (Or (Eq (iext a_2 a_7 a_6) False) (Eq False True)))))) % 12.64/12.80 Clause #326 (by clausification #[165]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_first (skS.0 8 a a_1 a_2 a_3) a_4) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_first (skS.0 7 a_5 a_6 a_7) a_8) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest (skS.0 7 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasCousin a_9 a_10) True) % 12.64/12.80 (Or (Eq (iext a_8 a_9 a_11) False) (Eq (iext a_4 a_11 a_10) False))))) % 12.64/12.80 Clause #327 (by superposition #[326, 139]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_first (skS.0 7 a a_1 a_2) a_3) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a_4 a_5 a_6 a_7)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasCousin a_8 a_9) True) % 12.64/12.80 (Or (Eq (iext a_3 a_8 a_10) False) % 12.64/12.80 (Or (Eq (iext (skS.0 9 a_4 a_5 a_6 a_7 a_11) a_10 a_9) False) (Eq False True))))) % 12.64/12.80 Clause #355 (by clausification #[325]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_first (skS.0 6 a a_1) a_2) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_first (skS.0 5 a_3) a_4) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest (skS.0 5 a_3) (skS.0 6 a a_1)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasUncle a_5 a_6) True) (Or (Eq (iext a_4 a_5 a_7) False) (Eq (iext a_2 a_7 a_6) False))))) % 12.64/12.80 Clause #356 (by superposition #[355, 276]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_first (skS.0 5 a) a_1) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a_2 a_3)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasUncle a_4 a_5) True) % 12.64/12.80 (Or (Eq (iext a_1 a_4 a_6) False) (Or (Eq (iext uri_ex_hasFather a_6 a_5) False) (Eq False True))))) % 12.64/12.80 Clause #357 (by clausification #[356]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_first (skS.0 5 a) a_1) False) % 12.64/12.80 (Or (Eq (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a_2 a_3)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasUncle a_4 a_5) True) % 12.64/12.80 (Or (Eq (iext a_1 a_4 a_6) False) (Eq (iext uri_ex_hasFather a_6 a_5) False)))) % 12.64/12.80 Clause #358 (by superposition #[357, 283]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.64/12.80 Or (Eq (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a_1 a_2)) False) % 12.64/12.80 (Or (Eq (iext uri_ex_hasUncle a_3 a_4) True) % 12.64/12.80 (Or (Eq (iext uri_ex_hasCousin a_3 a_5) False) (Or (Eq (iext uri_ex_hasFather a_5 a_4) False) (Eq False True)))) % 12.64/12.80 Clause #361 (by clausification #[358]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.64/12.82 Or (Eq (iext uri_rdf_rest (skS.0 5 a) (skS.0 6 a_1 a_2)) False) % 12.64/12.82 (Or (Eq (iext uri_ex_hasUncle a_3 a_4) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasCousin a_3 a_5) False) (Eq (iext uri_ex_hasFather a_5 a_4) False))) % 12.64/12.82 Clause #362 (by superposition #[361, 281]): ∀ (a a_1 a_2 : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasUncle a a_1) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasCousin a a_2) False) (Or (Eq (iext uri_ex_hasFather a_2 a_1) False) (Eq False True))) % 12.64/12.82 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasUncle a a_1) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasCousin a a_2) False) (Eq (iext uri_ex_hasFather a_2 a_1) False)) % 12.64/12.82 Clause #364 (by superposition #[363, 73]): ∀ (a : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasUncle uri_ex_alice a) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasFather uri_ex_bob a) False) (Eq False True)) % 12.64/12.82 Clause #368 (by clausification #[364]): ∀ (a : Iota), Or (Eq (iext uri_ex_hasUncle uri_ex_alice a) True) (Eq (iext uri_ex_hasFather uri_ex_bob a) False) % 12.64/12.82 Clause #369 (by superposition #[368, 71]): Or (Eq (iext uri_ex_hasUncle uri_ex_alice uri_ex_charly) True) (Eq False True) % 12.64/12.82 Clause #370 (by clausification #[369]): Eq (iext uri_ex_hasUncle uri_ex_alice uri_ex_charly) True % 12.64/12.82 Clause #371 (by backward demodulation #[370, 5]): Or (Eq True False) (Eq (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice) False) % 12.64/12.82 Clause #372 (by clausification #[371]): Eq (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice) False % 12.64/12.82 Clause #396 (by clausification #[327]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 12.64/12.82 Or (Eq (iext uri_rdf_first (skS.0 7 a a_1 a_2) a_3) False) % 12.64/12.82 (Or (Eq (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a_4 a_5 a_6 a_7)) False) % 12.64/12.82 (Or (Eq (iext uri_ex_hasCousin a_8 a_9) True) % 12.64/12.82 (Or (Eq (iext a_3 a_8 a_10) False) (Eq (iext (skS.0 9 a_4 a_5 a_6 a_7 a_11) a_10 a_9) False)))) % 12.64/12.82 Clause #397 (by superposition #[396, 154]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 12.64/12.82 Or (Eq (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a_3 a_4 a_5 a_6)) False) % 12.64/12.82 (Or (Eq (iext uri_ex_hasCousin a_7 a_8) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasUncle a_7 a_9) False) % 12.64/12.82 (Or (Eq (iext (skS.0 9 a_3 a_4 a_5 a_6 a_10) a_9 a_8) False) (Eq False True)))) % 12.64/12.82 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 12.64/12.82 Or (Eq (iext uri_rdf_rest (skS.0 7 a a_1 a_2) (skS.0 8 a_3 a_4 a_5 a_6)) False) % 12.64/12.82 (Or (Eq (iext uri_ex_hasCousin a_7 a_8) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasUncle a_7 a_9) False) (Eq (iext (skS.0 9 a_3 a_4 a_5 a_6 a_10) a_9 a_8) False))) % 12.64/12.82 Clause #399 (by superposition #[398, 152]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasCousin a a_1) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasUncle a a_2) False) % 12.64/12.82 (Or (Eq (iext (skS.0 9 a_3 a_4 a_5 a_6 a_7) a_2 a_1) False) (Eq False True))) % 12.64/12.82 Clause #400 (by clausification #[399]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasCousin a a_1) True) % 12.64/12.82 (Or (Eq (iext uri_ex_hasUncle a a_2) False) (Eq (iext (skS.0 9 a_3 a_4 a_5 a_6 a_7) a_2 a_1) False)) % 12.64/12.82 Clause #401 (by superposition #[400, 69]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasCousin uri_ex_bob a) True) % 12.64/12.82 (Or (Eq (iext (skS.0 9 a_1 a_2 a_3 a_4 a_5) uri_ex_dave a) False) (Eq False True)) % 12.64/12.82 Clause #409 (by clausification #[401]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.64/12.82 Or (Eq (iext uri_ex_hasCousin uri_ex_bob a) True) (Eq (iext (skS.0 9 a_1 a_2 a_3 a_4 a_5) uri_ex_dave a) False) % 12.64/12.82 Clause #410 (by superposition #[409, 92]): Or (Eq (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice) True) (Eq False True) % 12.64/12.82 Clause #411 (by clausification #[410]): Eq (iext uri_ex_hasCousin uri_ex_bob uri_ex_alice) True % 12.64/12.82 Clause #412 (by superposition #[411, 372]): Eq True False % 12.64/12.82 Clause #414 (by clausification #[412]): False % 12.64/12.82 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------