%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR039+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 25.52s 25.70s % Output : Proof 25.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.10 % Problem : CSR039+1 : TPTP v9.2.0. Released v3.4.0. % 0.10/0.11 % Command : duper %s % 0.11/0.32 % Computer : n012.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Oct 2 20:12:38 EDT 2025 % 0.11/0.32 % CPUTime : % 25.52/25.70 SZS status Theorem for theBenchmark.p % 25.52/25.70 SZS output start Proof for theBenchmark.p % 25.52/25.70 Clause #6 (by assumption #[]): Eq (genls c_tptpcol_2_2 c_tptpcol_1_1) True % 25.52/25.70 Clause #8 (by assumption #[]): Eq (genls c_tptpcol_3_16386 c_tptpcol_2_2) True % 25.52/25.70 Clause #10 (by assumption #[]): Eq (genls c_tptpcol_4_16387 c_tptpcol_3_16386) True % 25.52/25.70 Clause #12 (by assumption #[]): Eq (genls c_tptpcol_5_16388 c_tptpcol_4_16387) True % 25.52/25.70 Clause #14 (by assumption #[]): Eq (genls c_tptpcol_6_18436 c_tptpcol_5_16388) True % 25.52/25.70 Clause #16 (by assumption #[]): Eq (genls c_tptpcol_7_18437 c_tptpcol_6_18436) True % 25.52/25.70 Clause #18 (by assumption #[]): Eq (genls c_tptpcol_8_18438 c_tptpcol_7_18437) True % 25.52/25.70 Clause #20 (by assumption #[]): Eq (genls c_tptpcol_9_18439 c_tptpcol_8_18438) True % 25.52/25.70 Clause #22 (by assumption #[]): Eq (genls c_tptpcol_10_18567 c_tptpcol_9_18439) True % 25.52/25.70 Clause #24 (by assumption #[]): Eq (genls c_tptpcol_11_18631 c_tptpcol_10_18567) True % 25.52/25.70 Clause #26 (by assumption #[]): Eq (genls c_tptpcol_12_18663 c_tptpcol_11_18631) True % 25.52/25.70 Clause #28 (by assumption #[]): Eq (genls c_tptpcol_13_18664 c_tptpcol_12_18663) True % 25.52/25.70 Clause #30 (by assumption #[]): Eq (genls c_tptpcol_2_65537 c_tptpcol_1_65536) True % 25.52/25.70 Clause #32 (by assumption #[]): Eq (genls c_tptpcol_3_81921 c_tptpcol_2_65537) True % 25.52/25.70 Clause #34 (by assumption #[]): Eq (genls c_tptpcol_4_90113 c_tptpcol_3_81921) True % 25.52/25.70 Clause #36 (by assumption #[]): Eq (genls c_tptpcol_5_90114 c_tptpcol_4_90113) True % 25.52/25.70 Clause #38 (by assumption #[]): Eq (genls c_tptpcol_6_92162 c_tptpcol_5_90114) True % 25.52/25.70 Clause #40 (by assumption #[]): Eq (genls c_tptpcol_7_93186 c_tptpcol_6_92162) True % 25.52/25.70 Clause #42 (by assumption #[]): Eq (genls c_tptpcol_8_93698 c_tptpcol_7_93186) True % 25.52/25.70 Clause #44 (by assumption #[]): Eq (genls c_tptpcol_9_93699 c_tptpcol_8_93698) True % 25.52/25.70 Clause #46 (by assumption #[]): Eq (genls c_tptpcol_10_93700 c_tptpcol_9_93699) True % 25.52/25.70 Clause #48 (by assumption #[]): Eq (genls c_tptpcol_11_93764 c_tptpcol_10_93700) True % 25.52/25.70 Clause #50 (by assumption #[]): Eq (genls c_tptpcol_12_93765 c_tptpcol_11_93764) True % 25.52/25.70 Clause #52 (by assumption #[]): Eq (genls c_tptpcol_13_93766 c_tptpcol_12_93765) True % 25.52/25.70 Clause #54 (by assumption #[]): Eq (genls c_tptpcol_14_93774 c_tptpcol_13_93766) True % 25.52/25.70 Clause #56 (by assumption #[]): Eq (genls c_tptpcol_15_93775 c_tptpcol_14_93774) True % 25.52/25.70 Clause #58 (by assumption #[]): Eq (disjointwith c_tptpcol_1_1 c_tptpcol_1_65536) True % 25.52/25.70 Clause #72 (by assumption #[]): Eq (∀ (X Y : Iota), disjointwith X Y → disjointwith Y X) True % 25.52/25.70 Clause #73 (by assumption #[]): Eq (∀ (ARG1 OLD NEW : Iota), And (disjointwith ARG1 OLD) (genls NEW OLD) → disjointwith ARG1 NEW) True % 25.52/25.70 Clause #74 (by assumption #[]): Eq (∀ (OLD ARG2 NEW : Iota), And (disjointwith OLD ARG2) (genls NEW OLD) → disjointwith NEW ARG2) True % 25.52/25.70 Clause #133 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (genls X Y) (genls Y Z) → genls X Z) True % 25.52/25.70 Clause #158 (by assumption #[]): Eq % 25.52/25.70 (Not % 25.52/25.70 (mtvisible % 25.52/25.70 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwpoweripodsearchinfobrown_ipodhtml)) % 25.52/25.70 c_translation_7) → % 25.52/25.70 disjointwith c_tptpcol_15_93775 c_tptpcol_13_18664)) % 25.52/25.70 True % 25.52/25.70 Clause #391 (by clausification #[72]): ∀ (a : Iota), Eq (∀ (Y : Iota), disjointwith a Y → disjointwith Y a) True % 25.52/25.70 Clause #392 (by clausification #[391]): ∀ (a a_1 : Iota), Eq (disjointwith a a_1 → disjointwith a_1 a) True % 25.52/25.70 Clause #393 (by clausification #[392]): ∀ (a a_1 : Iota), Or (Eq (disjointwith a a_1) False) (Eq (disjointwith a_1 a) True) % 25.52/25.70 Clause #394 (by superposition #[393, 58]): Or (Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_1_1) True) (Eq False True) % 25.52/25.70 Clause #397 (by clausification #[394]): Eq (disjointwith c_tptpcol_1_65536 c_tptpcol_1_1) True % 25.52/25.70 Clause #402 (by clausification #[73]): ∀ (a : Iota), Eq (∀ (OLD NEW : Iota), And (disjointwith a OLD) (genls NEW OLD) → disjointwith a NEW) True % 25.52/25.70 Clause #403 (by clausification #[402]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a_1) → disjointwith a NEW) True % 25.52/25.70 Clause #404 (by clausification #[403]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a_1) → disjointwith a a_2) True % 25.52/25.72 Clause #405 (by clausification #[404]): ∀ (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) % 25.52/25.72 Clause #406 (by clausification #[405]): ∀ (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)) % 25.52/25.72 Clause #417 (by clausification #[74]): ∀ (a : Iota), Eq (∀ (ARG2 NEW : Iota), And (disjointwith a ARG2) (genls NEW a) → disjointwith NEW ARG2) True % 25.52/25.72 Clause #418 (by clausification #[417]): ∀ (a a_1 : Iota), Eq (∀ (NEW : Iota), And (disjointwith a a_1) (genls NEW a) → disjointwith NEW a_1) True % 25.52/25.72 Clause #419 (by clausification #[418]): ∀ (a a_1 a_2 : Iota), Eq (And (disjointwith a a_1) (genls a_2 a) → disjointwith a_2 a_1) True % 25.52/25.72 Clause #420 (by clausification #[419]): ∀ (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) % 25.52/25.72 Clause #421 (by clausification #[420]): ∀ (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)) % 25.52/25.72 Clause #423 (by superposition #[421, 397]): ∀ (a : Iota), Or (Eq (disjointwith a c_tptpcol_1_1) True) (Or (Eq (genls a c_tptpcol_1_65536) False) (Eq False True)) % 25.52/25.72 Clause #424 (by clausification #[158]): Eq % 25.52/25.72 (mtvisible % 25.52/25.72 (f_contentmtofcdafromeventfn (f_urlreferentfn (f_urlfn s_http_wwwpoweripodsearchinfobrown_ipodhtml)) % 25.52/25.72 c_translation_7) → % 25.52/25.72 disjointwith c_tptpcol_15_93775 c_tptpcol_13_18664) % 25.52/25.72 False % 25.52/25.72 Clause #426 (by clausification #[424]): Eq (disjointwith c_tptpcol_15_93775 c_tptpcol_13_18664) False % 25.52/25.72 Clause #566 (by clausification #[133]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (genls a Y) (genls Y Z) → genls a Z) True % 25.52/25.72 Clause #567 (by clausification #[566]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (genls a a_1) (genls a_1 Z) → genls a Z) True % 25.52/25.72 Clause #568 (by clausification #[567]): ∀ (a a_1 a_2 : Iota), Eq (And (genls a a_1) (genls a_1 a_2) → genls a a_2) True % 25.52/25.72 Clause #569 (by clausification #[568]): ∀ (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) % 25.52/25.72 Clause #570 (by clausification #[569]): ∀ (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)) % 25.52/25.72 Clause #572 (by superposition #[570, 14]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_18436 a) True) (Or (Eq (genls c_tptpcol_5_16388 a) False) (Eq False True)) % 25.52/25.72 Clause #574 (by superposition #[570, 10]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_16387 a) True) (Or (Eq (genls c_tptpcol_3_16386 a) False) (Eq False True)) % 25.52/25.72 Clause #575 (by superposition #[570, 8]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_16386 a) True) (Or (Eq (genls c_tptpcol_2_2 a) False) (Eq False True)) % 25.52/25.72 Clause #576 (by superposition #[570, 54]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_93774 a) True) (Or (Eq (genls c_tptpcol_13_93766 a) False) (Eq False True)) % 25.52/25.72 Clause #577 (by superposition #[570, 56]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_93775 a) True) (Or (Eq (genls c_tptpcol_14_93774 a) False) (Eq False True)) % 25.52/25.72 Clause #578 (by superposition #[570, 50]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_93765 a) True) (Or (Eq (genls c_tptpcol_11_93764 a) False) (Eq False True)) % 25.52/25.72 Clause #579 (by superposition #[570, 48]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_93764 a) True) (Or (Eq (genls c_tptpcol_10_93700 a) False) (Eq False True)) % 25.52/25.72 Clause #580 (by superposition #[570, 52]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_93766 a) True) (Or (Eq (genls c_tptpcol_12_93765 a) False) (Eq False True)) % 25.52/25.72 Clause #582 (by superposition #[570, 28]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_18664 a) True) (Or (Eq (genls c_tptpcol_12_18663 a) False) (Eq False True)) % 25.52/25.72 Clause #583 (by superposition #[570, 26]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_18663 a) True) (Or (Eq (genls c_tptpcol_11_18631 a) False) (Eq False True)) % 25.52/25.72 Clause #584 (by superposition #[570, 24]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_18631 a) True) (Or (Eq (genls c_tptpcol_10_18567 a) False) (Eq False True)) % 25.52/25.72 Clause #585 (by superposition #[570, 46]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_93700 a) True) (Or (Eq (genls c_tptpcol_9_93699 a) False) (Eq False True)) % 25.57/25.74 Clause #586 (by superposition #[570, 42]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_93698 a) True) (Or (Eq (genls c_tptpcol_7_93186 a) False) (Eq False True)) % 25.57/25.74 Clause #587 (by superposition #[570, 40]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_93186 a) True) (Or (Eq (genls c_tptpcol_6_92162 a) False) (Eq False True)) % 25.57/25.74 Clause #588 (by superposition #[570, 44]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_93699 a) True) (Or (Eq (genls c_tptpcol_8_93698 a) False) (Eq False True)) % 25.57/25.74 Clause #590 (by superposition #[570, 20]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_18439 a) True) (Or (Eq (genls c_tptpcol_8_18438 a) False) (Eq False True)) % 25.57/25.74 Clause #591 (by superposition #[570, 38]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_92162 a) True) (Or (Eq (genls c_tptpcol_5_90114 a) False) (Eq False True)) % 25.57/25.74 Clause #592 (by superposition #[570, 18]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_18438 a) True) (Or (Eq (genls c_tptpcol_7_18437 a) False) (Eq False True)) % 25.57/25.74 Clause #593 (by superposition #[570, 34]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_90113 a) True) (Or (Eq (genls c_tptpcol_3_81921 a) False) (Eq False True)) % 25.57/25.74 Clause #594 (by superposition #[570, 16]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_18437 a) True) (Or (Eq (genls c_tptpcol_6_18436 a) False) (Eq False True)) % 25.57/25.74 Clause #595 (by superposition #[570, 36]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_90114 a) True) (Or (Eq (genls c_tptpcol_4_90113 a) False) (Eq False True)) % 25.57/25.74 Clause #596 (by superposition #[570, 32]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_81921 a) True) (Or (Eq (genls c_tptpcol_2_65537 a) False) (Eq False True)) % 25.57/25.74 Clause #757 (by clausification #[423]): ∀ (a : Iota), Or (Eq (disjointwith a c_tptpcol_1_1) True) (Eq (genls a c_tptpcol_1_65536) False) % 25.57/25.74 Clause #781 (by clausification #[572]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_18436 a) True) (Eq (genls c_tptpcol_5_16388 a) False) % 25.57/25.74 Clause #782 (by superposition #[781, 12]): Or (Eq (genls c_tptpcol_6_18436 c_tptpcol_4_16387) True) (Eq False True) % 25.57/25.74 Clause #784 (by clausification #[782]): Eq (genls c_tptpcol_6_18436 c_tptpcol_4_16387) True % 25.57/25.74 Clause #785 (by superposition #[784, 570]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_18436 a) True) (Or (Eq True False) (Eq (genls c_tptpcol_4_16387 a) False)) % 25.57/25.74 Clause #799 (by clausification #[785]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_18436 a) True) (Eq (genls c_tptpcol_4_16387 a) False) % 25.57/25.74 Clause #801 (by clausification #[574]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_16387 a) True) (Eq (genls c_tptpcol_3_16386 a) False) % 25.57/25.74 Clause #822 (by clausification #[575]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_16386 a) True) (Eq (genls c_tptpcol_2_2 a) False) % 25.57/25.74 Clause #823 (by superposition #[822, 6]): Or (Eq (genls c_tptpcol_3_16386 c_tptpcol_1_1) True) (Eq False True) % 25.57/25.74 Clause #825 (by clausification #[823]): Eq (genls c_tptpcol_3_16386 c_tptpcol_1_1) True % 25.57/25.74 Clause #828 (by superposition #[825, 801]): Or (Eq (genls c_tptpcol_4_16387 c_tptpcol_1_1) True) (Eq True False) % 25.57/25.74 Clause #830 (by clausification #[828]): Eq (genls c_tptpcol_4_16387 c_tptpcol_1_1) True % 25.57/25.74 Clause #833 (by superposition #[830, 799]): Or (Eq (genls c_tptpcol_6_18436 c_tptpcol_1_1) True) (Eq True False) % 25.57/25.74 Clause #835 (by clausification #[833]): Eq (genls c_tptpcol_6_18436 c_tptpcol_1_1) True % 25.57/25.74 Clause #838 (by clausification #[576]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_14_93774 a) True) (Eq (genls c_tptpcol_13_93766 a) False) % 25.57/25.74 Clause #853 (by clausification #[577]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_15_93775 a) True) (Eq (genls c_tptpcol_14_93774 a) False) % 25.57/25.74 Clause #861 (by clausification #[578]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_93765 a) True) (Eq (genls c_tptpcol_11_93764 a) False) % 25.57/25.74 Clause #879 (by clausification #[579]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_93764 a) True) (Eq (genls c_tptpcol_10_93700 a) False) % 25.57/25.74 Clause #887 (by clausification #[580]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_93766 a) True) (Eq (genls c_tptpcol_12_93765 a) False) % 25.57/25.74 Clause #918 (by clausification #[582]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_18664 a) True) (Eq (genls c_tptpcol_12_18663 a) False) % 25.57/25.76 Clause #926 (by clausification #[583]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_12_18663 a) True) (Eq (genls c_tptpcol_11_18631 a) False) % 25.57/25.76 Clause #936 (by clausification #[584]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_11_18631 a) True) (Eq (genls c_tptpcol_10_18567 a) False) % 25.57/25.76 Clause #937 (by superposition #[936, 22]): Or (Eq (genls c_tptpcol_11_18631 c_tptpcol_9_18439) True) (Eq False True) % 25.57/25.76 Clause #939 (by clausification #[937]): Eq (genls c_tptpcol_11_18631 c_tptpcol_9_18439) True % 25.57/25.76 Clause #940 (by superposition #[939, 926]): Or (Eq (genls c_tptpcol_12_18663 c_tptpcol_9_18439) True) (Eq True False) % 25.57/25.76 Clause #942 (by clausification #[940]): Eq (genls c_tptpcol_12_18663 c_tptpcol_9_18439) True % 25.57/25.76 Clause #943 (by superposition #[942, 918]): Or (Eq (genls c_tptpcol_13_18664 c_tptpcol_9_18439) True) (Eq True False) % 25.57/25.76 Clause #945 (by clausification #[943]): Eq (genls c_tptpcol_13_18664 c_tptpcol_9_18439) True % 25.57/25.76 Clause #946 (by superposition #[945, 570]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_18664 a) True) (Or (Eq True False) (Eq (genls c_tptpcol_9_18439 a) False)) % 25.57/25.76 Clause #947 (by clausification #[585]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_10_93700 a) True) (Eq (genls c_tptpcol_9_93699 a) False) % 25.57/25.76 Clause #962 (by clausification #[586]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_93698 a) True) (Eq (genls c_tptpcol_7_93186 a) False) % 25.57/25.76 Clause #972 (by clausification #[946]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_13_18664 a) True) (Eq (genls c_tptpcol_9_18439 a) False) % 25.57/25.76 Clause #975 (by clausification #[587]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_93186 a) True) (Eq (genls c_tptpcol_6_92162 a) False) % 25.57/25.76 Clause #985 (by clausification #[588]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_93699 a) True) (Eq (genls c_tptpcol_8_93698 a) False) % 25.57/25.76 Clause #1017 (by clausification #[590]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_9_18439 a) True) (Eq (genls c_tptpcol_8_18438 a) False) % 25.57/25.76 Clause #1032 (by clausification #[591]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_6_92162 a) True) (Eq (genls c_tptpcol_5_90114 a) False) % 25.57/25.76 Clause #1047 (by clausification #[592]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_8_18438 a) True) (Eq (genls c_tptpcol_7_18437 a) False) % 25.57/25.76 Clause #1063 (by clausification #[593]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_4_90113 a) True) (Eq (genls c_tptpcol_3_81921 a) False) % 25.57/25.76 Clause #1072 (by clausification #[594]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_7_18437 a) True) (Eq (genls c_tptpcol_6_18436 a) False) % 25.57/25.76 Clause #1078 (by superposition #[1072, 835]): Or (Eq (genls c_tptpcol_7_18437 c_tptpcol_1_1) True) (Eq False True) % 25.57/25.76 Clause #1079 (by clausification #[1078]): Eq (genls c_tptpcol_7_18437 c_tptpcol_1_1) True % 25.57/25.76 Clause #1082 (by superposition #[1079, 1047]): Or (Eq (genls c_tptpcol_8_18438 c_tptpcol_1_1) True) (Eq True False) % 25.57/25.76 Clause #1084 (by clausification #[1082]): Eq (genls c_tptpcol_8_18438 c_tptpcol_1_1) True % 25.57/25.76 Clause #1087 (by superposition #[1084, 1017]): Or (Eq (genls c_tptpcol_9_18439 c_tptpcol_1_1) True) (Eq True False) % 25.57/25.76 Clause #1089 (by clausification #[1087]): Eq (genls c_tptpcol_9_18439 c_tptpcol_1_1) True % 25.57/25.76 Clause #1092 (by superposition #[1089, 972]): Or (Eq (genls c_tptpcol_13_18664 c_tptpcol_1_1) True) (Eq True False) % 25.57/25.76 Clause #1105 (by clausification #[595]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_5_90114 a) True) (Eq (genls c_tptpcol_4_90113 a) False) % 25.57/25.76 Clause #1124 (by clausification #[596]): ∀ (a : Iota), Or (Eq (genls c_tptpcol_3_81921 a) True) (Eq (genls c_tptpcol_2_65537 a) False) % 25.57/25.76 Clause #1125 (by superposition #[1124, 30]): Or (Eq (genls c_tptpcol_3_81921 c_tptpcol_1_65536) True) (Eq False True) % 25.57/25.76 Clause #1127 (by clausification #[1125]): Eq (genls c_tptpcol_3_81921 c_tptpcol_1_65536) True % 25.57/25.76 Clause #1131 (by superposition #[1127, 1063]): Or (Eq (genls c_tptpcol_4_90113 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.76 Clause #1133 (by clausification #[1131]): Eq (genls c_tptpcol_4_90113 c_tptpcol_1_65536) True % 25.57/25.76 Clause #1137 (by superposition #[1133, 1105]): Or (Eq (genls c_tptpcol_5_90114 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.76 Clause #1139 (by clausification #[1137]): Eq (genls c_tptpcol_5_90114 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1143 (by superposition #[1139, 1032]): Or (Eq (genls c_tptpcol_6_92162 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1145 (by clausification #[1143]): Eq (genls c_tptpcol_6_92162 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1149 (by superposition #[1145, 975]): Or (Eq (genls c_tptpcol_7_93186 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1152 (by clausification #[1149]): Eq (genls c_tptpcol_7_93186 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1156 (by superposition #[1152, 962]): Or (Eq (genls c_tptpcol_8_93698 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1158 (by clausification #[1156]): Eq (genls c_tptpcol_8_93698 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1162 (by superposition #[1158, 985]): Or (Eq (genls c_tptpcol_9_93699 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1164 (by clausification #[1162]): Eq (genls c_tptpcol_9_93699 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1168 (by superposition #[1164, 947]): Or (Eq (genls c_tptpcol_10_93700 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1170 (by clausification #[1168]): Eq (genls c_tptpcol_10_93700 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1174 (by superposition #[1170, 879]): Or (Eq (genls c_tptpcol_11_93764 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1176 (by clausification #[1174]): Eq (genls c_tptpcol_11_93764 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1180 (by superposition #[1176, 861]): Or (Eq (genls c_tptpcol_12_93765 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1183 (by clausification #[1180]): Eq (genls c_tptpcol_12_93765 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1187 (by superposition #[1183, 887]): Or (Eq (genls c_tptpcol_13_93766 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1189 (by clausification #[1187]): Eq (genls c_tptpcol_13_93766 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1193 (by superposition #[1189, 838]): Or (Eq (genls c_tptpcol_14_93774 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1195 (by clausification #[1193]): Eq (genls c_tptpcol_14_93774 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1199 (by superposition #[1195, 853]): Or (Eq (genls c_tptpcol_15_93775 c_tptpcol_1_65536) True) (Eq True False) % 25.57/25.79 Clause #1201 (by clausification #[1199]): Eq (genls c_tptpcol_15_93775 c_tptpcol_1_65536) True % 25.57/25.79 Clause #1204 (by superposition #[1201, 757]): Or (Eq (disjointwith c_tptpcol_15_93775 c_tptpcol_1_1) True) (Eq True False) % 25.57/25.79 Clause #1206 (by clausification #[1204]): Eq (disjointwith c_tptpcol_15_93775 c_tptpcol_1_1) True % 25.57/25.79 Clause #1209 (by superposition #[1206, 406]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_15_93775 a) True) (Or (Eq True False) (Eq (genls a c_tptpcol_1_1) False)) % 25.57/25.79 Clause #1580 (by clausification #[1092]): Eq (genls c_tptpcol_13_18664 c_tptpcol_1_1) True % 25.57/25.79 Clause #3238 (by clausification #[1209]): ∀ (a : Iota), Or (Eq (disjointwith c_tptpcol_15_93775 a) True) (Eq (genls a c_tptpcol_1_1) False) % 25.57/25.79 Clause #3243 (by superposition #[3238, 1580]): Or (Eq (disjointwith c_tptpcol_15_93775 c_tptpcol_13_18664) True) (Eq False True) % 25.57/25.79 Clause #3244 (by clausification #[3243]): Eq (disjointwith c_tptpcol_15_93775 c_tptpcol_13_18664) True % 25.57/25.79 Clause #3245 (by superposition #[3244, 426]): Eq True False % 25.57/25.79 Clause #3250 (by clausification #[3245]): False % 25.57/25.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------