%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR052+1 : TPTP v9.2.0. Released v3.4.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 07:46:14 PM UTC 2025 % Result : Theorem 4.93s 5.10s % Output : Proof 4.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR052+1 : TPTP v9.2.0. Released v3.4.0. % 0.03/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 20:43:23 EDT 2025 % 0.13/0.34 % CPUTime : % 4.93/5.10 SZS status Theorem for theBenchmark.p % 4.93/5.10 SZS output start Proof for theBenchmark.p % 4.93/5.10 Clause #7 (by assumption #[]): Eq (genls c_tptpcol_8_39940 c_tptpcol_7_39939) True % 4.93/5.10 Clause #9 (by assumption #[]): Eq (genls c_tptpcol_9_40196 c_tptpcol_8_39940) True % 4.93/5.10 Clause #11 (by assumption #[]): Eq (genls c_tptpcol_10_40324 c_tptpcol_9_40196) True % 4.93/5.10 Clause #13 (by assumption #[]): Eq (genls c_tptpcol_11_40388 c_tptpcol_10_40324) True % 4.93/5.10 Clause #15 (by assumption #[]): Eq (genls c_tptpcol_12_40420 c_tptpcol_11_40388) True % 4.93/5.10 Clause #17 (by assumption #[]): Eq (genls c_tptpcol_13_40421 c_tptpcol_12_40420) True % 4.93/5.10 Clause #19 (by assumption #[]): Eq (genls c_tptpcol_14_40429 c_tptpcol_13_40421) True % 4.93/5.10 Clause #21 (by assumption #[]): Eq (genls c_tptpcol_15_40430 c_tptpcol_14_40429) True % 4.93/5.10 Clause #76 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genls X Y) (genls Y Z) → genls X Z) True % 4.93/5.10 Clause #83 (by assumption #[]): Eq % 4.93/5.10 (Not % 4.93/5.10 (mtvisible % 4.93/5.10 (f_contentmtofcdafromeventfn % 4.93/5.10 (f_urlreferentfn (f_urlfn s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)) % 4.93/5.10 c_translation_33) → % 4.93/5.10 genls c_tptpcol_15_40430 c_tptpcol_7_39939)) % 4.93/5.10 True % 4.93/5.10 Clause #228 (by clausification #[83]): Eq % 4.93/5.10 (mtvisible % 4.93/5.10 (f_contentmtofcdafromeventfn % 4.93/5.10 (f_urlreferentfn (f_urlfn s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)) % 4.93/5.10 c_translation_33) → % 4.93/5.10 genls c_tptpcol_15_40430 c_tptpcol_7_39939) % 4.93/5.10 False % 4.93/5.10 Clause #230 (by clausification #[228]): Eq (genls c_tptpcol_15_40430 c_tptpcol_7_39939) False % 4.93/5.10 Clause #347 (by clausification #[76]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genls a Y) (genls Y Z) → genls a Z) True % 4.93/5.10 Clause #348 (by clausification #[347]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genls a a_1) (genls a_1 Z) → genls a Z) True % 4.93/5.10 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 : Iota), Eq (And (genls a a_1) (genls a_1 a_2) → genls a a_2) True % 4.93/5.10 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (genls a a_1) (genls a_1 a_2)) False) (Eq (genls a a_2) True) % 4.93/5.10 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 : Iota), Or (Eq (genls a a_1) True) (Or (Eq (genls a a_2) False) (Eq (genls a_2 a_1) False)) % 4.93/5.10 Clause #357 (by superposition #[351, 21]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_40430 a) True) (Or (Eq (genls c_tptpcol_14_40429 a) False) (Eq False True)) % 4.93/5.10 Clause #358 (by superposition #[351, 19]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_40429 a) True) (Or (Eq (genls c_tptpcol_13_40421 a) False) (Eq False True)) % 4.93/5.10 Clause #359 (by superposition #[351, 17]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Or (Eq (genls c_tptpcol_12_40420 a) False) (Eq False True)) % 4.93/5.10 Clause #387 (by clausification #[359]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Eq (genls c_tptpcol_12_40420 a) False) % 4.93/5.10 Clause #388 (by superposition #[387, 15]): Or (Eq (genls c_tptpcol_13_40421 c_tptpcol_11_40388) True) (Eq False True) % 4.93/5.10 Clause #394 (by clausification #[388]): Eq (genls c_tptpcol_13_40421 c_tptpcol_11_40388) True % 4.93/5.10 Clause #395 (by superposition #[394, 351]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Or (Eq True False) (Eq (genls c_tptpcol_11_40388 a) False)) % 4.93/5.10 Clause #409 (by clausification #[395]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Eq (genls c_tptpcol_11_40388 a) False) % 4.93/5.10 Clause #410 (by superposition #[409, 13]): Or (Eq (genls c_tptpcol_13_40421 c_tptpcol_10_40324) True) (Eq False True) % 4.93/5.10 Clause #417 (by clausification #[410]): Eq (genls c_tptpcol_13_40421 c_tptpcol_10_40324) True % 4.93/5.10 Clause #418 (by superposition #[417, 351]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Or (Eq True False) (Eq (genls c_tptpcol_10_40324 a) False)) % 4.93/5.10 Clause #419 (by clausification #[418]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Eq (genls c_tptpcol_10_40324 a) False) % 4.93/5.10 Clause #420 (by superposition #[419, 11]): Or (Eq (genls c_tptpcol_13_40421 c_tptpcol_9_40196) True) (Eq False True) % 4.93/5.10 Clause #423 (by clausification #[420]): Eq (genls c_tptpcol_13_40421 c_tptpcol_9_40196) True % 4.93/5.10 Clause #424 (by superposition #[423, 351]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Or (Eq True False) (Eq (genls c_tptpcol_9_40196 a) False)) % 4.93/5.11 Clause #425 (by clausification #[424]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Eq (genls c_tptpcol_9_40196 a) False) % 4.93/5.11 Clause #426 (by superposition #[425, 9]): Or (Eq (genls c_tptpcol_13_40421 c_tptpcol_8_39940) True) (Eq False True) % 4.93/5.11 Clause #427 (by clausification #[426]): Eq (genls c_tptpcol_13_40421 c_tptpcol_8_39940) True % 4.93/5.11 Clause #428 (by superposition #[427, 351]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Or (Eq True False) (Eq (genls c_tptpcol_8_39940 a) False)) % 4.93/5.11 Clause #429 (by clausification #[428]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_40421 a) True) (Eq (genls c_tptpcol_8_39940 a) False) % 4.93/5.11 Clause #430 (by superposition #[429, 7]): Or (Eq (genls c_tptpcol_13_40421 c_tptpcol_7_39939) True) (Eq False True) % 4.93/5.11 Clause #437 (by clausification #[430]): Eq (genls c_tptpcol_13_40421 c_tptpcol_7_39939) True % 4.93/5.11 Clause #479 (by clausification #[358]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_40429 a) True) (Eq (genls c_tptpcol_13_40421 a) False) % 4.93/5.11 Clause #486 (by superposition #[479, 437]): Or (Eq (genls c_tptpcol_14_40429 c_tptpcol_7_39939) True) (Eq False True) % 4.93/5.11 Clause #488 (by clausification #[486]): Eq (genls c_tptpcol_14_40429 c_tptpcol_7_39939) True % 4.93/5.11 Clause #503 (by clausification #[357]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_40430 a) True) (Eq (genls c_tptpcol_14_40429 a) False) % 4.93/5.11 Clause #506 (by superposition #[503, 488]): Or (Eq (genls c_tptpcol_15_40430 c_tptpcol_7_39939) True) (Eq False True) % 4.93/5.11 Clause #571 (by clausification #[506]): Eq (genls c_tptpcol_15_40430 c_tptpcol_7_39939) True % 4.93/5.11 Clause #572 (by superposition #[571, 230]): Eq True False % 4.93/5.11 Clause #574 (by clausification #[572]): False % 4.93/5.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------