%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR040+2 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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:08 PM UTC 2025 % Result : Theorem 116.33s 116.56s % Output : Proof 116.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : CSR040+2 : TPTP v9.2.0. Released v3.4.0. % 0.14/0.14 % Command : duper %s % 0.14/0.36 % Computer : n024.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Thu Oct 2 19:30:08 EDT 2025 % 0.14/0.36 % CPUTime : % 116.33/116.56 SZS status Theorem for theBenchmark.p % 116.33/116.56 SZS output start Proof for theBenchmark.p % 116.33/116.56 Clause #49 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_2_98304 OBJ → tptpcol_1_65536 OBJ) True % 116.33/116.56 Clause #68 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_4_106497 OBJ → tptpcol_3_98305 OBJ) True % 116.33/116.56 Clause #95 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_10_109061 OBJ → tptpcol_9_109060 OBJ) True % 116.33/116.56 Clause #113 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_13_109173 OBJ → tptpcol_12_109157 OBJ) True % 116.33/116.56 Clause #116 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_5_106498 OBJ → tptpcol_4_106497 OBJ) True % 116.33/116.56 Clause #123 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_1_65536 OBJ → tptpcol_0_0 OBJ) True % 116.33/116.56 Clause #150 (by assumption #[]): Eq (∀ (OBJ : Iota), fixedordercollection OBJ → collection OBJ) True % 116.33/116.56 Clause #184 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_8_109059 OBJ → tptpcol_7_108547 OBJ) True % 116.33/116.56 Clause #204 (by assumption #[]): Eq (∀ (OBJ : Iota), firstordercollection OBJ → fixedordercollection OBJ) True % 116.33/116.56 Clause #233 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_3_98305 OBJ → tptpcol_2_98304 OBJ) True % 116.33/116.56 Clause #241 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_9_109060 OBJ → tptpcol_8_109059 OBJ) True % 116.33/116.56 Clause #250 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_14_109181 OBJ → tptpcol_13_109173 OBJ) True % 116.33/116.56 Clause #265 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_15_109185 OBJ → tptpcol_14_109181 OBJ) True % 116.33/116.56 Clause #288 (by assumption #[]): Eq (∀ (OBJ : Iota), Not (And (collection OBJ) (individual OBJ))) True % 116.33/116.56 Clause #340 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_7_108547 OBJ → tptpcol_6_108546 OBJ) True % 116.33/116.56 Clause #342 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_11_109125 OBJ → tptpcol_10_109061 OBJ) True % 116.33/116.56 Clause #359 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_12_109157 OBJ → tptpcol_11_109125 OBJ) True % 116.33/116.56 Clause #444 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_0_0 OBJ → individual OBJ) True % 116.33/116.56 Clause #458 (by assumption #[]): Eq (∀ (OBJ : Iota), tptpcol_6_108546 OBJ → tptpcol_5_106498 OBJ) True % 116.33/116.56 Clause #474 (by assumption #[]): Eq (firstordercollection c_tptpcol_16_62187) True % 116.33/116.56 Clause #1103 (by assumption #[]): Eq % 116.33/116.56 (Not % 116.33/116.56 (mtvisible % 116.33/116.56 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwthedailybulletincompostcardsmar9chtm)) % 116.33/116.56 c_translation_14) → % 116.33/116.56 Not (tptpcol_15_109185 c_tptpcol_16_62187))) % 116.33/116.56 True % 116.33/116.56 Clause #1161 (by clausification #[49]): ∀ (a : Iota), Eq (tptpcol_2_98304 a → tptpcol_1_65536 a) True % 116.33/116.56 Clause #1162 (by clausification #[1161]): ∀ (a : Iota), Or (Eq (tptpcol_2_98304 a) False) (Eq (tptpcol_1_65536 a) True) % 116.33/116.56 Clause #1183 (by clausification #[68]): ∀ (a : Iota), Eq (tptpcol_4_106497 a → tptpcol_3_98305 a) True % 116.33/116.56 Clause #1184 (by clausification #[1183]): ∀ (a : Iota), Or (Eq (tptpcol_4_106497 a) False) (Eq (tptpcol_3_98305 a) True) % 116.33/116.56 Clause #1252 (by clausification #[444]): ∀ (a : Iota), Eq (tptpcol_0_0 a → individual a) True % 116.33/116.56 Clause #1253 (by clausification #[1252]): ∀ (a : Iota), Or (Eq (tptpcol_0_0 a) False) (Eq (individual a) True) % 116.33/116.56 Clause #1299 (by clausification #[95]): ∀ (a : Iota), Eq (tptpcol_10_109061 a → tptpcol_9_109060 a) True % 116.33/116.56 Clause #1300 (by clausification #[1299]): ∀ (a : Iota), Or (Eq (tptpcol_10_109061 a) False) (Eq (tptpcol_9_109060 a) True) % 116.33/116.56 Clause #1381 (by clausification #[113]): ∀ (a : Iota), Eq (tptpcol_13_109173 a → tptpcol_12_109157 a) True % 116.33/116.56 Clause #1382 (by clausification #[1381]): ∀ (a : Iota), Or (Eq (tptpcol_13_109173 a) False) (Eq (tptpcol_12_109157 a) True) % 116.33/116.56 Clause #1393 (by clausification #[116]): ∀ (a : Iota), Eq (tptpcol_5_106498 a → tptpcol_4_106497 a) True % 116.33/116.56 Clause #1394 (by clausification #[1393]): ∀ (a : Iota), Or (Eq (tptpcol_5_106498 a) False) (Eq (tptpcol_4_106497 a) True) % 116.33/116.56 Clause #1428 (by clausification #[123]): ∀ (a : Iota), Eq (tptpcol_1_65536 a → tptpcol_0_0 a) True % 116.33/116.56 Clause #1429 (by clausification #[1428]): ∀ (a : Iota), Or (Eq (tptpcol_1_65536 a) False) (Eq (tptpcol_0_0 a) True) % 116.33/116.56 Clause #1454 (by clausification #[265]): ∀ (a : Iota), Eq (tptpcol_15_109185 a → tptpcol_14_109181 a) True % 116.40/116.63 Clause #1455 (by clausification #[1454]): ∀ (a : Iota), Or (Eq (tptpcol_15_109185 a) False) (Eq (tptpcol_14_109181 a) True) % 116.40/116.63 Clause #1481 (by clausification #[150]): ∀ (a : Iota), Eq (fixedordercollection a → collection a) True % 116.40/116.63 Clause #1482 (by clausification #[1481]): ∀ (a : Iota), Or (Eq (fixedordercollection a) False) (Eq (collection a) True) % 116.40/116.63 Clause #1644 (by clausification #[241]): ∀ (a : Iota), Eq (tptpcol_9_109060 a → tptpcol_8_109059 a) True % 116.40/116.63 Clause #1645 (by clausification #[1644]): ∀ (a : Iota), Or (Eq (tptpcol_9_109060 a) False) (Eq (tptpcol_8_109059 a) True) % 116.40/116.63 Clause #1662 (by clausification #[233]): ∀ (a : Iota), Eq (tptpcol_3_98305 a → tptpcol_2_98304 a) True % 116.40/116.63 Clause #1663 (by clausification #[1662]): ∀ (a : Iota), Or (Eq (tptpcol_3_98305 a) False) (Eq (tptpcol_2_98304 a) True) % 116.40/116.63 Clause #1677 (by clausification #[250]): ∀ (a : Iota), Eq (tptpcol_14_109181 a → tptpcol_13_109173 a) True % 116.40/116.63 Clause #1678 (by clausification #[1677]): ∀ (a : Iota), Or (Eq (tptpcol_14_109181 a) False) (Eq (tptpcol_13_109173 a) True) % 116.40/116.63 Clause #1681 (by clausification #[204]): ∀ (a : Iota), Eq (firstordercollection a → fixedordercollection a) True % 116.40/116.63 Clause #1682 (by clausification #[1681]): ∀ (a : Iota), Or (Eq (firstordercollection a) False) (Eq (fixedordercollection a) True) % 116.40/116.63 Clause #1683 (by superposition #[1682, 474]): Or (Eq (fixedordercollection c_tptpcol_16_62187) True) (Eq False True) % 116.40/116.63 Clause #1684 (by clausification #[184]): ∀ (a : Iota), Eq (tptpcol_8_109059 a → tptpcol_7_108547 a) True % 116.40/116.63 Clause #1685 (by clausification #[1684]): ∀ (a : Iota), Or (Eq (tptpcol_8_109059 a) False) (Eq (tptpcol_7_108547 a) True) % 116.40/116.63 Clause #1686 (by clausification #[1683]): Eq (fixedordercollection c_tptpcol_16_62187) True % 116.40/116.63 Clause #1687 (by superposition #[1686, 1482]): Or (Eq True False) (Eq (collection c_tptpcol_16_62187) True) % 116.40/116.63 Clause #1688 (by clausification #[1687]): Eq (collection c_tptpcol_16_62187) True % 116.40/116.63 Clause #1699 (by clausification #[340]): ∀ (a : Iota), Eq (tptpcol_7_108547 a → tptpcol_6_108546 a) True % 116.40/116.63 Clause #1700 (by clausification #[1699]): ∀ (a : Iota), Or (Eq (tptpcol_7_108547 a) False) (Eq (tptpcol_6_108546 a) True) % 116.40/116.63 Clause #1706 (by clausification #[342]): ∀ (a : Iota), Eq (tptpcol_11_109125 a → tptpcol_10_109061 a) True % 116.40/116.63 Clause #1707 (by clausification #[1706]): ∀ (a : Iota), Or (Eq (tptpcol_11_109125 a) False) (Eq (tptpcol_10_109061 a) True) % 116.40/116.63 Clause #1985 (by clausification #[288]): ∀ (a : Iota), Eq (Not (And (collection a) (individual a))) True % 116.40/116.63 Clause #1986 (by clausification #[1985]): ∀ (a : Iota), Eq (And (collection a) (individual a)) False % 116.40/116.63 Clause #1987 (by clausification #[1986]): ∀ (a : Iota), Or (Eq (collection a) False) (Eq (individual a) False) % 116.40/116.63 Clause #1988 (by superposition #[1987, 1688]): Or (Eq (individual c_tptpcol_16_62187) False) (Eq False True) % 116.40/116.63 Clause #2164 (by clausification #[359]): ∀ (a : Iota), Eq (tptpcol_12_109157 a → tptpcol_11_109125 a) True % 116.40/116.63 Clause #2165 (by clausification #[2164]): ∀ (a : Iota), Or (Eq (tptpcol_12_109157 a) False) (Eq (tptpcol_11_109125 a) True) % 116.40/116.63 Clause #2242 (by clausification #[1988]): Eq (individual c_tptpcol_16_62187) False % 116.40/116.63 Clause #2642 (by clausification #[458]): ∀ (a : Iota), Eq (tptpcol_6_108546 a → tptpcol_5_106498 a) True % 116.40/116.63 Clause #2643 (by clausification #[2642]): ∀ (a : Iota), Or (Eq (tptpcol_6_108546 a) False) (Eq (tptpcol_5_106498 a) True) % 116.40/116.63 Clause #9147 (by clausification #[1103]): Eq % 116.40/116.63 (mtvisible % 116.40/116.63 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwthedailybulletincompostcardsmar9chtm)) % 116.40/116.63 c_translation_14) → % 116.40/116.63 Not (tptpcol_15_109185 c_tptpcol_16_62187)) % 116.40/116.63 False % 116.40/116.63 Clause #9149 (by clausification #[9147]): Eq (Not (tptpcol_15_109185 c_tptpcol_16_62187)) False % 116.40/116.63 Clause #9151 (by clausification #[9149]): Eq (tptpcol_15_109185 c_tptpcol_16_62187) True % 116.40/116.63 Clause #9152 (by superposition #[9151, 1455]): Or (Eq True False) (Eq (tptpcol_14_109181 c_tptpcol_16_62187) True) % 116.40/116.63 Clause #9168 (by clausification #[9152]): Eq (tptpcol_14_109181 c_tptpcol_16_62187) True % 116.40/116.63 Clause #9169 (by superposition #[9168, 1678]): Or (Eq True False) (Eq (tptpcol_13_109173 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9171 (by clausification #[9169]): Eq (tptpcol_13_109173 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9172 (by superposition #[9171, 1382]): Or (Eq True False) (Eq (tptpcol_12_109157 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9174 (by clausification #[9172]): Eq (tptpcol_12_109157 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9175 (by superposition #[9174, 2165]): Or (Eq True False) (Eq (tptpcol_11_109125 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9177 (by clausification #[9175]): Eq (tptpcol_11_109125 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9178 (by superposition #[9177, 1707]): Or (Eq True False) (Eq (tptpcol_10_109061 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9181 (by clausification #[9178]): Eq (tptpcol_10_109061 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9182 (by superposition #[9181, 1300]): Or (Eq True False) (Eq (tptpcol_9_109060 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9184 (by clausification #[9182]): Eq (tptpcol_9_109060 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9185 (by superposition #[9184, 1645]): Or (Eq True False) (Eq (tptpcol_8_109059 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9187 (by clausification #[9185]): Eq (tptpcol_8_109059 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9188 (by superposition #[9187, 1685]): Or (Eq True False) (Eq (tptpcol_7_108547 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9190 (by clausification #[9188]): Eq (tptpcol_7_108547 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9191 (by superposition #[9190, 1700]): Or (Eq True False) (Eq (tptpcol_6_108546 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9193 (by clausification #[9191]): Eq (tptpcol_6_108546 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9194 (by superposition #[9193, 2643]): Or (Eq True False) (Eq (tptpcol_5_106498 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9197 (by clausification #[9194]): Eq (tptpcol_5_106498 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9198 (by superposition #[9197, 1394]): Or (Eq True False) (Eq (tptpcol_4_106497 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9200 (by clausification #[9198]): Eq (tptpcol_4_106497 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9201 (by superposition #[9200, 1184]): Or (Eq True False) (Eq (tptpcol_3_98305 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9203 (by clausification #[9201]): Eq (tptpcol_3_98305 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9204 (by superposition #[9203, 1663]): Or (Eq True False) (Eq (tptpcol_2_98304 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9208 (by clausification #[9204]): Eq (tptpcol_2_98304 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9209 (by superposition #[9208, 1162]): Or (Eq True False) (Eq (tptpcol_1_65536 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9212 (by clausification #[9209]): Eq (tptpcol_1_65536 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9213 (by superposition #[9212, 1429]): Or (Eq True False) (Eq (tptpcol_0_0 c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9215 (by clausification #[9213]): Eq (tptpcol_0_0 c_tptpcol_16_62187) True % 116.52/116.72 Clause #9216 (by superposition #[9215, 1253]): Or (Eq True False) (Eq (individual c_tptpcol_16_62187) True) % 116.52/116.72 Clause #9218 (by clausification #[9216]): Eq (individual c_tptpcol_16_62187) True % 116.52/116.72 Clause #9219 (by superposition #[9218, 2242]): Eq True False % 116.52/116.72 Clause #9223 (by clausification #[9219]): False % 116.52/116.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------