%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB004+2 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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:21 PM UTC 2025 % Result : Theorem 9.04s 9.22s % Output : Proof 9.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB004+2 : TPTP v9.2.0. Released v5.2.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 11:44:08 EDT 2025 % 0.12/0.34 % CPUTime : % 9.04/9.22 SZS status Theorem for theBenchmark.p % 9.04/9.22 SZS output start Proof for theBenchmark.p % 9.04/9.22 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), ir X) True % 9.04/9.22 Clause #1 (by assumption #[]): Eq (∀ (X C : Iota), Iff (iext uri_rdf_type X C) (icext C X)) True % 9.04/9.22 Clause #2 (by assumption #[]): Eq (∀ (X : Iota), idc X → ic X) True % 9.04/9.22 Clause #3 (by assumption #[]): Eq (ic uri_owl_Class) True % 9.04/9.22 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_owl_Class X) (ic X)) True % 9.04/9.22 Clause #5 (by assumption #[]): Eq (ic uri_rdfs_Class) True % 9.04/9.22 Clause #6 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_rdfs_Class X) (ic X)) True % 9.04/9.22 Clause #7 (by assumption #[]): Eq (ic uri_rdfs_Datatype) True % 9.04/9.22 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_rdfs_Datatype X) (idc X)) True % 9.04/9.22 Clause #9 (by assumption #[]): Eq (ic uri_owl_Thing) True % 9.04/9.22 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_owl_Thing X) (ir X)) True % 9.04/9.22 Clause #11 (by assumption #[]): Eq % 9.04/9.22 (∀ (C1 C2 : Iota), % 9.04/9.22 Iff (iext uri_rdfs_subClassOf C1 C2) (And (And (ic C1) (ic C2)) (∀ (X : Iota), icext C1 X → icext C2 X))) % 9.04/9.22 True % 9.04/9.22 Clause #12 (by assumption #[]): Eq % 9.04/9.22 (∀ (C1 C2 : Iota), % 9.04/9.22 Iff (iext uri_owl_equivalentClass C1 C2) (And (And (ic C1) (ic C2)) (∀ (X : Iota), Iff (icext C1 X) (icext C2 X)))) % 9.04/9.22 True % 9.04/9.22 Clause #13 (by assumption #[]): Eq % 9.04/9.22 (Not % 9.04/9.22 (And % 9.04/9.22 (And % 9.04/9.22 (And (And (iext uri_rdf_type uri_owl_Class uri_owl_Thing) (iext uri_rdf_type uri_owl_Class uri_owl_Class)) % 9.04/9.22 (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing)) % 9.04/9.22 (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class)) % 9.04/9.22 (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class))) % 9.04/9.22 True % 9.04/9.22 Clause #14 (by clausification #[0]): ∀ (a : Iota), Eq (ir a) True % 9.04/9.22 Clause #15 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (iext uri_rdf_type a C) (icext C a)) True % 9.04/9.22 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_rdf_type a a_1) (icext a_1 a)) True % 9.04/9.22 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Or (Eq (iext uri_rdf_type a a_1) True) (Eq (icext a_1 a) False) % 9.04/9.22 Clause #19 (by clausification #[2]): ∀ (a : Iota), Eq (idc a → ic a) True % 9.04/9.22 Clause #20 (by clausification #[19]): ∀ (a : Iota), Or (Eq (idc a) False) (Eq (ic a) True) % 9.04/9.22 Clause #21 (by clausification #[4]): ∀ (a : Iota), Eq (Iff (icext uri_owl_Class a) (ic a)) True % 9.04/9.22 Clause #22 (by clausification #[21]): ∀ (a : Iota), Or (Eq (icext uri_owl_Class a) True) (Eq (ic a) False) % 9.04/9.22 Clause #23 (by clausification #[21]): ∀ (a : Iota), Or (Eq (icext uri_owl_Class a) False) (Eq (ic a) True) % 9.04/9.22 Clause #27 (by superposition #[22, 3]): Or (Eq (icext uri_owl_Class uri_owl_Class) True) (Eq False True) % 9.04/9.22 Clause #28 (by clausification #[27]): Eq (icext uri_owl_Class uri_owl_Class) True % 9.04/9.22 Clause #29 (by superposition #[28, 17]): Or (Eq (iext uri_rdf_type uri_owl_Class uri_owl_Class) True) (Eq True False) % 9.04/9.22 Clause #34 (by clausification #[6]): ∀ (a : Iota), Eq (Iff (icext uri_rdfs_Class a) (ic a)) True % 9.04/9.22 Clause #35 (by clausification #[34]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Class a) True) (Eq (ic a) False) % 9.04/9.22 Clause #36 (by clausification #[34]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Class a) False) (Eq (ic a) True) % 9.04/9.22 Clause #51 (by clausification #[8]): ∀ (a : Iota), Eq (Iff (icext uri_rdfs_Datatype a) (idc a)) True % 9.04/9.22 Clause #53 (by clausification #[51]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Datatype a) False) (Eq (idc a) True) % 9.04/9.22 Clause #58 (by clausification #[10]): ∀ (a : Iota), Eq (Iff (icext uri_owl_Thing a) (ir a)) True % 9.04/9.22 Clause #59 (by clausification #[58]): ∀ (a : Iota), Or (Eq (icext uri_owl_Thing a) True) (Eq (ir a) False) % 9.04/9.22 Clause #61 (by forward demodulation #[59, 14]): ∀ (a : Iota), Or (Eq (icext uri_owl_Thing a) True) (Eq True False) % 9.04/9.22 Clause #62 (by clausification #[61]): ∀ (a : Iota), Eq (icext uri_owl_Thing a) True % 9.04/9.22 Clause #63 (by superposition #[62, 17]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_owl_Thing) True) (Eq True False) % 9.04/9.22 Clause #65 (by clausification #[63]): ∀ (a : Iota), Eq (iext uri_rdf_type a uri_owl_Thing) True % 9.04/9.22 Clause #67 (by clausification #[11]): ∀ (a : Iota), % 9.07/9.25 Eq % 9.07/9.25 (∀ (C2 : Iota), % 9.07/9.25 Iff (iext uri_rdfs_subClassOf a C2) (And (And (ic a) (ic C2)) (∀ (X : Iota), icext a X → icext C2 X))) % 9.07/9.25 True % 9.07/9.25 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), % 9.07/9.25 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 % 9.07/9.25 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Eq (And (And (ic a) (ic a_1)) (∀ (X : Iota), icext a X → icext a_1 X)) False) % 9.07/9.25 Clause #70 (by clausification #[68]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) False) % 9.07/9.25 (Eq (And (And (ic a) (ic a_1)) (∀ (X : Iota), icext a X → icext a_1 X)) True) % 9.07/9.25 Clause #71 (by clausification #[69]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Or (Eq (And (ic a) (ic a_1)) False) (Eq (∀ (X : Iota), icext a X → icext a_1 X) False)) % 9.07/9.25 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Or (Eq (∀ (X : Iota), icext a X → icext a_1 X) False) (Or (Eq (ic a) False) (Eq (ic a_1) False))) % 9.07/9.25 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Or (Eq (ic a) False) % 9.07/9.25 (Or (Eq (ic a_1) False) (Eq (Not (icext a (skS.0 0 a a_1 a_2) → icext a_1 (skS.0 0 a a_1 a_2))) True))) % 9.07/9.25 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Or (Eq (ic a) False) % 9.07/9.25 (Or (Eq (ic a_1) False) (Eq (icext a (skS.0 0 a a_1 a_2) → icext a_1 (skS.0 0 a a_1 a_2)) False))) % 9.07/9.25 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Or (Eq (ic a) False) (Or (Eq (ic a_1) False) (Eq (icext a (skS.0 0 a a_1 a_2)) True))) % 9.07/9.25 Clause #76 (by clausification #[74]): ∀ (a a_1 a_2 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf a a_1) True) % 9.07/9.25 (Or (Eq (ic a) False) (Or (Eq (ic a_1) False) (Eq (icext a_1 (skS.0 0 a a_1 a_2)) False))) % 9.07/9.25 Clause #78 (by superposition #[75, 7]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype a) True) % 9.07/9.25 (Or (Eq (ic a) False) (Or (Eq (icext uri_rdfs_Datatype (skS.0 0 uri_rdfs_Datatype a a_1)) True) (Eq False True))) % 9.07/9.25 Clause #79 (by superposition #[75, 5]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class a) True) % 9.07/9.25 (Or (Eq (ic a) False) (Or (Eq (icext uri_rdfs_Class (skS.0 0 uri_rdfs_Class a a_1)) True) (Eq False True))) % 9.07/9.25 Clause #82 (by clausification #[29]): Eq (iext uri_rdf_type uri_owl_Class uri_owl_Class) True % 9.07/9.25 Clause #86 (by clausification #[12]): ∀ (a : Iota), % 9.07/9.25 Eq % 9.07/9.25 (∀ (C2 : Iota), % 9.07/9.25 Iff (iext uri_owl_equivalentClass a C2) (And (And (ic a) (ic C2)) (∀ (X : Iota), Iff (icext a X) (icext C2 X)))) % 9.07/9.25 True % 9.07/9.25 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), % 9.07/9.25 Eq % 9.07/9.25 (Iff (iext uri_owl_equivalentClass a a_1) (And (And (ic a) (ic a_1)) (∀ (X : Iota), Iff (icext a X) (icext a_1 X)))) % 9.07/9.25 True % 9.07/9.25 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.25 (Eq (And (And (ic a) (ic a_1)) (∀ (X : Iota), Iff (icext a X) (icext a_1 X))) False) % 9.07/9.25 Clause #90 (by clausification #[88]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.25 (Or (Eq (And (ic a) (ic a_1)) False) (Eq (∀ (X : Iota), Iff (icext a X) (icext a_1 X)) False)) % 9.07/9.25 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), % 9.07/9.25 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.25 (Or (Eq (∀ (X : Iota), Iff (icext a X) (icext a_1 X)) False) (Or (Eq (ic a) False) (Eq (ic a_1) False))) % 9.07/9.25 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 9.07/9.25 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.25 (Or (Eq (ic a) False) % 9.07/9.25 (Or (Eq (ic a_1) False) (Eq (Not (Iff (icext a (skS.0 1 a a_1 a_2)) (icext a_1 (skS.0 1 a a_1 a_2)))) True))) % 9.07/9.25 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 9.07/9.25 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.25 (Or (Eq (ic a) False) % 9.07/9.25 (Or (Eq (ic a_1) False) (Eq (Iff (icext a (skS.0 1 a a_1 a_2)) (icext a_1 (skS.0 1 a a_1 a_2))) False))) % 9.07/9.26 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 9.07/9.26 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.26 (Or (Eq (ic a) False) % 9.07/9.26 (Or (Eq (ic a_1) False) (Or (Eq (icext a (skS.0 1 a a_1 a_2)) False) (Eq (icext a_1 (skS.0 1 a a_1 a_2)) False)))) % 9.07/9.26 Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 9.07/9.26 Or (Eq (iext uri_owl_equivalentClass a a_1) True) % 9.07/9.26 (Or (Eq (ic a) False) % 9.07/9.26 (Or (Eq (ic a_1) False) (Or (Eq (icext a (skS.0 1 a a_1 a_2)) True) (Eq (icext a_1 (skS.0 1 a a_1 a_2)) True)))) % 9.07/9.26 Clause #99 (by superposition #[94, 3]): ∀ (a a_1 : Iota), % 9.07/9.26 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class a) True) % 9.07/9.26 (Or (Eq (ic a) False) % 9.07/9.26 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class a a_1)) False) % 9.07/9.26 (Or (Eq (icext a (skS.0 1 uri_owl_Class a a_1)) False) (Eq False True)))) % 9.07/9.26 Clause #111 (by clausification #[13]): Eq % 9.07/9.26 (And % 9.07/9.26 (And % 9.07/9.26 (And (And (iext uri_rdf_type uri_owl_Class uri_owl_Thing) (iext uri_rdf_type uri_owl_Class uri_owl_Class)) % 9.07/9.26 (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing)) % 9.07/9.26 (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class)) % 9.07/9.26 (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class)) % 9.07/9.26 False % 9.07/9.26 Clause #112 (by clausification #[111]): Or % 9.07/9.26 (Eq % 9.07/9.26 (And % 9.07/9.26 (And (And (iext uri_rdf_type uri_owl_Class uri_owl_Thing) (iext uri_rdf_type uri_owl_Class uri_owl_Class)) % 9.07/9.26 (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing)) % 9.07/9.26 (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class)) % 9.07/9.26 False) % 9.07/9.26 (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 Clause #113 (by clausification #[112]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or % 9.07/9.26 (Eq % 9.07/9.26 (And (And (iext uri_rdf_type uri_owl_Class uri_owl_Thing) (iext uri_rdf_type uri_owl_Class uri_owl_Class)) % 9.07/9.26 (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing)) % 9.07/9.26 False) % 9.07/9.26 (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False)) % 9.07/9.26 Clause #114 (by clausification #[113]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.26 (Or (Eq (And (iext uri_rdf_type uri_owl_Class uri_owl_Thing) (iext uri_rdf_type uri_owl_Class uri_owl_Class)) False) % 9.07/9.26 (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False))) % 9.07/9.26 Clause #115 (by clausification #[114]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.26 (Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False) % 9.07/9.26 (Or (Eq (iext uri_rdf_type uri_owl_Class uri_owl_Thing) False) % 9.07/9.26 (Eq (iext uri_rdf_type uri_owl_Class uri_owl_Class) False)))) % 9.07/9.26 Clause #116 (by forward demodulation #[115, 65]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.26 (Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False) % 9.07/9.26 (Or (Eq True False) (Eq (iext uri_rdf_type uri_owl_Class uri_owl_Class) False)))) % 9.07/9.26 Clause #117 (by clausification #[116]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.26 (Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False) % 9.07/9.26 (Eq (iext uri_rdf_type uri_owl_Class uri_owl_Class) False))) % 9.07/9.26 Clause #118 (by forward demodulation #[117, 82]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.26 (Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False) (Eq True False))) % 9.07/9.26 Clause #119 (by clausification #[118]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) False) % 9.07/9.26 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.26 (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False)) % 9.07/9.26 Clause #120 (by clausification #[70]): ∀ (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) % 9.07/9.28 Clause #122 (by clausification #[120]): ∀ (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) % 9.07/9.28 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf a a_1) False) (Or (Eq (icext a a_2) False) (Eq (icext a_1 a_2) True)) % 9.07/9.28 Clause #132 (by superposition #[76, 7]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype a) True) % 9.07/9.28 (Or (Eq (ic a) False) (Or (Eq (icext a (skS.0 0 uri_rdfs_Datatype a a_1)) False) (Eq False True))) % 9.07/9.28 Clause #133 (by superposition #[76, 5]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class a) True) % 9.07/9.28 (Or (Eq (ic a) False) (Or (Eq (icext a (skS.0 0 uri_rdfs_Class a a_1)) False) (Eq False True))) % 9.07/9.28 Clause #134 (by superposition #[76, 3]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class a) True) % 9.07/9.28 (Or (Eq (ic a) False) (Or (Eq (icext a (skS.0 0 uri_owl_Class a a_1)) False) (Eq False True))) % 9.07/9.28 Clause #138 (by clausification #[133]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class a) True) % 9.07/9.28 (Or (Eq (ic a) False) (Eq (icext a (skS.0 0 uri_rdfs_Class a a_1)) False)) % 9.07/9.28 Clause #142 (by superposition #[138, 3]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.28 (Or (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Class uri_owl_Class a)) False) (Eq False True)) % 9.07/9.28 Clause #143 (by clausification #[78]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype a) True) % 9.07/9.28 (Or (Eq (ic a) False) (Eq (icext uri_rdfs_Datatype (skS.0 0 uri_rdfs_Datatype a a_1)) True)) % 9.07/9.28 Clause #147 (by superposition #[143, 3]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Or (Eq (icext uri_rdfs_Datatype (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True) (Eq False True)) % 9.07/9.28 Clause #148 (by clausification #[147]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Eq (icext uri_rdfs_Datatype (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True) % 9.07/9.28 Clause #149 (by superposition #[148, 53]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Or (Eq True False) (Eq (idc (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True)) % 9.07/9.28 Clause #151 (by clausification #[149]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Eq (idc (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True) % 9.07/9.28 Clause #152 (by superposition #[151, 20]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Or (Eq True False) (Eq (ic (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True)) % 9.07/9.28 Clause #154 (by clausification #[152]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Eq (ic (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True) % 9.07/9.28 Clause #155 (by superposition #[154, 22]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.28 (Or (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True) (Eq True False)) % 9.07/9.28 Clause #168 (by clausification #[79]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class a) True) % 9.07/9.28 (Or (Eq (ic a) False) (Eq (icext uri_rdfs_Class (skS.0 0 uri_rdfs_Class a a_1)) True)) % 9.07/9.28 Clause #172 (by superposition #[168, 3]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.28 (Or (Eq (icext uri_rdfs_Class (skS.0 0 uri_rdfs_Class uri_owl_Class a)) True) (Eq False True)) % 9.07/9.28 Clause #225 (by superposition #[95, 3]): ∀ (a a_1 : Iota), % 9.07/9.28 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class a) True) % 9.07/9.28 (Or (Eq (ic a) False) % 9.07/9.28 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class a a_1)) True) % 9.07/9.28 (Or (Eq (icext a (skS.0 1 uri_owl_Class a a_1)) True) (Eq False True)))) % 9.07/9.28 Clause #296 (by clausification #[142]): ∀ (a : Iota), % 9.07/9.28 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.30 (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Class uri_owl_Class a)) False) % 9.07/9.30 Clause #313 (by clausification #[155]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.30 (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) True) % 9.07/9.30 Clause #315 (by clausification #[99]): ∀ (a a_1 : Iota), % 9.07/9.30 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class a) True) % 9.07/9.30 (Or (Eq (ic a) False) % 9.07/9.30 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class a a_1)) False) % 9.07/9.30 (Eq (icext a (skS.0 1 uri_owl_Class a a_1)) False))) % 9.07/9.30 Clause #318 (by superposition #[315, 5]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) True) % 9.07/9.30 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) % 9.07/9.30 (Or (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) (Eq False True))) % 9.07/9.30 Clause #368 (by clausification #[132]): ∀ (a a_1 : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype a) True) % 9.07/9.30 (Or (Eq (ic a) False) (Eq (icext a (skS.0 0 uri_rdfs_Datatype a a_1)) False)) % 9.07/9.30 Clause #372 (by superposition #[368, 3]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.30 (Or (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) False) (Eq False True)) % 9.07/9.30 Clause #391 (by clausification #[134]): ∀ (a a_1 : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class a) True) % 9.07/9.30 (Or (Eq (ic a) False) (Eq (icext a (skS.0 0 uri_owl_Class a a_1)) False)) % 9.07/9.30 Clause #392 (by superposition #[391, 9]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) True) % 9.07/9.30 (Or (Eq (icext uri_owl_Thing (skS.0 0 uri_owl_Class uri_owl_Thing a)) False) (Eq False True)) % 9.07/9.30 Clause #456 (by clausification #[372]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.30 (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Datatype uri_owl_Class a)) False) % 9.07/9.30 Clause #457 (by superposition #[456, 313]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.30 (Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) (Eq False True)) % 9.07/9.30 Clause #458 (by clausification #[457]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.30 (Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True) % 9.07/9.30 Clause #459 (by eliminate duplicate literals #[458]): Eq (iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_owl_Class) True % 9.07/9.30 Clause #460 (by backward demodulation #[459, 119]): Or (Eq True False) % 9.07/9.30 (Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.30 (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False)) % 9.07/9.30 Clause #476 (by clausification #[460]): Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) % 9.07/9.30 (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) False) % 9.07/9.30 Clause #484 (by clausification #[392]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) True) % 9.07/9.30 (Eq (icext uri_owl_Thing (skS.0 0 uri_owl_Class uri_owl_Thing a)) False) % 9.07/9.30 Clause #485 (by superposition #[484, 62]): Or (Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) True) (Eq False True) % 9.07/9.30 Clause #486 (by clausification #[485]): Eq (iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Thing) True % 9.07/9.30 Clause #490 (by backward demodulation #[486, 476]): Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False) (Eq True False) % 9.07/9.30 Clause #493 (by clausification #[490]): Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) False % 9.07/9.30 Clause #505 (by clausification #[172]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.30 (Eq (icext uri_rdfs_Class (skS.0 0 uri_rdfs_Class uri_owl_Class a)) True) % 9.07/9.30 Clause #506 (by superposition #[505, 36]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.30 (Or (Eq True False) (Eq (ic (skS.0 0 uri_rdfs_Class uri_owl_Class a)) True)) % 9.07/9.30 Clause #508 (by clausification #[506]): ∀ (a : Iota), % 9.07/9.30 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.32 (Eq (ic (skS.0 0 uri_rdfs_Class uri_owl_Class a)) True) % 9.07/9.32 Clause #509 (by superposition #[508, 22]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Class uri_owl_Class a)) True) (Eq True False)) % 9.07/9.32 Clause #530 (by clausification #[509]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.32 (Eq (icext uri_owl_Class (skS.0 0 uri_rdfs_Class uri_owl_Class a)) True) % 9.07/9.32 Clause #531 (by superposition #[530, 296]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.32 (Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) (Eq True False)) % 9.07/9.32 Clause #533 (by clausification #[531]): Or (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.32 (Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True) % 9.07/9.32 Clause #534 (by eliminate duplicate literals #[533]): Eq (iext uri_rdfs_subClassOf uri_rdfs_Class uri_owl_Class) True % 9.07/9.32 Clause #539 (by superposition #[534, 123]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (icext uri_rdfs_Class a) False) (Eq (icext uri_owl_Class a) True)) % 9.07/9.32 Clause #540 (by clausification #[539]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Class a) False) (Eq (icext uri_owl_Class a) True) % 9.07/9.32 Clause #684 (by clausification #[318]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) True) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) % 9.07/9.32 (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False)) % 9.07/9.32 Clause #685 (by forward demodulation #[684, 493]): ∀ (a : Iota), % 9.07/9.32 Or (Eq False True) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) % 9.07/9.32 (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False)) % 9.07/9.32 Clause #686 (by clausification #[685]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) % 9.07/9.32 (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) % 9.07/9.32 Clause #922 (by clausification #[225]): ∀ (a a_1 : Iota), % 9.07/9.32 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class a) True) % 9.07/9.32 (Or (Eq (ic a) False) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class a a_1)) True) % 9.07/9.32 (Eq (icext a (skS.0 1 uri_owl_Class a a_1)) True))) % 9.07/9.32 Clause #925 (by superposition #[922, 5]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) True) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Or (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) (Eq False True))) % 9.07/9.32 Clause #1031 (by clausification #[925]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (iext uri_owl_equivalentClass uri_owl_Class uri_rdfs_Class) True) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True)) % 9.07/9.32 Clause #1032 (by forward demodulation #[1031, 493]): ∀ (a : Iota), % 9.07/9.32 Or (Eq False True) % 9.07/9.32 (Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True)) % 9.07/9.32 Clause #1033 (by clausification #[1032]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 Clause #1034 (by superposition #[1033, 36]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Or (Eq True False) (Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True)) % 9.07/9.32 Clause #1037 (by clausification #[1034]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 Clause #1039 (by superposition #[1037, 23]): ∀ (a : Iota), % 9.07/9.32 Or (Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.32 (Or (Eq True False) (Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True)) % 9.07/9.32 Clause #1042 (by clausification #[1039]): ∀ (a : Iota), % 9.07/9.33 Or (Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) (Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.33 Clause #1043 (by eliminate duplicate literals #[1042]): ∀ (a : Iota), Eq (ic (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True % 9.07/9.33 Clause #1046 (by superposition #[1043, 35]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) (Eq True False) % 9.07/9.33 Clause #1065 (by clausification #[1046]): ∀ (a : Iota), Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True % 9.07/9.33 Clause #1067 (by superposition #[1065, 540]): ∀ (a : Iota), Or (Eq True False) (Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True) % 9.07/9.33 Clause #1073 (by clausification #[1067]): ∀ (a : Iota), Eq (icext uri_owl_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) True % 9.07/9.33 Clause #1074 (by backward demodulation #[1073, 686]): ∀ (a : Iota), Or (Eq True False) (Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False) % 9.07/9.33 Clause #1077 (by clausification #[1074]): ∀ (a : Iota), Eq (icext uri_rdfs_Class (skS.0 1 uri_owl_Class uri_rdfs_Class a)) False % 9.07/9.33 Clause #1078 (by superposition #[1077, 1065]): Eq False True % 9.07/9.33 Clause #1079 (by clausification #[1078]): False % 9.07/9.33 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------