%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR038+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:07 PM UTC 2025 % Result : Theorem 4.09s 4.25s % Output : Proof 4.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : CSR038+1 : TPTP v9.2.0. Released v3.4.0. % 0.06/0.13 % Command : duper %s % 0.14/0.35 % Computer : n027.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 20:42:23 EDT 2025 % 0.14/0.35 % CPUTime : % 4.09/4.25 SZS status Theorem for theBenchmark.p % 4.09/4.25 SZS output start Proof for theBenchmark.p % 4.09/4.25 Clause #0 (by assumption #[]): Eq % 4.09/4.25 (∀ (TERM INDEPCOL PRED DEPCOL : Iota), % 4.09/4.25 And (isa TERM INDEPCOL) (relationexistsall PRED DEPCOL INDEPCOL) → % 4.09/4.25 isa (f_relationexistsallfn TERM PRED DEPCOL INDEPCOL) DEPCOL) % 4.09/4.25 True % 4.09/4.25 Clause #5 (by assumption #[]): Eq % 4.09/4.25 (∀ (TERM : Iota), % 4.09/4.25 isa TERM (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription) → % 4.09/4.25 tptp_8_968 % 4.09/4.25 (f_relationexistsallfn TERM c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.25 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.25 TERM) % 4.09/4.25 True % 4.09/4.25 Clause #6 (by assumption #[]): Eq % 4.09/4.25 (relationexistsall c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.25 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.25 True % 4.09/4.25 Clause #7 (by assumption #[]): Eq % 4.09/4.25 (isa c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 % 4.09/4.25 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.25 True % 4.09/4.25 Clause #37 (by assumption #[]): Eq (∀ (X : Iota), isa X c_tptpcol_16_7738 → tptpcol_16_7738 X) True % 4.09/4.25 Clause #64 (by assumption #[]): Eq % 4.09/4.25 (Not % 4.09/4.25 (Exists fun X => % 4.09/4.25 mtvisible c_knowledgefragmentd3mt → % 4.09/4.25 And % 4.09/4.25 (tptp_8_968 X % 4.09/4.25 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.25 (tptpcol_16_7738 X))) % 4.09/4.25 True % 4.09/4.25 Clause #65 (by clausification #[0]): ∀ (a : Iota), % 4.09/4.25 Eq % 4.09/4.25 (∀ (INDEPCOL PRED DEPCOL : Iota), % 4.09/4.25 And (isa a INDEPCOL) (relationexistsall PRED DEPCOL INDEPCOL) → % 4.09/4.25 isa (f_relationexistsallfn a PRED DEPCOL INDEPCOL) DEPCOL) % 4.09/4.25 True % 4.09/4.25 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), % 4.09/4.25 Eq % 4.09/4.25 (∀ (PRED DEPCOL : Iota), % 4.09/4.25 And (isa a a_1) (relationexistsall PRED DEPCOL a_1) → isa (f_relationexistsallfn a PRED DEPCOL a_1) DEPCOL) % 4.09/4.25 True % 4.09/4.25 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 : Iota), % 4.09/4.25 Eq % 4.09/4.25 (∀ (DEPCOL : Iota), % 4.09/4.25 And (isa a a_1) (relationexistsall a_2 DEPCOL a_1) → isa (f_relationexistsallfn a a_2 DEPCOL a_1) DEPCOL) % 4.09/4.25 True % 4.09/4.25 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 : Iota), % 4.09/4.25 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.09/4.25 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 : Iota), % 4.09/4.25 Or (Eq (And (isa a a_1) (relationexistsall a_2 a_3 a_1)) False) % 4.09/4.25 (Eq (isa (f_relationexistsallfn a a_2 a_3 a_1) a_3) True) % 4.09/4.25 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 a_3 : Iota), % 4.09/4.25 Or (Eq (isa (f_relationexistsallfn a a_1 a_2 a_3) a_2) True) % 4.09/4.25 (Or (Eq (isa a a_3) False) (Eq (relationexistsall a_1 a_2 a_3) False)) % 4.09/4.25 Clause #73 (by clausification #[37]): ∀ (a : Iota), Eq (isa a c_tptpcol_16_7738 → tptpcol_16_7738 a) True % 4.09/4.25 Clause #74 (by clausification #[73]): ∀ (a : Iota), Or (Eq (isa a c_tptpcol_16_7738) False) (Eq (tptpcol_16_7738 a) True) % 4.09/4.25 Clause #77 (by clausification #[5]): ∀ (a : Iota), % 4.09/4.25 Eq % 4.09/4.25 (isa a (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription) → % 4.09/4.25 tptp_8_968 % 4.09/4.25 (f_relationexistsallfn a c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.25 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.25 a) % 4.09/4.25 True % 4.09/4.25 Clause #78 (by clausification #[77]): ∀ (a : Iota), % 4.09/4.25 Or % 4.09/4.25 (Eq (isa a (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.25 False) % 4.09/4.25 (Eq % 4.09/4.25 (tptp_8_968 % 4.09/4.25 (f_relationexistsallfn a c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.25 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.25 a) % 4.09/4.25 True) % 4.09/4.25 Clause #105 (by superposition #[7, 78]): Or % 4.09/4.25 (Eq % 4.09/4.25 (tptp_8_968 % 4.09/4.25 (f_relationexistsallfn % 4.09/4.25 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 % 4.09/4.25 c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.26 True) % 4.09/4.26 (Eq False True) % 4.09/4.26 Clause #106 (by superposition #[7, 70]): ∀ (a a_1 : Iota), % 4.09/4.26 Or % 4.09/4.26 (Eq % 4.09/4.26 (isa % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 a a_1 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 a_1) % 4.09/4.26 True) % 4.09/4.26 (Or % 4.09/4.26 (Eq % 4.09/4.26 (relationexistsall a a_1 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 False) % 4.09/4.26 (Eq False True)) % 4.09/4.26 Clause #293 (by clausification #[64]): Eq % 4.09/4.26 (Exists fun X => % 4.09/4.26 mtvisible c_knowledgefragmentd3mt → % 4.09/4.26 And % 4.09/4.26 (tptp_8_968 X % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.26 (tptpcol_16_7738 X)) % 4.09/4.26 False % 4.09/4.26 Clause #294 (by clausification #[293]): ∀ (a : Iota), % 4.09/4.26 Eq % 4.09/4.26 (mtvisible c_knowledgefragmentd3mt → % 4.09/4.26 And % 4.09/4.26 (tptp_8_968 a % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.26 (tptpcol_16_7738 a)) % 4.09/4.26 False % 4.09/4.26 Clause #296 (by clausification #[294]): ∀ (a : Iota), % 4.09/4.26 Eq % 4.09/4.26 (And % 4.09/4.26 (tptp_8_968 a % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.26 (tptpcol_16_7738 a)) % 4.09/4.26 False % 4.09/4.26 Clause #302 (by clausification #[296]): ∀ (a : Iota), % 4.09/4.26 Or % 4.09/4.26 (Eq % 4.09/4.26 (tptp_8_968 a % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.26 False) % 4.09/4.26 (Eq (tptpcol_16_7738 a) False) % 4.09/4.26 Clause #309 (by clausification #[105]): Eq % 4.09/4.26 (tptp_8_968 % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 c_tptp_8_968 % 4.09/4.26 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804) % 4.09/4.26 True % 4.09/4.26 Clause #310 (by superposition #[309, 302]): Or (Eq True False) % 4.09/4.26 (Eq % 4.09/4.26 (tptpcol_16_7738 % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 % 4.09/4.26 c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription))) % 4.09/4.26 False) % 4.09/4.26 Clause #317 (by clausification #[310]): Eq % 4.09/4.26 (tptpcol_16_7738 % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 c_tptp_8_968 % 4.09/4.26 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription))) % 4.09/4.26 False % 4.09/4.26 Clause #329 (by clausification #[106]): ∀ (a a_1 : Iota), % 4.09/4.26 Or % 4.09/4.26 (Eq % 4.09/4.26 (isa % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 a a_1 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 a_1) % 4.09/4.26 True) % 4.09/4.26 (Eq % 4.09/4.26 (relationexistsall a a_1 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 False) % 4.09/4.26 Clause #330 (by superposition #[329, 6]): Or % 4.09/4.26 (Eq % 4.09/4.26 (isa % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 % 4.09/4.26 c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 c_tptpcol_16_7738) % 4.09/4.26 True) % 4.09/4.26 (Eq False True) % 4.09/4.26 Clause #331 (by clausification #[330]): Eq % 4.09/4.26 (isa % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 c_tptp_8_968 % 4.09/4.26 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription)) % 4.09/4.26 c_tptpcol_16_7738) % 4.09/4.26 True % 4.09/4.26 Clause #332 (by superposition #[331, 74]): Or (Eq True False) % 4.09/4.26 (Eq % 4.09/4.26 (tptpcol_16_7738 % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 % 4.09/4.26 c_tptp_8_968 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription))) % 4.09/4.26 True) % 4.09/4.26 Clause #338 (by clausification #[332]): Eq % 4.09/4.26 (tptpcol_16_7738 % 4.09/4.26 (f_relationexistsallfn % 4.09/4.26 c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 c_tptp_8_968 % 4.09/4.26 c_tptpcol_16_7738 % 4.09/4.26 (f_subcollectionofwithrelationtotypefn c_issuingaprescription c_products c_correctivelensprescription))) % 4.09/4.26 True % 4.09/4.26 Clause #339 (by superposition #[338, 317]): Eq True False % 4.09/4.26 Clause #341 (by clausification #[339]): False % 4.09/4.26 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------