%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWB005+1 : TPTP v9.2.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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 113.30s 113.52s % Output : Proof 113.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB005+1 : TPTP v9.2.0. Released v5.2.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 11:49:23 EDT 2025 % 0.13/0.34 % CPUTime : % 113.30/113.52 SZS status Theorem for theBenchmark.p % 113.30/113.52 SZS output start Proof for theBenchmark.p % 113.30/113.52 Clause #0 (by assumption #[]): Eq (∀ (S P O : Iota), iext P S O → ip P) True % 113.30/113.52 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), ir X) True % 113.30/113.52 Clause #12 (by assumption #[]): Eq (∀ (P : Iota), Iff (iext uri_rdf_type P uri_rdf_Property) (ip P)) True % 113.30/113.52 Clause #23 (by assumption #[]): Eq (∀ (X C : Iota), Iff (iext uri_rdf_type X C) (icext C X)) True % 113.30/113.52 Clause #143 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_owl_ObjectProperty X) (ip X)) True % 113.30/113.52 Clause #153 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_rdfs_Resource X) (ir X)) True % 113.30/113.52 Clause #159 (by assumption #[]): Eq (∀ (X : Iota), Iff (icext uri_owl_Thing X) (ir X)) True % 113.30/113.52 Clause #548 (by assumption #[]): Eq % 113.30/113.52 (Not % 113.30/113.52 (And % 113.30/113.52 (And % 113.30/113.52 (And % 113.30/113.52 (And % 113.30/113.52 (And % 113.30/113.52 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.52 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.30/113.52 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 113.30/113.52 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 113.30/113.52 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 113.30/113.52 (iext uri_rdf_type uri_ex_o uri_rdfs_Resource)) % 113.30/113.52 (iext uri_rdf_type uri_ex_o uri_owl_Thing))) % 113.30/113.52 True % 113.30/113.52 Clause #549 (by assumption #[]): Eq (iext uri_ex_p uri_ex_s uri_ex_o) True % 113.30/113.52 Clause #550 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (P O : Iota), iext P a O → ip P) True % 113.30/113.52 Clause #551 (by clausification #[550]): ∀ (a a_1 : Iota), Eq (∀ (O : Iota), iext a a_1 O → ip a) True % 113.30/113.52 Clause #552 (by clausification #[551]): ∀ (a a_1 a_2 : Iota), Eq (iext a a_1 a_2 → ip a) True % 113.30/113.52 Clause #553 (by clausification #[552]): ∀ (a a_1 a_2 : Iota), Or (Eq (iext a a_1 a_2) False) (Eq (ip a) True) % 113.30/113.52 Clause #554 (by clausification #[1]): ∀ (a : Iota), Eq (ir a) True % 113.30/113.52 Clause #558 (by clausification #[12]): ∀ (a : Iota), Eq (Iff (iext uri_rdf_type a uri_rdf_Property) (ip a)) True % 113.30/113.52 Clause #559 (by clausification #[558]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_rdf_Property) True) (Eq (ip a) False) % 113.30/113.52 Clause #605 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (C : Iota), Iff (iext uri_rdf_type a C) (icext C a)) True % 113.30/113.52 Clause #606 (by clausification #[605]): ∀ (a a_1 : Iota), Eq (Iff (iext uri_rdf_type a a_1) (icext a_1 a)) True % 113.30/113.52 Clause #607 (by clausification #[606]): ∀ (a a_1 : Iota), Or (Eq (iext uri_rdf_type a a_1) True) (Eq (icext a_1 a) False) % 113.30/113.52 Clause #1137 (by superposition #[549, 553]): Or (Eq (ip uri_ex_p) True) (Eq False True) % 113.30/113.52 Clause #1139 (by clausification #[1137]): Eq (ip uri_ex_p) True % 113.30/113.52 Clause #1140 (by superposition #[1139, 559]): Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) True) (Eq True False) % 113.30/113.52 Clause #1772 (by clausification #[143]): ∀ (a : Iota), Eq (Iff (icext uri_owl_ObjectProperty a) (ip a)) True % 113.30/113.52 Clause #1773 (by clausification #[1772]): ∀ (a : Iota), Or (Eq (icext uri_owl_ObjectProperty a) True) (Eq (ip a) False) % 113.30/113.52 Clause #1842 (by superposition #[1773, 1139]): Or (Eq (icext uri_owl_ObjectProperty uri_ex_p) True) (Eq False True) % 113.30/113.52 Clause #1869 (by clausification #[1842]): Eq (icext uri_owl_ObjectProperty uri_ex_p) True % 113.30/113.52 Clause #1870 (by superposition #[1869, 607]): Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) True) (Eq True False) % 113.30/113.52 Clause #1978 (by clausification #[153]): ∀ (a : Iota), Eq (Iff (icext uri_rdfs_Resource a) (ir a)) True % 113.30/113.52 Clause #1979 (by clausification #[1978]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Resource a) True) (Eq (ir a) False) % 113.30/113.52 Clause #1981 (by forward demodulation #[1979, 554]): ∀ (a : Iota), Or (Eq (icext uri_rdfs_Resource a) True) (Eq True False) % 113.30/113.52 Clause #1982 (by clausification #[1981]): ∀ (a : Iota), Eq (icext uri_rdfs_Resource a) True % 113.30/113.52 Clause #1983 (by superposition #[1982, 607]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_rdfs_Resource) True) (Eq True False) % 113.30/113.52 Clause #1989 (by clausification #[159]): ∀ (a : Iota), Eq (Iff (icext uri_owl_Thing a) (ir a)) True % 113.30/113.52 Clause #1990 (by clausification #[1989]): ∀ (a : Iota), Or (Eq (icext uri_owl_Thing a) True) (Eq (ir a) False) % 113.30/113.54 Clause #1992 (by forward demodulation #[1990, 554]): ∀ (a : Iota), Or (Eq (icext uri_owl_Thing a) True) (Eq True False) % 113.30/113.54 Clause #1993 (by clausification #[1992]): ∀ (a : Iota), Eq (icext uri_owl_Thing a) True % 113.30/113.54 Clause #1994 (by superposition #[1993, 607]): ∀ (a : Iota), Or (Eq (iext uri_rdf_type a uri_owl_Thing) True) (Eq True False) % 113.30/113.54 Clause #3859 (by clausification #[1870]): Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) True % 113.30/113.54 Clause #8288 (by clausification #[1994]): ∀ (a : Iota), Eq (iext uri_rdf_type a uri_owl_Thing) True % 113.30/113.54 Clause #8293 (by clausification #[1983]): ∀ (a : Iota), Eq (iext uri_rdf_type a uri_rdfs_Resource) True % 113.30/113.54 Clause #12681 (by clausification #[1140]): Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) True % 113.30/113.54 Clause #13512 (by clausification #[548]): Eq % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 113.30/113.54 (iext uri_rdf_type uri_ex_o uri_rdfs_Resource)) % 113.30/113.54 (iext uri_rdf_type uri_ex_o uri_owl_Thing)) % 113.30/113.54 False % 113.30/113.54 Clause #13513 (by clausification #[13512]): Or % 113.30/113.54 (Eq % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 113.30/113.54 (iext uri_rdf_type uri_ex_o uri_rdfs_Resource)) % 113.30/113.54 False) % 113.30/113.54 (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.30/113.54 Clause #13514 (by clausification #[13513]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.30/113.54 (Or % 113.30/113.54 (Eq % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty)) % 113.30/113.54 False) % 113.30/113.54 (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False)) % 113.30/113.54 Clause #13515 (by clausification #[13514]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.30/113.54 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 113.30/113.54 (Or % 113.30/113.54 (Eq % 113.30/113.54 (And % 113.30/113.54 (And % 113.30/113.54 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdf_Property)) % 113.30/113.54 False) % 113.30/113.54 (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False))) % 113.30/113.54 Clause #13516 (by clausification #[13515]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.30/113.54 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 113.30/113.54 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 113.30/113.54 (Or % 113.30/113.54 (Eq % 113.30/113.54 (And % 113.30/113.54 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_owl_Thing)) % 113.30/113.54 False) % 113.30/113.54 (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False)))) % 113.30/113.54 Clause #13517 (by clausification #[13516]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.30/113.54 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 113.30/113.54 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 113.30/113.54 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.30/113.54 (Or % 113.30/113.54 (Eq % 113.30/113.54 (And (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) % 113.30/113.54 (iext uri_rdf_type uri_ex_p uri_rdfs_Resource)) % 113.38/113.56 False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False))))) % 113.38/113.56 Clause #13518 (by clausification #[13517]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (And (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) (iext uri_rdf_type uri_ex_s uri_owl_Thing)) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False)))))) % 113.38/113.56 Clause #13519 (by clausification #[13518]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_o uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))))) % 113.38/113.56 Clause #13520 (by forward demodulation #[13519, 8293]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq True False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))))) % 113.38/113.56 Clause #13521 (by clausification #[13520]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))))) % 113.38/113.56 Clause #13522 (by forward demodulation #[13521, 3859]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq True False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))))) % 113.38/113.56 Clause #13523 (by clausification #[13522]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdf_Property) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))) % 113.38/113.56 Clause #13524 (by forward demodulation #[13523, 12681]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq True False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))))) % 113.38/113.56 Clause #13525 (by clausification #[13524]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_owl_Thing) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.38/113.56 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.38/113.56 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))) % 113.38/113.56 Clause #13526 (by forward demodulation #[13525, 8288]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.44/113.62 (Or (Eq True False) % 113.44/113.62 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.44/113.62 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.44/113.62 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)))) % 113.44/113.62 Clause #13527 (by clausification #[13526]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.44/113.62 (Or (Eq (iext uri_rdf_type uri_ex_p uri_rdfs_Resource) False) % 113.44/113.62 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.44/113.62 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))) % 113.44/113.62 Clause #13528 (by forward demodulation #[13527, 8293]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.44/113.62 (Or (Eq True False) % 113.44/113.62 (Or (Eq (iext uri_rdf_type uri_ex_s uri_rdfs_Resource) False) % 113.44/113.62 (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False))) % 113.44/113.62 Clause #13529 (by clausification #[13528]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.44/113.62 (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)) % 113.44/113.62 Clause #13530 (by forward demodulation #[13529, 8293]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) % 113.44/113.62 (Or (Eq True False) (Eq (iext uri_rdf_type uri_ex_s uri_owl_Thing) False)) % 113.44/113.62 Clause #13531 (by clausification #[13530]): 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) % 113.44/113.62 Clause #13532 (by forward demodulation #[13531, 8288]): Or (Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False) (Eq True False) % 113.44/113.62 Clause #13533 (by clausification #[13532]): Eq (iext uri_rdf_type uri_ex_o uri_owl_Thing) False % 113.44/113.62 Clause #13534 (by superposition #[13533, 8288]): Eq False True % 113.44/113.62 Clause #13541 (by clausification #[13534]): False % 113.44/113.62 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------