%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR070+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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:21 PM UTC 2025 % Result : Theorem 4.82s 4.98s % Output : Proof 4.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : CSR070+1 : TPTP v9.2.0. Released v3.4.0. % 0.14/0.14 % Command : duper %s % 0.15/0.35 % Computer : n026.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 19:34:53 EDT 2025 % 0.15/0.36 % CPUTime : % 4.82/4.98 SZS status Theorem for theBenchmark.p % 4.82/4.98 SZS output start Proof for theBenchmark.p % 4.82/4.98 Clause #7 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), tptptypes_6_818 ARG1 ARG2 → tptptypes_5_802 ARG1 ARG2) True % 4.82/4.98 Clause #9 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), tptptypes_7_819 ARG1 ARG2 → tptptypes_6_818 ARG1 ARG2) True % 4.82/4.98 Clause #11 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), tptptypes_8_823 ARG1 ARG2 → tptptypes_7_819 ARG1 ARG2) True % 4.82/4.98 Clause #13 (by assumption #[]): Eq (∀ (ARG1 ARG2 : Iota), tptptypes_9_824 ARG1 ARG2 → tptptypes_8_823 ARG1 ARG2) True % 4.82/4.98 Clause #15 (by assumption #[]): Eq (genlmt c_tptp_spindlecollectormt c_tptp_member2668_mt) True % 4.82/4.98 Clause #18 (by assumption #[]): Eq % 4.82/4.98 (mtvisible c_tptp_member2668_mt → % 4.82/4.98 tptptypes_9_824 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.98 c_tptpcol_16_8886) % 4.82/4.98 True % 4.82/4.98 Clause #56 (by assumption #[]): Eq (∀ (SPECMT GENLMT : Iota), And (mtvisible SPECMT) (genlmt SPECMT GENLMT) → mtvisible GENLMT) True % 4.82/4.98 Clause #71 (by assumption #[]): Eq % 4.82/4.98 (Not % 4.82/4.98 (mtvisible c_tptp_spindlecollectormt → % 4.82/4.98 tptptypes_5_802 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.98 c_tptpcol_16_8886)) % 4.82/4.98 True % 4.82/4.98 Clause #74 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), tptptypes_6_818 a ARG2 → tptptypes_5_802 a ARG2) True % 4.82/4.98 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Eq (tptptypes_6_818 a a_1 → tptptypes_5_802 a a_1) True % 4.82/4.98 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (tptptypes_6_818 a a_1) False) (Eq (tptptypes_5_802 a a_1) True) % 4.82/4.98 Clause #87 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), tptptypes_7_819 a ARG2 → tptptypes_6_818 a ARG2) True % 4.82/4.98 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), Eq (tptptypes_7_819 a a_1 → tptptypes_6_818 a a_1) True % 4.82/4.98 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), Or (Eq (tptptypes_7_819 a a_1) False) (Eq (tptptypes_6_818 a a_1) True) % 4.82/4.98 Clause #101 (by clausification #[11]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), tptptypes_8_823 a ARG2 → tptptypes_7_819 a ARG2) True % 4.82/4.98 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), Eq (tptptypes_8_823 a a_1 → tptptypes_7_819 a a_1) True % 4.82/4.98 Clause #103 (by clausification #[102]): ∀ (a a_1 : Iota), Or (Eq (tptptypes_8_823 a a_1) False) (Eq (tptptypes_7_819 a a_1) True) % 4.82/4.98 Clause #112 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (ARG2 : Iota), tptptypes_9_824 a ARG2 → tptptypes_8_823 a ARG2) True % 4.82/4.98 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (tptptypes_9_824 a a_1 → tptptypes_8_823 a a_1) True % 4.82/4.98 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), Or (Eq (tptptypes_9_824 a a_1) False) (Eq (tptptypes_8_823 a a_1) True) % 4.82/4.98 Clause #131 (by clausification #[18]): Or (Eq (mtvisible c_tptp_member2668_mt) False) % 4.82/4.98 (Eq % 4.82/4.98 (tptptypes_9_824 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.98 c_tptpcol_16_8886) % 4.82/4.98 True) % 4.82/4.98 Clause #227 (by clausification #[56]): ∀ (a : Iota), Eq (∀ (GENLMT : Iota), And (mtvisible a) (genlmt a GENLMT) → mtvisible GENLMT) True % 4.82/4.98 Clause #228 (by clausification #[227]): ∀ (a a_1 : Iota), Eq (And (mtvisible a) (genlmt a a_1) → mtvisible a_1) True % 4.82/4.98 Clause #229 (by clausification #[228]): ∀ (a a_1 : Iota), Or (Eq (And (mtvisible a) (genlmt a a_1)) False) (Eq (mtvisible a_1) True) % 4.82/4.98 Clause #230 (by clausification #[229]): ∀ (a a_1 : Iota), Or (Eq (mtvisible a) True) (Or (Eq (mtvisible a_1) False) (Eq (genlmt a_1 a) False)) % 4.82/4.98 Clause #344 (by clausification #[71]): Eq % 4.82/4.98 (mtvisible c_tptp_spindlecollectormt → % 4.82/4.98 tptptypes_5_802 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.98 c_tptpcol_16_8886) % 4.82/4.98 False % 4.82/4.98 Clause #345 (by clausification #[344]): Eq (mtvisible c_tptp_spindlecollectormt) True % 4.82/4.98 Clause #346 (by clausification #[344]): Eq % 4.82/4.98 (tptptypes_5_802 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.98 c_tptpcol_16_8886) % 4.82/4.98 False % 4.82/4.98 Clause #347 (by superposition #[345, 230]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Or (Eq True False) (Eq (genlmt c_tptp_spindlecollectormt a) False)) % 4.82/4.99 Clause #348 (by clausification #[347]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Eq (genlmt c_tptp_spindlecollectormt a) False) % 4.82/4.99 Clause #350 (by superposition #[348, 15]): Or (Eq (mtvisible c_tptp_member2668_mt) True) (Eq False True) % 4.82/4.99 Clause #355 (by clausification #[350]): Eq (mtvisible c_tptp_member2668_mt) True % 4.82/4.99 Clause #356 (by backward demodulation #[355, 131]): Or (Eq True False) % 4.82/4.99 (Eq % 4.82/4.99 (tptptypes_9_824 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True) % 4.82/4.99 Clause #367 (by clausification #[356]): Eq % 4.82/4.99 (tptptypes_9_824 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True % 4.82/4.99 Clause #368 (by superposition #[367, 114]): Or (Eq True False) % 4.82/4.99 (Eq % 4.82/4.99 (tptptypes_8_823 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True) % 4.82/4.99 Clause #376 (by clausification #[368]): Eq % 4.82/4.99 (tptptypes_8_823 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True % 4.82/4.99 Clause #377 (by superposition #[376, 103]): Or (Eq True False) % 4.82/4.99 (Eq % 4.82/4.99 (tptptypes_7_819 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True) % 4.82/4.99 Clause #378 (by clausification #[377]): Eq % 4.82/4.99 (tptptypes_7_819 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True % 4.82/4.99 Clause #379 (by superposition #[378, 89]): Or (Eq True False) % 4.82/4.99 (Eq % 4.82/4.99 (tptptypes_6_818 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True) % 4.82/4.99 Clause #380 (by clausification #[379]): Eq % 4.82/4.99 (tptptypes_6_818 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True % 4.82/4.99 Clause #381 (by superposition #[380, 76]): Or (Eq True False) % 4.82/4.99 (Eq % 4.82/4.99 (tptptypes_5_802 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True) % 4.82/4.99 Clause #382 (by clausification #[381]): Eq % 4.82/4.99 (tptptypes_5_802 (f_subcollectionofwithrelationfromtypefn c_orientationvector c_orientation c_partiallytangible) % 4.82/4.99 c_tptpcol_16_8886) % 4.82/4.99 True % 4.82/4.99 Clause #383 (by superposition #[382, 346]): Eq True False % 4.82/4.99 Clause #384 (by clausification #[383]): False % 4.82/4.99 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------