%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB023+2 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:03:27 PM UTC 2025 % Result : Theorem 3.92s 4.13s % Output : Proof 3.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWB023+2 : TPTP v9.2.0. Released v5.2.0. % 0.10/0.13 % Command : duper %s % 0.12/0.34 % Computer : n012.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:56:53 EDT 2025 % 0.12/0.34 % CPUTime : % 3.92/4.13 SZS status Theorem for theBenchmark.p % 3.92/4.13 SZS output start Proof for theBenchmark.p % 3.92/4.13 Clause #0 (by assumption #[]): Eq (∀ (X C : Iota), Iff (iext uri_rdf_type X C) (icext C X)) True % 3.92/4.13 Clause #1 (by assumption #[]): Eq % 3.92/4.13 (∀ (Z S1 A1 : Iota), % 3.92/4.13 And (iext uri_rdf_first S1 A1) (iext uri_rdf_rest S1 uri_rdf_nil) → % 3.92/4.13 Iff (iext uri_owl_oneOf Z S1) (And (ic Z) (∀ (X : Iota), Iff (icext Z X) (Eq X A1)))) % 3.92/4.13 True % 3.92/4.13 Clause #3 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (iext uri_owl_sameAs X Y) (Eq X Y)) True % 3.92/4.13 Clause #4 (by assumption #[]): Eq (Not (And (iext uri_owl_sameAs uri_ex_w uri_ex_u) (iext uri_owl_sameAs uri_ex_w uri_ex_v))) True % 3.92/4.13 Clause #5 (by assumption #[]): Eq % 3.92/4.13 (Exists fun BNODE_o => % 3.92/4.13 Exists fun BNODE_l => % 3.92/4.13 And % 3.92/4.13 (And % 3.92/4.13 (And % 3.92/4.13 (And % 3.92/4.13 (And % 3.92/4.13 (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) (iext uri_rdf_type uri_ex_w BNODE_o)) % 3.92/4.13 (iext uri_rdf_type BNODE_o uri_owl_Class)) % 3.92/4.13 (iext uri_owl_oneOf BNODE_o BNODE_l)) % 3.92/4.13 (iext uri_rdf_first BNODE_l uri_ex_u)) % 3.92/4.13 (iext uri_rdf_first BNODE_l uri_ex_v)) % 3.92/4.13 (iext uri_rdf_rest BNODE_l uri_rdf_nil)) % 3.92/4.13 True % 3.92/4.13 Clause #6 (by clausification #[4]): Eq (And (iext uri_owl_sameAs uri_ex_w uri_ex_u) (iext uri_owl_sameAs uri_ex_w uri_ex_v)) False % 3.92/4.13 Clause #7 (by clausification #[6]): Or (Eq (iext uri_owl_sameAs uri_ex_w uri_ex_u) False) (Eq (iext uri_owl_sameAs uri_ex_w uri_ex_v) False) % 3.92/4.13 Clause #8 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (iext uri_rdf_type a C) (icext C a)) True % 3.92/4.13 Clause #9 (by clausification #[8]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_rdf_type a a_1) (icext a_1 a)) True % 3.92/4.13 Clause #11 (by clausification #[9]): ∀ (a a_1 : Iota), Or (Eq (iext uri_rdf_type a a_1) False) (Eq (icext a_1 a) True) % 3.92/4.13 Clause #12 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (iext uri_owl_sameAs a Y) (Eq a Y)) True % 3.92/4.13 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_owl_sameAs a a_1) (Eq a a_1)) True % 3.92/4.13 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Or (Eq (iext uri_owl_sameAs a a_1) True) (Eq (Eq a a_1) False) % 3.92/4.13 Clause #16 (by clausification #[14]): ∀ (a a_1 : Iota), Or (Eq (iext uri_owl_sameAs a a_1) True) (Ne a a_1) % 3.92/4.13 Clause #17 (by destructive equality resolution #[16]): ∀ (a : Iota), Eq (iext uri_owl_sameAs a a) True % 3.92/4.13 Clause #20 (by clausification #[1]): ∀ (a : Iota), % 3.92/4.13 Eq % 3.92/4.13 (∀ (S1 A1 : Iota), % 3.92/4.13 And (iext uri_rdf_first S1 A1) (iext uri_rdf_rest S1 uri_rdf_nil) → % 3.92/4.13 Iff (iext uri_owl_oneOf a S1) (And (ic a) (∀ (X : Iota), Iff (icext a X) (Eq X A1)))) % 3.92/4.13 True % 3.92/4.13 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), % 3.92/4.13 Eq % 3.92/4.13 (∀ (A1 : Iota), % 3.92/4.13 And (iext uri_rdf_first a A1) (iext uri_rdf_rest a uri_rdf_nil) → % 3.92/4.13 Iff (iext uri_owl_oneOf a_1 a) (And (ic a_1) (∀ (X : Iota), Iff (icext a_1 X) (Eq X A1)))) % 3.92/4.13 True % 3.92/4.13 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 3.92/4.13 Eq % 3.92/4.13 (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a uri_rdf_nil) → % 3.92/4.13 Iff (iext uri_owl_oneOf a_2 a) (And (ic a_2) (∀ (X : Iota), Iff (icext a_2 X) (Eq X a_1)))) % 3.92/4.13 True % 3.92/4.13 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), % 3.92/4.13 Or (Eq (And (iext uri_rdf_first a a_1) (iext uri_rdf_rest a uri_rdf_nil)) False) % 3.92/4.13 (Eq (Iff (iext uri_owl_oneOf a_2 a) (And (ic a_2) (∀ (X : Iota), Iff (icext a_2 X) (Eq X a_1)))) True) % 3.92/4.13 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 3.92/4.13 Or (Eq (Iff (iext uri_owl_oneOf a a_1) (And (ic a) (∀ (X : Iota), Iff (icext a X) (Eq X a_2)))) True) % 3.92/4.13 (Or (Eq (iext uri_rdf_first a_1 a_2) False) (Eq (iext uri_rdf_rest a_1 uri_rdf_nil) False)) % 3.92/4.13 Clause #26 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 3.92/4.13 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.13 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.13 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Eq (And (ic a_2) (∀ (X : Iota), Iff (icext a_2 X) (Eq X a_1))) True))) % 3.92/4.13 Clause #56 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 3.92/4.13 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.13 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Eq (∀ (X : Iota), Iff (icext a_2 X) (Eq X a_1)) True))) % 3.92/4.15 Clause #58 (by clausification #[56]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.15 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Eq (Iff (icext a_2 a_3) (Eq a_3 a_1)) True))) % 3.92/4.15 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.15 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Or (Eq (icext a_2 a_3) True) (Eq (Eq a_3 a_1) False)))) % 3.92/4.15 Clause #60 (by clausification #[58]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.15 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Or (Eq (icext a_2 a_3) False) (Eq (Eq a_3 a_1) True)))) % 3.92/4.15 Clause #61 (by clausification #[59]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.15 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Or (Eq (icext a_2 a_3) True) (Ne a_3 a_1)))) % 3.92/4.15 Clause #62 (by destructive equality resolution #[61]): ∀ (a a_1 a_2 : Iota), % 3.92/4.15 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Eq (icext a_2 a_1) True))) % 3.92/4.15 Clause #63 (by clausification #[5]): ∀ (a : Iota), % 3.92/4.15 Eq % 3.92/4.15 (Exists fun BNODE_l => % 3.92/4.15 And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) % 3.92/4.15 (iext uri_rdf_type uri_ex_w (skS.0 4 a))) % 3.92/4.15 (iext uri_rdf_type (skS.0 4 a) uri_owl_Class)) % 3.92/4.15 (iext uri_owl_oneOf (skS.0 4 a) BNODE_l)) % 3.92/4.15 (iext uri_rdf_first BNODE_l uri_ex_u)) % 3.92/4.15 (iext uri_rdf_first BNODE_l uri_ex_v)) % 3.92/4.15 (iext uri_rdf_rest BNODE_l uri_rdf_nil)) % 3.92/4.15 True % 3.92/4.15 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 3.92/4.15 Eq % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) % 3.92/4.15 (iext uri_rdf_type uri_ex_w (skS.0 4 a))) % 3.92/4.15 (iext uri_rdf_type (skS.0 4 a) uri_owl_Class)) % 3.92/4.15 (iext uri_owl_oneOf (skS.0 4 a) (skS.0 5 a a_1))) % 3.92/4.15 (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_u)) % 3.92/4.15 (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_v)) % 3.92/4.15 (iext uri_rdf_rest (skS.0 5 a a_1) uri_rdf_nil)) % 3.92/4.15 True % 3.92/4.15 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_rest (skS.0 5 a a_1) uri_rdf_nil) True % 3.92/4.15 Clause #66 (by clausification #[64]): ∀ (a a_1 : Iota), % 3.92/4.15 Eq % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) (iext uri_rdf_type uri_ex_w (skS.0 4 a))) % 3.92/4.15 (iext uri_rdf_type (skS.0 4 a) uri_owl_Class)) % 3.92/4.15 (iext uri_owl_oneOf (skS.0 4 a) (skS.0 5 a a_1))) % 3.92/4.15 (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_u)) % 3.92/4.15 (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_v)) % 3.92/4.15 True % 3.92/4.15 Clause #67 (by clausification #[60]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.15 Or (Eq (iext uri_rdf_first a a_1) False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest a uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 a) False) (Or (Eq (icext a_2 a_3) False) (Eq a_3 a_1)))) % 3.92/4.15 Clause #70 (by clausification #[66]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_v) True % 3.92/4.15 Clause #71 (by clausification #[66]): ∀ (a a_1 : Iota), % 3.92/4.15 Eq % 3.92/4.15 (And % 3.92/4.15 (And % 3.92/4.15 (And (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) (iext uri_rdf_type uri_ex_w (skS.0 4 a))) % 3.92/4.15 (iext uri_rdf_type (skS.0 4 a) uri_owl_Class)) % 3.92/4.15 (iext uri_owl_oneOf (skS.0 4 a) (skS.0 5 a a_1))) % 3.92/4.15 (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_u)) % 3.92/4.15 True % 3.92/4.15 Clause #73 (by superposition #[70, 62]): ∀ (a a_1 a_2 : Iota), % 3.92/4.15 Or (Eq True False) % 3.92/4.15 (Or (Eq (iext uri_rdf_rest (skS.0 5 a a_1) uri_rdf_nil) False) % 3.92/4.15 (Or (Eq (iext uri_owl_oneOf a_2 (skS.0 5 a a_1)) False) (Eq (icext a_2 uri_ex_v) True))) % 3.92/4.17 Clause #80 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), % 3.92/4.17 Or (Eq (iext uri_rdf_rest (skS.0 5 a a_1) uri_rdf_nil) False) % 3.92/4.17 (Or (Eq (iext uri_owl_oneOf a_2 (skS.0 5 a a_1)) False) (Eq (icext a_2 uri_ex_v) True)) % 3.92/4.17 Clause #81 (by forward demodulation #[80, 65]): ∀ (a a_1 a_2 : Iota), % 3.92/4.17 Or (Eq True False) (Or (Eq (iext uri_owl_oneOf a (skS.0 5 a_1 a_2)) False) (Eq (icext a uri_ex_v) True)) % 3.92/4.17 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), Or (Eq (iext uri_owl_oneOf a (skS.0 5 a_1 a_2)) False) (Eq (icext a uri_ex_v) True) % 3.92/4.17 Clause #92 (by clausification #[71]): ∀ (a a_1 : Iota), Eq (iext uri_rdf_first (skS.0 5 a a_1) uri_ex_u) True % 3.92/4.17 Clause #93 (by clausification #[71]): ∀ (a a_1 : Iota), % 3.92/4.17 Eq % 3.92/4.17 (And % 3.92/4.17 (And (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) (iext uri_rdf_type uri_ex_w (skS.0 4 a))) % 3.92/4.17 (iext uri_rdf_type (skS.0 4 a) uri_owl_Class)) % 3.92/4.17 (iext uri_owl_oneOf (skS.0 4 a) (skS.0 5 a a_1))) % 3.92/4.17 True % 3.92/4.17 Clause #96 (by superposition #[92, 67]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.17 Or (Eq True False) % 3.92/4.17 (Or (Eq (iext uri_rdf_rest (skS.0 5 a a_1) uri_rdf_nil) False) % 3.92/4.17 (Or (Eq (iext uri_owl_oneOf a_2 (skS.0 5 a a_1)) False) (Or (Eq (icext a_2 a_3) False) (Eq a_3 uri_ex_u)))) % 3.92/4.17 Clause #101 (by clausification #[96]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.17 Or (Eq (iext uri_rdf_rest (skS.0 5 a a_1) uri_rdf_nil) False) % 3.92/4.17 (Or (Eq (iext uri_owl_oneOf a_2 (skS.0 5 a a_1)) False) (Or (Eq (icext a_2 a_3) False) (Eq a_3 uri_ex_u))) % 3.92/4.17 Clause #102 (by forward demodulation #[101, 65]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.17 Or (Eq True False) % 3.92/4.17 (Or (Eq (iext uri_owl_oneOf a (skS.0 5 a_1 a_2)) False) (Or (Eq (icext a a_3) False) (Eq a_3 uri_ex_u))) % 3.92/4.17 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 3.92/4.17 Or (Eq (iext uri_owl_oneOf a (skS.0 5 a_1 a_2)) False) (Or (Eq (icext a a_3) False) (Eq a_3 uri_ex_u)) % 3.92/4.17 Clause #104 (by clausification #[93]): ∀ (a a_1 : Iota), Eq (iext uri_owl_oneOf (skS.0 4 a) (skS.0 5 a a_1)) True % 3.92/4.17 Clause #105 (by clausification #[93]): ∀ (a : Iota), % 3.92/4.17 Eq % 3.92/4.17 (And (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) (iext uri_rdf_type uri_ex_w (skS.0 4 a))) % 3.92/4.17 (iext uri_rdf_type (skS.0 4 a) uri_owl_Class)) % 3.92/4.17 True % 3.92/4.17 Clause #107 (by superposition #[104, 82]): ∀ (a : Iota), Or (Eq True False) (Eq (icext (skS.0 4 a) uri_ex_v) True) % 3.92/4.17 Clause #110 (by superposition #[104, 103]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (icext (skS.0 4 a) a_1) False) (Eq a_1 uri_ex_u)) % 3.92/4.17 Clause #120 (by clausification #[107]): ∀ (a : Iota), Eq (icext (skS.0 4 a) uri_ex_v) True % 3.92/4.17 Clause #124 (by clausification #[110]): ∀ (a a_1 : Iota), Or (Eq (icext (skS.0 4 a) a_1) False) (Eq a_1 uri_ex_u) % 3.92/4.17 Clause #126 (by superposition #[124, 120]): Or (Eq uri_ex_v uri_ex_u) (Eq False True) % 3.92/4.17 Clause #127 (by clausification #[126]): Eq uri_ex_v uri_ex_u % 3.92/4.17 Clause #128 (by backward demodulation #[127, 7]): Or (Eq (iext uri_owl_sameAs uri_ex_w uri_ex_v) False) (Eq (iext uri_owl_sameAs uri_ex_w uri_ex_v) False) % 3.92/4.17 Clause #130 (by backward demodulation #[127, 124]): ∀ (a a_1 : Iota), Or (Eq (icext (skS.0 4 a) a_1) False) (Eq a_1 uri_ex_v) % 3.92/4.17 Clause #137 (by eliminate duplicate literals #[128]): Eq (iext uri_owl_sameAs uri_ex_w uri_ex_v) False % 3.92/4.17 Clause #141 (by clausification #[105]): ∀ (a : Iota), % 3.92/4.17 Eq (And (iext uri_rdf_type uri_rdf_first uri_owl_FunctionalProperty) (iext uri_rdf_type uri_ex_w (skS.0 4 a))) True % 3.92/4.17 Clause #145 (by clausification #[141]): ∀ (a : Iota), Eq (iext uri_rdf_type uri_ex_w (skS.0 4 a)) True % 3.92/4.17 Clause #147 (by superposition #[145, 11]): ∀ (a : Iota), Or (Eq True False) (Eq (icext (skS.0 4 a) uri_ex_w) True) % 3.92/4.17 Clause #159 (by clausification #[147]): ∀ (a : Iota), Eq (icext (skS.0 4 a) uri_ex_w) True % 3.92/4.17 Clause #160 (by superposition #[159, 130]): Or (Eq True False) (Eq uri_ex_w uri_ex_v) % 3.92/4.17 Clause #162 (by clausification #[160]): Eq uri_ex_w uri_ex_v % 3.92/4.17 Clause #169 (by backward demodulation #[162, 137]): Eq (iext uri_owl_sameAs uri_ex_w uri_ex_w) False % 3.92/4.17 Clause #178 (by superposition #[169, 17]): Eq False True % 3.92/4.17 Clause #179 (by clausification #[178]): False % 3.92/4.17 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------