%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB013+2 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:24 PM UTC 2025 % Result : Theorem 64.02s 64.19s % Output : Proof 64.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWB013+2 : TPTP v9.2.0. Released v5.2.0. % 0.12/0.13 % Command : duper %s % 0.14/0.35 % Computer : n031.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 11:54:53 EDT 2025 % 0.14/0.35 % CPUTime : % 64.02/64.19 SZS status Theorem for theBenchmark.p % 64.02/64.19 SZS output start Proof for theBenchmark.p % 64.02/64.19 Clause #0 (by assumption #[]): Eq (∀ (X C : Iota), Iff (iext uri_rdf_type X C) (icext C X)) True % 64.02/64.19 Clause #1 (by assumption #[]): Eq % 64.02/64.19 (∀ (Z P C : Iota), % 64.02/64.19 And (iext uri_owl_someValuesFrom Z C) (iext uri_owl_onProperty Z P) → % 64.02/64.19 ∀ (X : Iota), Iff (icext Z X) (Exists fun Y => And (iext P X Y) (icext C Y))) % 64.02/64.19 True % 64.02/64.19 Clause #2 (by assumption #[]): Eq % 64.02/64.19 (∀ (C1 C2 : Iota), % 64.02/64.19 Iff (iext uri_rdfs_subClassOf C1 C2) (And (And (ic C1) (ic C2)) (∀ (X : Iota), icext C1 X → icext C2 X))) % 64.02/64.19 True % 64.02/64.19 Clause #3 (by assumption #[]): Eq % 64.02/64.19 (∀ (P1 P2 : Iota), % 64.02/64.19 Iff (iext uri_rdfs_subPropertyOf P1 P2) (And (And (ip P1) (ip P2)) (∀ (X Y : Iota), iext P1 X Y → iext P2 X Y))) % 64.02/64.19 True % 64.02/64.19 Clause #4 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (iext uri_owl_sameAs X Y) (Eq X Y)) True % 64.02/64.19 Clause #5 (by assumption #[]): Eq % 64.02/64.19 (∀ (P S1 P1 S2 P2 S3 P3 : Iota), % 64.02/64.19 And % 64.02/64.19 (And % 64.02/64.19 (And (And (And (iext uri_rdf_first S1 P1) (iext uri_rdf_rest S1 S2)) (iext uri_rdf_first S2 P2)) % 64.02/64.19 (iext uri_rdf_rest S2 S3)) % 64.02/64.19 (iext uri_rdf_first S3 P3)) % 64.02/64.19 (iext uri_rdf_rest S3 uri_rdf_nil) → % 64.02/64.19 Iff (iext uri_owl_propertyChainAxiom P S1) % 64.02/64.19 (And (And (And (And (ip P) (ip P1)) (ip P2)) (ip P3)) % 64.02/64.19 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext P1 Y0 Y1) (iext P2 Y1 Y2)) (iext P3 Y2 Y3) → iext P Y0 Y3))) % 64.02/64.19 True % 64.02/64.19 Clause #6 (by assumption #[]): Eq % 64.02/64.19 (∀ (P1 P2 : Iota), % 64.02/64.19 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)))) % 64.02/64.19 True % 64.02/64.19 Clause #7 (by assumption #[]): Eq (Not (iext uri_foaf_knows uri_ex_alice uri_ex_bob)) True % 64.02/64.19 Clause #8 (by assumption #[]): Eq % 64.02/64.19 (Exists fun BNODE_r => % 64.02/64.19 Exists fun BNODE_i => % 64.02/64.19 Exists fun BNODE_l1 => % 64.02/64.19 Exists fun BNODE_l2 => % 64.02/64.19 Exists fun BNODE_l3 => % 64.02/64.19 And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And % 64.02/64.19 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.02/64.19 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.02/64.19 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.02/64.19 (iext uri_rdfs_subClassOf uri_ex_Clique BNODE_r)) % 64.02/64.19 (iext uri_rdf_type BNODE_r uri_owl_Restriction)) % 64.02/64.19 (iext uri_owl_onProperty BNODE_r uri_ex_sameCliqueAs)) % 64.02/64.19 (iext uri_owl_someValuesFrom BNODE_r uri_ex_Clique)) % 64.02/64.19 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.02/64.19 (iext uri_owl_propertyChainAxiom uri_foaf_knows BNODE_l1)) % 64.02/64.19 (iext uri_rdf_first BNODE_l1 uri_rdf_type)) % 64.02/64.19 (iext uri_rdf_rest BNODE_l1 BNODE_l2)) % 64.02/64.19 (iext uri_rdf_first BNODE_l2 uri_ex_sameCliqueAs)) % 64.02/64.19 (iext uri_rdf_rest BNODE_l2 BNODE_l3)) % 64.02/64.19 (iext uri_rdf_first BNODE_l3 BNODE_i)) % 64.02/64.19 (iext uri_rdf_rest BNODE_l3 uri_rdf_nil)) % 64.02/64.19 (iext uri_owl_inverseOf BNODE_i uri_rdf_type)) % 64.02/64.19 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.02/64.19 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.02/64.19 (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang)) % 64.02/64.19 True % 64.02/64.19 Clause #9 (by clausification #[7]): Eq (iext uri_foaf_knows uri_ex_alice uri_ex_bob) False % 64.02/64.19 Clause #10 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (iext uri_rdf_type a C) (icext C a)) True % 64.05/64.22 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_rdf_type a a_1) (icext a_1 a)) True % 64.05/64.22 Clause #13 (by clausification #[11]): ∀ (a a_1 : Iota), Or (Eq (iext uri_rdf_type a a_1) False) (Eq (icext a_1 a) True) % 64.05/64.22 Clause #14 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (iext uri_owl_sameAs a Y) (Eq a Y)) True % 64.05/64.22 Clause #15 (by clausification #[14]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_owl_sameAs a a_1) (Eq a a_1)) True % 64.05/64.22 Clause #17 (by clausification #[15]): ∀ (a a_1 : Iota), Or (Eq (iext uri_owl_sameAs a a_1) False) (Eq (Eq a a_1) True) % 64.05/64.22 Clause #20 (by clausification #[17]): ∀ (a a_1 : Iota), Or (Eq (iext uri_owl_sameAs a a_1) False) (Eq a a_1) % 64.05/64.22 Clause #22 (by clausification #[1]): ∀ (a : Iota), % 64.05/64.22 Eq % 64.05/64.22 (∀ (P C : Iota), % 64.05/64.22 And (iext uri_owl_someValuesFrom a C) (iext uri_owl_onProperty a P) → % 64.05/64.22 ∀ (X : Iota), Iff (icext a X) (Exists fun Y => And (iext P X Y) (icext C Y))) % 64.05/64.22 True % 64.05/64.22 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 64.05/64.22 Eq % 64.05/64.22 (∀ (C : Iota), % 64.05/64.22 And (iext uri_owl_someValuesFrom a C) (iext uri_owl_onProperty a a_1) → % 64.05/64.22 ∀ (X : Iota), Iff (icext a X) (Exists fun Y => And (iext a_1 X Y) (icext C Y))) % 64.05/64.22 True % 64.05/64.22 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 64.05/64.22 Eq % 64.05/64.22 (And (iext uri_owl_someValuesFrom a a_1) (iext uri_owl_onProperty a a_2) → % 64.05/64.22 ∀ (X : Iota), Iff (icext a X) (Exists fun Y => And (iext a_2 X Y) (icext a_1 Y))) % 64.05/64.22 True % 64.05/64.22 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 64.05/64.22 Or (Eq (And (iext uri_owl_someValuesFrom a a_1) (iext uri_owl_onProperty a a_2)) False) % 64.05/64.22 (Eq (∀ (X : Iota), Iff (icext a X) (Exists fun Y => And (iext a_2 X Y) (icext a_1 Y))) True) % 64.05/64.22 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 64.05/64.22 Or (Eq (∀ (X : Iota), Iff (icext a X) (Exists fun Y => And (iext a_1 X Y) (icext a_2 Y))) True) % 64.05/64.22 (Or (Eq (iext uri_owl_someValuesFrom a a_2) False) (Eq (iext uri_owl_onProperty a a_1) False)) % 64.05/64.22 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), % 64.05/64.22 Or (Eq (iext uri_owl_someValuesFrom a a_1) False) % 64.05/64.22 (Or (Eq (iext uri_owl_onProperty a a_2) False) % 64.05/64.22 (Eq (Iff (icext a a_3) (Exists fun Y => And (iext a_2 a_3 Y) (icext a_1 Y))) True)) % 64.05/64.22 Clause #29 (by clausification #[27]): ∀ (a a_1 a_2 a_3 : Iota), % 64.05/64.22 Or (Eq (iext uri_owl_someValuesFrom a a_1) False) % 64.05/64.22 (Or (Eq (iext uri_owl_onProperty a a_2) False) % 64.05/64.22 (Or (Eq (icext a a_3) False) (Eq (Exists fun Y => And (iext a_2 a_3 Y) (icext a_1 Y)) True))) % 64.05/64.22 Clause #33 (by clausification #[2]): ∀ (a : Iota), % 64.05/64.22 Eq % 64.05/64.22 (∀ (C2 : Iota), % 64.05/64.22 Iff (iext uri_rdfs_subClassOf a C2) (And (And (ic a) (ic C2)) (∀ (X : Iota), icext a X → icext C2 X))) % 64.05/64.22 True % 64.05/64.22 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 64.05/64.22 Eq (Iff (iext uri_rdfs_subClassOf a a_1) (And (And (ic a) (ic a_1)) (∀ (X : Iota), icext a X → icext a_1 X))) True % 64.05/64.22 Clause #36 (by clausification #[34]): ∀ (a a_1 : Iota), % 64.05/64.22 Or (Eq (iext uri_rdfs_subClassOf a a_1) False) % 64.05/64.22 (Eq (And (And (ic a) (ic a_1)) (∀ (X : Iota), icext a X → icext a_1 X)) True) % 64.05/64.22 Clause #43 (by clausification #[36]): ∀ (a a_1 : Iota), Or (Eq (iext uri_rdfs_subClassOf a a_1) False) (Eq (∀ (X : Iota), icext a X → icext a_1 X) True) % 64.05/64.22 Clause #45 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), Or (Eq (iext uri_rdfs_subClassOf a a_1) False) (Eq (icext a a_2 → icext a_1 a_2) True) % 64.05/64.22 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), % 64.05/64.22 Or (Eq (iext uri_rdfs_subClassOf a a_1) False) (Or (Eq (icext a a_2) False) (Eq (icext a_1 a_2) True)) % 64.05/64.22 Clause #49 (by clausification #[3]): ∀ (a : Iota), % 64.05/64.22 Eq % 64.05/64.22 (∀ (P2 : Iota), % 64.05/64.22 Iff (iext uri_rdfs_subPropertyOf a P2) (And (And (ip a) (ip P2)) (∀ (X Y : Iota), iext a X Y → iext P2 X Y))) % 64.05/64.22 True % 64.05/64.22 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), % 64.05/64.22 Eq (Iff (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))) % 64.05/64.22 True % 64.05/64.22 Clause #52 (by clausification #[50]): ∀ (a a_1 : Iota), % 64.08/64.24 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) % 64.08/64.24 (Eq (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), iext a X Y → iext a_1 X Y)) True) % 64.08/64.24 Clause #61 (by clausification #[52]): ∀ (a a_1 : Iota), % 64.08/64.24 Or (Eq (iext uri_rdfs_subPropertyOf a a_1) False) (Eq (∀ (X Y : Iota), iext a X Y → iext a_1 X Y) True) % 64.08/64.24 Clause #63 (by clausification #[61]): ∀ (a a_1 a_2 : Iota), % 64.08/64.24 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) % 64.08/64.24 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 : Iota), % 64.08/64.24 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) % 64.08/64.24 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 : Iota), % 64.08/64.24 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)) % 64.08/64.24 Clause #68 (by clausification #[6]): ∀ (a : Iota), % 64.08/64.24 Eq % 64.08/64.24 (∀ (P2 : Iota), % 64.08/64.24 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)))) % 64.08/64.24 True % 64.08/64.24 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), % 64.08/64.24 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)))) % 64.08/64.24 True % 64.08/64.24 Clause #71 (by clausification #[69]): ∀ (a a_1 : Iota), % 64.08/64.24 Or (Eq (iext uri_owl_inverseOf a a_1) False) % 64.08/64.24 (Eq (And (And (ip a) (ip a_1)) (∀ (X Y : Iota), Iff (iext a X Y) (iext a_1 Y X))) True) % 64.08/64.24 Clause #80 (by clausification #[5]): ∀ (a : Iota), % 64.08/64.24 Eq % 64.08/64.24 (∀ (S1 P1 S2 P2 S3 P3 : Iota), % 64.08/64.24 And % 64.08/64.24 (And % 64.08/64.24 (And (And (And (iext uri_rdf_first S1 P1) (iext uri_rdf_rest S1 S2)) (iext uri_rdf_first S2 P2)) % 64.08/64.24 (iext uri_rdf_rest S2 S3)) % 64.08/64.24 (iext uri_rdf_first S3 P3)) % 64.08/64.24 (iext uri_rdf_rest S3 uri_rdf_nil) → % 64.08/64.24 Iff (iext uri_owl_propertyChainAxiom a S1) % 64.08/64.24 (And (And (And (And (ip a) (ip P1)) (ip P2)) (ip P3)) % 64.08/64.24 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext P1 Y0 Y1) (iext P2 Y1 Y2)) (iext P3 Y2 Y3) → iext a Y0 Y3))) % 64.08/64.24 True % 64.08/64.24 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), % 64.08/64.24 Eq % 64.08/64.24 (∀ (P1 S2 P2 S3 P3 : Iota), % 64.08/64.24 And % 64.08/64.24 (And % 64.08/64.24 (And (And (And (iext uri_rdf_first a P1) (iext uri_rdf_rest a S2)) (iext uri_rdf_first S2 P2)) % 64.08/64.24 (iext uri_rdf_rest S2 S3)) % 64.08/64.24 (iext uri_rdf_first S3 P3)) % 64.08/64.24 (iext uri_rdf_rest S3 uri_rdf_nil) → % 64.08/64.24 Iff (iext uri_owl_propertyChainAxiom a_1 a) % 64.08/64.24 (And (And (And (And (ip a_1) (ip P1)) (ip P2)) (ip P3)) % 64.08/64.24 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext P1 Y0 Y1) (iext P2 Y1 Y2)) (iext P3 Y2 Y3) → iext a_1 Y0 Y3))) % 64.08/64.24 True % 64.08/64.24 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), % 64.08/64.24 Eq % 64.08/64.24 (∀ (S2 P2 S3 P3 : Iota), % 64.08/64.24 And % 64.08/64.24 (And % 64.08/64.24 (And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a S2)) (iext uri_rdf_first S2 P2)) % 64.08/64.24 (iext uri_rdf_rest S2 S3)) % 64.08/64.24 (iext uri_rdf_first S3 P3)) % 64.08/64.24 (iext uri_rdf_rest S3 uri_rdf_nil) → % 64.08/64.24 Iff (iext uri_owl_propertyChainAxiom a_2 a) % 64.08/64.24 (And (And (And (And (ip a_2) (ip a_1)) (ip P2)) (ip P3)) % 64.08/64.24 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext P2 Y1 Y2)) (iext P3 Y2 Y3) → iext a_2 Y0 Y3))) % 64.08/64.24 True % 64.08/64.24 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 64.08/64.24 Eq % 64.08/64.24 (∀ (P2 S3 P3 : Iota), % 64.08/64.24 And % 64.08/64.24 (And % 64.08/64.24 (And (And (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a a_2)) (iext uri_rdf_first a_2 P2)) % 64.08/64.24 (iext uri_rdf_rest a_2 S3)) % 64.08/64.24 (iext uri_rdf_first S3 P3)) % 64.08/64.24 (iext uri_rdf_rest S3 uri_rdf_nil) → % 64.08/64.24 Iff (iext uri_owl_propertyChainAxiom a_3 a) % 64.08/64.24 (And (And (And (And (ip a_3) (ip a_1)) (ip P2)) (ip P3)) % 64.08/64.24 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext P2 Y1 Y2)) (iext P3 Y2 Y3) → iext a_3 Y0 Y3))) % 64.08/64.24 True % 64.08/64.24 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.08/64.24 Eq % 64.08/64.24 (∀ (S3 P3 : Iota), % 64.08/64.24 And % 64.08/64.24 (And % 64.08/64.24 (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)) % 64.08/64.26 (iext uri_rdf_rest a_2 S3)) % 64.08/64.26 (iext uri_rdf_first S3 P3)) % 64.08/64.26 (iext uri_rdf_rest S3 uri_rdf_nil) → % 64.08/64.26 Iff (iext uri_owl_propertyChainAxiom a_4 a) % 64.08/64.26 (And (And (And (And (ip a_4) (ip a_1)) (ip a_3)) (ip P3)) % 64.08/64.26 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2)) (iext P3 Y2 Y3) → iext a_4 Y0 Y3))) % 64.08/64.26 True % 64.08/64.26 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 64.08/64.26 Eq % 64.08/64.26 (∀ (P3 : Iota), % 64.08/64.26 And % 64.08/64.26 (And % 64.08/64.26 (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)) % 64.08/64.26 (iext uri_rdf_rest a_2 a_4)) % 64.08/64.26 (iext uri_rdf_first a_4 P3)) % 64.08/64.26 (iext uri_rdf_rest a_4 uri_rdf_nil) → % 64.08/64.26 Iff (iext uri_owl_propertyChainAxiom a_5 a) % 64.08/64.26 (And (And (And (And (ip a_5) (ip a_1)) (ip a_3)) (ip P3)) % 64.08/64.26 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2)) (iext P3 Y2 Y3) → iext a_5 Y0 Y3))) % 64.08/64.26 True % 64.08/64.26 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.26 Eq % 64.08/64.26 (And % 64.08/64.26 (And % 64.08/64.26 (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)) % 64.08/64.26 (iext uri_rdf_rest a_2 a_4)) % 64.08/64.26 (iext uri_rdf_first a_4 a_5)) % 64.08/64.26 (iext uri_rdf_rest a_4 uri_rdf_nil) → % 64.08/64.26 Iff (iext uri_owl_propertyChainAxiom a_6 a) % 64.08/64.26 (And (And (And (And (ip a_6) (ip a_1)) (ip a_3)) (ip a_5)) % 64.08/64.26 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2)) (iext a_5 Y2 Y3) → iext a_6 Y0 Y3))) % 64.08/64.26 True % 64.08/64.26 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.26 Or % 64.08/64.26 (Eq % 64.08/64.26 (And % 64.08/64.26 (And % 64.08/64.26 (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)) % 64.08/64.26 (iext uri_rdf_rest a_2 a_4)) % 64.08/64.26 (iext uri_rdf_first a_4 a_5)) % 64.08/64.26 (iext uri_rdf_rest a_4 uri_rdf_nil)) % 64.08/64.26 False) % 64.08/64.26 (Eq % 64.08/64.26 (Iff (iext uri_owl_propertyChainAxiom a_6 a) % 64.08/64.26 (And (And (And (And (ip a_6) (ip a_1)) (ip a_3)) (ip a_5)) % 64.08/64.26 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2)) (iext a_5 Y2 Y3) → iext a_6 Y0 Y3))) % 64.08/64.26 True) % 64.08/64.26 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.26 Or % 64.08/64.26 (Eq % 64.08/64.26 (Iff (iext uri_owl_propertyChainAxiom a a_1) % 64.08/64.26 (And (And (And (And (ip a) (ip a_2)) (ip a_3)) (ip a_4)) % 64.08/64.26 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_2 Y0 Y1) (iext a_3 Y1 Y2)) (iext a_4 Y2 Y3) → iext a Y0 Y3))) % 64.08/64.26 True) % 64.08/64.26 (Or % 64.08/64.26 (Eq % 64.08/64.26 (And % 64.08/64.26 (And (And (And (iext uri_rdf_first a_1 a_2) (iext uri_rdf_rest a_1 a_5)) (iext uri_rdf_first a_5 a_3)) % 64.08/64.26 (iext uri_rdf_rest a_5 a_6)) % 64.08/64.26 (iext uri_rdf_first a_6 a_4)) % 64.08/64.26 False) % 64.08/64.26 (Eq (iext uri_rdf_rest a_6 uri_rdf_nil) False)) % 64.08/64.26 Clause #90 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.26 Or % 64.08/64.26 (Eq % 64.08/64.26 (And % 64.08/64.26 (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)) % 64.08/64.26 (iext uri_rdf_rest a_2 a_4)) % 64.08/64.26 (iext uri_rdf_first a_4 a_5)) % 64.08/64.26 False) % 64.08/64.26 (Or (Eq (iext uri_rdf_rest a_4 uri_rdf_nil) False) % 64.08/64.26 (Or (Eq (iext uri_owl_propertyChainAxiom a_6 a) False) % 64.08/64.26 (Eq % 64.08/64.26 (And (And (And (And (ip a_6) (ip a_1)) (ip a_3)) (ip a_5)) % 64.08/64.26 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_1 Y0 Y1) (iext a_3 Y1 Y2)) (iext a_5 Y2 Y3) → iext a_6 Y0 Y3)) % 64.08/64.26 True))) % 64.08/64.26 Clause #111 (by clausification #[71]): ∀ (a a_1 : Iota), % 64.08/64.26 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) % 64.08/64.26 Clause #113 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 64.08/64.26 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) % 64.08/64.26 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 a_3 : Iota), % 64.08/64.26 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) % 64.08/64.26 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 a_3 : Iota), % 64.08/64.26 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)) % 64.08/64.27 Clause #119 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.08/64.27 Or (Eq (iext uri_owl_someValuesFrom a a_1) False) % 64.08/64.27 (Or (Eq (iext uri_owl_onProperty a a_2) False) % 64.08/64.27 (Or (Eq (icext a a_3) False) % 64.08/64.27 (Eq (And (iext a_2 a_3 (skS.0 9 a_2 a_3 a_1 a_4)) (icext a_1 (skS.0 9 a_2 a_3 a_1 a_4))) True))) % 64.08/64.27 Clause #121 (by clausification #[119]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.08/64.27 Or (Eq (iext uri_owl_someValuesFrom a a_1) False) % 64.08/64.27 (Or (Eq (iext uri_owl_onProperty a a_2) False) % 64.08/64.27 (Or (Eq (icext a a_3) False) (Eq (iext a_2 a_3 (skS.0 9 a_2 a_3 a_1 a_4)) True))) % 64.08/64.27 Clause #122 (by clausification #[8]): ∀ (a : Iota), % 64.08/64.27 Eq % 64.08/64.27 (Exists fun BNODE_i => % 64.08/64.27 Exists fun BNODE_l1 => % 64.08/64.27 Exists fun BNODE_l2 => % 64.08/64.27 Exists fun BNODE_l3 => % 64.08/64.27 And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.08/64.27 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.08/64.27 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.08/64.27 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.08/64.27 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.08/64.27 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.08/64.27 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.08/64.27 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.08/64.27 (iext uri_owl_propertyChainAxiom uri_foaf_knows BNODE_l1)) % 64.08/64.27 (iext uri_rdf_first BNODE_l1 uri_rdf_type)) % 64.08/64.27 (iext uri_rdf_rest BNODE_l1 BNODE_l2)) % 64.08/64.27 (iext uri_rdf_first BNODE_l2 uri_ex_sameCliqueAs)) % 64.08/64.27 (iext uri_rdf_rest BNODE_l2 BNODE_l3)) % 64.08/64.27 (iext uri_rdf_first BNODE_l3 BNODE_i)) % 64.08/64.27 (iext uri_rdf_rest BNODE_l3 uri_rdf_nil)) % 64.08/64.27 (iext uri_owl_inverseOf BNODE_i uri_rdf_type)) % 64.08/64.27 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.08/64.27 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.08/64.27 (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang)) % 64.08/64.27 True % 64.08/64.27 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 64.08/64.27 Eq % 64.08/64.27 (Exists fun BNODE_l1 => % 64.08/64.27 Exists fun BNODE_l2 => % 64.08/64.27 Exists fun BNODE_l3 => % 64.08/64.27 And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And % 64.08/64.27 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.08/64.27 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.08/64.27 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.08/64.27 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.08/64.27 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.08/64.28 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.08/64.28 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.08/64.28 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.08/64.28 (iext uri_owl_propertyChainAxiom uri_foaf_knows BNODE_l1)) % 64.08/64.28 (iext uri_rdf_first BNODE_l1 uri_rdf_type)) % 64.08/64.28 (iext uri_rdf_rest BNODE_l1 BNODE_l2)) % 64.08/64.28 (iext uri_rdf_first BNODE_l2 uri_ex_sameCliqueAs)) % 64.08/64.28 (iext uri_rdf_rest BNODE_l2 BNODE_l3)) % 64.08/64.28 (iext uri_rdf_first BNODE_l3 (skS.0 11 a a_1))) % 64.08/64.28 (iext uri_rdf_rest BNODE_l3 uri_rdf_nil)) % 64.08/64.28 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.08/64.28 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.08/64.28 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.08/64.28 (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang)) % 64.08/64.28 True % 64.08/64.28 Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 : Iota), % 64.08/64.28 Eq % 64.08/64.28 (Exists fun BNODE_l2 => % 64.08/64.28 Exists fun BNODE_l3 => % 64.08/64.28 And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.08/64.28 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.08/64.28 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.08/64.28 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.08/64.28 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.08/64.28 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.08/64.28 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.08/64.28 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.08/64.28 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.08/64.28 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.08/64.28 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) BNODE_l2)) % 64.08/64.28 (iext uri_rdf_first BNODE_l2 uri_ex_sameCliqueAs)) % 64.08/64.28 (iext uri_rdf_rest BNODE_l2 BNODE_l3)) % 64.08/64.28 (iext uri_rdf_first BNODE_l3 (skS.0 11 a a_1))) % 64.08/64.28 (iext uri_rdf_rest BNODE_l3 uri_rdf_nil)) % 64.08/64.28 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.08/64.28 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.08/64.28 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.08/64.28 (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang)) % 64.08/64.28 True % 64.08/64.28 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 a_3 : Iota), % 64.08/64.28 Eq % 64.08/64.28 (Exists fun BNODE_l3 => % 64.08/64.28 And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And % 64.08/64.28 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.08/64.28 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.08/64.28 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.08/64.29 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.08/64.29 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.08/64.29 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.08/64.29 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.08/64.29 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.08/64.29 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.08/64.29 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.08/64.29 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.08/64.29 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.08/64.29 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) BNODE_l3)) % 64.08/64.29 (iext uri_rdf_first BNODE_l3 (skS.0 11 a a_1))) % 64.08/64.29 (iext uri_rdf_rest BNODE_l3 uri_rdf_nil)) % 64.08/64.29 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.08/64.29 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.08/64.29 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.08/64.29 (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang)) % 64.08/64.29 True % 64.08/64.29 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.08/64.29 Eq % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.08/64.29 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.08/64.29 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.08/64.29 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.08/64.29 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.08/64.29 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.08/64.29 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.08/64.29 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.08/64.29 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.08/64.29 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.08/64.29 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.08/64.29 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.08/64.29 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.08/64.29 (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1))) % 64.08/64.29 (iext uri_rdf_rest (skS.0 14 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 64.08/64.29 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.08/64.29 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.08/64.29 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.08/64.29 (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang)) % 64.08/64.29 True % 64.08/64.29 Clause #127 (by clausification #[126]): Eq (iext uri_rdf_type uri_ex_bob uri_ex_JoesGang) True % 64.08/64.29 Clause #128 (by clausification #[126]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.08/64.29 Eq % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And % 64.08/64.29 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.08/64.29 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.08/64.31 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.08/64.31 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.08/64.31 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.08/64.31 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.08/64.31 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.08/64.31 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.08/64.31 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.08/64.31 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.08/64.31 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.08/64.31 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.08/64.31 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.08/64.31 (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1))) % 64.08/64.31 (iext uri_rdf_rest (skS.0 14 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 64.08/64.31 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.08/64.31 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.08/64.31 (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang)) % 64.08/64.31 True % 64.08/64.31 Clause #132 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.31 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.08/64.31 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.08/64.31 (Or % 64.08/64.31 (Eq % 64.08/64.31 (And (And (And (And (ip a_1) (ip a_3)) (ip a_4)) (ip a_5)) % 64.08/64.31 (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_3 Y0 Y1) (iext a_4 Y1 Y2)) (iext a_5 Y2 Y3) → iext a_1 Y0 Y3)) % 64.08/64.31 True) % 64.08/64.31 (Or % 64.08/64.31 (Eq % 64.08/64.31 (And (And (And (iext uri_rdf_first a_2 a_3) (iext uri_rdf_rest a_2 a_6)) (iext uri_rdf_first a_6 a_4)) % 64.08/64.31 (iext uri_rdf_rest a_6 a)) % 64.08/64.31 False) % 64.08/64.31 (Eq (iext uri_rdf_first a a_5) False)))) % 64.08/64.31 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.31 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.08/64.31 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.08/64.31 (Or % 64.08/64.31 (Eq % 64.08/64.31 (And (And (And (iext uri_rdf_first a_2 a_3) (iext uri_rdf_rest a_2 a_4)) (iext uri_rdf_first a_4 a_5)) % 64.08/64.31 (iext uri_rdf_rest a_4 a)) % 64.08/64.31 False) % 64.08/64.31 (Or (Eq (iext uri_rdf_first a a_6) False) % 64.08/64.31 (Eq (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_3 Y0 Y1) (iext a_5 Y1 Y2)) (iext a_6 Y2 Y3) → iext a_1 Y0 Y3) % 64.08/64.31 True)))) % 64.08/64.31 Clause #135 (by clausification #[133]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 64.08/64.31 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.08/64.31 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.08/64.31 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.08/64.31 (Or % 64.08/64.31 (Eq (∀ (Y0 Y1 Y2 Y3 : Iota), And (And (iext a_4 Y0 Y1) (iext a_5 Y1 Y2)) (iext a_3 Y2 Y3) → iext a_1 Y0 Y3) % 64.08/64.31 True) % 64.08/64.31 (Or % 64.08/64.31 (Eq (And (And (iext uri_rdf_first a_2 a_4) (iext uri_rdf_rest a_2 a_6)) (iext uri_rdf_first a_6 a_5)) False) % 64.08/64.31 (Eq (iext uri_rdf_rest a_6 a) False))))) % 64.08/64.31 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 64.08/64.31 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.08/64.31 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.08/64.31 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.08/64.31 (Or (Eq (And (And (iext uri_rdf_first a_2 a_4) (iext uri_rdf_rest a_2 a_5)) (iext uri_rdf_first a_5 a_6)) False) % 64.08/64.31 (Or (Eq (iext uri_rdf_rest a_5 a) False) % 64.08/64.31 (Eq (∀ (Y1 Y2 Y3 : Iota), And (And (iext a_4 a_7 Y1) (iext a_6 Y1 Y2)) (iext a_3 Y2 Y3) → iext a_1 a_7 Y3) % 64.08/64.31 True))))) % 64.08/64.31 Clause #137 (by clausification #[136]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 64.08/64.31 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.08/64.31 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.08/64.31 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.08/64.31 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.08/64.31 (Or % 64.17/64.33 (Eq (∀ (Y1 Y2 Y3 : Iota), And (And (iext a_5 a_6 Y1) (iext a_7 Y1 Y2)) (iext a_3 Y2 Y3) → iext a_1 a_6 Y3) % 64.17/64.33 True) % 64.17/64.33 (Or (Eq (And (iext uri_rdf_first a_2 a_5) (iext uri_rdf_rest a_2 a_4)) False) % 64.17/64.33 (Eq (iext uri_rdf_first a_4 a_7) False)))))) % 64.17/64.33 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 64.17/64.33 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.33 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.33 (Or (Eq (And (iext uri_rdf_first a_2 a_5) (iext uri_rdf_rest a_2 a_4)) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_4 a_6) False) % 64.17/64.33 (Eq (∀ (Y2 Y3 : Iota), And (And (iext a_5 a_7 a_8) (iext a_6 a_8 Y2)) (iext a_3 Y2 Y3) → iext a_1 a_7 Y3) % 64.17/64.33 True)))))) % 64.17/64.33 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 64.17/64.33 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.33 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_4 a_5) False) % 64.17/64.33 (Or % 64.17/64.33 (Eq (∀ (Y2 Y3 : Iota), And (And (iext a_6 a_7 a_8) (iext a_5 a_8 Y2)) (iext a_3 Y2 Y3) → iext a_1 a_7 Y3) % 64.17/64.33 True) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_2 a_6) False) (Eq (iext uri_rdf_rest a_2 a_4) False))))))) % 64.17/64.33 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 64.17/64.33 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.33 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_4 a_5) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_2 a_6) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_2 a_4) False) % 64.17/64.33 (Eq (∀ (Y3 : Iota), And (And (iext a_6 a_7 a_8) (iext a_5 a_8 a_9)) (iext a_3 a_9 Y3) → iext a_1 a_7 Y3) % 64.17/64.33 True))))))) % 64.17/64.33 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 64.17/64.33 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.33 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_4 a_5) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_2 a_6) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_2 a_4) False) % 64.17/64.33 (Eq (And (And (iext a_6 a_7 a_8) (iext a_5 a_8 a_9)) (iext a_3 a_9 a_10) → iext a_1 a_7 a_10) % 64.17/64.33 True))))))) % 64.17/64.33 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 64.17/64.33 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.33 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_4 a_5) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_2 a_6) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_2 a_4) False) % 64.17/64.33 (Or (Eq (And (And (iext a_6 a_7 a_8) (iext a_5 a_8 a_9)) (iext a_3 a_9 a_10)) False) % 64.17/64.33 (Eq (iext a_1 a_7 a_10) True)))))))) % 64.17/64.33 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 64.17/64.33 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.33 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_4 a_5) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_first a_2 a_6) False) % 64.17/64.33 (Or (Eq (iext uri_rdf_rest a_2 a_4) False) % 64.17/64.33 (Or (Eq (iext a_1 a_7 a_8) True) % 64.17/64.33 (Or (Eq (And (iext a_6 a_7 a_9) (iext a_5 a_9 a_10)) False) (Eq (iext a_3 a_10 a_8) False))))))))) % 64.17/64.33 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 64.17/64.34 Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 64.17/64.34 (Or (Eq (iext uri_owl_propertyChainAxiom a_1 a_2) False) % 64.17/64.34 (Or (Eq (iext uri_rdf_first a a_3) False) % 64.17/64.34 (Or (Eq (iext uri_rdf_rest a_4 a) False) % 64.17/64.34 (Or (Eq (iext uri_rdf_first a_4 a_5) False) % 64.17/64.34 (Or (Eq (iext uri_rdf_first a_2 a_6) False) % 64.17/64.34 (Or (Eq (iext uri_rdf_rest a_2 a_4) False) % 64.17/64.34 (Or (Eq (iext a_1 a_7 a_8) True) % 64.17/64.34 (Or (Eq (iext a_3 a_9 a_8) False) % 64.17/64.34 (Or (Eq (iext a_6 a_7 a_10) False) (Eq (iext a_5 a_10 a_9) False)))))))))) % 64.17/64.34 Clause #159 (by clausification #[128]): Eq (iext uri_rdf_type uri_ex_alice uri_ex_JoesGang) True % 64.17/64.34 Clause #160 (by clausification #[128]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.17/64.34 Eq % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.34 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.34 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.34 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.34 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.34 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.34 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.34 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.34 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.34 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.34 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.34 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.17/64.34 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.17/64.34 (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1))) % 64.17/64.34 (iext uri_rdf_rest (skS.0 14 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 64.17/64.34 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.17/64.34 (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique)) % 64.17/64.34 True % 64.17/64.34 Clause #164 (by clausification #[160]): Eq (iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique) True % 64.17/64.34 Clause #165 (by clausification #[160]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.17/64.34 Eq % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And % 64.17/64.34 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.34 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.34 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.34 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.34 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.34 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.34 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.34 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.34 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.34 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.34 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.34 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.17/64.34 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.17/64.35 (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1))) % 64.17/64.35 (iext uri_rdf_rest (skS.0 14 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 64.17/64.35 (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type)) % 64.17/64.35 True % 64.17/64.35 Clause #166 (by superposition #[164, 13]): Or (Eq True False) (Eq (icext uri_ex_Clique uri_ex_JoesGang) True) % 64.17/64.35 Clause #167 (by clausification #[165]): ∀ (a a_1 : Iota), Eq (iext uri_owl_inverseOf (skS.0 11 a a_1) uri_rdf_type) True % 64.17/64.35 Clause #168 (by clausification #[165]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.17/64.35 Eq % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.35 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.35 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.35 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.35 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.35 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.35 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.35 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.35 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.35 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.35 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.35 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.17/64.35 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.17/64.35 (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1))) % 64.17/64.35 (iext uri_rdf_rest (skS.0 14 a a_1 a_2 a_3 a_4) uri_rdf_nil)) % 64.17/64.35 True % 64.17/64.35 Clause #169 (by superposition #[167, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 64.17/64.35 Or (Eq True False) (Or (Eq (iext (skS.0 11 a a_1) a_2 a_3) True) (Eq (iext uri_rdf_type a_3 a_2) False)) % 64.17/64.35 Clause #178 (by clausification #[166]): Eq (icext uri_ex_Clique uri_ex_JoesGang) True % 64.17/64.35 Clause #185 (by clausification #[169]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (iext (skS.0 11 a a_1) a_2 a_3) True) (Eq (iext uri_rdf_type a_3 a_2) False) % 64.17/64.35 Clause #186 (by superposition #[185, 127]): ∀ (a a_1 : Iota), Or (Eq (iext (skS.0 11 a a_1) uri_ex_JoesGang uri_ex_bob) True) (Eq False True) % 64.17/64.35 Clause #189 (by clausification #[168]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_rest (skS.0 14 a a_1 a_2 a_3 a_4) uri_rdf_nil) True % 64.17/64.35 Clause #190 (by clausification #[168]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.17/64.35 Eq % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And % 64.17/64.35 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.35 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.35 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.35 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.35 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.35 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.35 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.35 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.35 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.35 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.35 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.35 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.17/64.35 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.17/64.37 (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1))) % 64.17/64.37 True % 64.17/64.37 Clause #192 (by superposition #[189, 144]): ∀ (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 a_14 : Iota), % 64.17/64.37 Or (Eq True False) % 64.17/64.37 (Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_first (skS.0 14 a_2 a_3 a_4 a_5 a_6) a_7) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_rest a_8 (skS.0 14 a_2 a_3 a_4 a_5 a_6)) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_first a_8 a_9) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_first a_1 a_10) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_rest a_1 a_8) False) % 64.17/64.37 (Or (Eq (iext a a_11 a_12) True) % 64.17/64.37 (Or (Eq (iext a_7 a_13 a_12) False) % 64.17/64.37 (Or (Eq (iext a_10 a_11 a_14) False) (Eq (iext a_9 a_14 a_13) False)))))))))) % 64.17/64.37 Clause #202 (by clausification #[186]): ∀ (a a_1 : Iota), Eq (iext (skS.0 11 a a_1) uri_ex_JoesGang uri_ex_bob) True % 64.17/64.37 Clause #274 (by clausification #[190]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1)) True % 64.17/64.37 Clause #275 (by clausification #[190]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 64.17/64.37 Eq % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.37 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.37 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.37 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.37 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.37 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.37 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.37 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.37 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.37 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.37 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.37 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.17/64.37 (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 64.17/64.37 True % 64.17/64.37 Clause #289 (by clausification #[192]): ∀ (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 a_14 : Iota), % 64.17/64.37 Or (Eq (iext uri_owl_propertyChainAxiom a a_1) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_first (skS.0 14 a_2 a_3 a_4 a_5 a_6) a_7) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_rest a_8 (skS.0 14 a_2 a_3 a_4 a_5 a_6)) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_first a_8 a_9) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_first a_1 a_10) False) % 64.17/64.37 (Or (Eq (iext uri_rdf_rest a_1 a_8) False) % 64.17/64.37 (Or (Eq (iext a a_11 a_12) True) % 64.17/64.37 (Or (Eq (iext a_7 a_13 a_12) False) % 64.17/64.37 (Or (Eq (iext a_10 a_11 a_14) False) (Eq (iext a_9 a_14 a_13) False))))))))) % 64.17/64.37 Clause #384 (by clausification #[275]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (iext uri_rdf_rest (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4)) True % 64.17/64.37 Clause #385 (by clausification #[275]): ∀ (a a_1 a_2 a_3 : Iota), % 64.17/64.37 Eq % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And % 64.17/64.37 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.37 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.37 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.37 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.37 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.37 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.37 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.37 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.38 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.38 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.38 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.38 (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs)) % 64.17/64.38 True % 64.17/64.38 Clause #401 (by clausification #[385]): ∀ (a a_1 a_2 a_3 : Iota), Eq (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) uri_ex_sameCliqueAs) True % 64.17/64.38 Clause #402 (by clausification #[385]): ∀ (a a_1 a_2 a_3 : Iota), % 64.17/64.38 Eq % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.38 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.38 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.38 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.38 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.38 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.38 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.38 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.38 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.38 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.38 (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3))) % 64.17/64.38 True % 64.17/64.38 Clause #414 (by clausification #[402]): ∀ (a a_1 a_2 a_3 : Iota), Eq (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) True % 64.17/64.38 Clause #415 (by clausification #[402]): ∀ (a a_1 a_2 : Iota), % 64.17/64.38 Eq % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.38 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.38 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.38 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.38 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.38 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.38 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.38 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.38 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.38 (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type)) % 64.17/64.38 True % 64.17/64.38 Clause #416 (by clausification #[415]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_rdf_first (skS.0 12 a a_1 a_2) uri_rdf_type) True % 64.17/64.38 Clause #417 (by clausification #[415]): ∀ (a a_1 a_2 : Iota), % 64.17/64.38 Eq % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.38 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.38 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.17/64.38 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.17/64.38 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.17/64.38 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.17/64.38 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.17/64.38 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.17/64.38 (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2))) % 64.17/64.38 True % 64.17/64.38 Clause #418 (by clausification #[417]): ∀ (a a_1 a_2 : Iota), Eq (iext uri_owl_propertyChainAxiom uri_foaf_knows (skS.0 12 a a_1 a_2)) True % 64.17/64.38 Clause #419 (by clausification #[417]): ∀ (a : Iota), % 64.17/64.38 Eq % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And % 64.17/64.38 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.17/64.38 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.17/64.38 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.24/64.40 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.24/64.40 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.24/64.40 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.24/64.40 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.24/64.40 (iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty)) % 64.24/64.40 True % 64.24/64.40 Clause #424 (by superposition #[418, 289]): ∀ (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 a_14 a_15 : Iota), % 64.24/64.40 Or (Eq True False) % 64.24/64.40 (Or (Eq (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) a_5) False) % 64.24/64.40 (Or (Eq (iext uri_rdf_rest a_6 (skS.0 14 a a_1 a_2 a_3 a_4)) False) % 64.24/64.40 (Or (Eq (iext uri_rdf_first a_6 a_7) False) % 64.24/64.40 (Or (Eq (iext uri_rdf_first (skS.0 12 a_8 a_9 a_10) a_11) False) % 64.24/64.40 (Or (Eq (iext uri_rdf_rest (skS.0 12 a_8 a_9 a_10) a_6) False) % 64.24/64.40 (Or (Eq (iext uri_foaf_knows a_12 a_13) True) % 64.24/64.40 (Or (Eq (iext a_5 a_14 a_13) False) % 64.24/64.40 (Or (Eq (iext a_11 a_12 a_15) False) (Eq (iext a_7 a_15 a_14) False))))))))) % 64.24/64.40 Clause #429 (by clausification #[419]): ∀ (a : Iota), % 64.24/64.40 Eq % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.24/64.40 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.24/64.40 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.24/64.40 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.24/64.40 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.24/64.40 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.24/64.40 (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique)) % 64.24/64.40 True % 64.24/64.40 Clause #439 (by clausification #[429]): ∀ (a : Iota), Eq (iext uri_owl_someValuesFrom (skS.0 10 a) uri_ex_Clique) True % 64.24/64.40 Clause #440 (by clausification #[429]): ∀ (a : Iota), % 64.24/64.40 Eq % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.24/64.40 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.24/64.40 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.24/64.40 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.24/64.40 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.24/64.40 (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs)) % 64.24/64.40 True % 64.24/64.40 Clause #443 (by superposition #[439, 121]): ∀ (a a_1 a_2 a_3 : Iota), % 64.24/64.40 Or (Eq True False) % 64.24/64.40 (Or (Eq (iext uri_owl_onProperty (skS.0 10 a) a_1) False) % 64.24/64.40 (Or (Eq (icext (skS.0 10 a) a_2) False) (Eq (iext a_1 a_2 (skS.0 9 a_1 a_2 uri_ex_Clique a_3)) True))) % 64.24/64.40 Clause #446 (by clausification #[443]): ∀ (a a_1 a_2 a_3 : Iota), % 64.24/64.40 Or (Eq (iext uri_owl_onProperty (skS.0 10 a) a_1) False) % 64.24/64.40 (Or (Eq (icext (skS.0 10 a) a_2) False) (Eq (iext a_1 a_2 (skS.0 9 a_1 a_2 uri_ex_Clique a_3)) True)) % 64.24/64.40 Clause #449 (by clausification #[440]): ∀ (a : Iota), Eq (iext uri_owl_onProperty (skS.0 10 a) uri_ex_sameCliqueAs) True % 64.24/64.40 Clause #450 (by clausification #[440]): ∀ (a : Iota), % 64.24/64.40 Eq % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.24/64.40 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.24/64.40 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.24/64.40 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.24/64.40 (iext uri_rdf_type (skS.0 10 a) uri_owl_Restriction)) % 64.24/64.40 True % 64.24/64.40 Clause #453 (by superposition #[449, 446]): ∀ (a a_1 a_2 : Iota), % 64.24/64.40 Or (Eq True False) % 64.24/64.40 (Or (Eq (icext (skS.0 10 a) a_1) False) % 64.24/64.40 (Eq (iext uri_ex_sameCliqueAs a_1 (skS.0 9 uri_ex_sameCliqueAs a_1 uri_ex_Clique a_2)) True)) % 64.24/64.40 Clause #456 (by clausification #[453]): ∀ (a a_1 a_2 : Iota), % 64.24/64.40 Or (Eq (icext (skS.0 10 a) a_1) False) % 64.24/64.40 (Eq (iext uri_ex_sameCliqueAs a_1 (skS.0 9 uri_ex_sameCliqueAs a_1 uri_ex_Clique a_2)) True) % 64.24/64.40 Clause #458 (by clausification #[450]): ∀ (a : Iota), % 64.24/64.40 Eq % 64.24/64.40 (And % 64.24/64.40 (And % 64.24/64.40 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.24/64.40 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.24/64.40 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.24/64.40 (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a))) % 64.24/64.42 True % 64.24/64.42 Clause #467 (by clausification #[458]): ∀ (a : Iota), Eq (iext uri_rdfs_subClassOf uri_ex_Clique (skS.0 10 a)) True % 64.24/64.42 Clause #468 (by clausification #[458]): Eq % 64.24/64.42 (And % 64.24/64.42 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) % 64.24/64.42 (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.24/64.42 (iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique)) % 64.24/64.42 True % 64.24/64.42 Clause #469 (by superposition #[467, 46]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (icext uri_ex_Clique a) False) (Eq (icext (skS.0 10 a_1) a) True)) % 64.24/64.42 Clause #478 (by clausification #[469]): ∀ (a a_1 : Iota), Or (Eq (icext uri_ex_Clique a) False) (Eq (icext (skS.0 10 a_1) a) True) % 64.24/64.42 Clause #479 (by superposition #[478, 178]): ∀ (a : Iota), Or (Eq (icext (skS.0 10 a) uri_ex_JoesGang) True) (Eq False True) % 64.24/64.42 Clause #480 (by clausification #[479]): ∀ (a : Iota), Eq (icext (skS.0 10 a) uri_ex_JoesGang) True % 64.24/64.42 Clause #482 (by superposition #[480, 456]): ∀ (a : Iota), % 64.24/64.42 Or (Eq True False) % 64.24/64.42 (Eq (iext uri_ex_sameCliqueAs uri_ex_JoesGang (skS.0 9 uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_Clique a)) True) % 64.24/64.42 Clause #491 (by clausification #[468]): Eq % 64.24/64.42 (And (iext uri_rdf_type uri_ex_Clique uri_owl_Class) (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs)) % 64.24/64.42 True % 64.24/64.42 Clause #492 (by clausification #[491]): Eq (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs) True % 64.24/64.42 Clause #494 (by superposition #[492, 65]): ∀ (a a_1 : Iota), % 64.24/64.42 Or (Eq True False) (Or (Eq (iext uri_ex_sameCliqueAs a a_1) False) (Eq (iext uri_owl_sameAs a a_1) True)) % 64.24/64.42 Clause #532 (by clausification #[494]): ∀ (a a_1 : Iota), Or (Eq (iext uri_ex_sameCliqueAs a a_1) False) (Eq (iext uri_owl_sameAs a a_1) True) % 64.24/64.42 Clause #540 (by clausification #[482]): ∀ (a : Iota), % 64.24/64.42 Eq (iext uri_ex_sameCliqueAs uri_ex_JoesGang (skS.0 9 uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_Clique a)) True % 64.24/64.42 Clause #542 (by superposition #[540, 532]): ∀ (a : Iota), % 64.24/64.42 Or (Eq True False) % 64.24/64.42 (Eq (iext uri_owl_sameAs uri_ex_JoesGang (skS.0 9 uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_Clique a)) True) % 64.24/64.42 Clause #544 (by clausification #[542]): ∀ (a : Iota), % 64.24/64.42 Eq (iext uri_owl_sameAs uri_ex_JoesGang (skS.0 9 uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_Clique a)) True % 64.24/64.42 Clause #545 (by superposition #[544, 20]): ∀ (a : Iota), Or (Eq True False) (Eq uri_ex_JoesGang (skS.0 9 uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_Clique a)) % 64.24/64.42 Clause #546 (by clausification #[545]): ∀ (a : Iota), Eq uri_ex_JoesGang (skS.0 9 uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_Clique a) % 64.24/64.42 Clause #547 (by backward demodulation #[546, 540]): Eq (iext uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_JoesGang) True % 64.24/64.42 Clause #592 (by clausification #[424]): ∀ (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 a_14 a_15 : Iota), % 64.24/64.42 Or (Eq (iext uri_rdf_first (skS.0 14 a a_1 a_2 a_3 a_4) a_5) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_rest a_6 (skS.0 14 a a_1 a_2 a_3 a_4)) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_first a_6 a_7) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_first (skS.0 12 a_8 a_9 a_10) a_11) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_rest (skS.0 12 a_8 a_9 a_10) a_6) False) % 64.24/64.42 (Or (Eq (iext uri_foaf_knows a_12 a_13) True) % 64.24/64.42 (Or (Eq (iext a_5 a_14 a_13) False) % 64.24/64.42 (Or (Eq (iext a_11 a_12 a_15) False) (Eq (iext a_7 a_15 a_14) False)))))))) % 64.24/64.42 Clause #593 (by superposition #[592, 274]): ∀ (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 a_14 : Iota), % 64.24/64.42 Or (Eq (iext uri_rdf_rest a (skS.0 14 a_1 a_2 a_3 a_4 a_5)) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_first a a_6) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_first (skS.0 12 a_7 a_8 a_9) a_10) False) % 64.24/64.42 (Or (Eq (iext uri_rdf_rest (skS.0 12 a_7 a_8 a_9) a) False) % 64.24/64.42 (Or (Eq (iext uri_foaf_knows a_11 a_12) True) % 64.24/64.42 (Or (Eq (iext (skS.0 11 a_1 a_2) a_13 a_12) False) % 64.24/64.42 (Or (Eq (iext a_10 a_11 a_14) False) (Or (Eq (iext a_6 a_14 a_13) False) (Eq False True)))))))) % 64.24/64.42 Clause #931 (by clausification #[593]): ∀ (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 a_14 : Iota), % 64.24/64.42 Or (Eq (iext uri_rdf_rest a (skS.0 14 a_1 a_2 a_3 a_4 a_5)) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_first a a_6) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_first (skS.0 12 a_7 a_8 a_9) a_10) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_rest (skS.0 12 a_7 a_8 a_9) a) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_11 a_12) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_1 a_2) a_13 a_12) False) % 64.24/64.44 (Or (Eq (iext a_10 a_11 a_14) False) (Eq (iext a_6 a_14 a_13) False))))))) % 64.24/64.44 Clause #932 (by superposition #[931, 384]): ∀ (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), % 64.24/64.44 Or (Eq (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) a_4) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_first (skS.0 12 a_5 a_6 a_7) a_8) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_rest (skS.0 12 a_5 a_6 a_7) (skS.0 13 a a_1 a_2 a_3)) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_9 a_10) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a a_1) a_11 a_10) False) % 64.24/64.44 (Or (Eq (iext a_8 a_9 a_12) False) (Or (Eq (iext a_4 a_12 a_11) False) (Eq False True))))))) % 64.24/64.44 Clause #1400 (by clausification #[932]): ∀ (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), % 64.24/64.44 Or (Eq (iext uri_rdf_first (skS.0 13 a a_1 a_2 a_3) a_4) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_first (skS.0 12 a_5 a_6 a_7) a_8) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_rest (skS.0 12 a_5 a_6 a_7) (skS.0 13 a a_1 a_2 a_3)) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_9 a_10) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a a_1) a_11 a_10) False) % 64.24/64.44 (Or (Eq (iext a_8 a_9 a_12) False) (Eq (iext a_4 a_12 a_11) False)))))) % 64.24/64.44 Clause #1401 (by superposition #[1400, 401]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 64.24/64.44 Or (Eq (iext uri_rdf_first (skS.0 12 a a_1 a_2) a_3) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a_4 a_5 a_6 a_7)) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_8 a_9) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_4 a_5) a_10 a_9) False) % 64.24/64.44 (Or (Eq (iext a_3 a_8 a_11) False) (Or (Eq (iext uri_ex_sameCliqueAs a_11 a_10) False) (Eq False True)))))) % 64.24/64.44 Clause #1685 (by clausification #[1401]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 64.24/64.44 Or (Eq (iext uri_rdf_first (skS.0 12 a a_1 a_2) a_3) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a_4 a_5 a_6 a_7)) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_8 a_9) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_4 a_5) a_10 a_9) False) % 64.24/64.44 (Or (Eq (iext a_3 a_8 a_11) False) (Eq (iext uri_ex_sameCliqueAs a_11 a_10) False))))) % 64.24/64.44 Clause #1686 (by superposition #[1685, 416]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 64.24/64.44 Or (Eq (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a_3 a_4 a_5 a_6)) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_7 a_8) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_3 a_4) a_9 a_8) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_type a_7 a_10) False) % 64.24/64.44 (Or (Eq (iext uri_ex_sameCliqueAs a_10 a_9) False) (Eq False True))))) % 64.24/64.44 Clause #1690 (by clausification #[1686]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 64.24/64.44 Or (Eq (iext uri_rdf_rest (skS.0 12 a a_1 a_2) (skS.0 13 a_3 a_4 a_5 a_6)) False) % 64.24/64.44 (Or (Eq (iext uri_foaf_knows a_7 a_8) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_3 a_4) a_9 a_8) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_type a_7 a_10) False) (Eq (iext uri_ex_sameCliqueAs a_10 a_9) False)))) % 64.24/64.44 Clause #1691 (by superposition #[1690, 414]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 64.24/64.44 Or (Eq (iext uri_foaf_knows a a_1) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_2 a_3) a_4 a_1) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_type a a_5) False) (Or (Eq (iext uri_ex_sameCliqueAs a_5 a_4) False) (Eq False True)))) % 64.24/64.44 Clause #1692 (by clausification #[1691]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 64.24/64.44 Or (Eq (iext uri_foaf_knows a a_1) True) % 64.24/64.44 (Or (Eq (iext (skS.0 11 a_2 a_3) a_4 a_1) False) % 64.24/64.44 (Or (Eq (iext uri_rdf_type a a_5) False) (Eq (iext uri_ex_sameCliqueAs a_5 a_4) False))) % 64.24/64.44 Clause #1695 (by superposition #[1692, 202]): ∀ (a a_1 : Iota), % 64.24/64.44 Or (Eq (iext uri_foaf_knows a uri_ex_bob) True) % 64.24/64.44 (Or (Eq (iext uri_rdf_type a a_1) False) % 64.24/64.44 (Or (Eq (iext uri_ex_sameCliqueAs a_1 uri_ex_JoesGang) False) (Eq False True))) % 64.24/64.44 Clause #1759 (by clausification #[1695]): ∀ (a a_1 : Iota), % 64.24/64.45 Or (Eq (iext uri_foaf_knows a uri_ex_bob) True) % 64.24/64.45 (Or (Eq (iext uri_rdf_type a a_1) False) (Eq (iext uri_ex_sameCliqueAs a_1 uri_ex_JoesGang) False)) % 64.24/64.45 Clause #1761 (by superposition #[1759, 159]): Or (Eq (iext uri_foaf_knows uri_ex_alice uri_ex_bob) True) % 64.24/64.45 (Or (Eq (iext uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_JoesGang) False) (Eq False True)) % 64.24/64.45 Clause #1790 (by clausification #[1761]): Or (Eq (iext uri_foaf_knows uri_ex_alice uri_ex_bob) True) % 64.24/64.45 (Eq (iext uri_ex_sameCliqueAs uri_ex_JoesGang uri_ex_JoesGang) False) % 64.24/64.45 Clause #1791 (by forward demodulation #[1790, 547]): Or (Eq (iext uri_foaf_knows uri_ex_alice uri_ex_bob) True) (Eq True False) % 64.24/64.45 Clause #1792 (by clausification #[1791]): Eq (iext uri_foaf_knows uri_ex_alice uri_ex_bob) True % 64.24/64.45 Clause #1793 (by superposition #[1792, 9]): Eq True False % 64.24/64.45 Clause #1794 (by clausification #[1793]): False % 64.24/64.45 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------