%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR044+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.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 5.35s 5.51s % Output : Proof 5.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : CSR044+1 : TPTP v9.2.0. Released v3.4.0. % 0.04/0.14 % Command : duper %s % 0.15/0.36 % Computer : n018.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Thu Oct 2 19:35:38 EDT 2025 % 0.15/0.36 % CPUTime : % 5.35/5.51 SZS status Theorem for theBenchmark.p % 5.35/5.51 SZS output start Proof for theBenchmark.p % 5.35/5.51 Clause #0 (by assumption #[]): Eq % 5.35/5.51 (∀ (TERM INDEPCOL PRED DEPCOL : Iota), % 5.35/5.51 And (isa TERM INDEPCOL) (relationallexists PRED INDEPCOL DEPCOL) → % 5.35/5.51 isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL) % 5.35/5.51 True % 5.35/5.51 Clause #7 (by assumption #[]): Eq (genlmt c_tptp_spindleheadmt c_cyclistsmt) True % 5.35/5.51 Clause #8 (by assumption #[]): Eq (genlmt c_tptp_member3633_mt c_tptp_spindleheadmt) True % 5.35/5.51 Clause #9 (by assumption #[]): Eq % 5.35/5.51 (∀ (TERM : Iota), % 5.35/5.51 And (mtvisible c_cyclistsmt) (executionbyfiringsquad TERM) → % 5.35/5.51 tptp_9_720 TERM (f_relationallexistsfn TERM c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.51 True % 5.35/5.51 Clause #10 (by assumption #[]): Eq (mtvisible c_cyclistsmt → relationallexists c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490) True % 5.35/5.51 Clause #11 (by assumption #[]): Eq (executionbyfiringsquad c_tptpexecutionbyfiringsquad_90) True % 5.35/5.51 Clause #27 (by assumption #[]): Eq (∀ (X : Iota), isa X c_tptpcol_16_29490 → tptpcol_16_29490 X) True % 5.35/5.51 Clause #30 (by assumption #[]): Eq (∀ (X : Iota), executionbyfiringsquad X → isa X c_executionbyfiringsquad) True % 5.35/5.51 Clause #42 (by assumption #[]): Eq (∀ (SPECMT GENLMT : Iota), And (mtvisible SPECMT) (genlmt SPECMT GENLMT) → mtvisible GENLMT) True % 5.35/5.51 Clause #45 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genlmt X Y) (genlmt Y Z) → genlmt X Z) True % 5.35/5.51 Clause #56 (by assumption #[]): Eq % 5.35/5.51 (Not % 5.35/5.51 (Exists fun X => % 5.35/5.51 mtvisible c_tptp_member3633_mt → And (tptp_9_720 c_tptpexecutionbyfiringsquad_90 X) (tptpcol_16_29490 X))) % 5.35/5.51 True % 5.35/5.51 Clause #57 (by clausification #[0]): ∀ (a : Iota), % 5.35/5.51 Eq % 5.35/5.51 (∀ (INDEPCOL PRED DEPCOL : Iota), % 5.35/5.51 And (isa a INDEPCOL) (relationallexists PRED INDEPCOL DEPCOL) → % 5.35/5.51 isa (f_relationallexistsfn a PRED INDEPCOL DEPCOL) DEPCOL) % 5.35/5.51 True % 5.35/5.51 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), % 5.35/5.51 Eq % 5.35/5.51 (∀ (PRED DEPCOL : Iota), % 5.35/5.51 And (isa a a_1) (relationallexists PRED a_1 DEPCOL) → isa (f_relationallexistsfn a PRED a_1 DEPCOL) DEPCOL) % 5.35/5.51 True % 5.35/5.51 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), % 5.35/5.51 Eq % 5.35/5.51 (∀ (DEPCOL : Iota), % 5.35/5.51 And (isa a a_1) (relationallexists a_2 a_1 DEPCOL) → isa (f_relationallexistsfn a a_2 a_1 DEPCOL) DEPCOL) % 5.35/5.51 True % 5.35/5.51 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 : Iota), % 5.35/5.51 Eq (And (isa a a_1) (relationallexists a_2 a_1 a_3) → isa (f_relationallexistsfn a a_2 a_1 a_3) a_3) True % 5.35/5.51 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 : Iota), % 5.35/5.51 Or (Eq (And (isa a a_1) (relationallexists a_2 a_1 a_3)) False) % 5.35/5.51 (Eq (isa (f_relationallexistsfn a a_2 a_1 a_3) a_3) True) % 5.35/5.51 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 : Iota), % 5.35/5.51 Or (Eq (isa (f_relationallexistsfn a a_1 a_2 a_3) a_3) True) % 5.35/5.51 (Or (Eq (isa a a_2) False) (Eq (relationallexists a_1 a_2 a_3) False)) % 5.35/5.51 Clause #67 (by clausification #[27]): ∀ (a : Iota), Eq (isa a c_tptpcol_16_29490 → tptpcol_16_29490 a) True % 5.35/5.51 Clause #68 (by clausification #[67]): ∀ (a : Iota), Or (Eq (isa a c_tptpcol_16_29490) False) (Eq (tptpcol_16_29490 a) True) % 5.35/5.51 Clause #75 (by clausification #[9]): ∀ (a : Iota), % 5.35/5.51 Eq % 5.35/5.51 (And (mtvisible c_cyclistsmt) (executionbyfiringsquad a) → % 5.35/5.51 tptp_9_720 a (f_relationallexistsfn a c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.51 True % 5.35/5.51 Clause #76 (by clausification #[75]): ∀ (a : Iota), % 5.35/5.51 Or (Eq (And (mtvisible c_cyclistsmt) (executionbyfiringsquad a)) False) % 5.35/5.51 (Eq (tptp_9_720 a (f_relationallexistsfn a c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) True) % 5.35/5.51 Clause #77 (by clausification #[76]): ∀ (a : Iota), % 5.35/5.51 Or (Eq (tptp_9_720 a (f_relationallexistsfn a c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) True) % 5.35/5.51 (Or (Eq (mtvisible c_cyclistsmt) False) (Eq (executionbyfiringsquad a) False)) % 5.35/5.51 Clause #86 (by clausification #[30]): ∀ (a : Iota), Eq (executionbyfiringsquad a → isa a c_executionbyfiringsquad) True % 5.35/5.51 Clause #87 (by clausification #[86]): ∀ (a : Iota), Or (Eq (executionbyfiringsquad a) False) (Eq (isa a c_executionbyfiringsquad) True) % 5.35/5.51 Clause #88 (by superposition #[87, 11]): Or (Eq (isa c_tptpexecutionbyfiringsquad_90 c_executionbyfiringsquad) True) (Eq False True) % 5.35/5.53 Clause #89 (by clausification #[10]): Or (Eq (mtvisible c_cyclistsmt) False) % 5.35/5.53 (Eq (relationallexists c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490) True) % 5.35/5.53 Clause #90 (by clausification #[88]): Eq (isa c_tptpexecutionbyfiringsquad_90 c_executionbyfiringsquad) True % 5.35/5.53 Clause #92 (by superposition #[90, 62]): ∀ (a a_1 : Iota), % 5.35/5.53 Or (Eq (isa (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 a c_executionbyfiringsquad a_1) a_1) True) % 5.35/5.53 (Or (Eq True False) (Eq (relationallexists a c_executionbyfiringsquad a_1) False)) % 5.35/5.53 Clause #175 (by clausification #[42]): ∀ (a : Iota), Eq (∀ (GENLMT : Iota), And (mtvisible a) (genlmt a GENLMT) → mtvisible GENLMT) True % 5.35/5.53 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), Eq (And (mtvisible a) (genlmt a a_1) → mtvisible a_1) True % 5.35/5.53 Clause #177 (by clausification #[176]): ∀ (a a_1 : Iota), Or (Eq (And (mtvisible a) (genlmt a a_1)) False) (Eq (mtvisible a_1) True) % 5.35/5.53 Clause #178 (by clausification #[177]): ∀ (a a_1 : Iota), Or (Eq (mtvisible a) True) (Or (Eq (mtvisible a_1) False) (Eq (genlmt a_1 a) False)) % 5.35/5.53 Clause #232 (by clausification #[45]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genlmt a Y) (genlmt Y Z) → genlmt a Z) True % 5.35/5.53 Clause #233 (by clausification #[232]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genlmt a a_1) (genlmt a_1 Z) → genlmt a Z) True % 5.35/5.53 Clause #234 (by clausification #[233]): ∀ (a a_1 a_2 : Iota), Eq (And (genlmt a a_1) (genlmt a_1 a_2) → genlmt a a_2) True % 5.35/5.53 Clause #235 (by clausification #[234]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (genlmt a a_1) (genlmt a_1 a_2)) False) (Eq (genlmt a a_2) True) % 5.35/5.53 Clause #236 (by clausification #[235]): ∀ (a a_1 a_2 : Iota), Or (Eq (genlmt a a_1) True) (Or (Eq (genlmt a a_2) False) (Eq (genlmt a_2 a_1) False)) % 5.35/5.53 Clause #240 (by superposition #[236, 8]): ∀ (a : Iota), % 5.35/5.53 Or (Eq (genlmt c_tptp_member3633_mt a) True) (Or (Eq (genlmt c_tptp_spindleheadmt a) False) (Eq False True)) % 5.35/5.53 Clause #306 (by clausification #[240]): ∀ (a : Iota), Or (Eq (genlmt c_tptp_member3633_mt a) True) (Eq (genlmt c_tptp_spindleheadmt a) False) % 5.35/5.53 Clause #307 (by superposition #[306, 7]): Or (Eq (genlmt c_tptp_member3633_mt c_cyclistsmt) True) (Eq False True) % 5.35/5.53 Clause #309 (by clausification #[307]): Eq (genlmt c_tptp_member3633_mt c_cyclistsmt) True % 5.35/5.53 Clause #340 (by clausification #[56]): Eq % 5.35/5.53 (Exists fun X => % 5.35/5.53 mtvisible c_tptp_member3633_mt → And (tptp_9_720 c_tptpexecutionbyfiringsquad_90 X) (tptpcol_16_29490 X)) % 5.35/5.53 False % 5.35/5.53 Clause #341 (by clausification #[340]): ∀ (a : Iota), % 5.35/5.53 Eq (mtvisible c_tptp_member3633_mt → And (tptp_9_720 c_tptpexecutionbyfiringsquad_90 a) (tptpcol_16_29490 a)) False % 5.35/5.53 Clause #342 (by clausification #[341]): Eq (mtvisible c_tptp_member3633_mt) True % 5.35/5.53 Clause #343 (by clausification #[341]): ∀ (a : Iota), Eq (And (tptp_9_720 c_tptpexecutionbyfiringsquad_90 a) (tptpcol_16_29490 a)) False % 5.35/5.53 Clause #344 (by superposition #[342, 178]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Or (Eq True False) (Eq (genlmt c_tptp_member3633_mt a) False)) % 5.35/5.53 Clause #351 (by clausification #[343]): ∀ (a : Iota), Or (Eq (tptp_9_720 c_tptpexecutionbyfiringsquad_90 a) False) (Eq (tptpcol_16_29490 a) False) % 5.35/5.53 Clause #352 (by clausification #[344]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Eq (genlmt c_tptp_member3633_mt a) False) % 5.35/5.53 Clause #355 (by superposition #[352, 309]): Or (Eq (mtvisible c_cyclistsmt) True) (Eq False True) % 5.35/5.53 Clause #362 (by clausification #[355]): Eq (mtvisible c_cyclistsmt) True % 5.35/5.53 Clause #363 (by backward demodulation #[362, 77]): ∀ (a : Iota), % 5.35/5.53 Or (Eq (tptp_9_720 a (f_relationallexistsfn a c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) True) % 5.35/5.53 (Or (Eq True False) (Eq (executionbyfiringsquad a) False)) % 5.35/5.53 Clause #364 (by backward demodulation #[362, 89]): Or (Eq True False) (Eq (relationallexists c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490) True) % 5.35/5.53 Clause #366 (by clausification #[92]): ∀ (a a_1 : Iota), % 5.35/5.53 Or (Eq (isa (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 a c_executionbyfiringsquad a_1) a_1) True) % 5.35/5.54 (Eq (relationallexists a c_executionbyfiringsquad a_1) False) % 5.35/5.54 Clause #369 (by clausification #[364]): Eq (relationallexists c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490) True % 5.35/5.54 Clause #370 (by superposition #[369, 366]): Or % 5.35/5.54 (Eq % 5.35/5.54 (isa % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490) % 5.35/5.54 c_tptpcol_16_29490) % 5.35/5.54 True) % 5.35/5.54 (Eq True False) % 5.35/5.54 Clause #399 (by clausification #[370]): Eq % 5.35/5.54 (isa (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490) % 5.35/5.54 c_tptpcol_16_29490) % 5.35/5.54 True % 5.35/5.54 Clause #400 (by superposition #[399, 68]): Or (Eq True False) % 5.35/5.54 (Eq % 5.35/5.54 (tptpcol_16_29490 % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.54 True) % 5.35/5.54 Clause #406 (by clausification #[400]): Eq % 5.35/5.54 (tptpcol_16_29490 % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.54 True % 5.35/5.54 Clause #419 (by clausification #[363]): ∀ (a : Iota), % 5.35/5.54 Or (Eq (tptp_9_720 a (f_relationallexistsfn a c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) True) % 5.35/5.54 (Eq (executionbyfiringsquad a) False) % 5.35/5.54 Clause #420 (by superposition #[419, 11]): Or % 5.35/5.54 (Eq % 5.35/5.54 (tptp_9_720 c_tptpexecutionbyfiringsquad_90 % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.54 True) % 5.35/5.54 (Eq False True) % 5.35/5.54 Clause #421 (by clausification #[420]): Eq % 5.35/5.54 (tptp_9_720 c_tptpexecutionbyfiringsquad_90 % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.54 True % 5.35/5.54 Clause #422 (by superposition #[421, 351]): Or (Eq True False) % 5.35/5.54 (Eq % 5.35/5.54 (tptpcol_16_29490 % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.54 False) % 5.35/5.54 Clause #425 (by clausification #[422]): Eq % 5.35/5.54 (tptpcol_16_29490 % 5.35/5.54 (f_relationallexistsfn c_tptpexecutionbyfiringsquad_90 c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490)) % 5.35/5.54 False % 5.35/5.54 Clause #426 (by superposition #[425, 406]): Eq False True % 5.35/5.54 Clause #428 (by clausification #[426]): False % 5.35/5.54 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------