%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR061+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.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:17 PM UTC 2025 % Result : Theorem 8.71s 8.92s % Output : Proof 8.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR061+1 : TPTP v9.2.0. Released v3.4.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n006.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 20:20:53 EDT 2025 % 0.14/0.34 % CPUTime : % 8.71/8.92 SZS status Theorem for theBenchmark.p % 8.71/8.92 SZS output start Proof for theBenchmark.p % 8.71/8.92 Clause #4 (by assumption #[]): Eq (genls c_tptpcol_4_106497 c_tptpcol_3_98305) True % 8.71/8.92 Clause #6 (by assumption #[]): Eq (genls c_tptpcol_5_110593 c_tptpcol_4_106497) True % 8.71/8.92 Clause #8 (by assumption #[]): Eq (genls c_tptpcol_6_112641 c_tptpcol_5_110593) True % 8.71/8.92 Clause #10 (by assumption #[]): Eq (genls c_tptpcol_7_113665 c_tptpcol_6_112641) True % 8.71/8.92 Clause #12 (by assumption #[]): Eq (genls c_tptpcol_8_114177 c_tptpcol_7_113665) True % 8.71/8.92 Clause #14 (by assumption #[]): Eq (genls c_tptpcol_4_114689 c_tptpcol_3_114688) True % 8.71/8.92 Clause #16 (by assumption #[]): Eq (genls c_tptpcol_5_114690 c_tptpcol_4_114689) True % 8.71/8.92 Clause #18 (by assumption #[]): Eq (genls c_tptpcol_6_116738 c_tptpcol_5_114690) True % 8.71/8.92 Clause #20 (by assumption #[]): Eq (genls c_tptpcol_7_117762 c_tptpcol_6_116738) True % 8.71/8.92 Clause #22 (by assumption #[]): Eq (genls c_tptpcol_8_117763 c_tptpcol_7_117762) True % 8.71/8.92 Clause #24 (by assumption #[]): Eq (genls c_tptpcol_9_118019 c_tptpcol_8_117763) True % 8.71/8.92 Clause #26 (by assumption #[]): Eq (genls c_tptpcol_10_118020 c_tptpcol_9_118019) True % 8.71/8.92 Clause #28 (by assumption #[]): Eq (genls c_tptpcol_11_118084 c_tptpcol_10_118020) True % 8.71/8.92 Clause #30 (by assumption #[]): Eq (genls c_tptpcol_12_118116 c_tptpcol_11_118084) True % 8.71/8.92 Clause #32 (by assumption #[]): Eq (genls c_tptpcol_13_118117 c_tptpcol_12_118116) True % 8.71/8.92 Clause #34 (by assumption #[]): Eq (genls c_tptpcol_14_118118 c_tptpcol_13_118117) True % 8.71/8.92 Clause #36 (by assumption #[]): Eq (disjointwith c_tptpcol_3_98305 c_tptpcol_3_114688) True % 8.71/8.92 Clause #50 (by assumption #[]): Eq (∀ (X Y : Iota), disjointwith X Y → disjointwith Y X) True % 8.71/8.92 Clause #51 (by assumption #[]): Eq (∀ (ARG1 OLD NEW : Iota), And (disjointwith ARG1 OLD) (genls NEW OLD) → disjointwith ARG1 NEW) True % 8.71/8.92 Clause #52 (by assumption #[]): Eq (∀ (OLD ARG2 NEW : Iota), And (disjointwith OLD ARG2) (genls NEW OLD) → disjointwith NEW ARG2) True % 8.71/8.92 Clause #91 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genls X Y) (genls Y Z) → genls X Z) True % 8.71/8.92 Clause #106 (by assumption #[]): Eq (Not (mtvisible c_timehasnoendmt → disjointwith c_tptpcol_8_114177 c_tptpcol_14_118118)) True % 8.71/8.92 Clause #289 (by clausification #[50]): ∀ (a : Iota), Eq (∀ (Y : Iota), disjointwith a Y → disjointwith Y a) True % 8.71/8.92 Clause #290 (by clausification #[289]): ∀ (a a_1 : Iota), Eq (disjointwith a a_1 → disjointwith a_1 a) True % 8.71/8.92 Clause #291 (by clausification #[290]): ∀ (a a_1 : Iota), Or (Eq (disjointwith a a_1) False) (Eq (disjointwith a_1 a) True) % 8.71/8.92 Clause #292 (by superposition #[291, 36]): Or (Eq (disjointwith c_tptpcol_3_114688 c_tptpcol_3_98305) True) (Eq False True) % 8.71/8.92 Clause #293 (by clausification #[292]): Eq (disjointwith c_tptpcol_3_114688 c_tptpcol_3_98305) True % 8.71/8.92 Clause #301 (by clausification #[51]): ∀ (a : Iota), Eq (∀ (OLD NEW : Iota), And (disjointwith a OLD) (genls NEW OLD) → disjointwith a NEW) True % 8.71/8.92 Clause #302 (by clausification #[301]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a_1) → disjointwith a NEW) True % 8.71/8.92 Clause #303 (by clausification #[302]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a_1) → disjointwith a a_2) True % 8.71/8.92 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (disjointwith a a_1) (genls a_2 a_1)) False) (Eq (disjointwith a a_2) True) % 8.71/8.92 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 : Iota), Or (Eq (disjointwith a a_1) True) (Or (Eq (disjointwith a a_2) False) (Eq (genls a_1 a_2) False)) % 8.71/8.92 Clause #307 (by superposition #[305, 293]): ∀ (a : Iota), % 8.71/8.92 Or (Eq (disjointwith c_tptpcol_3_114688 a) True) (Or (Eq (genls a c_tptpcol_3_98305) False) (Eq False True)) % 8.71/8.92 Clause #336 (by clausification #[52]): ∀ (a : Iota), Eq (∀ (ARG2 NEW : Iota), And (disjointwith a ARG2) (genls NEW a) → disjointwith NEW ARG2) True % 8.71/8.92 Clause #337 (by clausification #[336]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a) → disjointwith NEW a_1) True % 8.71/8.92 Clause #338 (by clausification #[337]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a) → disjointwith a_2 a_1) True % 8.79/8.94 Clause #339 (by clausification #[338]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (disjointwith a a_1) (genls a_2 a)) False) (Eq (disjointwith a_2 a_1) True) % 8.79/8.94 Clause #340 (by clausification #[339]): ∀ (a a_1 a_2 : Iota), Or (Eq (disjointwith a a_1) True) (Or (Eq (disjointwith a_2 a_1) False) (Eq (genls a a_2) False)) % 8.79/8.94 Clause #395 (by clausification #[91]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genls a Y) (genls Y Z) → genls a Z) True % 8.79/8.94 Clause #396 (by clausification #[395]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genls a a_1) (genls a_1 Z) → genls a Z) True % 8.79/8.94 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 : Iota), Eq (And (genls a a_1) (genls a_1 a_2) → genls a a_2) True % 8.79/8.94 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (genls a a_1) (genls a_1 a_2)) False) (Eq (genls a a_2) True) % 8.79/8.94 Clause #399 (by clausification #[398]): ∀ (a a_1 a_2 : Iota), Or (Eq (genls a a_1) True) (Or (Eq (genls a a_2) False) (Eq (genls a_2 a_1) False)) % 8.79/8.94 Clause #400 (by superposition #[399, 6]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_110593 a) True) (Or (Eq (genls c_tptpcol_4_106497 a) False) (Eq False True)) % 8.79/8.94 Clause #404 (by superposition #[399, 22]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_117763 a) True) (Or (Eq (genls c_tptpcol_7_117762 a) False) (Eq False True)) % 8.79/8.94 Clause #405 (by superposition #[399, 10]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_113665 a) True) (Or (Eq (genls c_tptpcol_6_112641 a) False) (Eq False True)) % 8.79/8.94 Clause #408 (by superposition #[399, 26]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_118020 a) True) (Or (Eq (genls c_tptpcol_9_118019 a) False) (Eq False True)) % 8.79/8.94 Clause #409 (by superposition #[399, 24]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_118019 a) True) (Or (Eq (genls c_tptpcol_8_117763 a) False) (Eq False True)) % 8.79/8.94 Clause #410 (by superposition #[399, 28]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_118084 a) True) (Or (Eq (genls c_tptpcol_10_118020 a) False) (Eq False True)) % 8.79/8.94 Clause #411 (by superposition #[399, 18]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_116738 a) True) (Or (Eq (genls c_tptpcol_5_114690 a) False) (Eq False True)) % 8.79/8.94 Clause #412 (by superposition #[399, 20]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_117762 a) True) (Or (Eq (genls c_tptpcol_6_116738 a) False) (Eq False True)) % 8.79/8.94 Clause #413 (by superposition #[399, 16]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_114690 a) True) (Or (Eq (genls c_tptpcol_4_114689 a) False) (Eq False True)) % 8.79/8.94 Clause #414 (by superposition #[399, 34]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_118118 a) True) (Or (Eq (genls c_tptpcol_13_118117 a) False) (Eq False True)) % 8.79/8.94 Clause #415 (by superposition #[399, 32]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_118117 a) True) (Or (Eq (genls c_tptpcol_12_118116 a) False) (Eq False True)) % 8.79/8.94 Clause #478 (by clausification #[106]): Eq (mtvisible c_timehasnoendmt → disjointwith c_tptpcol_8_114177 c_tptpcol_14_118118) False % 8.79/8.94 Clause #480 (by clausification #[478]): Eq (disjointwith c_tptpcol_8_114177 c_tptpcol_14_118118) False % 8.79/8.94 Clause #534 (by clausification #[307]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_3_114688 a) True) (Eq (genls a c_tptpcol_3_98305) False) % 8.79/8.94 Clause #576 (by clausification #[400]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_110593 a) True) (Eq (genls c_tptpcol_4_106497 a) False) % 8.79/8.94 Clause #577 (by superposition #[576, 4]): Or (Eq (genls c_tptpcol_5_110593 c_tptpcol_3_98305) True) (Eq False True) % 8.79/8.94 Clause #579 (by clausification #[577]): Eq (genls c_tptpcol_5_110593 c_tptpcol_3_98305) True % 8.79/8.94 Clause #580 (by superposition #[579, 534]): Or (Eq (disjointwith c_tptpcol_3_114688 c_tptpcol_5_110593) True) (Eq True False) % 8.79/8.94 Clause #596 (by clausification #[580]): Eq (disjointwith c_tptpcol_3_114688 c_tptpcol_5_110593) True % 8.79/8.94 Clause #599 (by superposition #[596, 305]): ∀ (a : Iota), % 8.79/8.94 Or (Eq (disjointwith c_tptpcol_3_114688 a) True) (Or (Eq True False) (Eq (genls a c_tptpcol_5_110593) False)) % 8.79/8.94 Clause #613 (by clausification #[599]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_3_114688 a) True) (Eq (genls a c_tptpcol_5_110593) False) % 8.79/8.94 Clause #628 (by clausification #[404]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_117763 a) True) (Eq (genls c_tptpcol_7_117762 a) False) % 8.79/8.96 Clause #637 (by clausification #[405]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_113665 a) True) (Eq (genls c_tptpcol_6_112641 a) False) % 8.79/8.96 Clause #638 (by superposition #[637, 8]): Or (Eq (genls c_tptpcol_7_113665 c_tptpcol_5_110593) True) (Eq False True) % 8.79/8.96 Clause #640 (by clausification #[638]): Eq (genls c_tptpcol_7_113665 c_tptpcol_5_110593) True % 8.79/8.96 Clause #641 (by superposition #[640, 613]): Or (Eq (disjointwith c_tptpcol_3_114688 c_tptpcol_7_113665) True) (Eq True False) % 8.79/8.96 Clause #643 (by clausification #[641]): Eq (disjointwith c_tptpcol_3_114688 c_tptpcol_7_113665) True % 8.79/8.96 Clause #647 (by superposition #[643, 340]): ∀ (a : Iota), % 8.79/8.96 Or (Eq (disjointwith a c_tptpcol_7_113665) True) (Or (Eq True False) (Eq (genls a c_tptpcol_3_114688) False)) % 8.79/8.96 Clause #702 (by clausification #[408]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_118020 a) True) (Eq (genls c_tptpcol_9_118019 a) False) % 8.79/8.96 Clause #712 (by clausification #[409]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_118019 a) True) (Eq (genls c_tptpcol_8_117763 a) False) % 8.79/8.96 Clause #726 (by clausification #[410]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_118084 a) True) (Eq (genls c_tptpcol_10_118020 a) False) % 8.79/8.96 Clause #745 (by clausification #[411]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_116738 a) True) (Eq (genls c_tptpcol_5_114690 a) False) % 8.79/8.96 Clause #761 (by clausification #[412]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_117762 a) True) (Eq (genls c_tptpcol_6_116738 a) False) % 8.79/8.96 Clause #785 (by clausification #[413]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_114690 a) True) (Eq (genls c_tptpcol_4_114689 a) False) % 8.79/8.96 Clause #786 (by superposition #[785, 14]): Or (Eq (genls c_tptpcol_5_114690 c_tptpcol_3_114688) True) (Eq False True) % 8.79/8.96 Clause #788 (by clausification #[786]): Eq (genls c_tptpcol_5_114690 c_tptpcol_3_114688) True % 8.79/8.96 Clause #791 (by superposition #[788, 745]): Or (Eq (genls c_tptpcol_6_116738 c_tptpcol_3_114688) True) (Eq True False) % 8.79/8.96 Clause #793 (by clausification #[791]): Eq (genls c_tptpcol_6_116738 c_tptpcol_3_114688) True % 8.79/8.96 Clause #796 (by superposition #[793, 761]): Or (Eq (genls c_tptpcol_7_117762 c_tptpcol_3_114688) True) (Eq True False) % 8.79/8.96 Clause #798 (by clausification #[796]): Eq (genls c_tptpcol_7_117762 c_tptpcol_3_114688) True % 8.79/8.96 Clause #801 (by superposition #[798, 628]): Or (Eq (genls c_tptpcol_8_117763 c_tptpcol_3_114688) True) (Eq True False) % 8.79/8.96 Clause #803 (by clausification #[801]): Eq (genls c_tptpcol_8_117763 c_tptpcol_3_114688) True % 8.79/8.96 Clause #806 (by superposition #[803, 712]): Or (Eq (genls c_tptpcol_9_118019 c_tptpcol_3_114688) True) (Eq True False) % 8.79/8.96 Clause #808 (by clausification #[414]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_118118 a) True) (Eq (genls c_tptpcol_13_118117 a) False) % 8.79/8.96 Clause #813 (by clausification #[806]): Eq (genls c_tptpcol_9_118019 c_tptpcol_3_114688) True % 8.79/8.96 Clause #816 (by superposition #[813, 702]): Or (Eq (genls c_tptpcol_10_118020 c_tptpcol_3_114688) True) (Eq True False) % 8.79/8.96 Clause #818 (by clausification #[816]): Eq (genls c_tptpcol_10_118020 c_tptpcol_3_114688) True % 8.79/8.96 Clause #821 (by superposition #[818, 726]): Or (Eq (genls c_tptpcol_11_118084 c_tptpcol_3_114688) True) (Eq True False) % 8.79/8.96 Clause #823 (by clausification #[821]): Eq (genls c_tptpcol_11_118084 c_tptpcol_3_114688) True % 8.79/8.96 Clause #828 (by clausification #[415]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_118117 a) True) (Eq (genls c_tptpcol_12_118116 a) False) % 8.79/8.96 Clause #829 (by superposition #[828, 30]): Or (Eq (genls c_tptpcol_13_118117 c_tptpcol_11_118084) True) (Eq False True) % 8.79/8.96 Clause #850 (by clausification #[829]): Eq (genls c_tptpcol_13_118117 c_tptpcol_11_118084) True % 8.79/8.96 Clause #851 (by superposition #[850, 808]): Or (Eq (genls c_tptpcol_14_118118 c_tptpcol_11_118084) True) (Eq True False) % 8.79/8.96 Clause #853 (by clausification #[851]): Eq (genls c_tptpcol_14_118118 c_tptpcol_11_118084) True % 8.79/8.96 Clause #1634 (by clausification #[647]): ∀ (a : Iota), Or (Eq (disjointwith a c_tptpcol_7_113665) True) (Eq (genls a c_tptpcol_3_114688) False) % 8.79/8.96 Clause #1638 (by superposition #[1634, 823]): Or (Eq (disjointwith c_tptpcol_11_118084 c_tptpcol_7_113665) True) (Eq False True) % 8.79/8.97 Clause #1662 (by clausification #[1638]): Eq (disjointwith c_tptpcol_11_118084 c_tptpcol_7_113665) True % 8.79/8.97 Clause #1664 (by superposition #[1662, 291]): Or (Eq True False) (Eq (disjointwith c_tptpcol_7_113665 c_tptpcol_11_118084) True) % 8.79/8.97 Clause #1667 (by clausification #[1664]): Eq (disjointwith c_tptpcol_7_113665 c_tptpcol_11_118084) True % 8.79/8.97 Clause #1671 (by superposition #[1667, 340]): ∀ (a : Iota), % 8.79/8.97 Or (Eq (disjointwith a c_tptpcol_11_118084) True) (Or (Eq True False) (Eq (genls a c_tptpcol_7_113665) False)) % 8.79/8.97 Clause #1706 (by clausification #[1671]): ∀ (a : Iota), Or (Eq (disjointwith a c_tptpcol_11_118084) True) (Eq (genls a c_tptpcol_7_113665) False) % 8.79/8.97 Clause #1707 (by superposition #[1706, 12]): Or (Eq (disjointwith c_tptpcol_8_114177 c_tptpcol_11_118084) True) (Eq False True) % 8.79/8.97 Clause #1708 (by clausification #[1707]): Eq (disjointwith c_tptpcol_8_114177 c_tptpcol_11_118084) True % 8.79/8.97 Clause #1711 (by superposition #[1708, 305]): ∀ (a : Iota), % 8.79/8.97 Or (Eq (disjointwith c_tptpcol_8_114177 a) True) (Or (Eq True False) (Eq (genls a c_tptpcol_11_118084) False)) % 8.79/8.97 Clause #1726 (by clausification #[1711]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_8_114177 a) True) (Eq (genls a c_tptpcol_11_118084) False) % 8.79/8.97 Clause #1728 (by superposition #[1726, 853]): Or (Eq (disjointwith c_tptpcol_8_114177 c_tptpcol_14_118118) True) (Eq False True) % 8.79/8.97 Clause #1729 (by clausification #[1728]): Eq (disjointwith c_tptpcol_8_114177 c_tptpcol_14_118118) True % 8.79/8.97 Clause #1730 (by superposition #[1729, 480]): Eq True False % 8.79/8.97 Clause #1735 (by clausification #[1730]): False % 8.79/8.97 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------