%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR045+2 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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 07:46:11 PM UTC 2025 % Result : Theorem 174.09s 174.41s % Output : Proof 174.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : CSR045+2 : TPTP v9.2.0. Released v3.4.0. % 0.07/0.14 % Command : duper %s % 0.15/0.36 % Computer : n013.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Thu Oct 2 19:25:53 EDT 2025 % 0.15/0.36 % CPUTime : % 174.09/174.41 SZS status Theorem for theBenchmark.p % 174.09/174.41 SZS output start Proof for theBenchmark.p % 174.09/174.41 Clause #32 (by assumption #[]): Eq (∀ (OBJ : Iota), partiallyintangibleindividual OBJ → individual OBJ) True % 174.09/174.41 Clause #82 (by assumption #[]): Eq (applicationcontext c_wamt_evalinitial_p14) True % 174.09/174.41 Clause #155 (by assumption #[]): Eq (∀ (OBJ : Iota), microtheory OBJ → aspatialinformationstore OBJ) True % 174.09/174.41 Clause #170 (by assumption #[]): Eq (∀ (OBJ : Iota), applicationcontext OBJ → microtheory OBJ) True % 174.09/174.41 Clause #228 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), genls ARG1 ARG2 → collection ARG1) True % 174.09/174.41 Clause #288 (by assumption #[]): Eq (∀ (OBJ : Iota), Not (And (collection OBJ) (individual OBJ))) True % 174.09/174.41 Clause #319 (by assumption #[]): Eq (∀ (OBJ : Iota), intangibleindividual OBJ → partiallyintangibleindividual OBJ) True % 174.09/174.41 Clause #381 (by assumption #[]): Eq (∀ (OBJ : Iota), aspatialinformationstore OBJ → intangibleindividual OBJ) True % 174.09/174.41 Clause #1103 (by assumption #[]): Eq (Not (Not (genls c_wamt_evalinitial_p14 c_tptpcol_15_80088))) True % 174.09/174.41 Clause #1140 (by clausification #[32]): ∀ (a : Iota), Eq (partiallyintangibleindividual a → individual a) True % 174.09/174.41 Clause #1141 (by clausification #[1140]): ∀ (a : Iota), Or (Eq (partiallyintangibleindividual a) False) (Eq (individual a) True) % 174.09/174.41 Clause #1211 (by clausification #[155]): ∀ (a : Iota), Eq (microtheory a → aspatialinformationstore a) True % 174.09/174.41 Clause #1212 (by clausification #[1211]): ∀ (a : Iota), Or (Eq (microtheory a) False) (Eq (aspatialinformationstore a) True) % 174.09/174.41 Clause #1221 (by clausification #[381]): ∀ (a : Iota), Eq (aspatialinformationstore a → intangibleindividual a) True % 174.09/174.41 Clause #1222 (by clausification #[1221]): ∀ (a : Iota), Or (Eq (aspatialinformationstore a) False) (Eq (intangibleindividual a) True) % 174.09/174.41 Clause #1469 (by clausification #[319]): ∀ (a : Iota), Eq (intangibleindividual a → partiallyintangibleindividual a) True % 174.09/174.41 Clause #1470 (by clausification #[1469]): ∀ (a : Iota), Or (Eq (intangibleindividual a) False) (Eq (partiallyintangibleindividual a) True) % 174.09/174.41 Clause #1604 (by clausification #[170]): ∀ (a : Iota), Eq (applicationcontext a → microtheory a) True % 174.09/174.41 Clause #1605 (by clausification #[1604]): ∀ (a : Iota), Or (Eq (applicationcontext a) False) (Eq (microtheory a) True) % 174.09/174.41 Clause #1606 (by superposition #[1605, 82]): Or (Eq (microtheory c_wamt_evalinitial_p14) True) (Eq False True) % 174.09/174.41 Clause #1607 (by clausification #[1606]): Eq (microtheory c_wamt_evalinitial_p14) True % 174.09/174.41 Clause #1608 (by superposition #[1607, 1212]): Or (Eq True False) (Eq (aspatialinformationstore c_wamt_evalinitial_p14) True) % 174.09/174.41 Clause #1609 (by clausification #[1608]): Eq (aspatialinformationstore c_wamt_evalinitial_p14) True % 174.09/174.41 Clause #1610 (by superposition #[1609, 1222]): Or (Eq True False) (Eq (intangibleindividual c_wamt_evalinitial_p14) True) % 174.09/174.41 Clause #1611 (by clausification #[1610]): Eq (intangibleindividual c_wamt_evalinitial_p14) True % 174.09/174.41 Clause #1612 (by superposition #[1611, 1470]): Or (Eq True False) (Eq (partiallyintangibleindividual c_wamt_evalinitial_p14) True) % 174.09/174.41 Clause #1613 (by clausification #[1612]): Eq (partiallyintangibleindividual c_wamt_evalinitial_p14) True % 174.09/174.41 Clause #1614 (by superposition #[1613, 1141]): Or (Eq True False) (Eq (individual c_wamt_evalinitial_p14) True) % 174.09/174.41 Clause #1615 (by clausification #[1614]): Eq (individual c_wamt_evalinitial_p14) True % 174.09/174.41 Clause #1801 (by clausification #[228]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), genls a ARG2 → collection a) True % 174.09/174.41 Clause #1802 (by clausification #[1801]): ∀ (a a_1 : Iota), Eq (genls a a_1 → collection a) True % 174.09/174.41 Clause #1803 (by clausification #[1802]): ∀ (a a_1 : Iota), Or (Eq (genls a a_1) False) (Eq (collection a) True) % 174.09/174.41 Clause #1985 (by clausification #[288]): ∀ (a : Iota), Eq (Not (And (collection a) (individual a))) True % 174.09/174.41 Clause #1986 (by clausification #[1985]): ∀ (a : Iota), Eq (And (collection a) (individual a)) False % 174.09/174.41 Clause #1987 (by clausification #[1986]): ∀ (a : Iota), Or (Eq (collection a) False) (Eq (individual a) False) % 174.09/174.41 Clause #9147 (by clausification #[1103]): Eq (Not (genls c_wamt_evalinitial_p14 c_tptpcol_15_80088)) False % 174.09/174.45 Clause #9148 (by clausification #[9147]): Eq (genls c_wamt_evalinitial_p14 c_tptpcol_15_80088) True % 174.09/174.45 Clause #9149 (by superposition #[9148, 1803]): Or (Eq True False) (Eq (collection c_wamt_evalinitial_p14) True) % 174.09/174.45 Clause #9158 (by clausification #[9149]): Eq (collection c_wamt_evalinitial_p14) True % 174.09/174.45 Clause #9159 (by superposition #[9158, 1987]): Or (Eq True False) (Eq (individual c_wamt_evalinitial_p14) False) % 174.09/174.45 Clause #9162 (by clausification #[9159]): Eq (individual c_wamt_evalinitial_p14) False % 174.09/174.45 Clause #9163 (by superposition #[9162, 1615]): Eq False True % 174.09/174.45 Clause #9164 (by clausification #[9163]): False % 174.09/174.45 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------