%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR045+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:10 PM UTC 2025 % Result : Theorem 4.33s 4.49s % Output : Proof 4.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR045+1 : TPTP v9.2.0. Released v3.4.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n016.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 20:18:53 EDT 2025 % 0.13/0.34 % CPUTime : % 4.33/4.49 SZS status Theorem for theBenchmark.p % 4.33/4.49 SZS output start Proof for theBenchmark.p % 4.33/4.49 Clause #0 (by assumption #[]): Eq (applicationcontext c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #2 (by assumption #[]): Eq (∀ (OBJ : Iota), microtheory OBJ → aspatialinformationstore OBJ) True % 4.33/4.49 Clause #5 (by assumption #[]): Eq (∀ (OBJ : Iota), intangibleindividual OBJ → partiallyintangibleindividual OBJ) True % 4.33/4.49 Clause #7 (by assumption #[]): Eq (∀ (OBJ : Iota), aspatialinformationstore OBJ → intangibleindividual OBJ) True % 4.33/4.49 Clause #9 (by assumption #[]): Eq (∀ (OBJ : Iota), partiallyintangibleindividual OBJ → individual OBJ) True % 4.33/4.49 Clause #13 (by assumption #[]): Eq (∀ (OBJ : Iota), applicationcontext OBJ → microtheory OBJ) True % 4.33/4.49 Clause #14 (by assumption #[]): Eq (∀ (OBJ : Iota), Not (And (collection OBJ) (individual OBJ))) True % 4.33/4.49 Clause #19 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), genls ARG1 ARG2 → collection ARG1) True % 4.33/4.49 Clause #68 (by assumption #[]): Eq (Not (Not (genls c_wamt_evalinitial_p14 c_tptpcol_15_80088))) True % 4.33/4.49 Clause #69 (by clausification #[2]): ∀ (a : Iota), Eq (microtheory a → aspatialinformationstore a) True % 4.33/4.49 Clause #70 (by clausification #[69]): ∀ (a : Iota), Or (Eq (microtheory a) False) (Eq (aspatialinformationstore a) True) % 4.33/4.49 Clause #71 (by clausification #[5]): ∀ (a : Iota), Eq (intangibleindividual a → partiallyintangibleindividual a) True % 4.33/4.49 Clause #72 (by clausification #[71]): ∀ (a : Iota), Or (Eq (intangibleindividual a) False) (Eq (partiallyintangibleindividual a) True) % 4.33/4.49 Clause #73 (by clausification #[7]): ∀ (a : Iota), Eq (aspatialinformationstore a → intangibleindividual a) True % 4.33/4.49 Clause #74 (by clausification #[73]): ∀ (a : Iota), Or (Eq (aspatialinformationstore a) False) (Eq (intangibleindividual a) True) % 4.33/4.49 Clause #75 (by clausification #[13]): ∀ (a : Iota), Eq (applicationcontext a → microtheory a) True % 4.33/4.49 Clause #76 (by clausification #[75]): ∀ (a : Iota), Or (Eq (applicationcontext a) False) (Eq (microtheory a) True) % 4.33/4.49 Clause #77 (by superposition #[76, 0]): Or (Eq (microtheory c_wamt_evalinitial_p14) True) (Eq False True) % 4.33/4.49 Clause #78 (by clausification #[77]): Eq (microtheory c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #79 (by superposition #[78, 70]): Or (Eq True False) (Eq (aspatialinformationstore c_wamt_evalinitial_p14) True) % 4.33/4.49 Clause #80 (by clausification #[79]): Eq (aspatialinformationstore c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #81 (by superposition #[80, 74]): Or (Eq True False) (Eq (intangibleindividual c_wamt_evalinitial_p14) True) % 4.33/4.49 Clause #82 (by clausification #[81]): Eq (intangibleindividual c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #83 (by superposition #[82, 72]): Or (Eq True False) (Eq (partiallyintangibleindividual c_wamt_evalinitial_p14) True) % 4.33/4.49 Clause #84 (by clausification #[83]): Eq (partiallyintangibleindividual c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #85 (by clausification #[9]): ∀ (a : Iota), Eq (partiallyintangibleindividual a → individual a) True % 4.33/4.49 Clause #86 (by clausification #[85]): ∀ (a : Iota), Or (Eq (partiallyintangibleindividual a) False) (Eq (individual a) True) % 4.33/4.49 Clause #87 (by superposition #[86, 84]): Or (Eq (individual c_wamt_evalinitial_p14) True) (Eq False True) % 4.33/4.49 Clause #88 (by clausification #[87]): Eq (individual c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #97 (by clausification #[14]): ∀ (a : Iota), Eq (Not (And (collection a) (individual a))) True % 4.33/4.49 Clause #98 (by clausification #[97]): ∀ (a : Iota), Eq (And (collection a) (individual a)) False % 4.33/4.49 Clause #99 (by clausification #[98]): ∀ (a : Iota), Or (Eq (collection a) False) (Eq (individual a) False) % 4.33/4.49 Clause #151 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), genls a ARG2 → collection a) True % 4.33/4.49 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), Eq (genls a a_1 → collection a) True % 4.33/4.49 Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), Or (Eq (genls a a_1) False) (Eq (collection a) True) % 4.33/4.49 Clause #453 (by clausification #[68]): Eq (Not (genls c_wamt_evalinitial_p14 c_tptpcol_15_80088)) False % 4.33/4.49 Clause #454 (by clausification #[453]): Eq (genls c_wamt_evalinitial_p14 c_tptpcol_15_80088) True % 4.33/4.49 Clause #455 (by superposition #[454, 153]): Or (Eq True False) (Eq (collection c_wamt_evalinitial_p14) True) % 4.33/4.49 Clause #463 (by clausification #[455]): Eq (collection c_wamt_evalinitial_p14) True % 4.33/4.49 Clause #464 (by superposition #[463, 99]): Or (Eq True False) (Eq (individual c_wamt_evalinitial_p14) False) % 4.33/4.49 Clause #467 (by clausification #[464]): Eq (individual c_wamt_evalinitial_p14) False % 4.33/4.49 Clause #468 (by superposition #[467, 88]): Eq False True % 4.33/4.49 Clause #501 (by clausification #[468]): False % 4.33/4.49 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------