%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR066+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:19 PM UTC 2025 % Result : Theorem 4.96s 5.21s % Output : Proof 4.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : CSR066+1 : TPTP v9.2.0. Released v3.4.0. % 0.09/0.15 % Command : duper %s % 0.15/0.37 % Computer : n029.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 300 % 0.15/0.37 % DateTime : Thu Oct 2 19:44:53 EDT 2025 % 0.15/0.37 % CPUTime : % 4.96/5.21 SZS status Theorem for theBenchmark.p % 4.96/5.21 SZS output start Proof for theBenchmark.p % 4.96/5.21 Clause #3 (by assumption #[]): Eq % 4.96/5.21 (∀ (TERM INDEPCOL PRED DEPCOL : Iota), % 4.96/5.21 And (isa TERM INDEPCOL) (relationexistsall PRED DEPCOL INDEPCOL) → % 4.96/5.21 isa (f_relationexistsallfn TERM PRED DEPCOL INDEPCOL) DEPCOL) % 4.96/5.21 True % 4.96/5.21 Clause #8 (by assumption #[]): Eq % 4.96/5.21 (∀ (TERM : Iota), % 4.96/5.21 shavingrazor_manual TERM → % 4.96/5.21 tptp_8_271 (f_relationexistsallfn TERM c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) TERM) % 4.96/5.21 True % 4.96/5.21 Clause #9 (by assumption #[]): Eq (relationexistsall c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) True % 4.96/5.21 Clause #10 (by assumption #[]): Eq (shavingrazor_manual c_theprototypicalshavingrazor_manual) True % 4.96/5.21 Clause #27 (by assumption #[]): Eq (∀ (X : Iota), shavingrazor_manual X → isa X c_shavingrazor_manual) True % 4.96/5.21 Clause #28 (by assumption #[]): Eq (∀ (X : Iota), isa X c_tptpcol_16_25972 → tptpcol_16_25972 X) True % 4.96/5.21 Clause #65 (by assumption #[]): Eq % 4.96/5.21 (Not % 4.96/5.21 (Exists fun X => % 4.96/5.21 mtvisible % 4.96/5.21 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_webnjiteducjohnsontreebiochhtm)) % 4.96/5.21 c_translation_21) → % 4.96/5.21 And (tptp_8_271 X c_theprototypicalshavingrazor_manual) (tptpcol_16_25972 X))) % 4.96/5.21 True % 4.96/5.21 Clause #66 (by clausification #[28]): ∀ (a : Iota), Eq (isa a c_tptpcol_16_25972 → tptpcol_16_25972 a) True % 4.96/5.21 Clause #67 (by clausification #[66]): ∀ (a : Iota), Or (Eq (isa a c_tptpcol_16_25972) False) (Eq (tptpcol_16_25972 a) True) % 4.96/5.21 Clause #75 (by clausification #[3]): ∀ (a : Iota), % 4.96/5.21 Eq % 4.96/5.21 (∀ (INDEPCOL PRED DEPCOL : Iota), % 4.96/5.21 And (isa a INDEPCOL) (relationexistsall PRED DEPCOL INDEPCOL) → % 4.96/5.21 isa (f_relationexistsallfn a PRED DEPCOL INDEPCOL) DEPCOL) % 4.96/5.21 True % 4.96/5.21 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), % 4.96/5.21 Eq % 4.96/5.21 (∀ (PRED DEPCOL : Iota), % 4.96/5.21 And (isa a a_1) (relationexistsall PRED DEPCOL a_1) → isa (f_relationexistsallfn a PRED DEPCOL a_1) DEPCOL) % 4.96/5.21 True % 4.96/5.21 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 : Iota), % 4.96/5.21 Eq % 4.96/5.21 (∀ (DEPCOL : Iota), % 4.96/5.21 And (isa a a_1) (relationexistsall a_2 DEPCOL a_1) → isa (f_relationexistsallfn a a_2 DEPCOL a_1) DEPCOL) % 4.96/5.21 True % 4.96/5.21 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 a_3 : Iota), % 4.96/5.21 Eq (And (isa a a_1) (relationexistsall a_2 a_3 a_1) → isa (f_relationexistsallfn a a_2 a_3 a_1) a_3) True % 4.96/5.21 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 4.96/5.21 Or (Eq (And (isa a a_1) (relationexistsall a_2 a_3 a_1)) False) % 4.96/5.21 (Eq (isa (f_relationexistsallfn a a_2 a_3 a_1) a_3) True) % 4.96/5.21 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 4.96/5.21 Or (Eq (isa (f_relationexistsallfn a a_1 a_2 a_3) a_2) True) % 4.96/5.21 (Or (Eq (isa a a_3) False) (Eq (relationexistsall a_1 a_2 a_3) False)) % 4.96/5.21 Clause #84 (by clausification #[27]): ∀ (a : Iota), Eq (shavingrazor_manual a → isa a c_shavingrazor_manual) True % 4.96/5.21 Clause #85 (by clausification #[84]): ∀ (a : Iota), Or (Eq (shavingrazor_manual a) False) (Eq (isa a c_shavingrazor_manual) True) % 4.96/5.21 Clause #86 (by superposition #[85, 10]): Or (Eq (isa c_theprototypicalshavingrazor_manual c_shavingrazor_manual) True) (Eq False True) % 4.96/5.21 Clause #87 (by clausification #[86]): Eq (isa c_theprototypicalshavingrazor_manual c_shavingrazor_manual) True % 4.96/5.21 Clause #89 (by superposition #[87, 80]): ∀ (a a_1 : Iota), % 4.96/5.21 Or (Eq (isa (f_relationexistsallfn c_theprototypicalshavingrazor_manual a a_1 c_shavingrazor_manual) a_1) True) % 4.96/5.21 (Or (Eq True False) (Eq (relationexistsall a a_1 c_shavingrazor_manual) False)) % 4.96/5.21 Clause #90 (by clausification #[8]): ∀ (a : Iota), % 4.96/5.21 Eq % 4.96/5.21 (shavingrazor_manual a → % 4.96/5.21 tptp_8_271 (f_relationexistsallfn a c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) a) % 4.96/5.21 True % 4.96/5.21 Clause #91 (by clausification #[90]): ∀ (a : Iota), % 4.96/5.21 Or (Eq (shavingrazor_manual a) False) % 4.96/5.21 (Eq (tptp_8_271 (f_relationexistsallfn a c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) a) True) % 4.96/5.21 Clause #92 (by superposition #[91, 10]): Or % 4.96/5.21 (Eq % 4.96/5.21 (tptp_8_271 % 4.96/5.21 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) % 4.96/5.21 c_theprototypicalshavingrazor_manual) % 4.96/5.22 True) % 4.96/5.22 (Eq False True) % 4.96/5.22 Clause #289 (by clausification #[92]): Eq % 4.96/5.22 (tptp_8_271 % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) % 4.96/5.22 c_theprototypicalshavingrazor_manual) % 4.96/5.22 True % 4.96/5.22 Clause #349 (by clausification #[65]): Eq % 4.96/5.22 (Exists fun X => % 4.96/5.22 mtvisible % 4.96/5.22 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_webnjiteducjohnsontreebiochhtm)) % 4.96/5.22 c_translation_21) → % 4.96/5.22 And (tptp_8_271 X c_theprototypicalshavingrazor_manual) (tptpcol_16_25972 X)) % 4.96/5.22 False % 4.96/5.22 Clause #350 (by clausification #[349]): ∀ (a : Iota), % 4.96/5.22 Eq % 4.96/5.22 (mtvisible % 4.96/5.22 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_webnjiteducjohnsontreebiochhtm)) % 4.96/5.22 c_translation_21) → % 4.96/5.22 And (tptp_8_271 a c_theprototypicalshavingrazor_manual) (tptpcol_16_25972 a)) % 4.96/5.22 False % 4.96/5.22 Clause #352 (by clausification #[350]): ∀ (a : Iota), Eq (And (tptp_8_271 a c_theprototypicalshavingrazor_manual) (tptpcol_16_25972 a)) False % 4.96/5.22 Clause #357 (by clausification #[352]): ∀ (a : Iota), Or (Eq (tptp_8_271 a c_theprototypicalshavingrazor_manual) False) (Eq (tptpcol_16_25972 a) False) % 4.96/5.22 Clause #358 (by superposition #[357, 289]): Or % 4.96/5.22 (Eq % 4.96/5.22 (tptpcol_16_25972 % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 % 4.96/5.22 c_shavingrazor_manual)) % 4.96/5.22 False) % 4.96/5.22 (Eq False True) % 4.96/5.22 Clause #359 (by clausification #[358]): Eq % 4.96/5.22 (tptpcol_16_25972 % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual)) % 4.96/5.22 False % 4.96/5.22 Clause #360 (by clausification #[89]): ∀ (a a_1 : Iota), % 4.96/5.22 Or (Eq (isa (f_relationexistsallfn c_theprototypicalshavingrazor_manual a a_1 c_shavingrazor_manual) a_1) True) % 4.96/5.22 (Eq (relationexistsall a a_1 c_shavingrazor_manual) False) % 4.96/5.22 Clause #361 (by superposition #[360, 9]): Or % 4.96/5.22 (Eq % 4.96/5.22 (isa % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) % 4.96/5.22 c_tptpcol_16_25972) % 4.96/5.22 True) % 4.96/5.22 (Eq False True) % 4.96/5.22 Clause #362 (by clausification #[361]): Eq % 4.96/5.22 (isa % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual) % 4.96/5.22 c_tptpcol_16_25972) % 4.96/5.22 True % 4.96/5.22 Clause #363 (by superposition #[362, 67]): Or (Eq True False) % 4.96/5.22 (Eq % 4.96/5.22 (tptpcol_16_25972 % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 % 4.96/5.22 c_shavingrazor_manual)) % 4.96/5.22 True) % 4.96/5.22 Clause #369 (by clausification #[363]): Eq % 4.96/5.22 (tptpcol_16_25972 % 4.96/5.22 (f_relationexistsallfn c_theprototypicalshavingrazor_manual c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual)) % 4.96/5.22 True % 4.96/5.22 Clause #370 (by superposition #[369, 359]): Eq True False % 4.96/5.22 Clause #372 (by clausification #[370]): False % 4.96/5.22 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------