%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR049+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:12 PM UTC 2025 % Result : Theorem 27.53s 27.69s % Output : Proof 27.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : CSR049+1 : TPTP v9.2.0. Released v3.4.0. % 0.09/0.15 % Command : duper %s % 0.14/0.36 % Computer : n019.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:51:38 EDT 2025 % 0.14/0.37 % CPUTime : % 27.53/27.69 SZS status Theorem for theBenchmark.p % 27.53/27.69 SZS output start Proof for theBenchmark.p % 27.53/27.69 Clause #6 (by assumption #[]): Eq (genls c_tptpcol_2_2 c_tptpcol_1_1) True % 27.53/27.69 Clause #8 (by assumption #[]): Eq (genls c_tptpcol_3_16386 c_tptpcol_2_2) True % 27.53/27.69 Clause #10 (by assumption #[]): Eq (genls c_tptpcol_4_24578 c_tptpcol_3_16386) True % 27.53/27.69 Clause #12 (by assumption #[]): Eq (genls c_tptpcol_5_24579 c_tptpcol_4_24578) True % 27.53/27.69 Clause #14 (by assumption #[]): Eq (genls c_tptpcol_6_26627 c_tptpcol_5_24579) True % 27.53/27.69 Clause #16 (by assumption #[]): Eq (genls c_tptpcol_7_26628 c_tptpcol_6_26627) True % 27.53/27.69 Clause #18 (by assumption #[]): Eq (genls c_tptpcol_8_26629 c_tptpcol_7_26628) True % 27.53/27.69 Clause #20 (by assumption #[]): Eq (genls c_tptpcol_9_26885 c_tptpcol_8_26629) True % 27.53/27.69 Clause #22 (by assumption #[]): Eq (genls c_tptpcol_10_26886 c_tptpcol_9_26885) True % 27.53/27.69 Clause #24 (by assumption #[]): Eq (genls c_tptpcol_11_26887 c_tptpcol_10_26886) True % 27.53/27.69 Clause #26 (by assumption #[]): Eq (genls c_tptpcol_12_26919 c_tptpcol_11_26887) True % 27.53/27.69 Clause #28 (by assumption #[]): Eq (genls c_tptpcol_13_26920 c_tptpcol_12_26919) True % 27.53/27.69 Clause #30 (by assumption #[]): Eq (genls c_tptpcol_14_26921 c_tptpcol_13_26920) True % 27.53/27.69 Clause #32 (by assumption #[]): Eq (genls c_tptpcol_15_26925 c_tptpcol_14_26921) True % 27.53/27.69 Clause #34 (by assumption #[]): Eq (genls c_tptpcol_16_26926 c_tptpcol_15_26925) True % 27.53/27.69 Clause #36 (by assumption #[]): Eq (genls c_tptpcol_2_65537 c_tptpcol_1_65536) True % 27.53/27.69 Clause #38 (by assumption #[]): Eq (genls c_tptpcol_3_81921 c_tptpcol_2_65537) True % 27.53/27.69 Clause #40 (by assumption #[]): Eq (genls c_tptpcol_4_90113 c_tptpcol_3_81921) True % 27.53/27.69 Clause #42 (by assumption #[]): Eq (genls c_tptpcol_5_90114 c_tptpcol_4_90113) True % 27.53/27.69 Clause #44 (by assumption #[]): Eq (genls c_tptpcol_6_92162 c_tptpcol_5_90114) True % 27.53/27.69 Clause #46 (by assumption #[]): Eq (genls c_tptpcol_7_92163 c_tptpcol_6_92162) True % 27.53/27.69 Clause #48 (by assumption #[]): Eq (genls c_tptpcol_8_92164 c_tptpcol_7_92163) True % 27.53/27.69 Clause #50 (by assumption #[]): Eq (genls c_tptpcol_9_92165 c_tptpcol_8_92164) True % 27.53/27.69 Clause #52 (by assumption #[]): Eq (genls c_tptpcol_10_92166 c_tptpcol_9_92165) True % 27.53/27.69 Clause #54 (by assumption #[]): Eq (genls c_tptpcol_11_92230 c_tptpcol_10_92166) True % 27.53/27.69 Clause #56 (by assumption #[]): Eq (genls c_tptpcol_12_92262 c_tptpcol_11_92230) True % 27.53/27.69 Clause #58 (by assumption #[]): Eq (genls c_tptpcol_13_92263 c_tptpcol_12_92262) True % 27.53/27.69 Clause #60 (by assumption #[]): Eq (genls c_tptpcol_14_92264 c_tptpcol_13_92263) True % 27.53/27.69 Clause #62 (by assumption #[]): Eq (genls c_tptpcol_15_92268 c_tptpcol_14_92264) True % 27.53/27.69 Clause #64 (by assumption #[]): Eq (genls c_tptpcol_16_92269 c_tptpcol_15_92268) True % 27.53/27.69 Clause #66 (by assumption #[]): Eq (disjointwith c_tptpcol_1_1 c_tptpcol_1_65536) True % 27.53/27.69 Clause #80 (by assumption #[]): Eq (∀ (X Y : Iota), disjointwith X Y → disjointwith Y X) True % 27.53/27.69 Clause #81 (by assumption #[]): Eq (∀ (ARG1 OLD NEW : Iota), And (disjointwith ARG1 OLD) (genls NEW OLD) → disjointwith ARG1 NEW) True % 27.53/27.69 Clause #82 (by assumption #[]): Eq (∀ (OLD ARG2 NEW : Iota), And (disjointwith OLD ARG2) (genls NEW OLD) → disjointwith NEW ARG2) True % 27.53/27.69 Clause #149 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genls X Y) (genls Y Z) → genls X Z) True % 27.53/27.69 Clause #164 (by assumption #[]): Eq (Not (mtvisible c_unitedstatesgeographypeoplemt → disjointwith c_tptpcol_16_26926 c_tptpcol_16_92269)) True % 27.53/27.69 Clause #426 (by clausification #[80]): ∀ (a : Iota), Eq (∀ (Y : Iota), disjointwith a Y → disjointwith Y a) True % 27.53/27.69 Clause #427 (by clausification #[426]): ∀ (a a_1 : Iota), Eq (disjointwith a a_1 → disjointwith a_1 a) True % 27.53/27.69 Clause #428 (by clausification #[427]): ∀ (a a_1 : Iota), Or (Eq (disjointwith a a_1) False) (Eq (disjointwith a_1 a) True) % 27.53/27.69 Clause #429 (by superposition #[428, 66]): Or (Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_1_1) True) (Eq False True) % 27.53/27.69 Clause #440 (by clausification #[81]): ∀ (a : Iota), Eq (∀ (OLD NEW : Iota), And (disjointwith a OLD) (genls NEW OLD) → disjointwith a NEW) True % 27.53/27.69 Clause #441 (by clausification #[440]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a_1) → disjointwith a NEW) True % 27.53/27.72 Clause #442 (by clausification #[441]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a_1) → disjointwith a a_2) True % 27.53/27.72 Clause #443 (by clausification #[442]): ∀ (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) % 27.53/27.72 Clause #444 (by clausification #[443]): ∀ (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)) % 27.53/27.72 Clause #452 (by clausification #[82]): ∀ (a : Iota), Eq (∀ (ARG2 NEW : Iota), And (disjointwith a ARG2) (genls NEW a) → disjointwith NEW ARG2) True % 27.53/27.72 Clause #453 (by clausification #[452]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a) → disjointwith NEW a_1) True % 27.53/27.72 Clause #454 (by clausification #[453]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a) → disjointwith a_2 a_1) True % 27.53/27.72 Clause #455 (by clausification #[454]): ∀ (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) % 27.53/27.72 Clause #456 (by clausification #[455]): ∀ (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)) % 27.53/27.72 Clause #478 (by clausification #[429]): Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_1_1) True % 27.53/27.72 Clause #483 (by superposition #[478, 444]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_1_65536 a) True) (Or (Eq True False) (Eq (genls a c_tptpcol_1_1) False)) % 27.53/27.72 Clause #638 (by clausification #[164]): Eq (mtvisible c_unitedstatesgeographypeoplemt → disjointwith c_tptpcol_16_26926 c_tptpcol_16_92269) False % 27.53/27.72 Clause #640 (by clausification #[638]): Eq (disjointwith c_tptpcol_16_26926 c_tptpcol_16_92269) False % 27.53/27.72 Clause #652 (by clausification #[149]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genls a Y) (genls Y Z) → genls a Z) True % 27.53/27.72 Clause #653 (by clausification #[652]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genls a a_1) (genls a_1 Z) → genls a Z) True % 27.53/27.72 Clause #654 (by clausification #[653]): ∀ (a a_1 a_2 : Iota), Eq (And (genls a a_1) (genls a_1 a_2) → genls a a_2) True % 27.53/27.72 Clause #655 (by clausification #[654]): ∀ (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) % 27.53/27.72 Clause #656 (by clausification #[655]): ∀ (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)) % 27.53/27.72 Clause #657 (by superposition #[656, 30]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_26921 a) True) (Or (Eq (genls c_tptpcol_13_26920 a) False) (Eq False True)) % 27.53/27.72 Clause #658 (by superposition #[656, 14]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_26627 a) True) (Or (Eq (genls c_tptpcol_5_24579 a) False) (Eq False True)) % 27.53/27.72 Clause #659 (by superposition #[656, 12]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_24579 a) True) (Or (Eq (genls c_tptpcol_4_24578 a) False) (Eq False True)) % 27.53/27.72 Clause #660 (by superposition #[656, 10]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_24578 a) True) (Or (Eq (genls c_tptpcol_3_16386 a) False) (Eq False True)) % 27.53/27.72 Clause #661 (by superposition #[656, 8]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_16386 a) True) (Or (Eq (genls c_tptpcol_2_2 a) False) (Eq False True)) % 27.53/27.72 Clause #663 (by superposition #[656, 22]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_26886 a) True) (Or (Eq (genls c_tptpcol_9_26885 a) False) (Eq False True)) % 27.53/27.72 Clause #664 (by superposition #[656, 20]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_26885 a) True) (Or (Eq (genls c_tptpcol_8_26629 a) False) (Eq False True)) % 27.53/27.72 Clause #665 (by superposition #[656, 26]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_26919 a) True) (Or (Eq (genls c_tptpcol_11_26887 a) False) (Eq False True)) % 27.53/27.72 Clause #666 (by superposition #[656, 24]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_26887 a) True) (Or (Eq (genls c_tptpcol_10_26886 a) False) (Eq False True)) % 27.53/27.72 Clause #667 (by superposition #[656, 18]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_26629 a) True) (Or (Eq (genls c_tptpcol_7_26628 a) False) (Eq False True)) % 27.53/27.72 Clause #668 (by superposition #[656, 28]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_26920 a) True) (Or (Eq (genls c_tptpcol_12_26919 a) False) (Eq False True)) % 27.53/27.74 Clause #669 (by superposition #[656, 16]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_26628 a) True) (Or (Eq (genls c_tptpcol_6_26627 a) False) (Eq False True)) % 27.53/27.74 Clause #670 (by superposition #[656, 64]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_16_92269 a) True) (Or (Eq (genls c_tptpcol_15_92268 a) False) (Eq False True)) % 27.53/27.74 Clause #671 (by superposition #[656, 62]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_92268 a) True) (Or (Eq (genls c_tptpcol_14_92264 a) False) (Eq False True)) % 27.53/27.74 Clause #672 (by superposition #[656, 60]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_92264 a) True) (Or (Eq (genls c_tptpcol_13_92263 a) False) (Eq False True)) % 27.53/27.74 Clause #673 (by superposition #[656, 58]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_92263 a) True) (Or (Eq (genls c_tptpcol_12_92262 a) False) (Eq False True)) % 27.53/27.74 Clause #674 (by superposition #[656, 56]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_92262 a) True) (Or (Eq (genls c_tptpcol_11_92230 a) False) (Eq False True)) % 27.53/27.74 Clause #675 (by superposition #[656, 46]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_92163 a) True) (Or (Eq (genls c_tptpcol_6_92162 a) False) (Eq False True)) % 27.53/27.74 Clause #676 (by superposition #[656, 42]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_90114 a) True) (Or (Eq (genls c_tptpcol_4_90113 a) False) (Eq False True)) % 27.53/27.74 Clause #677 (by superposition #[656, 44]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_92162 a) True) (Or (Eq (genls c_tptpcol_5_90114 a) False) (Eq False True)) % 27.53/27.74 Clause #678 (by superposition #[656, 40]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_90113 a) True) (Or (Eq (genls c_tptpcol_3_81921 a) False) (Eq False True)) % 27.53/27.74 Clause #679 (by superposition #[656, 54]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_92230 a) True) (Or (Eq (genls c_tptpcol_10_92166 a) False) (Eq False True)) % 27.53/27.74 Clause #680 (by superposition #[656, 52]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_92166 a) True) (Or (Eq (genls c_tptpcol_9_92165 a) False) (Eq False True)) % 27.53/27.74 Clause #681 (by superposition #[656, 38]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_81921 a) True) (Or (Eq (genls c_tptpcol_2_65537 a) False) (Eq False True)) % 27.53/27.74 Clause #683 (by superposition #[656, 50]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_92165 a) True) (Or (Eq (genls c_tptpcol_8_92164 a) False) (Eq False True)) % 27.53/27.74 Clause #684 (by superposition #[656, 34]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_16_26926 a) True) (Or (Eq (genls c_tptpcol_15_26925 a) False) (Eq False True)) % 27.53/27.74 Clause #685 (by superposition #[656, 48]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_92164 a) True) (Or (Eq (genls c_tptpcol_7_92163 a) False) (Eq False True)) % 27.53/27.74 Clause #686 (by superposition #[656, 32]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_26925 a) True) (Or (Eq (genls c_tptpcol_14_26921 a) False) (Eq False True)) % 27.53/27.74 Clause #806 (by clausification #[483]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_1_65536 a) True) (Eq (genls a c_tptpcol_1_1) False) % 27.53/27.74 Clause #821 (by clausification #[657]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_26921 a) True) (Eq (genls c_tptpcol_13_26920 a) False) % 27.53/27.74 Clause #831 (by clausification #[658]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_26627 a) True) (Eq (genls c_tptpcol_5_24579 a) False) % 27.53/27.74 Clause #843 (by clausification #[659]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_24579 a) True) (Eq (genls c_tptpcol_4_24578 a) False) % 27.53/27.74 Clause #853 (by clausification #[660]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_24578 a) True) (Eq (genls c_tptpcol_3_16386 a) False) % 27.53/27.74 Clause #867 (by clausification #[661]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_16386 a) True) (Eq (genls c_tptpcol_2_2 a) False) % 27.53/27.74 Clause #868 (by superposition #[867, 6]): Or (Eq (genls c_tptpcol_3_16386 c_tptpcol_1_1) True) (Eq False True) % 27.53/27.74 Clause #870 (by clausification #[868]): Eq (genls c_tptpcol_3_16386 c_tptpcol_1_1) True % 27.53/27.74 Clause #873 (by superposition #[870, 853]): Or (Eq (genls c_tptpcol_4_24578 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.74 Clause #875 (by clausification #[873]): Eq (genls c_tptpcol_4_24578 c_tptpcol_1_1) True % 27.53/27.74 Clause #878 (by superposition #[875, 843]): Or (Eq (genls c_tptpcol_5_24579 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #880 (by clausification #[878]): Eq (genls c_tptpcol_5_24579 c_tptpcol_1_1) True % 27.53/27.76 Clause #883 (by superposition #[880, 831]): Or (Eq (genls c_tptpcol_6_26627 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #885 (by clausification #[883]): Eq (genls c_tptpcol_6_26627 c_tptpcol_1_1) True % 27.53/27.76 Clause #901 (by clausification #[663]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_26886 a) True) (Eq (genls c_tptpcol_9_26885 a) False) % 27.53/27.76 Clause #916 (by clausification #[664]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_26885 a) True) (Eq (genls c_tptpcol_8_26629 a) False) % 27.53/27.76 Clause #934 (by clausification #[665]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_26919 a) True) (Eq (genls c_tptpcol_11_26887 a) False) % 27.53/27.76 Clause #939 (by clausification #[666]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_26887 a) True) (Eq (genls c_tptpcol_10_26886 a) False) % 27.53/27.76 Clause #954 (by clausification #[667]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_26629 a) True) (Eq (genls c_tptpcol_7_26628 a) False) % 27.53/27.76 Clause #969 (by clausification #[668]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_26920 a) True) (Eq (genls c_tptpcol_12_26919 a) False) % 27.53/27.76 Clause #988 (by clausification #[669]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_26628 a) True) (Eq (genls c_tptpcol_6_26627 a) False) % 27.53/27.76 Clause #994 (by superposition #[988, 885]): Or (Eq (genls c_tptpcol_7_26628 c_tptpcol_1_1) True) (Eq False True) % 27.53/27.76 Clause #995 (by clausification #[994]): Eq (genls c_tptpcol_7_26628 c_tptpcol_1_1) True % 27.53/27.76 Clause #998 (by superposition #[995, 954]): Or (Eq (genls c_tptpcol_8_26629 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1000 (by clausification #[998]): Eq (genls c_tptpcol_8_26629 c_tptpcol_1_1) True % 27.53/27.76 Clause #1003 (by superposition #[1000, 916]): Or (Eq (genls c_tptpcol_9_26885 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1005 (by clausification #[1003]): Eq (genls c_tptpcol_9_26885 c_tptpcol_1_1) True % 27.53/27.76 Clause #1008 (by superposition #[1005, 901]): Or (Eq (genls c_tptpcol_10_26886 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1010 (by clausification #[1008]): Eq (genls c_tptpcol_10_26886 c_tptpcol_1_1) True % 27.53/27.76 Clause #1013 (by superposition #[1010, 939]): Or (Eq (genls c_tptpcol_11_26887 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1015 (by clausification #[1013]): Eq (genls c_tptpcol_11_26887 c_tptpcol_1_1) True % 27.53/27.76 Clause #1018 (by superposition #[1015, 934]): Or (Eq (genls c_tptpcol_12_26919 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1020 (by clausification #[670]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_16_92269 a) True) (Eq (genls c_tptpcol_15_92268 a) False) % 27.53/27.76 Clause #1025 (by clausification #[1018]): Eq (genls c_tptpcol_12_26919 c_tptpcol_1_1) True % 27.53/27.76 Clause #1028 (by superposition #[1025, 969]): Or (Eq (genls c_tptpcol_13_26920 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1030 (by clausification #[1028]): Eq (genls c_tptpcol_13_26920 c_tptpcol_1_1) True % 27.53/27.76 Clause #1033 (by superposition #[1030, 821]): Or (Eq (genls c_tptpcol_14_26921 c_tptpcol_1_1) True) (Eq True False) % 27.53/27.76 Clause #1035 (by clausification #[1033]): Eq (genls c_tptpcol_14_26921 c_tptpcol_1_1) True % 27.53/27.76 Clause #1039 (by clausification #[671]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_92268 a) True) (Eq (genls c_tptpcol_14_92264 a) False) % 27.53/27.76 Clause #1057 (by clausification #[672]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_92264 a) True) (Eq (genls c_tptpcol_13_92263 a) False) % 27.53/27.76 Clause #1068 (by clausification #[673]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_92263 a) True) (Eq (genls c_tptpcol_12_92262 a) False) % 27.53/27.76 Clause #1082 (by clausification #[674]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_92262 a) True) (Eq (genls c_tptpcol_11_92230 a) False) % 27.53/27.76 Clause #1097 (by clausification #[675]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_92163 a) True) (Eq (genls c_tptpcol_6_92162 a) False) % 27.53/27.76 Clause #1110 (by clausification #[676]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_90114 a) True) (Eq (genls c_tptpcol_4_90113 a) False) % 27.53/27.76 Clause #1124 (by clausification #[677]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_92162 a) True) (Eq (genls c_tptpcol_5_90114 a) False) % 27.53/27.76 Clause #1138 (by clausification #[678]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_90113 a) True) (Eq (genls c_tptpcol_3_81921 a) False) % 27.63/27.78 Clause #1152 (by clausification #[679]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_92230 a) True) (Eq (genls c_tptpcol_10_92166 a) False) % 27.63/27.78 Clause #1167 (by clausification #[680]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_92166 a) True) (Eq (genls c_tptpcol_9_92165 a) False) % 27.63/27.78 Clause #1182 (by clausification #[681]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_81921 a) True) (Eq (genls c_tptpcol_2_65537 a) False) % 27.63/27.78 Clause #1183 (by superposition #[1182, 36]): Or (Eq (genls c_tptpcol_3_81921 c_tptpcol_1_65536) True) (Eq False True) % 27.63/27.78 Clause #1185 (by clausification #[1183]): Eq (genls c_tptpcol_3_81921 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1188 (by superposition #[1185, 1138]): Or (Eq (genls c_tptpcol_4_90113 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1190 (by clausification #[1188]): Eq (genls c_tptpcol_4_90113 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1193 (by superposition #[1190, 1110]): Or (Eq (genls c_tptpcol_5_90114 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1195 (by clausification #[1193]): Eq (genls c_tptpcol_5_90114 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1198 (by superposition #[1195, 1124]): Or (Eq (genls c_tptpcol_6_92162 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1200 (by clausification #[1198]): Eq (genls c_tptpcol_6_92162 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1203 (by superposition #[1200, 1097]): Or (Eq (genls c_tptpcol_7_92163 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1207 (by clausification #[1203]): Eq (genls c_tptpcol_7_92163 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1221 (by clausification #[683]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_92165 a) True) (Eq (genls c_tptpcol_8_92164 a) False) % 27.63/27.78 Clause #1236 (by clausification #[684]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_16_26926 a) True) (Eq (genls c_tptpcol_15_26925 a) False) % 27.63/27.78 Clause #1250 (by clausification #[685]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_92164 a) True) (Eq (genls c_tptpcol_7_92163 a) False) % 27.63/27.78 Clause #1256 (by superposition #[1250, 1207]): Or (Eq (genls c_tptpcol_8_92164 c_tptpcol_1_65536) True) (Eq False True) % 27.63/27.78 Clause #1257 (by clausification #[1256]): Eq (genls c_tptpcol_8_92164 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1260 (by superposition #[1257, 1221]): Or (Eq (genls c_tptpcol_9_92165 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1262 (by clausification #[1260]): Eq (genls c_tptpcol_9_92165 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1265 (by superposition #[1262, 1167]): Or (Eq (genls c_tptpcol_10_92166 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1267 (by clausification #[1265]): Eq (genls c_tptpcol_10_92166 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1270 (by superposition #[1267, 1152]): Or (Eq (genls c_tptpcol_11_92230 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1272 (by clausification #[1270]): Eq (genls c_tptpcol_11_92230 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1275 (by superposition #[1272, 1082]): Or (Eq (genls c_tptpcol_12_92262 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1277 (by clausification #[1275]): Eq (genls c_tptpcol_12_92262 c_tptpcol_1_65536) True % 27.63/27.78 Clause #1280 (by superposition #[1277, 1068]): Or (Eq (genls c_tptpcol_13_92263 c_tptpcol_1_65536) True) (Eq True False) % 27.63/27.78 Clause #1282 (by clausification #[686]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_26925 a) True) (Eq (genls c_tptpcol_14_26921 a) False) % 27.63/27.78 Clause #1288 (by superposition #[1282, 1035]): Or (Eq (genls c_tptpcol_15_26925 c_tptpcol_1_1) True) (Eq False True) % 27.63/27.78 Clause #1295 (by clausification #[1288]): Eq (genls c_tptpcol_15_26925 c_tptpcol_1_1) True % 27.63/27.78 Clause #1298 (by superposition #[1295, 1236]): Or (Eq (genls c_tptpcol_16_26926 c_tptpcol_1_1) True) (Eq True False) % 27.63/27.78 Clause #1300 (by clausification #[1298]): Eq (genls c_tptpcol_16_26926 c_tptpcol_1_1) True % 27.63/27.78 Clause #1302 (by superposition #[1300, 806]): Or (Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_16_26926) True) (Eq True False) % 27.63/27.78 Clause #1304 (by clausification #[1302]): Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_16_26926) True % 27.63/27.78 Clause #1308 (by superposition #[1304, 456]): ∀ (a : Iota), % 27.63/27.78 Or (Eq (disjointwith a c_tptpcol_16_26926) True) (Or (Eq True False) (Eq (genls a c_tptpcol_1_65536) False)) % 27.64/27.81 Clause #1348 (by clausification #[1280]): Eq (genls c_tptpcol_13_92263 c_tptpcol_1_65536) True % 27.64/27.81 Clause #1351 (by superposition #[1348, 1057]): Or (Eq (genls c_tptpcol_14_92264 c_tptpcol_1_65536) True) (Eq True False) % 27.64/27.81 Clause #1353 (by clausification #[1351]): Eq (genls c_tptpcol_14_92264 c_tptpcol_1_65536) True % 27.64/27.81 Clause #1356 (by superposition #[1353, 1039]): Or (Eq (genls c_tptpcol_15_92268 c_tptpcol_1_65536) True) (Eq True False) % 27.64/27.81 Clause #1358 (by clausification #[1356]): Eq (genls c_tptpcol_15_92268 c_tptpcol_1_65536) True % 27.64/27.81 Clause #1361 (by superposition #[1358, 1020]): Or (Eq (genls c_tptpcol_16_92269 c_tptpcol_1_65536) True) (Eq True False) % 27.64/27.81 Clause #1363 (by clausification #[1361]): Eq (genls c_tptpcol_16_92269 c_tptpcol_1_65536) True % 27.64/27.81 Clause #3703 (by clausification #[1308]): ∀ (a : Iota), Or (Eq (disjointwith a c_tptpcol_16_26926) True) (Eq (genls a c_tptpcol_1_65536) False) % 27.64/27.81 Clause #3715 (by superposition #[3703, 1363]): Or (Eq (disjointwith c_tptpcol_16_92269 c_tptpcol_16_26926) True) (Eq False True) % 27.64/27.81 Clause #3716 (by clausification #[3715]): Eq (disjointwith c_tptpcol_16_92269 c_tptpcol_16_26926) True % 27.64/27.81 Clause #3718 (by superposition #[3716, 428]): Or (Eq True False) (Eq (disjointwith c_tptpcol_16_26926 c_tptpcol_16_92269) True) % 27.64/27.81 Clause #3721 (by clausification #[3718]): Eq (disjointwith c_tptpcol_16_26926 c_tptpcol_16_92269) True % 27.64/27.81 Clause #3722 (by superposition #[3721, 640]): Eq True False % 27.64/27.81 Clause #3727 (by clausification #[3722]): False % 27.64/27.81 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------