%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB005+2 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:03:21 PM UTC 2025 % Result : Theorem 3.65s 3.85s % Output : Proof 3.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWB005+2 : TPTP v9.2.0. Released v5.2.0. % 0.06/0.13 % Command : duper %s % 0.12/0.34 % Computer : n021.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:47:38 EDT 2025 % 0.12/0.34 % CPUTime : % 3.65/3.85 SZS status Theorem for theBenchmark.p % 3.65/3.85 SZS output start Proof for theBenchmark.p % 3.65/3.85 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), ir X) True % 3.65/3.85 Clause #1 (by assumption #[]): Eq (∀ (S P O : Iota), iext P S O → ip P) True % 3.65/3.85 Clause #2 (by assumption #[]): Eq (∀ (P : Iota), Iff (iext uri_rdf_type P uri_rdf_Property) (ip P)) True % 3.65/3.85 Clause #3 (by assumption #[]): Eq (∀ (X C : Iota), Iff (iext uri_rdf_type X C) (icext C X)) True % 3.65/3.85 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), Iff (ir X) (icext uri_rdfs_Resource X)) True % 3.65/3.85 Clause #5 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_owl_Thing X) (ir X)) True % 3.65/3.85 Clause #6 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_owl_ObjectProperty X) (ip X)) True % 3.65/3.85 Clause #7 (by assumption #[]): Eq % 3.65/3.85 (Not % 3.65/3.85 (And % 3.65/3.85 (And % 3.65/3.85 (And % 3.65/3.85 (And % 3.65/3.85 (And % 3.65/3.85 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.85 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.85 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 3.65/3.85 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 3.65/3.85 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 3.65/3.85 (iext uri_rdf_type uri_ex_o uri_rdfs_Resource)) % 3.65/3.85 (iext uri_rdf_type uri_ex_o uri_owl_Thing))) % 3.65/3.85 True % 3.65/3.85 Clause #8 (by assumption #[]): Eq (iext uri_ex_p uri_ex_s uri_ex_o) True % 3.65/3.85 Clause #9 (by clausification #[0]): ∀ (a : Iota), Eq (ir a) True % 3.65/3.85 Clause #10 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (P O : Iota), iext P a O → ip P) True % 3.65/3.85 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (∀ (O : Iota), iext a a_1 O → ip a) True % 3.65/3.85 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), Eq (iext a a_1 a_2 → ip a) True % 3.65/3.85 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 : Iota), Or (Eq (iext a a_1 a_2) False) (Eq (ip a) True) % 3.65/3.85 Clause #14 (by superposition #[13, 8]): Or (Eq (ip uri_ex_p) True) (Eq False True) % 3.65/3.85 Clause #15 (by clausification #[14]): Eq (ip uri_ex_p) True % 3.65/3.85 Clause #16 (by clausification #[6]): ∀ (a : Iota), Eq (Iff (icext uri_owl_ObjectProperty a) (ip a)) True % 3.65/3.85 Clause #17 (by clausification #[16]): ∀ (a : Iota), Or (Eq (icext uri_owl_ObjectProperty a) True) (Eq (ip a) False) % 3.65/3.85 Clause #19 (by superposition #[17, 15]): Or (Eq (icext uri_owl_ObjectProperty uri_ex_p) True) (Eq False True) % 3.65/3.85 Clause #20 (by clausification #[2]): ∀ (a : Iota), Eq (Iff (iext uri_rdf_type a uri_rdf_Property) (ip a)) True % 3.65/3.85 Clause #21 (by clausification #[20]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_rdf_Property) True) (Eq (ip a) False) % 3.65/3.85 Clause #23 (by superposition #[21, 15]): Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) True) (Eq False True) % 3.65/3.85 Clause #24 (by clausification #[19]): Eq (icext uri_owl_ObjectProperty uri_ex_p) True % 3.65/3.85 Clause #26 (by clausification #[23]): Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) True % 3.65/3.85 Clause #31 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (iext uri_rdf_type a C) (icext C a)) True % 3.65/3.85 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_rdf_type a a_1) (icext a_1 a)) True % 3.65/3.85 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Or (Eq (iext uri_rdf_type a a_1) True) (Eq (icext a_1 a) False) % 3.65/3.85 Clause #35 (by superposition #[33, 24]): Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) True) (Eq False True) % 3.65/3.85 Clause #39 (by clausification #[35]): Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) True % 3.65/3.85 Clause #41 (by clausification #[5]): ∀ (a : Iota), Eq (Iff (icext uri_owl_Thing a) (ir a)) True % 3.65/3.85 Clause #42 (by clausification #[41]): ∀ (a : Iota), Or (Eq (icext uri_owl_Thing a) True) (Eq (ir a) False) % 3.65/3.85 Clause #44 (by forward demodulation #[42, 9]): ∀ (a : Iota), Or (Eq (icext uri_owl_Thing a) True) (Eq True False) % 3.65/3.85 Clause #45 (by clausification #[44]): ∀ (a : Iota), Eq (icext uri_owl_Thing a) True % 3.65/3.85 Clause #46 (by superposition #[45, 33]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_owl_Thing) True) (Eq True False) % 3.65/3.85 Clause #47 (by clausification #[4]): ∀ (a : Iota), Eq (Iff (ir a) (icext uri_rdfs_Resource a)) True % 3.65/3.85 Clause #49 (by clausification #[47]): ∀ (a : Iota), Or (Eq (ir a) False) (Eq (icext uri_rdfs_Resource a) True) % 3.65/3.86 Clause #51 (by forward demodulation #[49, 9]): ∀ (a : Iota), Or (Eq True False) (Eq (icext uri_rdfs_Resource a) True) % 3.65/3.86 Clause #52 (by clausification #[51]): ∀ (a : Iota), Eq (icext uri_rdfs_Resource a) True % 3.65/3.86 Clause #53 (by superposition #[52, 33]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_rdfs_Resource) True) (Eq True False) % 3.65/3.86 Clause #54 (by clausification #[53]): ∀ (a : Iota), Eq (iext uri_rdf_type a uri_rdfs_Resource) True % 3.65/3.86 Clause #55 (by clausification #[46]): ∀ (a : Iota), Eq (iext uri_rdf_type a uri_owl_Thing) True % 3.65/3.86 Clause #57 (by clausification #[7]): Eq % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 3.65/3.86 (iext uri_rdf_type uri_ex_o uri_rdfs_Resource)) % 3.65/3.86 (iext uri_rdf_type uri_ex_o uri_owl_Thing)) % 3.65/3.86 False % 3.65/3.86 Clause #58 (by clausification #[57]): Or % 3.65/3.86 (Eq % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 3.65/3.86 (iext uri_rdf_type uri_ex_o uri_rdfs_Resource)) % 3.65/3.86 False) % 3.65/3.86 (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.86 Clause #59 (by clausification #[58]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.86 (Or % 3.65/3.86 (Eq % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 3.65/3.86 False) % 3.65/3.86 (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False)) % 3.65/3.86 Clause #60 (by clausification #[59]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.86 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 3.65/3.86 (Or % 3.65/3.86 (Eq % 3.65/3.86 (And % 3.65/3.86 (And % 3.65/3.86 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 3.65/3.86 False) % 3.65/3.86 (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False))) % 3.65/3.86 Clause #61 (by clausification #[60]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.86 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 3.65/3.86 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 3.65/3.86 (Or % 3.65/3.86 (Eq % 3.65/3.86 (And % 3.65/3.86 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 3.65/3.86 False) % 3.65/3.86 (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False)))) % 3.65/3.86 Clause #62 (by clausification #[61]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.86 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 3.65/3.86 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 3.65/3.86 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.86 (Or % 3.65/3.86 (Eq % 3.65/3.86 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 3.65/3.86 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 3.65/3.86 False) % 3.65/3.86 (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False))))) % 3.65/3.86 Clause #63 (by clausification #[62]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False)))))) % 3.65/3.88 Clause #64 (by clausification #[63]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))))) % 3.65/3.88 Clause #65 (by forward demodulation #[64, 54]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq True False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))))) % 3.65/3.88 Clause #66 (by clausification #[65]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))))) % 3.65/3.88 Clause #67 (by forward demodulation #[66, 39]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq True False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))))) % 3.65/3.88 Clause #68 (by clausification #[67]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))) % 3.65/3.88 Clause #69 (by forward demodulation #[68, 26]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq True False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))) % 3.65/3.88 Clause #70 (by clausification #[69]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))) % 3.65/3.88 Clause #71 (by forward demodulation #[70, 55]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq True False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))) % 3.65/3.88 Clause #72 (by clausification #[71]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))) % 3.65/3.88 Clause #73 (by forward demodulation #[72, 54]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq True False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 3.65/3.88 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))) % 3.65/3.88 Clause #74 (by clausification #[73]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)) % 3.65/3.88 Clause #75 (by forward demodulation #[74, 54]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 3.65/3.88 (Or (Eq True False) (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)) % 3.65/3.88 Clause #76 (by clausification #[75]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False) % 3.65/3.88 Clause #77 (by forward demodulation #[76, 55]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) (Eq True False) % 3.65/3.88 Clause #78 (by clausification #[77]): Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False % 3.65/3.88 Clause #79 (by superposition #[78, 55]): Eq False True % 3.65/3.88 Clause #80 (by clausification #[79]): False % 3.65/3.88 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------